awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
n : ℕ∞
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = n
top :
  ∀ (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = ⊤),
    height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * ⊤ + (↑m : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * n + (↑m : ℕ∞)
have coe : ∀ (n : ℕ) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)),
  height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
Tactic: cases n with | top => simp | coe n =>
    induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
    lia
Cleared hypotheses: n, h'
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := βᵒᵈ) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)
have h₁ : ∀ (x : βᵒᵈ),
  krullDim.{u_1}
      (↑(Set.preimage (β := βᵒᵈ)
            (⇑((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f : OrderHom.{u_1, u_2} αᵒᵈ βᵒᵈ) : (a : αᵒᵈ) → βᵒᵈ) {x}) :
        Type u_1) ≤
    (↑m : WithBot ℕ∞)
Tactic: apply height_le_of_krullDim_preimage_le (f := f.dual)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
⊢ krullDim α ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * krullDim β + (↑m : WithBot ℕ∞)
have rw : ∀ (i : α),
  (↑(height i) : WithBot ℕ∞) ≤
    (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
Tactic: rw [Order.krullDim_eq_iSup_height, Order.krullDim_eq_iSup_height, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
⊢ ∀ (i : α),
    (↑(height i) : WithBot ℕ∞) ≤
      (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
have refine : ∀ (x : α),
  (fun (a : ℕ∞) ↦ (↑a : WithBot ℕ∞))
      (HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := β) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)) ≤
    (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
Tactic: refine fun x ↦ (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)).trans ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) +
      (↑m : WithBot ℕ∞) ≤
    (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
have bc : 0 ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
bc : 0 ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1
⊢ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) +
      (↑m : WithBot ℕ∞) ≤
    (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
have bc₁ : (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) ≤ ⨆ (a : β), (↑(height a) : WithBot ℕ∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
e : α ↪o β
⊢ krullDim α ≤ krullDim β
have this : ∀ (b : β), Subsingleton.{u_1 + 1} (↑(Set.preimage (β := β) (⇑e : (a : α) → β) {b}) : Type u_1)
Tactic: have (b : β) : Subsingleton (e ⁻¹' {b}) := Set.Subsingleton.coe_sort <|
    Set.Subsingleton.preimage Set.subsingleton_singleton e.injective
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r b c
have suffices : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
Tactic: suffices r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c)) by
    simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
have apply : r (b ⊓ c) d
Tactic: apply (h₄ (inf_le_of_left_le hbd) _).1
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)
have rw : r (y ⊓ (x ⊓ z)) (y ⊓ z)
Tactic: rw [inf_comm x, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)
have suffices : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
Tactic: suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
⊢ r (w ⊓ y) (x ⊓ z)
have have : ∀ (compatible_left_inf : ∀ {x y t : α} (hh : r x y), r (x ⊓ t) (y ⊓ t)), r (w ⊓ y) (x ⊓ z)
Tactic: have compatible_left_inf {x y t : α} (hh : r x y) : r (x ⊓ t) (y ⊓ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊓ t) _ _ ((x ⊔ y) ⊓ t)
            (inf_le_inf_right _ inf_le_left) (inf_le_inf_right _ le_sup_left)
            (inf_le_inf_right _ inf_le_right) (inf_le_inf_right _ le_sup_right)
            (h₄ inf_le_sup (h₂.mp hh)).1
-- Lean 4 proof step from Mathlib.Order.Lattice.Congruence (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x y z : α
h1 : r w x
h2 : r y z
⊢ r (w ⊔ y) (x ⊔ z)
have have : ∀ (compatible_left_sup : ∀ {x y t : α} (hh : r x y), r (x ⊔ t) (y ⊔ t)), r (w ⊔ y) (x ⊔ z)
Tactic: have compatible_left_sup {x y t : α} (hh : r x y) : r (x ⊔ t) (y ⊔ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊔ t) _ _ ((x ⊔ y) ⊔ t)
        (sup_le_sup_right inf_le_left _) (sup_le_sup_right le_sup_left _)
        (sup_le_sup_right inf_le_right _) (sup_le_sup_right le_sup_right _)
        (h₄ inf_le_sup (h₂.mp hh)).2
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ a ⊔ c = c
have rw : a ⊔ (b ⊔ c) = b ⊔ c
Tactic: rw [← hbc, ← sup_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
rw : a ⊔ (b ⊔ c) = b ⊔ c
⊢ a ⊔ c = c
have rw₁ : a ⊔ b ⊔ c = b ⊔ c
Tactic: rw [← hbc, ← sup_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
rw : a ⊔ (b ⊔ c) = b ⊔ c
rw₁ : a ⊔ b ⊔ c = b ⊔ c
⊢ a ⊔ c = c
have rw₂ : b ⊔ c = b ⊔ c
Tactic: rw [← hbc, ← sup_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ⊔ b = b
hba : b ⊔ a = a
⊢ a = b
have rwa : b ⊔ a = b
Tactic: rwa [← hba, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b
have rw : a ⊔ a ⊔ b = a ⊔ b
Tactic: rw [← sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
rw : a ⊔ a ⊔ b = a ⊔ b
⊢ a ⊔ (a ⊔ b) = a ⊔ b
have rw₁ : a ⊔ b = a ⊔ b
Tactic: rw [← sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ b ⊔ (a ⊔ b) = a ⊔ b
have rw : a ⊔ b ⊔ b = a ⊔ b
Tactic: rw [sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
rw : a ⊔ b ⊔ b = a ⊔ b
⊢ b ⊔ (a ⊔ b) = a ⊔ b
have rw₁ : a ⊔ (b ⊔ b) = a ⊔ b
Tactic: rw [sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
rw : a ⊔ b ⊔ b = a ⊔ b
rw₁ : a ⊔ (b ⊔ b) = a ⊔ b
⊢ b ⊔ (a ⊔ b) = a ⊔ b
have rw₂ : a ⊔ b = a ⊔ b
Tactic: rw [sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
⊢ a ⊔ b ⊔ c = c
have rwa : a ⊔ (b ⊔ c) = c
Tactic: rwa [sup_assoc, hbc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ a ⊓ c = c
have rw : a ⊓ (b ⊓ c) = b ⊓ c
Tactic: rw [← hbc, ← inf_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
rw : a ⊓ (b ⊓ c) = b ⊓ c
⊢ a ⊓ c = c
have rw₁ : a ⊓ b ⊓ c = b ⊓ c
Tactic: rw [← hbc, ← inf_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
rw : a ⊓ (b ⊓ c) = b ⊓ c
rw₁ : a ⊓ b ⊓ c = b ⊓ c
⊢ a ⊓ c = c
have rw₂ : b ⊓ c = b ⊓ c
Tactic: rw [← hbc, ← inf_assoc, hab]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
hba : b ⊓ a = a
hab : a ⊓ b = b
⊢ a = b
have rwa : b ⊓ a = b
Tactic: rwa [← hba, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ a ⊓ (a ⊓ b) = a ⊓ b
have rw : a ⊓ a ⊓ b = a ⊓ b
Tactic: rw [← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
rw : a ⊓ a ⊓ b = a ⊓ b
⊢ a ⊓ (a ⊓ b) = a ⊓ b
have rw₁ : a ⊓ b = a ⊓ b
Tactic: rw [← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ b ⊓ (a ⊓ b) = a ⊓ b
have rw : a ⊓ b ⊓ b = a ⊓ b
Tactic: rw [inf_comm, inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
rw : a ⊓ b ⊓ b = a ⊓ b
⊢ b ⊓ (a ⊓ b) = a ⊓ b
have rw₁ : a ⊓ (b ⊓ b) = a ⊓ b
Tactic: rw [inf_comm, inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
rw : a ⊓ b ⊓ b = a ⊓ b
rw₁ : a ⊓ (b ⊓ b) = a ⊓ b
⊢ b ⊓ (a ⊓ b) = a ⊓ b
have rw₂ : a ⊓ b = a ⊓ b
Tactic: rw [inf_comm, inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b c : α
hac : b ⊓ a = a
hbc : c ⊓ a = a
⊢ b ⊓ c ⊓ a = a
have rwa : b ⊓ (c ⊓ a) = a
Tactic: rwa [inf_assoc, hbc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ≤ b ↔ ∃ (c : α), b = a ⊔ c
have mp : a ≤ b → ∃ (c : α), b = a ⊔ c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
mp : a ≤ b → ∃ (c : α), b = a ⊔ c
⊢ a ≤ b ↔ ∃ (c : α), b = a ⊔ c
have mpr : (∃ (c : α), b = a ⊔ c) → a ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
⊢ a ⊔ b = b ⊔ a
have a₁ : a ⊔ b ≤ b ⊔ a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
a₁ : a ⊔ b ≤ b ⊔ a
⊢ a ⊔ b = b ⊔ a
have a₂ : b ⊔ a ≤ a ⊔ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x
have simp : (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
Tactic: simp only [sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
have rw : a ≤ x ∧ b ≤ x ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
Tactic: rw [and_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a
have rw : c ⊔ (a ⊔ b) = c ⊔ b ⊔ a
Tactic: rw [sup_comm, sup_comm a, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : c ⊔ (a ⊔ b) = c ⊔ b ⊔ a
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a
have rw₁ : c ⊔ (b ⊔ a) = c ⊔ b ⊔ a
Tactic: rw [sup_comm, sup_comm a, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : c ⊔ (a ⊔ b) = c ⊔ b ⊔ a
rw₁ : c ⊔ (b ⊔ a) = c ⊔ b ⊔ a
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a
have rw₂ : c ⊔ (b ⊔ a) = c ⊔ (b ⊔ a)
Tactic: rw [sup_comm, sup_comm a, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
have rw : a ⊔ b ⊔ c = b ⊔ (a ⊔ c)
Tactic: rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ b ⊔ c = b ⊔ (a ⊔ c)
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
have rw₁ : a ⊔ b ⊔ c = b ⊔ a ⊔ c
Tactic: rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ b ⊔ c = b ⊔ (a ⊔ c)
rw₁ : a ⊔ b ⊔ c = b ⊔ a ⊔ c
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
have rw₂ : b ⊔ a ⊔ c = b ⊔ a ⊔ c
Tactic: rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b
have rw : a ⊔ (b ⊔ c) = a ⊔ c ⊔ b
Tactic: rw [sup_assoc, sup_assoc, sup_comm b]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = a ⊔ c ⊔ b
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b
have rw₁ : a ⊔ (b ⊔ c) = a ⊔ (c ⊔ b)
Tactic: rw [sup_assoc, sup_assoc, sup_comm b]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = a ⊔ c ⊔ b
rw₁ : a ⊔ (b ⊔ c) = a ⊔ (c ⊔ b)
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b
have rw₂ : a ⊔ (c ⊔ b) = a ⊔ (c ⊔ b)
Tactic: rw [sup_assoc, sup_assoc, sup_comm b]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
have rw : a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
Tactic: rw [sup_assoc, sup_left_comm b, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c d : α
rw : a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
have rw₁ : a ⊔ (c ⊔ (b ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
Tactic: rw [sup_assoc, sup_left_comm b, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c d : α
rw : a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
rw₁ : a ⊔ (c ⊔ (b ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
have rw₂ : a ⊔ c ⊔ (b ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
Tactic: rw [sup_assoc, sup_left_comm b, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = b ⊔ c ⊔ a
have rw : a ⊔ (b ⊔ c) = b ⊔ c ⊔ a
Tactic: rw [sup_assoc, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = b ⊔ c ⊔ a
⊢ a ⊔ b ⊔ c = b ⊔ c ⊔ a
have rw₁ : b ⊔ c ⊔ a = b ⊔ c ⊔ a
Tactic: rw [sup_assoc, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)
have rw : b ⊔ c ⊔ a = b ⊔ (c ⊔ a)
Tactic: rw [sup_comm, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : b ⊔ c ⊔ a = b ⊔ (c ⊔ a)
⊢ a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)
have rw₁ : b ⊔ (c ⊔ a) = b ⊔ (c ⊔ a)
Tactic: rw [sup_comm, sup_assoc]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
have rw : a ⊔ (b ⊔ c) = a ⊔ a ⊔ (b ⊔ c)
Tactic: rw [sup_sup_sup_comm, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = a ⊔ a ⊔ (b ⊔ c)
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
have rw₁ : a ⊔ (b ⊔ c) = a ⊔ (b ⊔ c)
Tactic: rw [sup_sup_sup_comm, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
have rw : a ⊔ b ⊔ c = a ⊔ b ⊔ (c ⊔ c)
Tactic: rw [sup_sup_sup_comm, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ b ⊔ c = a ⊔ b ⊔ (c ⊔ c)
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
have rw₁ : a ⊔ b ⊔ c = a ⊔ b ⊔ c
Tactic: rw [sup_sup_sup_comm, sup_idem]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c
have simp : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
Tactic: simp only [sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
have rw : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
Tactic: rw [← H, @sup_le_iff α A, H, H]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
rw : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
have rw₁ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
Tactic: rw [← H, @sup_le_iff α A, H, H]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
rw : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₁ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
have rw₂ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
Tactic: rw [← H, @sup_le_iff α A, H, H]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
rw : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₁ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₂ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
have rw₃ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
Tactic: rw [← H, @sup_le_iff α A, H, H]