[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.fst = d.fst
⊢ c = d
[PROOFSTEP]
obtain ⟨⟨s₁, t₁⟩, h₁, _⟩ := c
[GOAL]
case mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁✝ t₂ : Set β
d : Concept α β r
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
closure_snd✝ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
h : { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ }.toProd.fst = d.fst
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ } = d
[PROOFSTEP]
obtain ⟨⟨s₂, t₂⟩, h₂, _⟩ := d
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
closure_snd✝¹ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
closure_snd✝ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h :
  { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ }.toProd.fst =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }.toProd.fst
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }
[PROOFSTEP]
dsimp at h₁ h₂ h
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r s₁ = t₁
closure_snd✝¹ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r s₂ = t₂
closure_snd✝ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h : s₁ = s₂
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }
[PROOFSTEP]
substs h h₁ h₂
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁ t₂ : Set β
s₁ : Set α
closure_snd✝¹ closure_snd✝ : extentClosure r (s₁, intentClosure r s₁).snd = (s₁, intentClosure r s₁).fst
⊢ { toProd := (s₁, intentClosure r s₁), closure_fst := (_ : intentClosure r s₁ = intentClosure r s₁),
      closure_snd := closure_snd✝¹ } =
    { toProd := (s₁, intentClosure r s₁), closure_fst := (_ : intentClosure r s₁ = intentClosure r s₁),
      closure_snd := closure_snd✝ }
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd = d.snd
⊢ c = d
[PROOFSTEP]
obtain ⟨⟨s₁, t₁⟩, _, h₁⟩ := c
[GOAL]
case mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁✝ t₂ : Set β
d : Concept α β r
s₁ : Set α
t₁ : Set β
closure_fst✝ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
h : { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ }.toProd.snd = d.snd
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ } = d
[PROOFSTEP]
obtain ⟨⟨s₂, t₂⟩, _, h₂⟩ := d
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
h₂ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h :
  { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ }.toProd.snd =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }.toProd.snd
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ } =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }
[PROOFSTEP]
dsimp at h₁ h₂ h
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r t₁ = s₁
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
h₂ : extentClosure r t₂ = s₂
h : t₁ = t₂
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ } =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }
[PROOFSTEP]
substs h h₁ h₂
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁✝ t₂ t₁ : Set β
closure_fst✝¹ closure_fst✝ : intentClosure r (extentClosure r t₁, t₁).fst = (extentClosure r t₁, t₁).snd
⊢ { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝¹,
      closure_snd := (_ : extentClosure r t₁ = extentClosure r t₁) } =
    { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝,
      closure_snd := (_ : extentClosure r t₁ = extentClosure r t₁) }
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ c d : Concept α β r
⊢ intentClosure r (extentClosure r (c.snd ∩ d.snd), c.snd ∩ d.snd).fst =
    (extentClosure r (c.snd ∩ d.snd), c.snd ∩ d.snd).snd
[PROOFSTEP]
rw [← c.closure_fst, ← d.closure_fst, ← intentClosure_union, intentClosure_extentClosure_intentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ c d : Concept α β r
⊢ extentClosure r (c.fst ∩ d.fst, intentClosure r (c.fst ∩ d.fst)).snd =
    (c.fst ∩ d.fst, intentClosure r (c.fst ∩ d.fst)).fst
[PROOFSTEP]
rw [← c.closure_snd, ← d.closure_snd, ← extentClosure_union, extentClosure_intentClosure_extentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊆ d.snd ↔ d ≤ c
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ d ≤ c
[PROOFSTEP]
rw [← fst_subset_fst_iff, ← c.closure_snd, ← d.closure_snd]
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ extentClosure r d.snd ⊆ extentClosure r c.snd
[PROOFSTEP]
exact extentClosure_anti _ h
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ c.snd ⊆ d.snd
[PROOFSTEP]
rw [← c.closure_fst, ← d.closure_fst]
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ intentClosure r c.fst ⊆ intentClosure r d.fst
[PROOFSTEP]
exact intentClosure_anti _ h
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊂ d.snd ↔ d < c
[PROOFSTEP]
rw [ssubset_iff_subset_not_subset, lt_iff_le_not_le, snd_subset_snd_iff, snd_subset_snd_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ : Concept α β r
src✝ : SemilatticeInf (Concept α β r) := instSemilatticeInfConcept
c d e : Concept α β r
⊢ c ≤ e → d ≤ e → c ⊔ d ≤ e
[PROOFSTEP]
simp_rw [← snd_subset_snd_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ : Concept α β r
src✝ : SemilatticeInf (Concept α β r) := instSemilatticeInfConcept
c d e : Concept α β r
⊢ e.snd ⊆ c.snd → e.snd ⊆ d.snd → e.snd ⊆ (c ⊔ d).snd
[PROOFSTEP]
exact subset_inter
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
S : Set (Concept α β r)
⊢ intentClosure r
      (extentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.snd), ⋂ (c : Concept α β r) (_ : c ∈ S), c.snd).fst =
    (extentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.snd), ⋂ (c : Concept α β r) (_ : c ∈ S), c.snd).snd
[PROOFSTEP]
simp_rw [← closure_fst, ← intentClosure_iUnion₂, intentClosure_extentClosure_intentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
S : Set (Concept α β r)
⊢ extentClosure r
      (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst, intentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst)).snd =
    (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst, intentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst)).fst
[PROOFSTEP]
simp_rw [← closure_snd, ← extentClosure_Union₂, extentClosure_intentClosure_extentClosure]


[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : PartialOrder α
x y : α
⊢ x ≤ y → y = x ↔ ¬x < y
[PROOFSTEP]
rw [lt_iff_le_and_ne, not_and, Classical.not_not, eq_comm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ min a b = if b ≤ a then b else a
[PROOFSTEP]
rw [min_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rcases lt_trichotomy a b with (lt | eq | gt)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_pos lt.le, if_neg (not_le.mpr lt)]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_pos eq.le, if_pos eq.ge, eq]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ max a b = if b ≤ a then a else b
[PROOFSTEP]
rw [max_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rcases lt_trichotomy a b with (lt | eq | gt)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_pos lt.le, if_neg (not_le.mpr lt)]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_pos eq.le, if_pos eq.ge, eq]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c
[PROOFSTEP]
rw [comm, comm b, comm _ c, comm a]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
[PROOFSTEP]
exact assoc _ _ _
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
h : toLE = toLE
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
cases h
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
have : A_lt = B_lt := by
  funext a b
  show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
  rw [A_iff, B_iff]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ A_lt = B_lt
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
a b : α
⊢ A_lt a b = B_lt a b
[PROOFSTEP]
show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
a b : α
⊢ (a < b) = (a < b)
[PROOFSTEP]
rw [A_iff, B_iff]
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
this : A_lt = B_lt
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
cases this
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
h : toPreorder = toPreorder
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
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✝
[PROOFSTEP]
cases h
[GOAL]
case mk.mk.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_le B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
B_decidableEq : DecidableEq α
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
h : toPartialOrder = toPartialOrder
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ B_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
cases h
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
B_decidableEq : DecidableEq α
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ B_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableLE = B_decidableLE := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
B_decidableEq : DecidableEq α
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableEq = B_decidableEq := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableLT = B_decidableLT := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_min = B_min := by
  funext a b
  exact (A_min_def _ _).trans (B_min_def _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ A_min = B_min
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
a b : α
⊢ A_min a b = B_min a b
[PROOFSTEP]
exact (A_min_def _ _).trans (B_min_def _ _).symm
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
this : A_min = B_min
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
cases this
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_max = B_max := by
  funext a b
  exact (A_max_def _ _).trans (B_max_def _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
⊢ A_max = B_max
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
a b : α
⊢ A_max a b = B_max a b
[PROOFSTEP]
exact (A_max_def _ _).trans (B_max_def _ _).symm
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
this : A_max = B_max
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
cases this
[GOAL]
case refl.refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_compare = B_compare := by
  funext a b
  exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ A_compare = B_compare
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
a b : α
⊢ A_compare a b = B_compare a b
[PROOFSTEP]
exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
[GOAL]
case refl.refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
this : A_compare = B_compare
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.a.a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ max a b = if a ≤ b then a else b
[PROOFSTEP]
rw [max_comm, max_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ (if b ≤ a then a else b) = if a ≤ b then a else b
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ min a b = if a ≤ b then b else a
[PROOFSTEP]
rw [min_comm, min_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ (if b ≤ a then b else a) = if a ≤ b then b else a
[PROOFSTEP]
rfl
[GOAL]
ι✝ : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι✝ → Type u_2
r : α✝ → α✝ → Prop
ι : Type u
α : ι → Type v
inst✝ : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i
[PROOFSTEP]
simp (config := { contextual := true }) [lt_iff_le_not_le, Pi.le_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b
[PROOFSTEP]
inhabit ι
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b
[PROOFSTEP]
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
[PROOFSTEP]
simp (config := { contextual := true }) [update_le_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update x i b ↔ a ≤ b
[PROOFSTEP]
simp [update_le_update_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ x ≤ update x i a ↔ x i ≤ a
[PROOFSTEP]
simp [le_update_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ x ↔ a ≤ x i
[PROOFSTEP]
simp [update_le_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ x < update x i a ↔ x i < a
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a < x ↔ a < x i
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b
[PROOFSTEP]
simpa [Pi.lt_def] using le_of_lt
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ min x y = if x < y then x else y
[PROOFSTEP]
rw [min_comm, min_def, ← ite_not]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y
[PROOFSTEP]
simp only [not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ max x y = if x < y then y else x
[PROOFSTEP]
rw [max_comm, max_def, ← ite_not]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then y else x) = if x < y then y else x
[PROOFSTEP]
simp only [not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
[PROOFSTEP]
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
[PROOFSTEP]
simp only [h, compareOfLessAndEq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
have : ¬f a = f b := by rename_i h; exact inj.ne h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ ¬f a = f b
[PROOFSTEP]
rename_i h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : ¬a < b
h : ¬a = b
⊢ ¬f a = f b
[PROOFSTEP]
exact inj.ne h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
this : ¬f a = f b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
have : f a = f b := by rename_i h; exact congrArg f h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ f a = f b
[PROOFSTEP]
rename_i h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : ¬a < b
h : a = b
⊢ f a = f b
[PROOFSTEP]
exact congrArg f h
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
this : f a = f b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), min a b = if a ≤ b then a else b
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ min x y = if x ≤ y then x else y
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = f (if x ≤ y then x else y)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = if x ≤ y then f x else f y
[PROOFSTEP]
exact (hinf _ _).trans (min_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), max a b = if a ≤ b then b else a
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ max x y = if x ≤ y then y else x
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = f (if x ≤ y then y else x)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = if x ≤ y then f y else f x
[PROOFSTEP]
exact (hsup _ _).trans (max_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), min a b = if a ≤ b then a else b
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ min x y = if x ≤ y then x else y
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = f (if x ≤ y then x else y)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = if x ≤ y then f x else f y
[PROOFSTEP]
exact (hinf _ _).trans (min_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), max a b = if a ≤ b then b else a
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ max x y = if x ≤ y then y else x
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = f (if x ≤ y then y else x)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = if x ≤ y then f y else f x
[PROOFSTEP]
exact (hsup _ _).trans (max_def _ _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
by_cases h₁ : y.1 ≤ x.1
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_le h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
exact Or.inl ⟨LE.le.lt_of_not_le h.1.1 h₁, h.1.2⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
[PROOFSTEP]
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
[GOAL]
case refine'_2.inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y
[PROOFSTEP]
exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_le h.1⟩
[GOAL]
case refine'_2.inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
[PROOFSTEP]
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_le h.2⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α
[PROOFSTEP]
convert @OrderDual.denselyOrdered αᵒᵈ _
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
simp_rw [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ a_2,
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
[PROOFSTEP]
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
[GOAL]
case inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h₁
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
c : α
ha : a.fst < c
hb : c < b.fst
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
[GOAL]
case inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h₂
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
classical
simp_rw [Pi.lt_def]
rintro ⟨hab, i, hi⟩
obtain ⟨c, ha, hb⟩ := exists_between hi
exact
  ⟨Function.update a i c, ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_same]⟩,
    update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_same]⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
simp_rw [Pi.lt_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ (a ≤ b ∧ ∃ i, a i < b i) → ∃ a_2, (a ≤ a_2 ∧ ∃ i, a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ i, a_2 i < b i
[PROOFSTEP]
rintro ⟨hab, i, hi⟩
[GOAL]
case intro.intro
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between hi
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
[PROOFSTEP]
exact
  ⟨Function.update a i c, ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_same]⟩,
    update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_same]⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i
[PROOFSTEP]
rwa [update_same]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i
[PROOFSTEP]
rwa [update_same]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z
[PROOFSTEP]
by_contra hne
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ False
[PROOFSTEP]
simp only [not_or, ← Ne.def] at hne
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False
[PROOFSTEP]
cases' hne.1.lt_or_lt with h₁ h₁
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False
[PROOFSTEP]
cases' hne.2.1.lt_or_lt with h₂ h₂
[GOAL]
case inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False
[PROOFSTEP]
cases' hne.2.1.lt_or_lt with h₂ h₂
[GOAL]
case inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inl.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False
case inl.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : z < x
⊢ False
case inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : x < z
⊢ False
case inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : z < x
⊢ False
case inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : x < z
⊢ False
case inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : z < x
⊢ False
case inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : x < z
⊢ False
case inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : z < x
⊢ False
[PROOFSTEP]
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a : PUnit), a ≤ a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝ : PUnit
⊢ a✝ ≤ a✝
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b c : PUnit), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝² b✝ c✝ : PUnit
a✝¹ : a✝² ≤ b✝
a✝ : b✝ ≤ c✝
⊢ a✝² ≤ c✝
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
simp only [not_true, and_false, forall_const]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝² b✝ : PUnit
a✝¹ : a✝² ≤ b✝
a✝ : b✝ ≤ a✝²
⊢ a✝² = b✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a ≤ b ∨ b ≤ a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝ b✝ : PUnit
⊢ a✝ ≤ b✝ ∨ b✝ ≤ a✝
[PROOFSTEP]
exact Or.inl trivial


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
[PROOFSTEP]
refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
⊢ Acc r x
[PROOFSTEP]
by_contra hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
⊢ False
[PROOFSTEP]
obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
⊢ False
[PROOFSTEP]
refine' hm ⟨_, fun y hy => _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
⊢ Acc r y
[PROOFSTEP]
by_contra hy'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False
[PROOFSTEP]
exact hm' y hy' hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (WellFounded.succ wf x)
[PROOFSTEP]
rw [WellFounded.succ, dif_pos h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (min wf {y | r x y} h)
[PROOFSTEP]
apply min_mem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) ↔ r y x ∨ y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) → r y x ∨ y = x
[PROOFSTEP]
intro h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
⊢ r y x ∨ y = x
[PROOFSTEP]
have : ¬r x y := by
  intro hy
  rw [WellFounded.succ, dif_pos] at h'
  exact wo.wf.not_lt_min _ h hy h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
⊢ ¬r x y
[PROOFSTEP]
intro hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
hy : r x y
⊢ False
[PROOFSTEP]
rw [WellFounded.succ, dif_pos] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h'✝ : r y (if h : ∃ y, r x y then min (_ : WellFounded r) {y | r x y} h else x)
h' : r y (min (_ : WellFounded r) {y | r x y} ?hc)
hy : r x y
⊢ False
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (if h : ∃ y, r x y then min (_ : WellFounded r) {y | r x y} h else x)
hy : r x y
⊢ ∃ y, r x y
[PROOFSTEP]
exact wo.wf.not_lt_min _ h hy h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
⊢ r y x ∨ y = x
[PROOFSTEP]
rcases trichotomous_of r x y with (hy | hy | hy)
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r x y
⊢ r y x ∨ y = x
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exfalso
[GOAL]
case mp.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r x y
⊢ False
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exact this hy
[GOAL]
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
right
[GOAL]
case mp.inr.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exact hy.symm
[GOAL]
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
left
[GOAL]
case mp.inr.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x
[PROOFSTEP]
exact hy
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y x ∨ y = x → r y (WellFounded.succ (_ : WellFounded r) x)
[PROOFSTEP]
rintro (hy | rfl)
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
hy : r y x
⊢ r y (WellFounded.succ (_ : WellFounded r) x)
case mpr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
[PROOFSTEP]
exact _root_.trans hy (wo.wf.lt_succ h)
[GOAL]
case mpr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
[PROOFSTEP]
exact wo.wf.lt_succ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ f b ≤ g b
[PROOFSTEP]
obtain ⟨c, hc⟩ : g b ∈ Set.range f := by
  rw [hfg]
  exact Set.mem_range_self b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range f
[PROOFSTEP]
rw [hfg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range g
[PROOFSTEP]
exact Set.mem_range_self b
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
⊢ f b ≤ g b
[PROOFSTEP]
cases' lt_or_le c b with hcb hbc
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hcb : c < b
⊢ f b ≤ g b
[PROOFSTEP]
rw [H c hcb] at hc
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : c < b
⊢ f b ≤ g b
[PROOFSTEP]
rw [hg.injective hc] at hcb
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : b < b
⊢ f b ≤ g b
[PROOFSTEP]
exact hcb.false.elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ g b
[PROOFSTEP]
rw [← hc]
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ f c
[PROOFSTEP]
exact hf.monotone hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
⊢ f = g
[PROOFSTEP]
funext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
a : β
⊢ f a = g a
[PROOFSTEP]
apply h.induction a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
[PROOFSTEP]
exact fun b H =>
  le_antisymm (eq_strictMono_iff_eq_range_aux hf hg hfg H)
    (eq_strictMono_iff_eq_range_aux hg hf hfg.symm fun a hab => (H a hab).symm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
⊢ ∀ (n : β), n ≤ f n
[PROOFSTEP]
by_contra' h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False
[PROOFSTEP]
have h₂ := h.min_mem _ h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : min h (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False
[PROOFSTEP]
exact h.not_lt_min _ h₁ (hf h₂) h₂