Avoiding tactic mode

Stream: new members

[jsodd]

I'm trying to figure out some of the ways term mode proofs work, and I found a spot where I cannot avoid using "by". I know that it's always possible to avoid it, so I decided to ask here.

example (f : X → Y) (g : Y → Z) : Injective (g ∘ f) → Injective f :=
  fun h a₁ a₂ H ↦ h (by rw [comp_apply, comp_apply]; congr)

P.S. The motivation for this question is pure curiosity, just trying to understand the language better.

[Luigi Massacci]

example (f : X → Y) (g : Y → Z) : Injective (g ∘ f) → Injective f :=
  fun h a₁ a₂ H ↦ h <| congrArg g H

[Luigi Massacci]

In this case I just guessed it, but remember you can always use docs#Lean.Parser.Tactic.showTerm to see what the tactics have created (though in general it will be a horrible mess)

[jsodd]

Thanks! I was also trying to guess how to use this with Exists, as here:

example (f : X → Y) (g : Y → Z) : Surjective (g ∘ f) → Surjective g :=
  fun h a ↦ _

[jsodd]

I use show_term a lot! It frequently gives overcomplicated feedback, but still very useful

[Luigi Massacci]

example (f : X → Y) (g : Y → Z) : Surjective (g ∘ f) → Surjective g :=
  fun h a ↦ Exists.elim (h a) (fun x hx ↦ Exists.intro (f x) hx)

[Luigi Massacci]

Here maybe a look at #tpil might be useful for you

[Luigi Massacci]

More in general you need to look at what are the constructors / destructors for these types

[jsodd]

Thank you again! This is what I'm trying to understand better, yes.

[Kevin Buzzard]

Using dot notation and anonymous constructors golfs it to

example (f : X → Y) (g : Y → Z) : Surjective (g ∘ f) → Surjective g :=
  fun h a ↦ (h a).elim (fun x hx ↦ ⟨f x, hx⟩)

(Just mentioning these as more term mode tips).