α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ A = B
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
have ss : A.toInf = B.toInf := by ext; apply SemilatticeInf.ext_inf H
case mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
B : SemilatticeInf α
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝ inf_le_right✝ le_inf✝ = B
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ A = B
cases A
case mk.mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝¹ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
case mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
B : SemilatticeInf α
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝ inf_le_right✝ le_inf✝ = B
cases B
case mk.mk.refl
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
case mk.mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝¹ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
cases PartialOrder.ext H
no goals
case mk.mk.refl
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
congr
case inf.h.h
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = x✝¹ ⊓ x✝
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ toInf = toInf
ext
no goals
case inf.h.h
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = x✝¹ ⊓ x✝
apply SemilatticeInf.ext_inf H