case mk
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
A B : PartialOrder α
h : toPreorder = toPreorder
⊢ A = B
cases A
case mk.mk
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
toPreorder✝¹ : Preorder α
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
case mk
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B
cases B
case mk.mk.refl
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
case mk.mk
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
toPreorder✝¹ : Preorder α
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
cases h
no goals
case mk.mk.refl
ι : Type ?u.12814
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.12825
r : α✝ → α✝ → Prop
α : Type u_1
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
congr