-- Mathlib/Order/Lattice.lean
theorem Lattice.ext {α} {A B : Lattice α} (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B

Proof state:
case mk
α : Type u_1
B : Lattice α
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝ = B

Tactic:
cases B

Result:
case mk.mk
α : Type u_1
toSemilatticeSup✝¹ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝¹ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝

Proof state:
α : Type u_1
A B : Lattice α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
cases A

Result:
case mk
α : Type u_1
B : Lattice α
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝ = B

Proof state:
case mk.mk.refl.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝

Tactic:
congr

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
toSemilatticeSup✝¹ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝¹ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝

Tactic:
cases SemilatticeSup.ext H

Result:
case mk.mk.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝¹ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝

Proof state:
case mk.mk.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝¹ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝

Tactic:
cases SemilatticeInf.ext H

Result:
case mk.mk.refl.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf✝ inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf✝ inf_le_left✝ inf_le_right✝ le_inf✝