awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
refine_3 : ∀ (x y : α) (h : x < y), ∃ (a : α), x < a ∧ a < y
⊢ DenselyOrdered α

Tactic:
refine ⟨fun x y h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x y : α
h : x < y
⊢ IsUnit y

Tactic:
(ne_zero_of_lt h).isUnit

Premises used: Ne.isUnit, ne_zero_of_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x y : α
h : x < y
refine_3 : ∀ (y : αˣ) (h : x < (↑y : α)), ∃ (a : α), x < a ∧ a < (↑y : α)
⊢ ∃ (a : α), x < a ∧ a < y

Tactic:
lift y to αˣ using (ne_zero_of_lt h).isUnit

Premises used: Ne.isUnit, ne_zero_of_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
refine_3 : ∀ (h : 0 < (↑y : α)), ∃ (a : α), 0 < a ∧ a < (↑y : α)
refine_3₁ : ∀ (hx : 0 < x), ∃ (a : α), x < a ∧ a < (↑y : α)
⊢ ∃ (a : α), x < a ∧ a < (↑y : α)

Tactic:
obtain rfl | hx := eq_zero_or_pos x

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y : αˣ
h : 0 < (↑y : α)
refine_3 : ∀ (z : αˣ) (hz : 1 < z), ∃ (a : α), 0 < a ∧ a < (↑y : α)
⊢ ∃ (a : α), 0 < a ∧ a < (↑y : α)

Tactic:
obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)

Premises used: exists_one_lt'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y : αˣ
h : 0 < (↑y : α)
z : αˣ
hz : 1 < z
⊢ 0 < (↑(y * z⁻¹) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y : αˣ
h : 0 < (↑y : α)
z : αˣ
hz : 1 < z
⊢ y * z⁻¹ < y

Tactic:
simp [hz]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y : αˣ
h : 0 < (↑y : α)
z : αˣ
hz : 1 < z
⊢ ∃ (a : α), 0 < a ∧ a < (↑y : α)

Tactic:
exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
hx : 0 < x
⊢ IsUnit x

Tactic:
hx.ne'.isUnit

Premises used: Ne.isUnit, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
x : α
y : αˣ
h : x < (↑y : α)
hx : 0 < x
refine_3 : ∀ (x : αˣ) (h : (↑x : α) < (↑y : α)) (hx : 0 < (↑x : α)), ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)
⊢ ∃ (a : α), x < a ∧ a < (↑y : α)

Tactic:
lift x to αˣ using hx.ne'.isUnit

Premises used: Ne.isUnit, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y x : αˣ
h : (↑x : α) < (↑y : α)
hx : 0 < (↑x : α)
refine_3 : ∀ (z : αˣ) (hz : x < z) (hz' : z < y), ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)
⊢ ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)

Tactic:
obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)

Premises used: Iff.mpr, Units.val_lt_val, DenselyOrdered.dense
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y x : αˣ
h : (↑x : α) < (↑y : α)
hx : 0 < (↑x : α)
z : αˣ
hz : x < z
hz' : z < y
⊢ (↑x : α) < (↑z : α) ∧ (↑z : α) < (↑y : α)

Tactic:
simp [hz, hz']
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
h_1 : Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
H₁ : Nontrivial.{u_1} αˣ
H₂ : DenselyOrdered.{u_1} αˣ
y x : αˣ
h : (↑x : α) < (↑y : α)
hx : 0 < (↑x : α)
z : αˣ
hz : x < z
hz' : z < y
⊢ ∃ (a : α), (↑x : α) < a ∧ a < (↑y : α)

Tactic:
exact ⟨z, by simp [hz, hz']⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ

Tactic:
have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → Nontrivial.{u_1} αˣ
inr : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → Nontrivial.{u_1} αˣ
inl₁ inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → Nontrivial.{u_1} αˣ
⊢ Nontrivial.{u_1} αˣ

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst_1 : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ
inl : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
inr : ¬DenselyOrdered α → ¬(Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ) → DenselyOrdered.{u_1} αˣ
inl₁ inl₂ : DenselyOrdered α → Nontrivial.{u_1} αˣ → DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
inst_1 : Nontrivial.{u_1} αˣ
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ

Tactic:
have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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} αˣ
inr₇ : ¬DenselyOrdered α → DenselyOrdered α → ¬DenselyOrdered.{u_1} αˣ → DenselyOrdered.{u_1} αˣ
⊢ DenselyOrdered.{u_1} αˣ ↔ DenselyOrdered α

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
a : α
ha :
  LT.lt (α := Multiplicative αᵒᵈ) (0 : Multiplicative αᵒᵈ)
    ((Multiplicative.ofAdd : (a : αᵒᵈ) → Multiplicative αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) :
      Multiplicative αᵒᵈ)
b c : α
hbc : c < b
⊢ a ≠ ⊤

Tactic:
simpa using ha.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedAddCommMonoidWithTop α
⊢ ∀ ⦃a : Multiplicative αᵒᵈ⦄ (ha : 0 < a) ⦃b c : Multiplicative αᵒᵈ⦄ (hbc : b < c), a * b < a * c

Tactic:
simpa [← ofAdd_add, ← toDual_add]
      using fun a ha b c hbc ↦ add_right_strictMono_of_ne_top (by simpa using ha.ne') hbc

Premises used: add_right_strictMono_of_ne_top, ofAdd_add, toDual_add
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedAddCommMonoidWithTop α
x : α
⊢ Eq (α := Multiplicative αᵒᵈ)
      ((Multiplicative.ofAdd : (a : αᵒᵈ) → Multiplicative αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) :
        Multiplicative αᵒᵈ)
      (0 : Multiplicative αᵒᵈ) ↔
    x = ⊤

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative, OrderDual
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedAddCommMonoidWithTop α
x : Multiplicative αᵒᵈ
⊢ Eq (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Multiplicative.toAdd : (a : Multiplicative αᵒᵈ) → αᵒᵈ) x : αᵒᵈ) : α)
      (⊤ : α) ↔
    x = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative, OrderDual
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedAddCommMonoidWithTop α
⊢ Eq.{u_1 + 1} (α := Multiplicative αᵒᵈ)
    ((Multiplicative.ofAdd : (a : αᵒᵈ) → Multiplicative αᵒᵈ) ⊥ : Multiplicative αᵒᵈ) (0 : Multiplicative αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedAddCommMonoidWithTop α
⊢ Eq.{u_1 + 1} (α := α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Multiplicative.toAdd : (a : Multiplicative αᵒᵈ) → αᵒᵈ) 0 : αᵒᵈ) : α) (⊤ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithZero α) 0 ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x y : WithZero α
⊢ x ≤ y ↔ ∀ (a : α), x = (↑a : WithZero α) → ∃ (b : α), y = (↑b : WithZero α) ∧ a ≤ b

Tactic:
WithBot.le_iff_forall

Premises used: WithBot.le_iff_forall, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a b : α
⊢ (↑a : WithZero α) ≤ (↑b : WithZero α) ↔ a ≤ b

Tactic:
WithBot.coe_le_coe

Premises used: WithBot.coe_le_coe, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a : α
⊢ ¬(↑a : WithZero α) ≤ 0

Tactic:
WithBot.not_coe_le_bot _

Premises used: WithBot.not_coe_le_bot, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a : WithZero α
⊢ 0 ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x : WithZero α
⊢ x ≤ 0 ↔ x = 0

Tactic:
WithBot.le_bot_iff

Premises used: WithZero, WithBot.le_bot_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x : WithZero α
a : α
⊢ (↑a : WithZero α) ≤ x ↔ ∃ (b : α), x = (↑b : WithZero α) ∧ a ≤ b

Tactic:
WithBot.coe_le_iff

Premises used: WithBot.coe_le_iff, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x : WithZero α
b : α
⊢ x ≤ (↑b : WithZero α) ↔ ∀ (a : α), x = (↑a : WithZero α) → a ≤ b

Tactic:
WithBot.le_coe_iff

Premises used: WithBot.le_coe_iff, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a : α
h : IsMax a
⊢ IsMax (↑a : WithZero α)

Tactic:
h.withBot

Premises used: IsMax.withBot, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
y : WithZero α
a : α
hy : y ≠ 0
⊢ a ≤ unzero hy ↔ (↑a : WithZero α) ≤ y

Tactic:
WithBot.le_unbot_iff _

Premises used: WithBot.le_unbot_iff, WithZero.unzero, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x : WithZero α
b : α
hx : x ≠ 0
⊢ unzero hx ≤ b ↔ x ≤ (↑b : WithZero α)

Tactic:
WithBot.unbot_le_iff _

Premises used: WithZero.unzero, WithZero, WithZero.coe, WithBot.unbot_le_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a : α
inst_1 : One α
⊢ 1 ≤ (↑a : WithZero α) ↔ 1 ≤ a

Tactic:
coe_le_coe

Premises used: WithZero.coe_le_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
a : α
inst_1 : One α
⊢ (↑a : WithZero α) ≤ 1 ↔ a ≤ 1

Tactic:
coe_le_coe

Premises used: WithZero.coe_le_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LE α
x y : WithZero α
hx : x ≠ 0
hy : y ≠ 0
⊢ unzero hx ≤ unzero hy ↔ x ≤ y

Tactic:
WithBot.unbot_le_unbot_iff ..

Premises used: WithZero.unzero, WithBot.unbot_le_unbot_iff, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x y : WithZero α
⊢ x < y ↔
    (x = 0 ∧ ∃ (b : α), y = (↑b : WithZero α)) ∨
      ∃ (a : α), ∃ (b : α), a < b ∧ x = (↑a : WithZero α) ∧ y = (↑b : WithZero α)

Tactic:
WithBot.lt_def

Premises used: WithBot.lt_def, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x y : WithZero α
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithZero α) ∧ ∀ (a : α), x = (↑a : WithZero α) → a < b

Tactic:
WithBot.lt_iff_exists

Premises used: WithZero, WithZero.coe, WithBot.lt_iff_exists
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ (↑a : WithZero α) < (↑b : WithZero α) ↔ a < b

Tactic:
simp [lt_def]

Premises used: WithZero.lt_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
a : α
⊢ 0 < (↑a : WithZero α)

Tactic:
simp [lt_def]

Premises used: WithZero.lt_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
a : WithZero α
⊢ ¬a < 0

Tactic:
simp [lt_def]

Premises used: WithZero.lt_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x y : WithZero α
⊢ x < y ↔ ∃ (b : α), y = (↑b : WithZero α) ∧ x < (↑b : WithZero α)

Tactic:
WithBot.lt_iff_exists_coe

Premises used: WithBot.lt_iff_exists_coe, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x : WithZero α
b : α
⊢ x < (↑b : WithZero α) ↔ ∀ (a : α), x = (↑a : WithZero α) → a < b

Tactic:
WithBot.lt_coe_iff

Premises used: WithBot.lt_coe_iff, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x : WithZero α
⊢ 0 < x ↔ x ≠ 0

Tactic:
WithBot.bot_lt_iff_ne_bot

Premises used: WithZero, WithBot.bot_lt_iff_ne_bot
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
y : WithZero α
a : α
hy : y ≠ 0
⊢ a < unzero hy ↔ (↑a : WithZero α) < y

Tactic:
WithBot.lt_unbot_iff _

Premises used: WithZero.unzero, WithBot.lt_unbot_iff, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
x : WithZero α
b : α
hx : x ≠ 0
⊢ unzero hx < b ↔ x < (↑b : WithZero α)

Tactic:
WithBot.unbot_lt_iff _

Premises used: WithBot.unbot_lt_iff, WithZero.unzero, WithZero, WithZero.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
a : α
inst_1 : One α
⊢ 1 < (↑a : WithZero α) ↔ 1 < a

Tactic:
coe_lt_coe

Premises used: WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LT α
a : α
inst_1 : One α
⊢ (↑a : WithZero α) < 1 ↔ a < 1

Tactic:
coe_lt_coe

Premises used: WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 α)

Tactic:
⟨fun a b c hbc => ?_⟩

Premises used: CovariantClass.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x y : WithZero α
a b : α
inst_2 : Mul α
inst_3 : MulLeftMono α
refine : ∀ (a b c : WithZero α) (hbc : b ≤ c), a * b ≤ a * c
⊢ MulLeftMono.{u_1} (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe : ∀ (a : α), (↑a : WithZero α) * b ≤ (↑a : WithZero α) * c
⊢ a * b ≤ a * c

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
⊢ 0 * b ≤ 0 * c

Tactic:
zero_le

Premises used: zero_le, Option.map₂
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
⊢ 0 * b ≤ 0 * c

Tactic:
exact zero_le

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

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 : α
hbc : 0 ≤ c
⊢ (↑a_1 : WithZero α) * 0 ≤ (↑a_1 : WithZero α) * c

Tactic:
zero_le

Premises used: zero_le, Option.map₂
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 : α
hbc : 0 ≤ c
⊢ (↑a_1 : WithZero α) * 0 ≤ (↑a_1 : WithZero α) * c

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe :
  ∀ (c : α) (hbc' : a_2 ≤ c) (hbc : (↑a_2 : WithZero α) ≤ (↑c : WithZero α)),
    (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * (↑c : WithZero α)
⊢ (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * c

Tactic:
rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩

Premises used: WithZero.coe_le_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 α)
coe : a_1 * a_2 ≤ a_1 * c
⊢ (↑a_1 : WithZero α) * (↑a_2 : WithZero α) ≤ (↑a_1 : WithZero α) * (↑c : WithZero α)

Tactic:
rw [← coe_mul _ c, ← coe_mul, coe_le_coe]

Premises used: WithZero.coe_le_coe, WithZero.coe_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 * a_2 ≤ a_1 * c

Tactic:
mul_le_mul_right hbc' _

Premises used: mul_le_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 * a_2 ≤ a_1 * c

Tactic:
exact mul_le_mul_right hbc' _

Premises used: mul_le_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono.{u_1} (WithZero α)

Tactic:
⟨fun a b c hbc => ?_⟩

Premises used: CovariantClass.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
refine : ∀ (a b c : WithZero α) (hbc : b ≤ c), a + b ≤ a + c
⊢ AddLeftMono.{u_1} (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe : ∀ (a : α), (↑a : WithZero α) + b ≤ (↑a : WithZero α) + c
⊢ a + b ≤ a + c

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
zero : b ≤ 0 + c
zero₁ zero₂ zero₃ zero₄ : b ≤ c
⊢ 0 + b ≤ 0 + c

Tactic:
rwa [zero_add, zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe₁ : ∀ (a_1 : α) (hbc : (↑a_1 : WithZero α) ≤ c), (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + c
⊢ (↑a : WithZero α) + b ≤ (↑a : WithZero α) + c

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe₁ : ∀ (a_1 : α) (hbc : 0 ≤ (↑a_1 : WithZero α)), (↑a : WithZero α) ≤ (↑a : WithZero α) + (↑a_1 : WithZero α)
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + c

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
coe coe₁ : (↑a : WithZero α) ≤ (↑a : WithZero α)
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddZeroClass α
inst_2 : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a a_1 : α
hbc : 0 ≤ (↑a_1 : WithZero α)
coe : a ≤ a + a_1
⊢ (↑a : WithZero α) ≤ (↑a : WithZero α) + (↑a_1 : WithZero α)

Tactic:
rw [← coe_add, coe_le_coe]

Premises used: WithZero.coe_le_coe, WithZero.coe_add