awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inr₃ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inl₄ inl₅ inl₆ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₇ inl₈ inl₉ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₄ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬Nontrivial.{u_1} αˣ → DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₅ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬DenselyOrdered.{u_1} αˣ → DenselyOrdered α
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inr₃ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inl₄ inl₅ inl₆ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₇ inl₈ inl₉ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₄ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬Nontrivial.{u_1} αˣ → DenselyOrdered α
inr₅ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬DenselyOrdered.{u_1} αˣ → DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₆ : ¬DenselyOrdered α → DenselyOrdered α → ¬Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₁ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inr₁ :
  ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → (DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α)
inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₃ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₂ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inr₃ : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inl₄ inl₅ inl₆ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inl₇ inl₈ inl₉ :
  DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered α → DenselyOrdered.{u_1} αˣ
inr₄ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬Nontrivial.{u_1} αˣ → DenselyOrdered α
inr₅ : ¬DenselyOrdered α → DenselyOrdered.{u_1} αˣ → ¬DenselyOrdered.{u_1} αˣ → DenselyOrdered α
inr₆ : ¬DenselyOrdered α → DenselyOrdered α → ¬Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α
have inr₇ : ¬DenselyOrdered α → DenselyOrdered α → ¬DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b : α
inst_2 : Mul α
inst_3 : MulLeftMono α
⊢ MulLeftMono.{u_1} (WithZero α)
have refine : ∀ (a b c : WithZero α) (hbc : b ≤ c), a * b ≤ a * c
Tactic: refine ⟨fun a b c hbc => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a_1 b_1 : α
inst_2 : Mul α
inst_3 : MulLeftMono α
a b c : WithZero α
hbc : b ≤ c
⊢ a * b ≤ a * c
have zero : 0 * b ≤ 0 * c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a_1 b_1 : α
inst_2 : Mul α
inst_3 : MulLeftMono α
a b c : WithZero α
hbc : b ≤ c
zero : 0 * b ≤ 0 * c
⊢ a * b ≤ a * c
have coe : ∀ (a : α), (↑a : WithZero α) * b ≤ (↑a : WithZero α) * c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b_1 : α
inst_2 : Mul α
inst_3 : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
a_1 : α
⊢ (↑a_1 : WithZero α) * b ≤ (↑a_1 : WithZero α) * c
have coe : ∀ (hbc : 0 ≤ c), (↑a_1 : WithZero α) * 0 ≤ (↑a_1 : WithZero α) * c
Tactic: induction b
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b_1 : α
inst_2 : Mul α
inst_3 : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
a_1 : α
coe : ∀ (hbc : 0 ≤ c), (↑a_1 : WithZero α) * 0 ≤ (↑a_1 : WithZero α) * c
⊢ (↑a_1 : WithZero α) * b ≤ (↑a_1 : WithZero α) * c
have coe₁ : ∀ (a : α) (hbc : (↑a : WithZero α) ≤ c), (↑a_1 : WithZero α) * (↑a : WithZero α) ≤ (↑a_1 : WithZero α) * c
Tactic: induction b
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b : α
inst_2 : Mul α
inst_3 : MulLeftMono α
c : WithZero α
a_1 a_2 : α
hbc : (↑a_2 : WithZero α) ≤ c
⊢ (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * c
have coe : ∀ (c : α) (hbc' : a_2 ≤ c) (hbc : (↑a_2 : WithZero α) ≤ (↑c : WithZero α)),
  (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * (↑c : WithZero α)
Tactic: rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b : α
inst_2 : Mul α
inst_3 : MulLeftMono α
a_1 a_2 c : α
hbc' : a_2 ≤ c
hbc : (↑a_2 : WithZero α) ≤ (↑c : WithZero α)
⊢ (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * (↑c : WithZero α)
have coe : a_1 * a_2 ≤ a_1 * c
Tactic: rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono.{u_1} (WithZero α)
have refine : ∀ (a b c : WithZero α) (hbc : b ≤ c), a + b ≤ a + c
Tactic: refine ⟨fun a b c hbc => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c
have zero : 0 + b ≤ 0 + c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
zero : 0 + b ≤ 0 + c
⊢ a + b ≤ a + c
have coe : ∀ (a : α), (↑a : WithZero α) + b ≤ (↑a : WithZero α) + c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c
have zero : b ≤ 0 + c
Tactic: rwa [zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a : α
⊢ (↑a : WithZero α) + b ≤ (↑a : WithZero α) + c
have coe : ∀ (hbc : 0 ≤ c), (↑a : WithZero α) + 0 ≤ (↑a : WithZero α) + c
Tactic: induction b
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a : α
coe : ∀ (hbc : 0 ≤ c), (↑a : WithZero α) + 0 ≤ (↑a : WithZero α) + c
⊢ (↑a : WithZero α) + b ≤ (↑a : WithZero α) + c
have coe₁ : ∀ (a_1 : α) (hbc : (↑a_1 : WithZero α) ≤ c), (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + c
Tactic: induction b
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a : α
hbc : 0 ≤ c
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + c
have coe : ∀ (hbc : LE.le.{u_1} (α := WithZero α) 0 0), (↑a : WithZero α) ≤ (↑a : WithZero α) + 0
Tactic: induction c
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a : α
hbc : 0 ≤ c
coe : ∀ (hbc : LE.le.{u_1} (α := WithZero α) 0 0), (↑a : WithZero α) ≤ (↑a : WithZero α) + 0
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + c
have coe₁ : ∀ (a_1 : α) (hbc : 0 ≤ (↑a_1 : WithZero α)), (↑a : WithZero α) ≤ (↑a : WithZero α) + (↑a_1 : WithZero α)
Tactic: induction c
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a : α
hbc : LE.le.{u_1} (α := WithZero α) 0 0
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + 0
have coe : (↑a : WithZero α) ≤ (↑a : WithZero α)
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a a_1 : α
hbc : 0 ≤ (↑a_1 : WithZero α)
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + (↑a_1 : WithZero α)
have coe : a ≤ a + a_1
Tactic: rw [← coe_add, coe_le_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a a_1 : α
hbc : (↑a_1 : WithZero α) ≤ c
⊢ (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + c
have coe : ∀ (c : α) (hbc' : a_1 ≤ c) (hbc : (↑a_1 : WithZero α) ≤ (↑c : WithZero α)),
  (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + (↑c : WithZero α)
Tactic: rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a a_1 c : α
hbc' : a_1 ≤ c
hbc : (↑a_1 : WithZero α) ≤ (↑c : WithZero α)
⊢ (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + (↑c : WithZero α)
have coe : a + a_1 ≤ a + c
Tactic: rw [← coe_add, ← coe_add _ c, coe_le_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a_1 b_1 : α
inst_2 : Add α
inst_3 : ExistsAddOfLE α
a b : WithZero α
⊢ a ≤ b → ∃ (c : WithZero α), b = a + c
have zero : 0 ≤ b → ∃ (c : WithZero α), b = 0 + c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a_1 b_1 : α
inst_2 : Add α
inst_3 : ExistsAddOfLE α
a b : WithZero α
zero : 0 ≤ b → ∃ (c : WithZero α), b = 0 + c
⊢ a ≤ b → ∃ (c : WithZero α), b = a + c
have coe : ∀ (a : α), (↑a : WithZero α) ≤ b → ∃ (c : WithZero α), b = (↑a : WithZero α) + c
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b_1 : α
inst_2 : Add α
inst_3 : ExistsAddOfLE α
b : WithZero α
a_1 : α
⊢ (↑a_1 : WithZero α) ≤ b → ∃ (c : WithZero α), b = (↑a_1 : WithZero α) + c
have coe : (↑a_1 : WithZero α) ≤ 0 → ∃ (c : WithZero α), 0 = (↑a_1 : WithZero α) + c
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b_1 : α
inst_2 : Add α
inst_3 : ExistsAddOfLE α
b : WithZero α
a_1 : α
coe : (↑a_1 : WithZero α) ≤ 0 → ∃ (c : WithZero α), 0 = (↑a_1 : WithZero α) + c
⊢ (↑a_1 : WithZero α) ≤ b → ∃ (c : WithZero α), b = (↑a_1 : WithZero α) + c
have coe₁ : ∀ (a : α), (↑a_1 : WithZero α) ≤ (↑a : WithZero α) → ∃ (c : WithZero α), (↑a : WithZero α) = (↑a_1 : WithZero α) + c
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b : α
inst_2 : Add α
inst_3 : ExistsAddOfLE α
a_1 a_2 : α
h : (↑a_1 : WithZero α) ≤ (↑a_2 : WithZero α)
⊢ ∃ (c : WithZero α), (↑a_2 : WithZero α) = (↑a_1 : WithZero α) + c
have coe : ∀ (c : α) (h : (↑a_1 : WithZero α) ≤ (↑(a_1 + c) : WithZero α)),
  ∃ (c_1 : WithZero α), (↑(a_1 + c) : WithZero α) = (↑a_1 : WithZero α) + c_1
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
Cleared hypotheses: a_2, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
⊢ ∃ (y : WithZero α), y ≠ 0 ∧ y < x
have obtain : ∀ (z : α) (hlt : z < unzero hx), ∃ (y : WithZero α), y ≠ 0 ∧ y < x
Tactic: obtain ⟨z, hlt⟩ := exists_lt (WithZero.unzero hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
z : α
hlt : z < unzero hx
⊢ ∃ (y : WithZero α), y ≠ 0 ∧ y < x
have hlt₁ : (↑z : WithZero α) < x
Tactic: rw [← WithZero.coe_lt_coe, WithZero.coe_unzero hx] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
have rwa : ∀
  (h :
    (↑(unzero ha) : WithZero (Multiplicative α)) <
      (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
  (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← toAdd_lt, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) <
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
have rwa₁ : ∀ (h : unzero ha < (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← toAdd_lt, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) <
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
rwa₁ : ∀ (h : unzero ha < (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
have rwa₂ : ∀
  (h :
    LT.lt (α := α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α)
      ((toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) : α)),
  (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← toAdd_lt, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) <
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
rwa₁ : ∀ (h : unzero ha < (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
rwa₂ :
  ∀
    (h :
      LT.lt (α := α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α)
        ((toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) : α)),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
have rwa₃ : ∀ (h : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b), (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← toAdd_lt, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
⊢ a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa : (↑(unzero ha) : WithZero (Multiplicative α)) < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
rwa :
  (↑(unzero ha) : WithZero (Multiplicative α)) <
    (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
⊢ a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa₁ : unzero ha < (ofAdd : (a : α) → Multiplicative α) b
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
rwa :
  (↑(unzero ha) : WithZero (Multiplicative α)) <
    (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa₁ : unzero ha < (ofAdd : (a : α) → Multiplicative α) b
⊢ a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
have rwa₂ : LT.lt (α := Multiplicative α)
  ((ofAdd : (a : α) → Multiplicative α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α) : Multiplicative α)
  ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α)
Tactic: rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
have rwa : ∀
  (h :
    (↑(unzero ha) : WithZero (Multiplicative α)) ≤
      (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
  (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) ≤
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
have rwa₁ : ∀ (h : unzero ha ≤ (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))
rwa :
  ∀
    (h :
      (↑(unzero ha) : WithZero (Multiplicative α)) ≤
        (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa₁ : ∀ (h : unzero ha ≤ (ofAdd : (a : α) → Multiplicative α) b), (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
have rwa₂ : ∀
  (h :
    LE.le (α := α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α)
      ((toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) : α)),
  (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
Tactic: rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h
Cleared hypotheses: h