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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
⊢ f a c = f a b * f b c

Tactic:
obtain rbc | rcb := total_of r b c

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c

case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = b⁻¹

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (b * a) = b⁻¹
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = 1 * ↑((liftRight f g h) x)

Tactic:
one_mul,

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = ↑((liftRight f g h) x)
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ ↑u₁ * ↑u₂⁻¹ = 1

Tactic:
rw [h, u₂.mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ ↑b⁻¹ * a = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ 1 * a = a * 1

Tactic:
one_mul,

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ a = a * 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * 1 = 1 * b

Tactic:
one_mul,

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * 1 = b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (b * a) = 1 / b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * b / a = b

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ b * a / a = b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * (b / a) = b

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ b / a * a = b
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (1 * y) = 1 * f y

Tactic:
one_mul,

Goal state after:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f y = 1 * f y
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b

Tactic:
mul_comm,

Goal state after:
M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ b * a / a = b
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
simp only [noZeroDivisors_iff, or_iff_not_imp_right]

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * (1 * b)

Tactic:
one_mul,

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * b
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ 0 / a = 0

Tactic:
rw [div_eq_mul_inv, zero_mul]

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ (n * n).sqrt * (n * n).sqrt = n * n

Tactic:
sqrt_eq

Goal state after:
x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ n * n = n * n
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ b = c * a ↔ b = a * c

Tactic:
by rw [mul_comm]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)

Tactic:
intro p₁ hp₁ p₂ hp₂

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)

Tactic:
intro p₁ hp₁ p₂ hp₂

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n✝ : ℕ
a b : M
u✝ u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = ↑u
⊢ x ^ (n - 1 + 1) = ↑u

Tactic:
Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)

Goal state after:
M : Type u_1
inst✝ : Monoid M
n✝ : ℕ
a b : M
u✝ u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = ↑u
⊢ x ^ n = ↑u
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
h : mk0 a ha = mk0 b hb
⊢ a = b

Tactic:
by injection h

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : G₀ → Prop
⊢ (∃ u, p ↑u) ↔ ∃ x, x ≠ 0 ∧ p x

Tactic:
simp [exists0]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b

Tactic:
mul_comm,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ b * a / a = b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a

Tactic:
mul_comm,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ 1 * a / (a * b) = 1 / b

Tactic:
one_mul,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ a / (a * b) = 1 / b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c * b / (a * c) = b / a

Tactic:
mul_comm,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ b * c / (a * c) = b / a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ a / b * (c / a) = c / b

Tactic:
mul_comm,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ c / a * (a / b) = c / b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a = 1 * ↑⋯.unit

Tactic:
one_mul,

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a = ↑⋯.unit
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ b ^ 2 + a ^ 2 - 2 * b * a = (b - a) ^ 2

Tactic:
sub_sq'

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ b ^ 2 + a ^ 2 - 2 * b * a = b ^ 2 + a ^ 2 - 2 * b * a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a * (2 * b) + 1 * (2 * b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
one_mul,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
by
  rcases k with rfl | k; · simp
  simpa [mul_comm (k + 1)] using k.two_dvd_mul_add_one

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

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

Tactic:
one_mul,

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

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

Tactic:
one_mul,

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

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

Tactic:
one_mul,

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

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

Tactic:
one_mul,

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3

Tactic:
← two_add_one_eq_three

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2 + 1
Module: Mathlib.Algebra.Order.Monoid.NatCast

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

Tactic:
← two_add_one_eq_three

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 2 + 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
one_mul,

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

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

Tactic:
one_mul,

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulRightMono α
a b : α
⊢ cmp (a / b * b) (1 * b) = cmp a b

Tactic:
one_mul,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulRightMono α
a b : α
⊢ cmp (a / b * b) b = cmp a b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ c

Tactic:
exact hc.le

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

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

Tactic:
by
    rw [pow_succ]; exact le_mul_of_one_le_right (pow_nonneg (zero_le_one.trans h) _) h

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₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 ≤ a
hn : 0 ≤ n
⊢ 1 ≤ a ^ n

Tactic:
simpa using zpow_right_mono₀ ha hn

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₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 ≤ a
hn : n ≤ 0
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_mono₀ ha hn

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
⊢ a < b * c⁻¹ ↔ a * c < b

Tactic:
by
  rw [← mul_lt_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_lt_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✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  apply mul_lt_mul hac (by gcongr; assumption) _ hc
  exact inv_pos.2 (hd.trans_le hdb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with

Goal state after:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ 1 * a ⊓ (a ⊓ 1) = a ⊓ 1

Tactic:
one_mul,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ a ⊓ (a ⊓ 1) = a ⊓ 1
Module: Mathlib.Algebra.Order.Group.Lattice

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

Tactic:
mul_comm,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b * (a ⊓ b)⁻¹ * (a ⊓ b) = a * b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
by
  obtain ha | ha := le_total a 1
  · rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
    exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n
  · rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

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

Goal state before:
pp: case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : b⁻¹ * a⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b

Tactic:
mul_comm,

Goal state after:
case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a⁻¹ * b⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ |a / b|ₘ < n

Tactic:
by
  rw [mabs_div_lt_iff, div_lt_iff_lt_mul, div_lt_iff_lt_mul]
  exact ⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩

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_comm,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
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 ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
mul_comm,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ ((b ⊔ a) ⊓ c) * (b ⊔ a ⊔ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ gcdA 0 s = 0

Tactic:
by
  rw [gcdA, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ 1 * (r % k) % k = r % k

Tactic:
one_mul,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ r % k % k = r % k
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ a_n * ↑p.succ + b_n * ↑q.succ = ↑(p + 1) * a_n + ↑(q + 1) * b_n

Tactic:
mul_comm,

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ ↑p.succ * a_n + b_n * ↑q.succ = ↑(p + 1) * a_n + ↑(q + 1) * b_n
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ ↑(a.toNat * (p + 1) + b.toNat * (q + 1)) = ↑n

Tactic:
have : a * p.succ + b * q.succ = n := by rw [add_mul, ← add_assoc,
    add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm, mul_comm b_n]

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑(a.toNat * (p + 1) + b.toNat * (q + 1)) = ↑n
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:
rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (ra ?_)
  simp

Goal state after:
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»]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ ((∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a) ↔ ∀ (b : β), ∃ a, f a = b
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_total m n with h | h

Goal state after:
case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_total m n with h | h
  · rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
    exact mono_cast h
  · rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

Goal state after: