mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Semiconj

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + -b) x y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x⁻¹ʳ ≠ 0 → IsUnit x

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ ¬x⁻¹ʳ = 0 → IsUnit x
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 ∨ ∃ u, a = ↑u

Tactic:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 ∨ ¬a = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n

Tactic:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * d = c * b

Tactic:
← mul_one a,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * 1 * d = c * b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑n) x
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑(n + 1)) x
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]

Tactic:
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
    congr 1
    exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommGroup α
inst✝ : AddCommGroup β
a b : α
n : Multiplicative ℤ
⊢ ((zpowersHom α).toFun (a * b)) n = ((zpowersHom α).toFun a * (zpowersHom α).toFun b) n

Tactic:
simp [mul_zpow]

Goal state after:
Module: Mathlib.Algebra.Field.Defs

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ q • 1 = ↑q

Tactic:
rw [NNRat.smul_def, mul_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ f (2 * a + 1) = 2 * f a + 1

Tactic:
by simp [two_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
n : ℕ
ha : Odd a
⊢ Odd (a ^ n)

Tactic:
induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: n : ℕ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ (∃ x, n = 2 * x) ∨ ∃ x, n = 2 * x + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)

Tactic:
simpa using

Goal state after:
case succ
k : ℕ
⊢ 2 ∣ k * (k + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id

Tactic:
hf.iterate_odd hn

Goal state after:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f = id
hn : Odd n
⊢ f = id
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ ¬Even n

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ Odd n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLE α
h : a ≤ b
⊢ ∃ c, 1 ≤ c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ c_1, 1 ≤ c_1 ∧ a * c_1 = a * c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a / c ≤ b / c ↔ a ≤ b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * c⁻¹ ≤ b * c⁻¹ ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a / c < b / c ↔ a < b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * c⁻¹ < b * c⁻¹ ↔ a < b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a < c / b ↔ a * b < c

Tactic:
by
  rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d

Tactic:
simpa using

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ b = d
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ a < a

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MulOneClass α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : MulOneClass α
inst✝ : LE α
a b : α
⊢ a ≤ b → a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
simpa using

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂

Tactic:
contrapose!
  exact fun h => mul_le_mul' h.1 h.2

Goal state after:
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, b < a

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : a < 0
hb : 0 < b
⊢ a * b < 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : a < 0
hb : 0 < b
⊢ a * b < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < b
⊢ 0 < a * b ↔ 0 < a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < b
⊢ 0 < a * b ↔ 0 < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : a < 1
⊢ a * b < b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : a < 1
⊢ a * b < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : b < 1
⊢ a * b < a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : b < 1
⊢ a * b < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : 1 < b
⊢ a < a * b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : 1 < b
⊢ a < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ 1 ≤ b ^ 1

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ a * b ≤ a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
n : ℕ
⊢ a ^ (n + 2) ≤ b ^ (n + 2)

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
n : ℕ
⊢ a * (a * a ^ n) ≤ b * (b * b ^ n)
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ b * a ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : MulPosStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < b * a

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : MulPosStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < b * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ 2

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a * a
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ a * b < a * c

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ a * b < a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ (0 + 1)

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
x✝ : 1 ≠ 0
⊢ a ^ 1 < b ^ 1

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
x✝ : 1 ≠ 0
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ b * a < c * a

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ b * a < c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) < b ^ (n + 2)

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ n * a * a < b ^ n * b * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
m : ℕ
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
m : ℕ
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m