awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x ∧ z < y
have right : z < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
right : z < x
⊢ z < x ∧ z < y
have right₁ : z < y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (hypothesis)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
⊢ IsOrderedAddMonoid.{u_1} (WithZero α)
have this : AddLeftMono.{u_1} (WithZero α)
Tactic: have := WithZero.addLeftMono zero_le
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
a : α
h : 0 < (↑a : WithZero α)
b c : α
hbc : (↑b : WithZero α) < (↑c : WithZero α)
⊢ (↑a : WithZero α) * (↑b : WithZero α) < (↑a : WithZero α) * (↑c : WithZero α)
have norm_cast : ∀ (hbc : b < c), a * b < a * c
Tactic: norm_cast at *
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log ≤ y.log ↔ x ≤ y
have lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log ≤ y.log ↔ (↑x : WithZero (Multiplicative G)) ≤ y
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log ≤ y.log ↔ (↑x : WithZero (Multiplicative G)) ≤ y
have lift : ∀ (y : Multiplicative G),
  (↑x : WithZero (Multiplicative G)).log ≤ (↑y : WithZero (Multiplicative G)).log ↔
    (↑x : WithZero (Multiplicative G)) ≤ (↑y : WithZero (Multiplicative G))
Tactic: lift y to Multiplicative G using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log < y.log ↔ x < y
have lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log < y.log ↔ (↑x : WithZero (Multiplicative G)) < y
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log < y.log ↔ (↑x : WithZero (Multiplicative G)) < y
have lift : ∀ (y : Multiplicative G),
  (↑x : WithZero (Multiplicative G)).log < (↑y : WithZero (Multiplicative G)).log ↔
    (↑x : WithZero (Multiplicative G)) < (↑y : WithZero (Multiplicative G))
Tactic: lift y to Multiplicative G using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x.log ≤ a ↔ x ≤ exp a
have lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log ≤ a ↔ (↑x : WithZero (Multiplicative G)) ≤ exp a
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x.log < a ↔ x < exp a
have lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log < a ↔ (↑x : WithZero (Multiplicative G)) < exp a
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a ≤ x.log ↔ exp a ≤ x
have lift : ∀ (x : Multiplicative G), a ≤ (↑x : WithZero (Multiplicative G)).log ↔ exp a ≤ (↑x : WithZero (Multiplicative G))
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a < x.log ↔ exp a < x
have lift : ∀ (x : Multiplicative G), a < (↑x : WithZero (Multiplicative G)).log ↔ exp a < (↑x : WithZero (Multiplicative G))
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
⊢ x ≤ exp a
have inl : ∀ (hxa : log 0 ≤ a), 0 ≤ exp a
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x, hxa
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
inl : ∀ (hxa : log 0 ≤ a), 0 ≤ exp a
⊢ x ≤ exp a
have inr : ∀ (hx : x ≠ 0), x ≤ exp a
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
⊢ x < exp a
have inl : ∀ (hxa : log 0 < a), 0 < exp a
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x, hxa
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
inl : ∀ (hxa : log 0 < a), 0 < exp a
⊢ x < exp a
have inr : ∀ (hx : x ≠ 0), x < exp a
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
⊢ x < y * exp 1 ↔ x ≤ y
have lift : ∀ (y : Multiplicative ℤ), x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
Tactic: lift y to Multiplicative ℤ using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
⊢ x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
have inl : 0 < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ 0 ≤ (↑y : WithZero (Multiplicative ℤ))
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
inl : 0 < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ 0 ≤ (↑y : WithZero (Multiplicative ℤ))
⊢ x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
have inr : ∀ (hx : x ≠ 0), x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
⊢ x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
have inr : ∀ (x : Multiplicative ℤ),
  (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
Tactic: lift x to Multiplicative ℤ using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
y x : Multiplicative ℤ
⊢ (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
have inr : (↑x : WithZero (Multiplicative ℤ)).log < ((↑y : WithZero (Multiplicative ℤ)) * exp 1).log ↔
  (↑x : WithZero (Multiplicative ℤ)).log ≤ (↑y : WithZero (Multiplicative ℤ)).log
Tactic: rw [← log_le_log, ← log_lt_log]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
y x : Multiplicative ℤ
inr :
  (↑x : WithZero (Multiplicative ℤ)).log < ((↑y : WithZero (Multiplicative ℤ)) * exp 1).log ↔
    (↑x : WithZero (Multiplicative ℤ)).log ≤ (↑y : WithZero (Multiplicative ℤ)).log
⊢ (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
have inr₁ : (↑x : WithZero (Multiplicative ℤ)) ≠ 0
Tactic: rw [← log_le_log, ← log_lt_log]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
y x : Multiplicative ℤ
inr :
  (↑x : WithZero (Multiplicative ℤ)).log < ((↑y : WithZero (Multiplicative ℤ)) * exp 1).log ↔
    (↑x : WithZero (Multiplicative ℤ)).log ≤ (↑y : WithZero (Multiplicative ℤ)).log
inr₁ : (↑x : WithZero (Multiplicative ℤ)) ≠ 0
⊢ (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
have inr₂ : (↑y : WithZero (Multiplicative ℤ)) * exp 1 ≠ 0
Tactic: rw [← log_le_log, ← log_lt_log]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
y x : Multiplicative ℤ
inr :
  (↑x : WithZero (Multiplicative ℤ)).log < ((↑y : WithZero (Multiplicative ℤ)) * exp 1).log ↔
    (↑x : WithZero (Multiplicative ℤ)).log ≤ (↑y : WithZero (Multiplicative ℤ)).log
inr₁ : (↑x : WithZero (Multiplicative ℤ)) ≠ 0
inr₂ : (↑y : WithZero (Multiplicative ℤ)) * exp 1 ≠ 0
inr₃ : (↑x : WithZero (Multiplicative ℤ)) ≠ 0
⊢ (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
have inr₄ : (↑y : WithZero (Multiplicative ℤ)) ≠ 0
Tactic: rw [← log_le_log, ← log_lt_log]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x
have obtain : ∀ (y : WithZero (Multiplicative ℤ)) (hnz : y ≠ 0) (hyx : y < x), ∃ (k : ℕ), exp (-(↑k : ℤ)) < x
Tactic: obtain ⟨y, hnz, hyx⟩ := WithZero.exists_ne_zero_and_lt hx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x
have h : exp (-(↑(-y.log).toNat : ℤ)) < x
Tactic: use (-y.log).toNat
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ exp (-(↑(-y.log).toNat : ℤ)) < x
have apply : exp (-(↑(-y.log).toNat : ℤ)) ≤ y
Tactic: apply lt_of_le_of_lt _ hyx
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ exp (-(↑(-y.log).toNat : ℤ)) ≤ y
have rw : -y.log ≤ (↑(-y.log).toNat : ℤ)
Tactic: rw [← WithZero.le_log_iff_exp_le hnz, Int.neg_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
have obtain : ∀ (z : WithZero (Multiplicative ℤ)) (hz : z ≠ 0) (hzx : z ≤ x) (hzy : z ≤ y),
  ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
Tactic: obtain ⟨z, hz, hzx, hzy⟩ := WithZero.exists_ne_zero_and_le_and_le hx hy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
have obtain : ∀ (k : ℕ) (hk : exp (-(↑k : ℤ)) < z), ∃ (k : ℕ), exp (-(↑k : ℤ)) < x ∧ exp (-(↑k : ℤ)) < y
Tactic: obtain ⟨k, hk⟩ := exists_exp_neg_natCast_lt hz
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
⊢ x ≤ exp x.log
have zero : LE.le.{u_3} (α := WithZero (Multiplicative G)) 0 (exp (log 0))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Canonical (goal)
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
zero : LE.le.{u_3} (α := WithZero (Multiplicative G)) 0 (exp (log 0))
⊢ x ≤ exp x.log
have coe : ∀ (a : Multiplicative G), (↑a : WithZero (Multiplicative G)) ≤ (↑a : WithZero (Multiplicative G))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
have pos : ∀ (h : 0 = a), s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
have neg : ∀ (h : 0 ≠ a), s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
have pos : ∀ (h : 0 = a), a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
have neg : ∀ (h : 0 ≠ a), a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
have pos : ∀ (h : 0 = a), s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
a : G₀
inst_2 : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
pos : ∀ (h : 0 = a), s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
⊢ s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
have neg : ∀ (h : 0 ≠ a), s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
Tactic: by_cases! h : 0 = a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a
have inl : sup ∅ f / a = sup ∅ fun (i : ι) ↦ f i / a
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
inl : sup ∅ f / a = sup ∅ fun (i : ι) ↦ f i / a
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a
have inr : ∀ (hs : s.Nonempty), s.sup f / a = s.sup fun (i : ι) ↦ f i / a
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a
have inr : s.sup' hs f / a = s.sup fun (i : ι) ↦ f i / a
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
inr : s.sup' hs f / a = s.sup fun (i : ι) ↦ f i / a
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a
have inr₁ : s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
G₀ : Type u_3
inst : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
inr : s.sup' hs f / a = s.sup fun (i : ι) ↦ f i / a
inr₁ : s.sup' hs f / a = s.sup' hs fun (i : ι) ↦ f i / a
⊢ s.sup f / a = s.sup fun (i : ι) ↦ f i / a
have inr₂ : Eq.{u_3 + 1} (α := G₀) (s.sup' hs fun (i : ι) ↦ f i / a) (s.sup' hs fun (i : ι) ↦ f i / a)
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
⊢ Monotone (α := M₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inl M₀ N₀) : (a : M₀) → WithZero (M₀ˣ × N₀ˣ))
have refine : Monotone (α := M₀) (β := WithZero M₀ˣ)
  (⇑(↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ)
Tactic: refine (WithZero.map'_mono MonoidHom.inl_mono).comp ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
x y : M₀
⊢ x ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) x :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inl : 0 ≤ y →
  LE.le (α := WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 : WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y : WithZero M₀ˣ)
Tactic: obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
x y : M₀
inl :
  0 ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
⊢ x ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) x :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inr : ∀ (x : M₀ˣ),
  (↑x : M₀) ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
Tactic: obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
⊢ 0 ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inl : LE.le.{u_1} (α := M₀) 0 0 →
  LE.le (α := WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 : WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 : WithZero M₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
inl :
  LE.le.{u_1} (α := M₀) 0 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
⊢ 0 ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inl₁ : ∀ (y : M₀ˣ),
  0 ≤ (↑y : M₀) →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
        WithZero M₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
x : M₀ˣ
⊢ (↑x : M₀) ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inr : (↑x : M₀) ≤ 0 →
  LE.le (α := WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
      WithZero M₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 : WithZero M₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y