awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : DecidableLE α
a : α
⊢ ¬(↑a : WithZero α) ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : DecidableLT α
x : WithZero α
⊢ ¬x < 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : DecidableLT α
a : α
⊢ 0 < (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithZero α
zero : 0 ≤ y ∨ y ≤ 0
coe : ∀ (a : α), (↑a : WithZero α) ≤ y ∨ y ≤ (↑a : WithZero α)
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) 0 0 ∨ LE.le.{u_1} (α := WithZero α) 0 0
zero₁ : ∀ (a : α), 0 ≤ (↑a : WithZero α) ∨ (↑a : WithZero α) ≤ 0
⊢ 0 ≤ y ∨ y ≤ 0

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 ∨ 0 ≤ (↑a : WithZero α)
coe₁ : ∀ (a_1 : α), (↑a : WithZero α) ≤ (↑a_1 : WithZero α) ∨ (↑a_1 : WithZero α) ≤ (↑a : WithZero α)
⊢ (↑a : WithZero α) ≤ y ∨ y ≤ (↑a : WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ LE.le.{u_1} (α := WithZero α) 0 0 ∨ LE.le.{u_1} (α := WithZero α) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
⊢ 0 ≤ (↑a : WithZero α) ∨ (↑a : WithZero α) ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
⊢ (↑a : WithZero α) ≤ 0 ∨ 0 ≤ (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a a_1 : α
coe : a ≤ a_1 ∨ a_1 ≤ a
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) ∨ (↑a_1 : WithZero α) ≤ (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a a_1 : α
⊢ a ≤ a_1 ∨ a_1 ≤ a

Tactic:
simpa using Std.Total.total ..

Premises used: Std.Total.total
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ (↑a : WithZero α) ≤ max (↑b : WithZero α) (↑c : WithZero α) ↔ a ≤ max b c

Tactic:
simp only [WithZero.coe_le_coe, le_max_iff]

Premises used: WithZero.coe_le_coe, le_max_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ min (↑a : WithZero α) (↑b : WithZero α) ≤ (↑c : WithZero α) ↔ min a b ≤ c

Tactic:
simp only [WithZero.coe_le_coe, min_le_iff]

Premises used: min_le_iff, WithZero.coe_le_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≠ 0

Tactic:
simp [min_eq_iff, hx, hy]

Premises used: min_eq_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ min x y ≤ y

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrder α
x y : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
obtain : ∀ (z' : WithZero α) (hnz' : z' ≠ 0) (hzx : z' ≤ x) (hzy : z' ≤ y), ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y

Tactic:
obtain ⟨z', hnz', hzx, hzy⟩ := exists_ne_zero_and_le_and_le hx hy

Premises used: WithZero.exists_ne_zero_and_le_and_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
obtain : ∀ (z : WithZero α) (hnz : z ≠ 0) (hlt : z < z'), ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y

Tactic:
obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'

Premises used: WithZero.exists_ne_zero_and_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 < y
⊢ ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y

Tactic:
use z, hnz
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
right₁ : z < y
⊢ z < x ∧ z < y

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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

Tactic:
lt_of_lt_of_le hlt ‹z' ≤ _›

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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

Tactic:
exact lt_of_lt_of_le hlt ‹z' ≤ _›

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 < y

Tactic:
lt_of_lt_of_le hlt ‹z' ≤ _›

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 < y

Tactic:
exact lt_of_lt_of_le hlt ‹z' ≤ _›

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono.{u_1} (WithZero α)

Tactic:
have := WithZero.addLeftMono zero_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono.{u_1} (WithZero α)
⊢ ∀ (a b : WithZero α), a ≤ b → ∀ (c : WithZero α), c + a ≤ c + b

Tactic:
simpa [add_comm] using fun _ _ ↦ add_le_add_left

Premises used: add_le_add_left, add_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono.{u_1} (WithZero α)
⊢ IsOrderedAddMonoid.{u_1} (WithZero α)

Tactic:
exact ⟨fun _ _ ↦ add_le_add_left, by simpa [add_comm] using fun _ _ ↦ add_le_add_left⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
a : α
h : 0 < (↑a : WithZero α)
c : α
h_1 : 0 < (↑c : WithZero α)
⊢ (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑c : WithZero α)

Tactic:
simp [← WithZero.coe_mul]

Premises used: WithZero.coe_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 α)
norm_cast : ∀ (hbc : b < c), a * b < a * c
⊢ (↑a : WithZero α) * (↑b : WithZero α) < (↑a : WithZero α) * (↑c : WithZero α)

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
a : α
h : 0 < (↑a : WithZero α)
b c : α
hbc : b < c
⊢ a * b < a * c

Tactic:
mul_lt_mul_right hbc _

Premises used: mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
a : α
h : 0 < (↑a : WithZero α)
b c : α
hbc : b < c
⊢ a * b < a * c

Tactic:
exact mul_lt_mul_right hbc _

Premises used: mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a b : G
⊢ exp a ≤ exp b ↔ a ≤ b

Tactic:
simp [exp]

Premises used: WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a b : G
⊢ exp a < exp b ↔ a < b

Tactic:
simp [exp]

Premises used: WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
⊢ 0 < exp a

Tactic:
simp [exp]

Premises used: WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log ≤ y.log ↔ (↑x : WithZero (Multiplicative G)) ≤ y
⊢ x.log ≤ y.log ↔ x ≤ y

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ y ≠ 0

Tactic:
hy
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
lift :
  ∀ (y : Multiplicative G),
    (↑x : WithZero (Multiplicative G)).log ≤ (↑y : WithZero (Multiplicative G)).log ↔
      (↑x : WithZero (Multiplicative G)) ≤ (↑y : WithZero (Multiplicative G))
⊢ (↑x : WithZero (Multiplicative G)).log ≤ y.log ↔ (↑x : WithZero (Multiplicative G)) ≤ y

Tactic:
lift y to Multiplicative G using hy

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log ≤ (↑y : WithZero (Multiplicative G)).log ↔
    (↑x : WithZero (Multiplicative G)) ≤ (↑y : WithZero (Multiplicative G))

Tactic:
simp [log]

Premises used: WithZero.log
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log < y.log ↔ (↑x : WithZero (Multiplicative G)) < y
⊢ x.log < y.log ↔ x < y

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
lift :
  ∀ (y : Multiplicative G),
    (↑x : WithZero (Multiplicative G)).log < (↑y : WithZero (Multiplicative G)).log ↔
      (↑x : WithZero (Multiplicative G)) < (↑y : WithZero (Multiplicative G))
⊢ (↑x : WithZero (Multiplicative G)).log < y.log ↔ (↑x : WithZero (Multiplicative G)) < y

Tactic:
lift y to Multiplicative G using hy

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
inst_1 : AddGroup G
x y : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log < (↑y : WithZero (Multiplicative G)).log ↔
    (↑x : WithZero (Multiplicative G)) < (↑y : WithZero (Multiplicative G))

Tactic:
simp [log]

Premises used: WithZero.log
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log ≤ a ↔ (↑x : WithZero (Multiplicative G)) ≤ exp a
⊢ x.log ≤ a ↔ x ≤ exp a

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log ≤ a ↔ (↑x : WithZero (Multiplicative G)) ≤ exp a

Tactic:
simpa [log, exp] using .rfl

Premises used: WithZero.log, WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
lift : ∀ (x : Multiplicative G), (↑x : WithZero (Multiplicative G)).log < a ↔ (↑x : WithZero (Multiplicative G)) < exp a
⊢ x.log < a ↔ x < exp a

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : Multiplicative G
⊢ (↑x : WithZero (Multiplicative G)).log < a ↔ (↑x : WithZero (Multiplicative G)) < exp a

Tactic:
simpa [log, exp] using .rfl

Premises used: WithZero.log, WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
lift : ∀ (x : Multiplicative G), a ≤ (↑x : WithZero (Multiplicative G)).log ↔ exp a ≤ (↑x : WithZero (Multiplicative G))
⊢ a ≤ x.log ↔ exp a ≤ x

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : Multiplicative G
⊢ a ≤ (↑x : WithZero (Multiplicative G)).log ↔ exp a ≤ (↑x : WithZero (Multiplicative G))

Tactic:
simpa [log, exp] using .rfl

Premises used: WithZero.log, WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
lift : ∀ (x : Multiplicative G), a < (↑x : WithZero (Multiplicative G)).log ↔ exp a < (↑x : WithZero (Multiplicative G))
⊢ a < x.log ↔ exp a < x

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : Multiplicative G
⊢ a < (↑x : WithZero (Multiplicative G)).log ↔ exp a < (↑x : WithZero (Multiplicative G))

Tactic:
simpa [log, exp] using .rfl

Premises used: WithZero.log, WithZero.exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
inr : ∀ (hx : x ≠ 0), x ≤ exp a
⊢ x ≤ exp a

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
hxa : log 0 ≤ a
⊢ 0 ≤ exp a

Tactic:
simp [← log_le_iff_le_exp, *]

Premises used: WithZero.log_le_iff_le_exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
hx : x ≠ 0
⊢ x ≤ exp a

Tactic:
simp [← log_le_iff_le_exp, *]

Premises used: WithZero.log_le_iff_le_exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
inr : ∀ (hx : x ≠ 0), x < exp a
⊢ x < exp a

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
hxa : log 0 < a
⊢ 0 < exp a

Tactic:
simp [← log_lt_iff_lt_exp, *]

Premises used: WithZero.log_lt_iff_lt_exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
hx : x ≠ 0
⊢ x < exp a

Tactic:
simp [← log_lt_iff_lt_exp, *]

Premises used: WithZero.log_lt_iff_lt_exp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hax : exp a ≤ x
⊢ a ≤ x.log

Tactic:
(le_log_iff_exp_le (exp_pos.trans_le hax).ne').2 hax

Premises used: Iff.mpr, WithZero.le_log_iff_exp_le, LT.lt.ne', LT.lt.trans_le, WithZero.exp_pos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
G : Type u_3
inst : Preorder G
a : G
inst_1 : AddGroup G
x : WithZero (Multiplicative G)
hax : exp a < x
⊢ a < x.log

Tactic:
(lt_log_iff_exp_lt (exp_pos.trans hax).ne').2 hax

Premises used: Iff.mpr, LT.lt.ne', WithZero.lt_log_iff_exp_lt, WithZero.exp_pos, LT.lt.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
inst : Preorder G
a b : G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
⊢ ∀ {a b : G},
    LE.le (α := (WithZero (Multiplicative G))ˣ)
        ((expEquiv : (a : G) → (WithZero (Multiplicative G))ˣ) a : (WithZero (Multiplicative G))ˣ)
        ((expEquiv : (a : G) → (WithZero (Multiplicative G))ˣ) b : (WithZero (Multiplicative G))ˣ) ↔
      a ≤ b

Tactic:
simp [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
inst : Preorder G
a b : G
inst_1 : AddGroup G
x y : WithZero (Multiplicative G)
⊢ ∀ {a b : (WithZero (Multiplicative G))ˣ},
    LE.le (α := G) ((logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) a : G)
        ((logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) b : G) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
⊢ y ≠ 0

Tactic:
hy
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
lift : ∀ (y : Multiplicative ℤ), x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
⊢ x < y * exp 1 ↔ x ≤ y

Tactic:
lift y to Multiplicative ℤ using hy

Premises used: Int, Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
inl : 0 < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ 0 ≤ (↑y : WithZero (Multiplicative ℤ))
inr : ∀ (hx : x ≠ 0), x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))
⊢ x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
y : Multiplicative ℤ
⊢ 0 < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ 0 ≤ (↑y : WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
inr :
  ∀ (x : Multiplicative ℤ),
    (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
      (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))
⊢ x < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔ x ≤ (↑y : WithZero (Multiplicative ℤ))

Tactic:
lift x to Multiplicative ℤ using hx

Premises used: Int, Multiplicative
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
inr₄ : (↑y : WithZero (Multiplicative ℤ)) ≠ 0
⊢ (↑x : WithZero (Multiplicative ℤ)) < (↑y : WithZero (Multiplicative ℤ)) * exp 1 ↔
    (↑x : WithZero (Multiplicative ℤ)) ≤ (↑y : WithZero (Multiplicative ℤ))

Tactic:
rw [← log_le_log, ← log_lt_log]

Premises used: WithZero.log_le_log, WithZero.log_lt_log
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
y x : Multiplicative ℤ
⊢ (↑x : WithZero (Multiplicative ℤ)).log < ((↑y : WithZero (Multiplicative ℤ)) * exp 1).log ↔
    (↑x : WithZero (Multiplicative ℤ)).log ≤ (↑y : WithZero (Multiplicative ℤ)).log

Tactic:
simp [log_mul, Int.lt_add_one_iff]

Premises used: WithZero.log_mul, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
y x : Multiplicative ℤ
⊢ (↑x : WithZero (Multiplicative ℤ)) ≠ 0

Tactic:
simp [log_mul, Int.lt_add_one_iff]

Premises used: WithZero.log_mul, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
y x : Multiplicative ℤ
⊢ (↑y : WithZero (Multiplicative ℤ)) * exp 1 ≠ 0

Tactic:
simp [log_mul, Int.lt_add_one_iff]

Premises used: WithZero.log_mul, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
y x : Multiplicative ℤ
⊢ (↑y : WithZero (Multiplicative ℤ)) ≠ 0

Tactic:
simp [log_mul, Int.lt_add_one_iff]

Premises used: WithZero.log_mul, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
obtain : ∀ (y : WithZero (Multiplicative ℤ)) (hnz : y ≠ 0) (hyx : y < x), ∃ (k : ℕ), exp (-(↑k : ℤ)) < x
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x

Tactic:
obtain ⟨y, hnz, hyx⟩ := WithZero.exists_ne_zero_and_lt hx

Premises used: WithZero.exists_ne_zero_and_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
h : exp (-(↑(-y.log).toNat : ℤ)) < x
⊢ ∃ (k : ℕ), exp (-(↑k : ℤ)) < x

Tactic:
use (-y.log).toNat

Premises used: WithZero.log, Int.toNat, Neg.neg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
apply : exp (-(↑(-y.log).toNat : ℤ)) ≤ y
⊢ exp (-(↑(-y.log).toNat : ℤ)) < x

Tactic:
apply lt_of_le_of_lt _ hyx

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
rw : -y.log ≤ (↑(-y.log).toNat : ℤ)
⊢ exp (-(↑(-y.log).toNat : ℤ)) ≤ y

Tactic:
rw [← WithZero.le_log_iff_exp_le hnz, Int.neg_le_iff]

Premises used: Int.neg_le_iff, WithZero.le_log_iff_exp_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ -y.log ≤ (↑(-y.log).toNat : ℤ)

Tactic:
Int.self_le_toNat _

Premises used: Int.self_le_toNat
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ -y.log ≤ (↑(-y.log).toNat : ℤ)

Tactic:
exact Int.self_le_toNat _

Premises used: Int.self_le_toNat