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

Proof state:
case mk.mk.refl.e_inf.h.h
α : Type u_1
toPartialOrder✝ : PartialOrder α
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
x✝¹ x✝ : α
⊢ inf✝¹ x✝¹ x✝ = inf✝ x✝¹ x✝

Tactic:
apply SemilatticeInf.ext_inf H

Result:
no goals

Proof state:
case mk
α : Type u_1
B : SemilatticeInf α
toPartialOrder✝ : PartialOrder α
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
toPartialOrder✝¹ : PartialOrder α
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
toPartialOrder✝ : PartialOrder α
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
α : Type u_1
toPartialOrder✝¹ : PartialOrder α
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
toPartialOrder✝ : PartialOrder α
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 PartialOrder.ext H

Result:
case mk.mk.refl
α : Type u_1
toPartialOrder✝ : PartialOrder α
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.e_inf
α : Type u_1
toPartialOrder✝ : PartialOrder α
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
⊢ inf✝¹ = inf✝

Tactic:
ext

Result:
case mk.mk.refl.e_inf.h.h
α : Type u_1
toPartialOrder✝ : PartialOrder α
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
x✝¹ x✝ : α
⊢ inf✝¹ x✝¹ x✝ = inf✝ x✝¹ x✝

Proof state:
case mk.mk.refl
α : Type u_1
toPartialOrder✝ : PartialOrder α
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:
congr

Result:
case mk.mk.refl.e_inf
α : Type u_1
toPartialOrder✝ : PartialOrder α
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
⊢ inf✝¹ = inf✝

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

Tactic:
cases A

Result:
case mk
α : Type u_1
B : SemilatticeInf α
toPartialOrder✝ : PartialOrder α
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