mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ n.binCast = ↑n

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
case ind
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → m.binCast = ↑m
⊢ k.binCast = ↑k
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ 1 * a = a

Tactic:
one_mul

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a = a
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
smul_sub,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • y - b • x + x
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ a * b + 1 * b = a * b + b

Tactic:
one_mul

Goal state after:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ a * b + b = a * b + b
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ 1 * b + a * b = b + a * b

Tactic:
one_mul

Goal state after:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ b + a * b = b + a * b
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ n + n = n + n
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ ↑n * a + a = ↑n * a + 1 * a

Tactic:
one_mul

Goal state after:
case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ ↑n * a + a = ↑n * a + a
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -0 = 0

Tactic:
← zero_mul (0 : α),

Goal state after:
α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -(0 * 0) = 0 * 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * b - 1 * b = a * b - b

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * b - b = a * b - b
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ 1 * b - a * b = b - a * b

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ b - a * b = b - a * b
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f n = g n

Tactic:
by rw [f.apply_mnat, g.apply_mnat, h]

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
f : M →* N
⊢ { toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } f =
    ({ toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ } * { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ }) f

Tactic:
exact mul_comp g₁ g₂ f

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ 1 * 1 = 1

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : toMulHom✝¹.toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), toMulHom✝¹.toFun (x + y) = toMulHom✝¹.toFun x + toMulHom✝¹.toFun y
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMulHom✝¹ = toMulHom✝

Tactic:
apply DFunLike.coe_injective

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : toMulHom✝¹.toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), toMulHom✝¹.toFun (x + y) = toMulHom✝¹.toFun x + toMulHom✝¹.toFun y
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ⇑toMulHom✝¹ = ⇑toMulHom✝
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ x.val

Tactic:
by
  simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : (↑toMonoidHom✝¹).toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), (↑toMonoidHom✝¹).toFun (x + y) = (↑toMonoidHom✝¹).toFun x + (↑toMonoidHom✝¹).toFun y
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝

Tactic:
apply DFunLike.coe_injective

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : (↑toMonoidHom✝¹).toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), (↑toMonoidHom✝¹).toFun (x + y) = (↑toMonoidHom✝¹).toFun x + (↑toMonoidHom✝¹).toFun y
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ⇑toMonoidHom✝¹ = ⇑toMonoidHom✝
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ 1 * y = y

Tactic:
one_mul

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c : G₀
m n : ℕ
a b : G₀
h : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! h
      exact (Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero

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

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

Tactic:
zpow_neg

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a + 1 * b

Tactic:
one_mul

Goal state after:
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a + b
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ 1 * -1 = -1

Tactic:
one_mul

Goal state after:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ -1 = -1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑(a ^ 2) = ↑(b ^ 2) ↔ ↑a = ↑b ∨ ↑a = ↑(-b)

Tactic:
val_pow_eq_pow_val,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑a ^ 2 = ↑b ^ 2 ↔ ↑a = ↑b ∨ ↑a = ↑(-b)
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c = min (min a c) b

Tactic:
min_assoc,

Goal state after:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min (min a c) b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a ≤ b + c ↔ a - c ≤ b

Tactic:
tsub_le_iff_right

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a ≤ b + c ↔ a ≤ b + c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
one_mul

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

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

Tactic:
one_mul

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

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

Tactic:
one_mul

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

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

Tactic:
one_mul

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

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

Tactic:
one_mul

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

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

Tactic:
one_mul

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ b < a ↔ b < a
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 ↔ a ≤ b * c

Tactic:
← mul_le_mul_iff_right c,

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
· exact mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'

Goal state after:
case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
min_le_iff,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ a ≤ max c d ∨ b ≤ max c d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
min_le_iff,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ a ≤ max c d ∨ b ≤ max c d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ a ≤ b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a < b * a ↔ a < b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a * b < b ↔ 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 α
inst✝ : MulPosReflectLE α
a0 : 0 < a
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosMono α
inst✝ : MulPosReflectLE α
a0 : 0 < a
⊢ a ≤ b * a ↔ 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✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
a0 : 0 < a
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
a0 : 0 < a
⊢ a < b * a ↔ 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✝¹ : MulPosMono α
inst✝ : MulPosReflectLE α
b0 : 0 < b
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosMono α
inst✝ : MulPosReflectLE α
b0 : 0 < b
⊢ a * b ≤ b ↔ 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 α
inst✝ : MulPosReflectLT α
b0 : 0 < b
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
b0 : 0 < b
⊢ a * b < b ↔ a * b < b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) = d * b

Tactic:
by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb : b ≤ 1
⊢ 1 * b ≤ 1

Tactic:
one_mul

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb : b ≤ 1
⊢ b ≤ 1
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) = d * b

Tactic:
by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 * a⁻¹ ≤ b

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ a⁻¹ ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 * a⁻¹ < b

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ a⁻¹ < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 * b ≤ a ↔ b ≤ a

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 * b < a ↔ b < a

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ b < a ↔ b < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a ≤ 1 * b ↔ a ≤ b

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a < 1 * b ↔ a < b

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a < b ↔ a < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : MulPosReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : MulPosReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
· grind [mul_le_mul_of_nonpos_right hbc ha]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 * b ≤ a ↔ b ≤ a

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 * b < a ↔ b < a

Tactic:
one_mul

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b < a ↔ b < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c

Tactic:
rw [inv_mul_le_iff₀ hc, mul_comm]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
rw [mul_inv]
    exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * ((a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹))

Tactic:
mul_inv_cancel_comm_assoc,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊓ b)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
by
  rw [xgcdAux, Nat.strongRec_eq]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 * 1 = 1

Tactic:
one_mul

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x ↦ x * b) x = (fun x ↦ x * b) y
⊢ x * (b * a) = y * (b * a)

Tactic:
rw [← mul_assoc, ← mul_assoc]

Goal state after:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x ↦ x * b) x = (fun x ↦ x * b) y
⊢ x * b * a = y * b * a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b * a = 1 * a

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b * a = a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ 1 * a = a

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ a = a