awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
n : ℕ
rw : LE.le (α := ℤ) (↑(a / (↑n : ℤ)).natAbs : ℤ) (↑a.natAbs : ℤ)
⊢ |a / (↑n : ℤ)| ≤ |a|

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs]

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
n : ℕ
⊢ LE.le (α := ℤ) (↑(a / (↑n : ℤ)).natAbs : ℤ) (↑a.natAbs : ℤ)

Tactic:
ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Premises used: Nat.zero_le, _private.0.Int.abs_ediv_le_abs.match_2, HDiv.hDiv, Nat.div_le_self, LE.le, Nat.cast, Int.natAbs, Int.ofNat_le_ofNat_of_le, Int.negSucc, Nat.succ, Nat.succ_le_succ
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
n : ℕ
⊢ LE.le (α := ℤ) (↑(a / (↑n : ℤ)).natAbs : ℤ) (↑a.natAbs : ℤ)

Tactic:
exact ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Premises used: _private.0.Int.abs_ediv_le_abs.match_2, HDiv.hDiv, Nat.div_le_self, LE.le, Int.ofNat_le_ofNat_of_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
this : ∀ (a : ℤ) (n : ℕ), |a / (↑n : ℤ)| ≤ |a|
a b : ℤ
n : ℕ
rw : |a / (↑n : ℤ)| ≤ |a|
⊢ |a / -(↑n : ℤ)| ≤ |a|

Tactic:
rw [Int.ediv_neg, abs_neg]

Premises used: abs_neg, Int.ediv_neg
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
this : ∀ (a : ℤ) (n : ℕ), |a / (↑n : ℤ)| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / (↑n : ℤ)| ≤ |a|

Tactic:
apply this
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
z : ℤ
hz : z ≠ 0
rw : Eq (α := ℤ) (↑z.sign.natAbs : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ |z.sign| = 1

Tactic:
rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]

Premises used: Int.natAbs_sign_of_ne_zero, Int.ofNat_one, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
az : a = 0
⊢ a.sign = a / |a|

Tactic:
simp [az]
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
az : a = 0
⊢ a.sign = |a| / a

Tactic:
simp [az]
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
rw : HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ) = 1 ↔ a ^ n = 1
rw₁ : a ^ n.natAbs = 1 ↔ a ^ n = 1
rw₂ rw₃ : a ^ n = 1 ↔ a ^ n = 1
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]

Premises used: zpow_natCast, pow_natAbs_eq_one, Int.natCast_natAbs
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
hg' : BddAbove (g '' range f)
rwa : BddAbove (range (g ∘ f))
rwa₁ rwa₂ rwa₃ rwa₄ : BddAbove (g '' range f)
⊢ BddAbove.{u_3} (α := γ) (range fun (x : α) ↦ g (f x))

Tactic:
rwa [← Function.comp_def, Set.range_comp]

Premises used: Set.range_comp, Function.comp_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
suffices : BddAbove (g '' range f)
⊢ BddAbove.{u_3} (α := γ) (range fun (x : α) ↦ g (f x))

Tactic:
suffices hg' : BddAbove (g '' range f) by
    rwa [← Function.comp_def, Set.range_comp]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
a : α
⊢ Membership.mem (γ := Set β) {x : β | 0 ≤ x} (f a)

Tactic:
hf0 a

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
a : α
⊢ Membership.mem (γ := Set β) {x : β | 0 ≤ x} (f a)

Tactic:
exact hf0 a
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
apply : (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
⊢ BddAbove (g '' range f)

Tactic:
apply hg.map_bddAbove (by rintro x ⟨a, rfl⟩; exact hf0 a)

Premises used: MonotoneOn.map_bddAbove
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
obtain : ∀ (b : β) (hb : b ∈ upperBounds (range f)), (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
⊢ (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty

Tactic:
obtain ⟨b, hb⟩ := hf
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
right : Membership.mem (γ := Set β) {x : β | 0 ≤ x} b
⊢ (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty

Tactic:
use b, hb
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ ∀ (a : α), f a ≤ b

Tactic:
simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hb

Premises used: Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff, mem_upperBounds
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : ∀ (a : α), f a ≤ b
⊢ Membership.mem (γ := Set β) {x : β | 0 ≤ x} b

Tactic:
le_trans (hf0 Classical.ofNonempty) (hb Classical.ofNonempty)

Premises used: Classical.ofNonempty, Set.Mem, setOf, le_trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
b : β
hb : ∀ (a : α), f a ≤ b
⊢ Membership.mem (γ := Set β) {x : β | 0 ≤ x} b

Tactic:
exact le_trans (hf0 Classical.ofNonempty) (hb Classical.ofNonempty)

Premises used: Classical.ofNonempty, le_trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Bounds
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
u v : α → β
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Mul β
inst_4 : PosMulMono β
inst_5 : MulPosMono β
hu : BddAbove (range u)
hu0 : 0 ≤ u
hv : BddAbove (range v)
hv0 : 0 ≤ v
⊢ BddAbove (range (u * v))

Tactic:
letI : Zero (β × β) := ⟨(0, 0)⟩
  BddAbove.range_comp_of_nonneg (f := fun i ↦ (u i, v i)) (g := fun x ↦ x.1 * x.2)
    (bddAbove_range_prod.mpr ⟨hu, hv⟩) (fun x ↦ ⟨hu0 x, hv0 x⟩) ((monotone_fst.monotoneOn _).mul
      (monotone_snd.monotoneOn _) (fun _ hx ↦ hx.1) (fun _ hx ↦ hx.2))

Premises used: bddAbove_range_prod, Iff.mpr, monotone_fst, BddAbove.range_comp_of_nonneg, setOf, LE.le, MonotoneOn.mul, And.right, And.left, And.intro, monotone_snd, Monotone.monotoneOn, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ MulPosStrictMono α

Tactic:
posMulStrictMono_iff_mulPosStrictMono.1 inferInstance

Premises used: inferInstance, posMulStrictMono_iff_mulPosStrictMono, Iff.mp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
inl : a * 0 ≤ b * 0
inr : ∀ (hc : c ≠ 0), a * c ≤ b * c
⊢ a * c ≤ b * c

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
⊢ a * 0 ≤ b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
inr : ∀ (hab : a ≤ a), a * c ≤ a * c
inr₁ : ∀ (hab : a < b), a * c ≤ b * c
⊢ a * c ≤ b * c

Tactic:
obtain rfl | hab := hab.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a c : α
hc : c ≠ 0
hab : a ≤ a
⊢ a * c ≤ a * c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab_1 : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c

Tactic:
(mul_lt_mul_of_pos_right hab hc.pos).le

Premises used: Ne.pos, LT.lt.le, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b_1 : α
n : ℕ
a b : α
hab_1 : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c

Tactic:
exact (mul_lt_mul_of_pos_right hab hc.pos).le

Premises used: Ne.pos, LT.lt.le, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n_1 n : ℕ
hn : n ≠ 0
⊢ Function.Injective (β := α) fun (a : α) ↦ a ^ n

Tactic:
simpa using (pow_left_strictMonoOn₀ (M₀ := α) hn).injOn

Premises used: StrictMonoOn.injOn, pow_left_strictMonoOn₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : Additive αᵒᵈ
hab :
  Eq (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (⊤ + a) : αᵒᵈ) : α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)
⊢ ⊤ + a = ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : Additive αᵒᵈ
⊢ Eq (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (⊤ + a) : αᵒᵈ) : α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)

Tactic:
simp [bot_eq_zero]

Premises used: bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ ⦃x : Additive αᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x

Tactic:
simp +contextual [IsRegular.of_ne_zero, bot_eq_zero]

Premises used: IsRegular.of_ne_zero, bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : (Additive α)ᵒᵈ
h :
  Eq (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (⊤ + a) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)
⊢ ⊤ + a = ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : (Additive α)ᵒᵈ
h :
  HMul.hMul (α := α) (β := α) (⊥ : α)
      ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) a : Additive α) :
        α) =
    ⊥
⊢ Eq (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (⊤ + a) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a_1 b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ HMul.hMul (α := α) (β := α) (⊥ : α)
      ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) a : Additive α) :
        α) =
    ⊥

Tactic:
simp [bot_eq_zero (α := α)]

Premises used: bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
simp : ∀ (a : α), ¬a = ⊥ → IsRegular a
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ (a : α), ¬a = ⊥ → IsRegular a

Tactic:
simp +contextual [bot_eq_zero, IsRegular.of_ne_zero]

Premises used: IsRegular.of_ne_zero, bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst_1 : NoZeroDivisors α
hn : n ≠ 0
simp_rw : a ^ n ≠ 0 ↔ a ≠ 0
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
simp_rw [pos_iff_ne_zero, pow_ne_zero_iff hn]

Premises used: pos_iff_ne_zero, pow_ne_zero_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
u : αˣ
⊢ 0 < (↑u : α)

Tactic:
u.ne_zero.pos

Premises used: Ne.pos, Units.ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
contrapose! : ∀ (h : b ≤ a * c⁻¹), b * c ≤ a
⊢ a * c⁻¹ < b

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a

Tactic:
simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le zero_le h

Premises used: zero_le, inv_inv, mul_inv_le_of_le_mul₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
rw : ∀ (h : a < c * b), a * b⁻¹ < c
⊢ b⁻¹ * a < c

Tactic:
rw [mul_comm] at *

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < c * b
⊢ a * b⁻¹ < c

Tactic:
mul_inv_lt_of_lt_mul₀ h

Premises used: mul_inv_lt_of_lt_mul₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c : α
h : a < c * b
⊢ a * b⁻¹ < c

Tactic:
exact mul_inv_lt_of_lt_mul₀ h

Premises used: mul_inv_lt_of_lt_mul₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ a ≠ 0

Tactic:
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ a⁻¹ ≤ c⁻¹

Tactic:
rw [← inv_le_inv₀ ha.pos hc] at hh

Premises used: Ne.pos, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
hh₁ : a⁻¹ ≤ c⁻¹
⊢ a ≠ 0

Tactic:
rw [← inv_le_inv₀ ha.pos hc] at hh

Premises used: Ne.pos, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d

Tactic:
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le (inv_pos.2 hc)

Premises used: Iff.mpr, zero_le, mul_lt_mul_of_le_of_lt_of_nonneg_of_pos, inv_mul_cancel_left₀, inv_pos, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : Additive αᵒᵈ), ⊤ + x = ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
hab :
  Eq.{u_1 + 1} (α := α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (-⊤) : αᵒᵈ) : α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)
⊢ Eq.{u_1 + 1} (α := Additive αᵒᵈ) (-⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Eq.{u_1 + 1} (α := α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) (-⊤) : αᵒᵈ) : α)
    ((OrderDual.ofDual : (a : αᵒᵈ) → α) ((Additive.toMul : (a : Additive αᵒᵈ) → αᵒᵈ) ⊤ : αᵒᵈ) : α)

Tactic:
simp [bot_eq_zero]

Premises used: bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ ⦃x : Additive αᵒᵈ⦄, x ≠ ⊤ → x + -x = 0

Tactic:
simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
      -ofDual_eq_zero]

Premises used: OrderDual.ext_iff, Additive.ext_iff, bot_eq_zero, ofDual_eq_zero, Additive.toMul_eq_top
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (x : (Additive α)ᵒᵈ), ⊤ + x = ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
h :
  Eq.{u_1 + 1} (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (-⊤) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)
⊢ Eq.{u_1 + 1} (α := (Additive α)ᵒᵈ) (-⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
h : Eq.{u_1 + 1} (α := α) ⊥⁻¹ ⊥
⊢ Eq.{u_1 + 1} (α := α)
    ((Additive.toMul : (a : Additive α) → α)
        ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) (-⊤) : Additive α) :
      α)
    ((Additive.toMul : (a : Additive α) → α) ((OrderDual.ofDual : (a : (Additive α)ᵒᵈ) → Additive α) ⊤ : Additive α) :
      α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ Eq.{u_1 + 1} (α := α) ⊥⁻¹ ⊥

Tactic:
simp [bot_eq_zero]

Premises used: bot_eq_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
simp :
  ∀ (a : α),
    ¬a = ⊥ →
      HAdd.hAdd (α := (Additive α)ᵒᵈ) (β := (Additive α)ᵒᵈ)
          ((OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
              ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
            (Additive α)ᵒᵈ)
          (-(OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
                ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
            (Additive α)ᵒᵈ) =
        0
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → x + -x = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ (a : α),
    ¬a = ⊥ →
      HAdd.hAdd (α := (Additive α)ᵒᵈ) (β := (Additive α)ᵒᵈ)
          ((OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
              ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
            (Additive α)ᵒᵈ)
          (-(OrderDual.toDual : (a : Additive α) → (Additive α)ᵒᵈ)
                ((Additive.ofMul : (a : α) → Additive α) a : Additive α) :
            (Additive α)ᵒᵈ) =
        0

Tactic:
simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
      -ofDual_eq_zero]

Premises used: OrderDual.ext_iff, Additive.ext_iff, bot_eq_zero, ofDual_eq_zero, Additive.toMul_eq_top
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ

Tactic:
⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Premises used: _private.0.denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units.match_1, And.intro, Iff.intro, DenselyOrdered
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
refine_1 : ∀ (H : DenselyOrdered α), Nontrivial.{u_1} αˣ
refine_2 : ∀ (H : DenselyOrdered α), DenselyOrdered.{u_1} αˣ
refine_3 :
  Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ →
    ∀ (H₁ : Nontrivial.{u_1} αˣ) (H₂ : DenselyOrdered.{u_1} αˣ), DenselyOrdered α
⊢ DenselyOrdered α ↔ Nontrivial.{u_1} αˣ ∧ DenselyOrdered.{u_1} αˣ

Tactic:
refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
refine_1 : ∀ (x : α) (hx : 0 < x) (hx' : x < 1), Nontrivial.{u_1} αˣ
⊢ Nontrivial.{u_1} αˣ

Tactic:
obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)

Premises used: exists_between, zero_lt_one'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ Units.mk0 x ⋯ ≠ 1

Tactic:
simpa [Units.ext_iff] using hx'.ne

Premises used: Units.ext_iff, LT.lt.ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ Nontrivial.{u_1} αˣ

Tactic:
exact ⟨Units.mk0 x hx.ne', 1, by simpa [Units.ext_iff] using hx'.ne⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered.{u_1} αˣ

Tactic:
⟨fun x y h ↦ ?_⟩

Premises used: DenselyOrdered.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
refine_2 : ∀ (x y : αˣ) (h : x < y), ∃ (a : αˣ), x < a ∧ a < y
⊢ DenselyOrdered.{u_1} αˣ

Tactic:
refine ⟨fun x y h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
refine_2 : ∀ (z : α) (hz : (↑x : α) < z ∧ z < (↑y : α)), ∃ (a : αˣ), x < a ∧ a < y
⊢ ∃ (a : αˣ), x < a ∧ a < y

Tactic:
obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)

Premises used: Iff.mpr, exists_between, Units.val_lt_val
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
z : α
hz : (↑x : α) < z ∧ z < (↑y : α)
⊢ x < Units.mk0 z ⋯ ∧ Units.mk0 z ⋯ < y

Tactic:
simp [← Units.val_lt_val, hz]

Premises used: Units.val_lt_val
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x y : αˣ
h : x < y
z : α
hz : (↑x : α) < z ∧ z < (↑y : α)
⊢ ∃ (a : αˣ), x < a ∧ a < y

Tactic:
refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩
-- 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} αˣ
⊢ DenselyOrdered α

Tactic:
⟨fun x y h ↦ ?_⟩

Premises used: DenselyOrdered.mk