-- Mathlib/Control/Traversable/Basic.lean
theorem coe_inj ⦃η η' : ApplicativeTransformation F G⦄ (h : (η : ∀ α, F α → G α) = η') :
    η = η'

Proof state:
case mk.mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝¹ β (x <*> y) = app✝¹ (α → β) x <*> app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} => { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ }.app α) =
    fun {α} => { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }

Tactic:
congr

Result:
no goals

Proof state:
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : (fun {α} => η.app α) = fun {α} => η'.app α
⊢ η = η'

Tactic:
cases η

Result:
case mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η' : ApplicativeTransformation F G
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} => { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α) =
    fun {α} => η'.app α
⊢ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } = η'

Proof state:
case mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η' : ApplicativeTransformation F G
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} => { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α) =
    fun {α} => η'.app α
⊢ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } = η'

Tactic:
cases η'

Result:
case mk.mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝¹ β (x <*> y) = app✝¹ (α → β) x <*> app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} => { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ }.app α) =
    fun {α} => { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }