case intro
α : Type u_2
β : α → Type u_3
γ : Type u_1
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂
α : Type u_2
β : α → Type u_3
γ : Type u_1
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType fun a => β a
a₂ : α
f₂ : β a₂ → WType fun a => β a
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
case intro.e_f.h
α : Type u_2
β : α → Type u_3
γ : Type u_1
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x
case intro
α : Type u_2
β : α → Type u_3
γ : Type u_1
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂
congr with x
no goals
case intro.e_f.h
α : Type u_2
β : α → Type u_3
γ : Type u_1
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x : _)