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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ ↑a * (↑a⁻¹ * b) = b

Tactic:
rw [← mul_assoc, mul_inv, one_mul]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1

Tactic:
rwa [← mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * a⁻¹ = 1

Tactic:
h.mul_inv_cancel

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N)))
      ((fun u ↦ { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ }) (u₁, u₂)) =
    (u₁, u₂)

Tactic:
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv,
      MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ (MonoidHom.mk' (fun u ↦ { val := (↑u).1, inv := (↑u⁻¹).1, val_inv := ⋯, inv_val := ⋯ }) ⋯)
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹), val_inv := ⋯, inv_val := ⋯ } =
      u₁ ∧
    (MonoidHom.mk' (fun u ↦ { val := (↑u).2, inv := (↑u⁻¹).2, val_inv := ⋯, inv_val := ⋯ }) ⋯)
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹), val_inv := ⋯, inv_val := ⋯ } =
      u₂
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (0 * a) = f 0

Tactic:
by simp only [mul, zero, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case negSucc
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ f.subtypePerm hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm ⋯

Tactic:
| negSucc n =>

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * σ = σ ↔ i = j

Tactic:
mul_eq_right,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j = 1 ↔ i = j
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ n * b = 0

Tactic:
by
  rw [show n = n - m + m by lia, pow_add, mul_assoc, h]
  simp

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

Goal state before:
pp: x✝ : ℤ
⊢ x✝ ^ 0 = 1

Tactic:
by simp [Int.pow_zero]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑1 = 1

Tactic:
cast_natCast,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)

Tactic:
cast_natCast,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑(n + 1)
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑↑m + ↑-[n+1]

Tactic:
cast_natCast,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑m + ↑-[n+1]
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n - ↑m.succ = ↑-[m+1] + ↑↑n

Tactic:
cast_natCast,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n - ↑m.succ = ↑-[m+1] + ↑n
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (if hnm : n < m then lt n hnm
    else
      ge n ⋯
        (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯)) =
    ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
dif_neg (Int.not_lt.mpr hn)

Goal state after:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ ge n ⋯
      (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    ge n hn fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
add_mul,

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

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

Tactic:
add_mul,

Goal state after:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ 1 * b + a * b = b + a * b
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 + 1) * a

Tactic:
add_mul,

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

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ ¬IsSquare (-1)

Tactic:
rintro ⟨a | a, ⟨⟩⟩

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑m * ↑(m ^ n) = ↑m * ↑m ^ n

Tactic:
cast_pow m n

Goal state after:
α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑m * ↑m ^ n = ↑m * ↑m ^ n
Module: Mathlib.Algebra.Ring.Basic

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

Tactic:
by rw [neg_inv]

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

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
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) g
⊢ { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g

Tactic:
cases g

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✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
g : α →+* β
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) g
⊢ { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g

Tactic:
cases g

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✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f ((x + y) * x + (x + y) * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
add_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x + (x + y) * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x + (x + y) * y) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
add_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * x + y * x + (x * y + y * y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f x * f x + f (y * x) + (f (x * y) + f y * f y) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
add_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f x * f x + f (y * x) + (f (x * y) + f y * f y) = f x * (f x + f y) + f y * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Subsingleton M₀
⊢ IsUnit a

pp: case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Nontrivial M₀
⊢ IsUnit a

Tactic:
· convert! h

Goal state after:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Nontrivial M₀
⊢ IsUnit a
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
⊢ a * d = c / d * b * d ↔ a * d = c * b

Tactic:
hbd.right_comm,

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
⊢ a * d = c / d * d * b ↔ a * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h),

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
simp only [divp, add_mul, mul_inv_rev, val_mul]
  rw [mul_comm (↑u₁ * b), mul_comm b]
  rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * (a - b) + b * (a - b)
Module: Mathlib.Algebra.Ring.Commute

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

Tactic:
rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑(Int.negSucc z) • a = -1 • ↑↑z.succ • a

Tactic:
simp [← smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case negSucc
R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M
a✝ : ℕ
⊢ (Int.negSucc a✝ • x) • y = Int.negSucc a✝ • x • y

Tactic:
simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: α : Type u_4
inst✝ : NonAssocSemiring α
⊢ (Set.range fun x ↦ 2 * x) = {a | Even a}

Tactic:
ext x
  simp [eq_comm, two_mul, Even]

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

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

Tactic:
add_mul,

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
add_mul,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    a ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)
Module: Mathlib.Order.MinMax

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

Tactic:
by cases le_total a b <;> simp [*]

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

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

Tactic:
add_comm c,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - (d + c) ≤ a - c + (b - d)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ c * a = b * a ↔ c = b

Tactic:
by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_left (h.lt_of_ne h') a |>.ne

Goal state after:
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✝ : MulRightStrictMono α
h : a * b = c * d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
obtain hac | rfl | hca := lt_trichotomy a c

Goal state after:
case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

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 ∨ a < a ∨ b < d

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
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ c + a ≤ c + b

Tactic:
add_comm c,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ c + 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.Logic.Embedding.Basic

Goal state before:
pp: case mk
α : Sort u
β : Sort v
g : α ↪ β
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝, inj' := inj'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, inj' := inj'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
α : Sort u
β : Sort v
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝¹, inj' := inj'✝¹ }.toFun = { toFun := toFun✝, inj' := inj'✝ }.toFun
⊢ { toFun := toFun✝¹, inj' := inj'✝¹ } = { toFun := toFun✝, inj' := inj'✝ }
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 + a * (a + b) = a ^ 2 + (a + b) * b

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 + a * (a + b) = a ^ 2 + (a * b + b * b)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ (2 + 2) * (a * b) = 2 * a * b + 2 * a * b

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 2 * (a * b) + 2 * (a * b) = 2 * a * b + 2 * a * b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r →r s
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h : (fun o ↦ o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ } = (fun o ↦ o.toFun) g
⊢ { toFun := toFun✝, map_rel' := map_rel'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
map_rel'✝¹ : ∀ {a b : α}, r a b → s (toFun✝¹ a) (toFun✝¹ b)
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h :
  (fun o ↦ o.toFun) { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } =
    (fun o ↦ o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ }
⊢ { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } = { toFun := toFun✝, map_rel' := map_rel'✝ }
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
⊢ f x = f y → x = y

Tactic:
hxy

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ x = y

Tactic:
hxy

Goal state after:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ x = y

Tactic:
hxy

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y
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 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]

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

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : α →o β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝, monotone' := monotone'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, monotone' := monotone'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun = { toFun := toFun✝, monotone' := monotone'✝ }.toFun
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹ } = { toFun := toFun✝, monotone' := monotone'✝ }