awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α)
⊢ a ≤ a + a_1

Tactic:
le_add_of_nonneg_right (h _)

Premises used: le_add_of_nonneg_right
-- 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 α)
⊢ a ≤ a + a_1

Tactic:
exact le_add_of_nonneg_right (h _)

Premises used: le_add_of_nonneg_right
-- 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 a_1 : α
hbc : (↑a_1 : WithZero α) ≤ c
coe :
  ∀ (c : α) (hbc' : a_1 ≤ c) (hbc : (↑a_1 : WithZero α) ≤ (↑c : WithZero α)),
    (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + (↑c : WithZero α)
⊢ (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : 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
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 α)
coe : a + a_1 ≤ a + c
⊢ (↑a : WithZero α) + (↑a_1 : WithZero α) ≤ (↑a : WithZero α) + (↑c : WithZero α)

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

Premises used: WithZero.coe_le_coe, WithZero.coe_add
-- 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 c : α
hbc' : a_1 ≤ c
hbc : (↑a_1 : WithZero α) ≤ (↑c : WithZero α)
⊢ a + a_1 ≤ a + c

Tactic:
gcongr
-- 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 : Add α
inst_3 : ExistsAddOfLE α
a b : WithZero α
zero : 0 ≤ b → ∃ (c : WithZero α), b = 0 + c
coe : ∀ (a : α), (↑a : WithZero α) ≤ b → ∃ (c : WithZero α), b = (↑a : WithZero α) + c
⊢ a ≤ b → ∃ (c : WithZero α), 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 : Add α
inst_3 : ExistsAddOfLE α
b : WithZero α
⊢ 0 ≤ b → ∃ (c : WithZero α), b = 0 + c

Tactic:
simp
-- 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 : Add α
inst_3 : ExistsAddOfLE α
b : WithZero α
a_1 : α
coe : (↑a_1 : WithZero α) ≤ 0 → ∃ (c : WithZero α), 0 = (↑a_1 : WithZero α) + c
coe₁ :
  ∀ (a : α), (↑a_1 : WithZero α) ≤ (↑a : WithZero α) → ∃ (c : WithZero α), (↑a : WithZero α) = (↑a_1 : WithZero α) + c
⊢ (↑a_1 : WithZero α) ≤ b → ∃ (c : 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 : Add α
inst_3 : ExistsAddOfLE α
a_1 : α
⊢ (↑a_1 : WithZero α) ≤ 0 → ∃ (c : WithZero α), 0 = (↑a_1 : WithZero α) + c

Tactic:
simp
-- 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 : Add α
inst_3 : ExistsAddOfLE α
a_1 a_2 : α
h : (↑a_1 : WithZero α) ≤ (↑a_2 : WithZero α)
coe :
  ∀ (c : α) (h : (↑a_1 : WithZero α) ≤ (↑(a_1 + c) : WithZero α)),
    ∃ (c_1 : WithZero α), (↑(a_1 + c) : WithZero α) = (↑a_1 : WithZero α) + c_1
⊢ ∃ (c : WithZero α), (↑a_2 : WithZero α) = (↑a_1 : WithZero α) + c

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)

Premises used: ExistsAddOfLE.exists_add_of_le, Iff.mp, WithZero.coe_le_coe, 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 : Add α
inst_3 : ExistsAddOfLE α
a_1 c : α
h : (↑a_1 : WithZero α) ≤ (↑(a_1 + c) : WithZero α)
⊢ ∃ (c_1 : WithZero α), (↑(a_1 + c) : WithZero α) = (↑a_1 : WithZero α) + c_1

Tactic:
⟨c, rfl⟩

Premises used: WithZero.coe, Exists.intro, 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 : Add α
inst_3 : ExistsAddOfLE α
a_1 c : α
h : (↑a_1 : WithZero α) ≤ (↑(a_1 + c) : WithZero α)
⊢ ∃ (c_1 : WithZero α), (↑(a_1 + c) : WithZero α) = (↑a_1 : WithZero α) + c_1

Tactic:
exact ⟨c, rfl⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →* β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Monotone.{u_1, u_2} (α := WithZero α) (β := WithZero β) (⇑(map' f) : (a : WithZero α) → WithZero β)

Tactic:
simpa [Monotone, WithZero.forall]

Premises used: Monotone, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : MulOneClass α
inst_3 : MulOneClass β
f : α →* β
hf : StrictMono.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ StrictMono.{u_1, u_2} (α := WithZero α) (β := WithZero β) (⇑(map' f) : (a : WithZero α) → WithZero β)

Tactic:
simpa [StrictMono, WithZero.forall]

Premises used: StrictMono, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
obtain : ∀ (z : α) (hlt : z < unzero hx), ∃ (y : WithZero α), y ≠ 0 ∧ y < x
⊢ ∃ (y : WithZero α), y ≠ 0 ∧ y < x

Tactic:
obtain ⟨z, hlt⟩ := exists_lt (WithZero.unzero hx)

Premises used: WithZero.unzero, NoMinOrder.exists_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
z : α
hlt : z < unzero hx
⊢ (↑z : WithZero α) < x

Tactic:
rw [← WithZero.coe_lt_coe, WithZero.coe_unzero hx] at hlt

Premises used: WithZero.coe_unzero, WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
z : α
hlt : (↑z : WithZero α) < x
⊢ ∃ (y : WithZero α), y ≠ 0 ∧ y < x

Tactic:
⟨z, WithZero.coe_ne_zero, hlt⟩

Premises used: WithZero.coe_ne_zero, And.intro, WithZero.coe, Exists.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
x : WithZero α
inst_1 : NoMinOrder α
hx : x ≠ 0
z : α
hlt : (↑z : WithZero α) < x
⊢ ∃ (y : WithZero α), y ≠ 0 ∧ y < x

Tactic:
exact ⟨z, WithZero.coe_ne_zero, hlt⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (h : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b), (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

Premises used: WithZero.coe_unzero, toAdd_ofAdd, Multiplicative.toAdd_lt, WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
rwa₂ :
  LT.lt (α := Multiplicative α)
    ((ofAdd : (a : α) → Multiplicative α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α) : Multiplicative α)
    ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α)
rwa₃ rwa₄ rwa₅ rwa₆ : (toAdd : (a : Multiplicative α) → α) (unzero ha) < b
⊢ a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))

Tactic:
rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]

Premises used: ofAdd_toAdd, Multiplicative.ofAdd_lt, WithZero.coe_unzero, WithZero.unzero, WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
⊢ a < (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α)) ↔
    (toAdd : (a : Multiplicative α) → α) (unzero ha) < b

Tactic:
⟨toAdd_unzero_lt_of_lt_ofAdd ha, lt_ofAdd_of_toAdd_unzero_lt ha⟩

Premises used: Iff.intro, WithZero.toAdd_unzero_lt_of_lt_ofAdd, WithZero.lt_ofAdd_of_toAdd_unzero_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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 :
      LE.le (α := α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α)
        ((toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α) : α)),
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (h : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b), (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b

Tactic:
rwa [← coe_unzero ha, coe_le_coe, ← toAdd_le, toAdd_ofAdd] at h

Premises used: WithZero.coe_unzero, toAdd_ofAdd, Multiplicative.toAdd_le, WithZero.coe_le_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
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
rwa₂ :
  LE.le (α := Multiplicative α)
    ((ofAdd : (a : α) → Multiplicative α) ((toAdd : (a : Multiplicative α) → α) (unzero ha) : α) : Multiplicative α)
    ((ofAdd : (a : α) → Multiplicative α) b : Multiplicative α)
rwa₃ rwa₄ rwa₅ rwa₆ : (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b
⊢ a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α))

Tactic:
rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]

Premises used: Multiplicative.ofAdd_le, ofAdd_toAdd, WithZero.coe_unzero, WithZero.unzero, WithZero.coe_le_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
⊢ a ≤ (↑((ofAdd : (a : α) → Multiplicative α) b) : WithZero (Multiplicative α)) ↔
    (toAdd : (a : Multiplicative α) → α) (unzero ha) ≤ b

Tactic:
⟨toAdd_unzero_le_of_lt_ofAdd ha, le_ofAdd_of_toAdd_unzero_le ha⟩

Premises used: WithZero.le_ofAdd_of_toAdd_unzero_le, Iff.intro, WithZero.toAdd_unzero_le_of_lt_ofAdd
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
⊢ MulLeftReflectLT.{u_1} (WithZero α)

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

Premises used: ContravariantClass.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
refine : ∀ (a b c : WithZero α) (h : a * b < a * c), b < c
⊢ MulLeftReflectLT.{u_1} (WithZero α)

Tactic:
refine ⟨fun a b c h => ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
⊢ a * c ≠ 0

Tactic:
have := h.ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
zero : ∀ (h : 0 * b < 0 * c) (this : 0 * c ≠ 0), b < c
coe : ∀ (a : α) (h : (↑a : WithZero α) * b < (↑a : WithZero α) * c) (this : (↑a : WithZero α) * c ≠ 0), b < c
⊢ b < c

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c

Tactic:
simp at this
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b c : WithZero α
a : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * c
this : (↑a : WithZero α) * c ≠ 0
coe : ∀ (h : (↑a : WithZero α) * b < (↑a : WithZero α) * 0) (this : (↑a : WithZero α) * 0 ≠ 0), b < 0
coe₁ :
  ∀ (a_1 : α) (h : (↑a : WithZero α) * b < (↑a : WithZero α) * (↑a_1 : WithZero α))
    (this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0), b < (↑a_1 : WithZero α)
⊢ b < c

Tactic:
induction c
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b : WithZero α
a : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * 0
this : (↑a : WithZero α) * 0 ≠ 0
⊢ b < 0

Tactic:
simp at this
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
b : WithZero α
a a_1 : α
h : (↑a : WithZero α) * b < (↑a : WithZero α) * (↑a_1 : WithZero α)
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
coe : ∀ (h : (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑a_1 : WithZero α)), 0 < (↑a_1 : WithZero α)
coe₁ :
  ∀ (a_2 : α) (h : (↑a : WithZero α) * (↑a_2 : WithZero α) < (↑a : WithZero α) * (↑a_1 : WithZero α)),
    (↑a_2 : WithZero α) < (↑a_1 : WithZero α)
⊢ b < (↑a_1 : WithZero α)

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a a_1 : α
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
h : (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑a_1 : WithZero α)
⊢ 0 < (↑a_1 : WithZero α)

Tactic:
zero_lt_coe _

Premises used: WithZero.zero_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a a_1 : α
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
a_2 : α
h : (↑a : WithZero α) * (↑a_2 : WithZero α) < (↑a : WithZero α) * (↑a_1 : WithZero α)
⊢ (↑a_2 : WithZero α) < (↑a_1 : WithZero α)

Tactic:
coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)

Premises used: Iff.mpr, lt_of_mul_lt_mul_left', Iff.mp, WithZero.coe_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Mul α
inst_2 : MulLeftReflectLT α
a a_1 : α
this : (↑a : WithZero α) * (↑a_1 : WithZero α) ≠ 0
h : (↑a : WithZero α) * 0 < (↑a : WithZero α) * (↑a_1 : WithZero α)
⊢ 0 < (↑a_1 : WithZero α)

Tactic:
exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]

Premises used: WithZero.zero_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
zero :
  LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
coe :
  ∀ (a : α),
    (↑a : WithZero α) ≤
      match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ x ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
zero₁ :
  ∀ (a : α),
    LE.le (α := WithZero α) (0 : WithZero α)
      (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α) :
        WithZero α)
⊢ LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) ≤
      match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 : α
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y : WithZero α
zero :
  y ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)
coe :
  ∀ (a : α),
    y ≤
      match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) x, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
zero₁ :
  ∀ (a : α),
    (↑a : WithZero α) ≤
      match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y : WithZero α
a : α
coe :
  LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)
coe₁ :
  ∀ (a_1 : α),
    (↑a_1 : WithZero α) ≤
      match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α)
⊢ y ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ (↑a : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
simp