awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
⊢ cmpLE x y = cmp x y
have pos : ∀ (xy : x ≤ y), cmpLE x y = cmp x y
Tactic: by_cases xy : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
pos : ∀ (xy : x ≤ y), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y
have neg : ∀ (xy : ¬x ≤ y), cmpLE x y = cmp x y
Tactic: by_cases xy : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y
have pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : x ≤ y
pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y
have neg : ∀ (yx : ¬y ≤ x), cmpLE x y = cmp x y
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y
have pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y
have neg : ∀ (yx : ¬y ≤ x), cmpLE x y = cmp x y
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
have neg : False
Tactic: simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
⊢ o.swap.Compares a b ↔ o.Compares b a
have lt : lt.swap.Compares a b ↔ lt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt : Ordering.lt.swap.Compares a b ↔ Ordering.lt.Compares b a
⊢ o.swap.Compares a b ↔ o.Compares b a
have eq : eq.swap.Compares a b ↔ eq.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt : Ordering.lt.swap.Compares a b ↔ Ordering.lt.Compares b a
eq : Ordering.eq.swap.Compares a b ↔ Ordering.eq.Compares b a
⊢ o.swap.Compares a b ↔ o.Compares b a
have gt : gt.swap.Compares a b ↔ gt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap
have rw : o.swap.swap = o'.swap ↔ o = o'.swap
Tactic: rw [← swap_inj, swap_swap]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
o o' : Ordering
rw : o.swap.swap = o'.swap ↔ o = o'.swap
⊢ o.swap = o' ↔ o = o'.swap
have rw₁ : o = o'.swap ↔ o = o'.swap
Tactic: rw [← swap_inj, swap_swap]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'
have refine : ∀ (ho : o.Compares a' b'), o.Compares a b
Tactic: refine ⟨h, fun ho => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
⊢ o.Compares a b
have inl : ∀ (hab : a < b), o.Compares a b
Tactic: rcases lt_trichotomy a b with hab | hab | hab
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
inl : ∀ (hab : a < b), o.Compares a b
⊢ o.Compares a b
have inr : ∀ (hab : a = b), o.Compares a b
Tactic: rcases lt_trichotomy a b with hab | hab | hab
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
inl : ∀ (hab : a < b), o.Compares a b
inr : ∀ (hab : a = b), o.Compares a b
⊢ o.Compares a b
have inr₁ : ∀ (hab : b < a), o.Compares a b
Tactic: rcases lt_trichotomy a b with hab | hab | hab
-- Lean 4 proof step from Mathlib.Order.Compare (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b
have hab₁ : lt.Compares a b
Tactic: have hab : Compares Ordering.lt a b := hab
-- Lean 4 proof step from Mathlib.Order.Compare (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b
have hab₁ : eq.Compares a b
Tactic: have hab : Compares Ordering.eq a b := hab
-- Lean 4 proof step from Mathlib.Order.Compare (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b
have hab₁ : gt.Compares a b
Tactic: have hab : Compares Ordering.gt a b := hab
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
⊢ o.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ o.Compares b a
have lt : lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ lt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt :
  Ordering.lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.lt.Compares b a
⊢ o.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ o.Compares b a
have eq : eq.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ eq.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt :
  Ordering.lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.lt.Compares b a
eq :
  Ordering.eq.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.eq.Compares b a
⊢ o.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ o.Compares b a
have gt : gt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ gt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
o : Ordering
⊢ o.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ o.Compares b a
have lt : lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ lt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
o : Ordering
lt :
  Ordering.lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.lt.Compares b a
⊢ o.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ o.Compares b a
have eq : eq.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ eq.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
o : Ordering
lt :
  Ordering.lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.lt.Compares b a
eq :
  Ordering.eq.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.eq.Compares b a
⊢ o.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ o.Compares b a
have gt : gt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ gt.Compares b a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b
have inl : ∀ (h : a < b), (cmp a b).Compares a b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), (cmp a b).Compares a b
⊢ (cmp a b).Compares a b
have inr : ∀ (h : a = b), (cmp a b).Compares a b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), (cmp a b).Compares a b
inr : ∀ (h : a = b), (cmp a b).Compares a b
⊢ (cmp a b).Compares a b
have inr₁ : ∀ (h : b < a), (cmp a b).Compares a b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have pos : ∀ (h : a < b),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
pos :
  ∀ (h : a < b),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have neg : ∀ (h : ¬a < b),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : a < b
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have pos : ∀ (h₂ : b < a),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h₂ : b < a
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : a < b
pos :
  ∀ (h₂ : b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have neg : ∀ (h₂ : ¬b < a),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h₂ : b < a
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : ¬a < b
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have pos : ∀ (h₂ : b < a),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h₂ : b < a
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : ¬a < b
pos :
  ∀ (h₂ : b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
have neg : ∀ (h₂ : ¬b < a),
  (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
Tactic: by_cases h₂ : b < a
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
⊢ cmp x x = eq
have rw : x = x
Tactic: rw [cmp_eq_eq_iff]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
have rwa : cmp y x = (cmp x' y').swap
Tactic: rwa [← cmp_swap x', ← cmp_swap, swap_inj]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rwa : cmp y x = (cmp x' y').swap
⊢ cmp y x = cmp y' x'
have rwa₁ : (cmp x y).swap = (cmp x' y').swap
Tactic: rwa [← cmp_swap x', ← cmp_swap, swap_inj]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'
have rwa : cmp x y = (cmp y' x').swap
Tactic: rwa [← cmp_swap y', ← cmp_swap, swap_inj]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
rwa : cmp x y = (cmp y' x').swap
⊢ cmp x y = cmp x' y'
have rwa₁ : (cmp y x).swap = (cmp y' x').swap
Tactic: rwa [← cmp_swap y', ← cmp_swap, swap_inj]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'
have rw : cmp x y = lt ↔ x' < y'
Tactic: rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : cmp x y = lt ↔ x' < y'
⊢ x < y ↔ x' < y'
have rw₁ : cmp x y = lt ↔ cmp x' y' = lt
Tactic: rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : cmp x y = lt ↔ x' < y'
rw₁ : cmp x y = lt ↔ cmp x' y' = lt
⊢ x < y ↔ x' < y'
have rw₂ : cmp x' y' = lt ↔ cmp x' y' = lt
Tactic: rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'
have rw : ¬y < x ↔ ¬y' < x'
Tactic: rw [← not_lt, ← not_lt]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
have h₁ : y < x ↔ y' < x'
Tactic: apply not_congr
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'
have h₁ : cmp y x = cmp y' x'
Tactic: apply lt_iff_lt_of_cmp_eq_cmp
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'
have rw : x ≤ y ∧ y ≤ x ↔ x' = y'
Tactic: rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : x ≤ y ∧ y ≤ x ↔ x' = y'
⊢ x = y ↔ x' = y'
have rw₁ : x ≤ y ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
Tactic: rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : x ≤ y ∧ y ≤ x ↔ x' = y'
rw₁ : x ≤ y ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
⊢ x = y ↔ x' = y'
have rw₂ : x' ≤ y' ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
Tactic: rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : x ≤ y ∧ y ≤ x ↔ x' = y'
rw₁ : x ≤ y ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
rw₂ : x' ≤ y' ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
⊢ x = y ↔ x' = y'
have rw₃ : x' ≤ y' ∧ y' ≤ x' ↔ x' ≤ y' ∧ y' ≤ x'
Tactic: rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₁ : Eq.{u + 1} (α := α) (⨆ (a_1 : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊓ a)
  (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
rw₁ :
  Eq.{u + 1} (α := α) (⨆ (a_1 : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊓ a)
    (⨆ (i : ι), f i ⊓ a)
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₂ : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ a) (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
have rw : sInf (range fun (i : ι) ↦ f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
Tactic: rw [iInf, sInf_sup_eq, iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
rw : sInf (range fun (i : ι) ↦ f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
⊢ (⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
have rw₁ : Eq.{u + 1} (α := α) (⨅ (a_1 : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊔ a)
  (⨅ (i : ι), f i ⊔ a)
Tactic: rw [iInf, sInf_sup_eq, iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
rw : sInf (range fun (i : ι) ↦ f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
rw₁ :
  Eq.{u + 1} (α := α) (⨅ (a_1 : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊔ a)
    (⨅ (i : ι), f i ⊔ a)
⊢ (⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a
have rw₂ : Eq.{u + 1} (α := α) (⨅ (i : ι), f i ⊔ a) (⨅ (i : ι), f i ⊔ a)
Tactic: rw [iInf, sInf_sup_eq, iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))
have refine : LE.le.{u} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))
Tactic: refine le_antisymm ?_ le_iInf_iSup
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
have simp_rw : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
  (⨅ (i : Set α),
    ⨅ (_ : Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) i), ⨆ (b : (↑i : Type u)), (↑b : α))
Tactic: simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
simp_rw :
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (i : Set α),
      ⨅ (_ : Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) i), ⨆ (b : (↑i : Type u)), (↑b : α))
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
have simp_rw₁ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨅ (i : ι), ⨆ (b : (↑(range (f i)) : Type u)), (↑b : α))
Tactic: simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
simp_rw :
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (i : Set α),
      ⨅ (_ : Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) i), ⨆ (b : (↑i : Type u)), (↑b : α))
simp_rw₁ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨅ (i : ι), ⨆ (b : (↑(range (f i)) : Type u)), (↑b : α))
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
have simp_rw₂ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨅ (i : ι), ⨆ i_1 ∈ range (f i), i_1)
Tactic: simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]