mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * 1

Tactic:
mul_one

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
mul_one

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1)
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a - a * b = a - a * b
Module: Mathlib.Data.Nat.Cast.Basic

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

Tactic:
mul_one

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ a * ↑n + a = a * ↑n + a
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * ↑n

Tactic:
by
  induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -(1 / a * 1) = -(1 / a)

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -(1 / a) = -(1 / a)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
mul_one

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = b * 1 * c ↔ d * a = b * c

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = b * c ↔ d * a = b * c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
inv_pow,

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

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

Tactic:
inv_pow,

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_pow,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_pow,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.Ring.Units

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

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₁⁻¹ + ↑u₂⁻¹ * 1 * b

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₁⁻¹ + ↑u₂⁻¹ * b
Module: Mathlib.Algebra.Ring.Commute

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

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = a * a - 1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a * a = 1 * 1

Tactic:
mul_one

Goal state after:
R : Type u
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a * a = 1
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
by
  rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]

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:
mul_one

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ ↑q = ↑q
Module: Mathlib.Algebra.Field.Defs

Goal state before:
pp: A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ ↑m * 1 = ↑m

Tactic:
mul_one

Goal state after:
A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ ↑m = ↑m
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocSemiring R
m : ℕ
⊢ ↑m * 1 = ↑m

Tactic:
mul_one

Goal state after:
R : Type u_5
inst✝ : NonAssocSemiring R
m : ℕ
⊢ ↑m = ↑m
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ ↑m * 1 = ↑m

Tactic:
mul_one

Goal state after:
R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ ↑m = ↑m
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
obtain hbd | rfl | hdb := lt_trichotomy b d
    · grind
    · exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm
    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
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✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
a b : α
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
mul_one

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

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

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
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✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
ha hb : 1 ≤ 1
⊢ 1 * 1 = 1

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
ha hb : 1 ≤ 1
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a

Tactic:
mul_one

Goal state after:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a

Tactic:
mul_one

Goal state after:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ 1 ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
mul_one

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
a : α
n : ℕ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
by simp [pow_succ]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
a0 : 0 < a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
mul_one

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

Tactic:
mul_one

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

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
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✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a * b < a ↔ a * b < a * 1

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a * b < a ↔ 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₀
a b : G₀
ha : 0 < a
⊢ a * 1 ≤ b ↔ a ≤ b

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT 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✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ b ≤ a * 1 ↔ b ≤ a

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ 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₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ a⁻¹ * 1 ≤ b

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT 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✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ a⁻¹ * 1 < b

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT 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✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a * 1 < b ↔ a < b

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT 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✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ b < a * 1 ↔ b < a

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ 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₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b * 1

Tactic:
mul_one

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ 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 c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b

Tactic:
by
  rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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 c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c

Tactic:
by
  rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
neg_mul_eq_mul_neg,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

Tactic:
neg_mul_eq_mul_neg,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f g : α →o β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f x) ↔ IsMax x

Tactic:
by
  refine ⟨f.strictMono.isMax_of_apply, ?_⟩
  conv_lhs => rw [← f.symm_apply_apply x]
  exact f.symm.strictMono.isMax_of_apply

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨f c, by simpa using hc⟩

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 ⊔ 1 ⊔ (b / a ⊔ 1) = |b / a|ₘ

Tactic:
sup_sup_sup_comm,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ (1 ⊔ 1) = |b / a|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ |a|

Tactic:
abs_eq_natAbs

Goal state after:
a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ ↑a.natAbs
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))

Tactic:
sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ max a b / min a b = |a / b|ₘ

Tactic:
rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]

Goal state after:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n + 1

Tactic:
apply zero_lt_one.trans_le

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ ↑n + 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
⊢ ∀ {s t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
| H1 a b h IH =>

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

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k) % ↑k).toNat = ((↑n * n.gcdA k + ↑k * n.gcdB k) % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

pp: case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n

Tactic:
· intro h
    rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
    exact ⟨_, _, rfl⟩

Goal state after:
case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → a.gcd b ∣ n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
⊢ a = a * 1

Tactic:
mul_one

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
⊢ a = a
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0

Tactic:
by
  rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (ra ?_)
  simp

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
⊢ a = a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Surjective ⇑(map' f) ↔ Surjective ⇑f

Tactic:
simp only [Surjective, «forall»]
  refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩
  · obtain ⟨a, hab⟩ := h.2 b
    induction a using WithZero.recZeroCoe <;>
    simp at hab
    grind
  · obtain ⟨a, ha⟩ := h b
    use a
    simp [ha]

Goal state after: