case refl
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ : α
b₁ : β a₁
⊢ a₁ = a₁ ∧ HEq b₁ b₁
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
h : { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
⊢ a₁ = a₂ ∧ HEq b₁ b₂
cases h
no goals
case refl
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ : α
b₁ : β a₁
⊢ a₁ = a₁ ∧ HEq b₁ b₁
exact ⟨rfl, heq_of_eq rfl⟩
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ : α
b₁ b₂ : β a₁
x✝ : a₁ = a₁ ∧ HEq b₁ b₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
x✝ : a₁ = a₂ ∧ HEq b₁ b₂
h₁ : a₁ = a₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
subst h₁
no goals
α : Type u_1
α₁ : Type ?u.1977
α₂ : Type ?u.1980
β : α → Type u_2
β₁ : α₁ → Type ?u.1990
β₂ : α₂ → Type ?u.1995
a₁ : α
b₁ b₂ : β a₁
x✝ : a₁ = a₁ ∧ HEq b₁ b₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
rw [eq_of_heq h₂]