awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
refine :
  ∀ (a : Rˣ),
    Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1))
      (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
⊢ ∃ (a : Rˣ),
    ∀ (b : Rˣ),
      Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (b * a))
        (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) b)

Tactic:
refine ⟨-1, fun a ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : Rˣ
inl :
  ∀ (h : (↑a : R) < 0),
    Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1))
      (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
inr :
  ∀ (h : 0 < (↑a : R)),
    Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1))
      (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
⊢ Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)

Tactic:
obtain h | h := lt_or_gt_of_ne a.ne_zero

Premises used: lt_or_gt_of_ne, Units.ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : Rˣ
h : (↑a : R) < 0
⊢ Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)

Tactic:
simp [h, h.le]

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Ring.Units
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : Rˣ
h : 0 < (↑a : R)
⊢ Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)

Tactic:
simp [h, xor_comm, h.le]

Premises used: xor_comm, LT.lt.le
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : α
⊢ (↑(a * b) : WithTop α) = (↑a : WithTop α) * (↑b : WithTop α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
h : a ≠ 0
rw : Eq.{u_1 + 1} (α := WithTop α) (if a = 0 then 0 else ⊤) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ a * ⊤ = ⊤

Tactic:
rw [mul_top', if_neg h]

Premises used: WithTop.mul_top', if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : b ≠ 0
rw : Eq.{u_1 + 1} (α := WithTop α) (if b = 0 then 0 else ⊤) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ * b = ⊤

Tactic:
rw [top_mul', if_neg hb]

Premises used: WithTop.top_mul', if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
⊢ HMul.hMul (α := WithTop α) ⊤ ⊤ = ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
top : ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b
coe :
  ∀ (a : α),
    (↑a : WithTop α) * b =
      if (↑a : WithTop α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) b
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
top :
  HMul.hMul (α := WithTop α) ⊤ ⊤ =
    if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ ⊤
top₁ :
  ∀ (a : α),
    ⊤ * (↑a : WithTop α) =
      if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ (↑a : WithTop α) = 0 then 0
      else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ (↑a : WithTop α)
⊢ ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
a : α
coe :
  (↑a : WithTop α) * ⊤ =
    if (↑a : WithTop α) = 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) ⊤
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithTop α) * (↑a_1 : WithTop α) =
      if (↑a : WithTop α) = 0 ∨ (↑a_1 : WithTop α) = 0 then 0
      else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) (↑a_1 : WithTop α)
⊢ (↑a : WithTop α) * b = if (↑a : WithTop α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
⊢ HMul.hMul (α := WithTop α) ⊤ ⊤ =
    if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ ⊤

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
⊢ ⊤ * (↑a : WithTop α) =
    if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ (↑a : WithTop α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ (↑a : WithTop α)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
⊢ (↑a : WithTop α) * ⊤ =
    if (↑a : WithTop α) = 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) ⊤

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a a_1 : α
⊢ (↑a : WithTop α) * (↑a_1 : WithTop α) =
    if (↑a : WithTop α) = 0 ∨ (↑a_1 : WithTop α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) (↑a_1 : WithTop α)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
rw :
  Eq (α := WithTop α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b) ⊤ ↔
    a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
⊢ a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
rw [mul_def]

Premises used: WithTop.mul_def
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
⊢ Eq (α := WithTop α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b) ⊤ ↔
    a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
simp : Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (a : α) ↦ Option.some (a * b))
⊢ ⊤ * (↑b : WithTop α) = Option.bind ⊤ fun (a : α) ↦ Option.some (a * b)

Tactic:
simp [top_mul, hb]

Premises used: WithTop.top_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
⊢ Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (a : α) ↦ Option.some (a * b))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
simp : Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (b : α) ↦ Option.some (a * b))
⊢ (↑a : WithTop α) * ⊤ = Option.bind ⊤ fun (b : α) ↦ Option.some (a * b)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (b : α) ↦ Option.some (a * b))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
pos : ∀ (ha : a = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
neg : ∀ (ha : ¬a = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
pos₁ : untopD 0 0 = untopD 0 0 * untopD 0 b
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 (↑0 : WithTop α) * untopD 0 b
pos₃ : 0 = 0 * untopD 0 b
pos₄ pos₅ : Eq.{u_1 + 1} (α := α) 0 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]

Premises used: MulZeroClass.zero_mul, WithTop.coe_zero, WithTop.untopD_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
pos : ∀ (hb : b = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
neg : ∀ (hb : ¬b = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
pos₁ : untopD 0 0 = untopD 0 a * untopD 0 0
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 a * untopD 0 (↑0 : WithTop α)
pos₃ : 0 = untopD 0 a * 0
pos₄ pos₅ : Eq.{u_1 + 1} (α := α) 0 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]

Premises used: WithTop.coe_zero, MulZeroClass.mul_zero, WithTop.untopD_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
neg₁ : ∀ (a : α) (ha : ¬(↑a : WithTop α) = 0), untopD 0 ((↑a : WithTop α) * b) = untopD 0 (↑a : WithTop α) * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 ⊤ * untopD 0 b
neg₁ : 0 = 0 * untopD 0 b
neg₂ neg₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b

Tactic:
rw [top_mul hb, untopD_top, zero_mul]

Premises used: WithTop.top_mul, WithTop.untopD_top, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithTop α) = 0
neg :
  ∀ (hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
neg₁ :
  ∀ (a_1 : α) (hb : ¬(↑a_1 : WithTop α) = 0),
    untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
⊢ untopD 0 ((↑a : WithTop α) * b) = untopD 0 (↑a : WithTop α) * untopD 0 b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
neg₁ : 0 = untopD 0 (↑a : WithTop α) * 0
neg₂ neg₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤

Tactic:
rw [mul_top ha, untopD_top, mul_zero]

Premises used: WithTop.untopD_top, WithTop.mul_top, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
a_1 : α
hb : ¬(↑a_1 : WithTop α) = 0
neg : untopD 0 (↑(a * a_1) : WithTop α) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
neg₁ : a * a_1 = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
neg₂ : a * a_1 = a * untopD 0 (↑a_1 : WithTop α)
neg₃ neg₄ : a * a_1 = a * a_1
⊢ untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)

Tactic:
rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]

Premises used: WithTop.coe_mul, WithTop.untopD_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
simp [mul_eq_top_iff, *]

Premises used: WithTop.mul_eq_top_iff
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
rw : ∀ (ha : a ≠ ⊤) (hb : b ≠ ⊤), a * b ≠ ⊤
⊢ a * b < ⊤

Tactic:
rw [WithTop.lt_top_iff_ne_top] at *

Premises used: WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
mul_ne_top ha hb

Premises used: WithTop.mul_ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
exact mul_ne_top ha hb

Premises used: WithTop.mul_ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
⊢ NoZeroDivisors.{u_1} (WithTop α)

Tactic:
⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩

Premises used: Decidable.byContradiction, NoZeroDivisors.mk
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
refine : ∀ {a b : WithTop α} (h₁ : a * b = 0) (h₂ : ¬(a = 0 ∨ b = 0)), False
⊢ NoZeroDivisors.{u_1} (WithTop α)

Tactic:
refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
a_1 b_1 : WithTop α
h₁ : a_1 * b_1 = 0
h₂ : ¬(a_1 = 0 ∨ b_1 = 0)
⊢ Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) a_1 b_1) 0

Tactic:
rw [mul_def, if_neg h₂] at h₁

Premises used: WithTop.mul_def, if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
a_1 b_1 : WithTop α
h₁ : a_1 * b_1 = 0
h₂ : ¬(a_1 = 0 ∨ b_1 = 0)
h₃ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) a_1 b_1) 0
⊢ ¬(a_1 = 0 ∨ b_1 = 0)

Tactic:
rw [mul_def, if_neg h₂] at h₁

Premises used: WithTop.mul_def, if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
a_1 b_1 : WithTop α
h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) a_1 b_1) 0
h₂ : ¬(a_1 = 0 ∨ b_1 = 0)
rcases :
  ∀ (a b : α) (hab : a * b = 0)
    (h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) (Option.some a) (Option.some b)) 0)
    (h₂ : ¬(Option.some a = 0 ∨ Option.some b = 0)), False
⊢ False

Tactic:
rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩

Premises used: Iff.mp, Option.mem_map₂_iff, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a_1 b_1 : WithTop α
inst_2 : NoZeroDivisors α
a b : α
hab : a * b = 0
h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) (Option.some a) (Option.some b)) 0
h₂ : ¬(Option.some a = 0 ∨ Option.some b = 0)
⊢ False

Tactic:
h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))

Premises used: WithTop.some, congr_arg, Or.imp, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a_1 b_1 : WithTop α
inst_2 : NoZeroDivisors α
a b : α
hab : a * b = 0
h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) (Option.some a) (Option.some b)) 0
h₂ : ¬(Option.some a = 0 ∨ Option.some b = 0)
⊢ False

Tactic:
exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))

Premises used: WithTop.some, congr_arg, Or.imp, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ a ≠ ⊤

Tactic:
hinf
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
lift : ∀ (a : α) (h₀ : 0 < (↑a : WithTop α)), StrictMono (β := WithTop α) fun (x : WithTop α) ↦ (↑a : WithTop α) * x
⊢ StrictMono (β := WithTop α) fun (x : WithTop α) ↦ a * x

Tactic:
lift a to α using hinf
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
⊢ b ≠ ⊤

Tactic:
hbc.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
lift :
  ∀ (b : α) (hbc : (↑b : WithTop α) < c),
    LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
      ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) c)
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) b)
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) c)

Tactic:
lift b to α using hbc.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c : WithTop α
b : α
hbc : (↑b : WithTop α) < ⊤
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) ⊤)

Tactic:
simp [← coe_mul, mul_top h₀.ne']

Premises used: WithTop.mul_top, LT.lt.ne', WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c_1 : WithTop α
b c : α
hbc : (↑b : WithTop α) < (↑c : WithTop α)
simp : ∀ (h₀ : 0 < a) (hbc : b < c), a * b < a * c
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑c : WithTop α))

Tactic:
simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *

Premises used: WithTop.coe_lt_coe, gt_iff_lt, WithTop.coe_pos, WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
c_1 : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ a * b < a * c

Tactic:
mul_lt_mul_of_pos_left hbc h₀

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
c_1 : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ a * b < a * c

Tactic:
exact mul_lt_mul_of_pos_left hbc h₀

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c : WithTop α
b : α
hbc : (↑b : WithTop α) < c
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) c)

Tactic:
match c with
  | ⊤ => simp [← coe_mul, mul_top h₀.ne']
  | (c : α) =>
  simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
  exact mul_lt_mul_of_pos_left hbc h₀
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ a ≠ ⊤

Tactic:
hinf
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
lift : ∀ (a : α) (h₀ : 0 < (↑a : WithTop α)), StrictMono (β := WithTop α) fun (x : WithTop α) ↦ x * (↑a : WithTop α)
⊢ StrictMono (β := WithTop α) fun (x : WithTop α) ↦ x * a

Tactic:
lift a to α using hinf
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
⊢ b ≠ ⊤

Tactic:
hbc.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
lift :
  ∀ (b : α) (hbc : (↑b : WithTop α) < c),
    LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
      ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) c)
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) b)
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) c)

Tactic:
lift b to α using hbc.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c : WithTop α
b : α
hbc : (↑b : WithTop α) < ⊤
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) ⊤)

Tactic:
simp [← coe_mul, top_mul h₀.ne']

Premises used: WithTop.top_mul, LT.lt.ne', WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c_1 : WithTop α
b c : α
hbc : (↑b : WithTop α) < (↑c : WithTop α)
simp : ∀ (h₀ : 0 < a) (hbc : b < c), b * a < c * a
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑c : WithTop α))

Tactic:
simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *

Premises used: WithTop.coe_lt_coe, gt_iff_lt, WithTop.coe_pos, WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
c_1 : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
ha : 0 < a
⊢ b * a < c * a

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c : WithTop α
b : α
hbc : (↑b : WithTop α) < c
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) c)

Tactic:
match c with
  | ⊤ => simp [← coe_mul, top_mul h₀.ne']
  | (c : α) =>
  simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
  gcongr
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑1 : WithTop α) * (↑a : WithTop α) = (↑a : WithTop α)
rw₁ : (↑(1 * a) : WithTop α) = (↑a : WithTop α)
rw₂ rw₃ : (↑a : WithTop α) = (↑a : WithTop α)
⊢ 1 * (↑a : WithTop α) = (↑a : WithTop α)

Tactic:
rw [← coe_one, ← coe_mul, one_mul]

Premises used: WithTop.coe_one, WithTop.coe_mul, one_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑a : WithTop α) * (↑1 : WithTop α) = (↑a : WithTop α)
rw₁ : (↑(a * 1) : WithTop α) = (↑a : WithTop α)
rw₂ rw₃ : (↑a : WithTop α) = (↑a : WithTop α)
⊢ (↑a : WithTop α) * 1 = (↑a : WithTop α)

Tactic:
rw [← coe_one, ← coe_mul, mul_one]

Premises used: WithTop.coe_one, WithTop.coe_mul, mul_one