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

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
rw [zpow_add_one]

Goal state after:
case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ ↑n * g)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)

Tactic:
exact h_inv _ ih

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / (a / b) = b

Tactic:
by simp

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / b / a = b⁻¹

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommGroup α
n : ℕ
a : α
⊢ ↑n • a = n • a

Tactic:
by simp

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
x✝¹ x✝ : Mˣ
⊢ ↑{ val := f ↑(x✝¹ * x✝), inv := f (x✝¹ * x✝).inv, val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := f ↑x✝¹, inv := f x✝¹.inv, val_inv := ⋯, inv_val := ⋯ } *
        { val := f ↑x✝, inv := f x✝.inv, val_inv := ⋯, inv_val := ⋯ })

Tactic:
by simp

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

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

Tactic:
h 1

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

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

Tactic:
rw [one_mul]

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
⊢ ∀ (x y : G →* M), (x * y).toHomUnits = x.toHomUnits * y.toHomUnits

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁴ : EquivLike F α β
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Mul P
inst✝ : Unique α
⊢ ∀ (x y : α → M), (Equiv.funUnique α M).toFun (x * y) = (Equiv.funUnique α M).toFun x * (Equiv.funUnique α M).toFun y

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x : M
hx : IsUnit (f x)
⊢ f (EquivLike.inv f 1) = f 1

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x✝ : M
hx : IsUnit (f x✝)
x y : N
⊢ f ({ toFun := EquivLike.inv f, map_one' := ⋯ }.toFun (x * y)) =
    f ({ toFun := EquivLike.inv f, map_one' := ⋯ }.toFun x * { toFun := EquivLike.inv f, map_one' := ⋯ }.toFun y)

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
⊢ ∀ (a : M), IsUnit (f a) → IsUnit a

Tactic:
by simp

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
⊢ ∀ (a : M × N), 1 * a = a

Tactic:
by simp

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
⊢ ∀ (a : M × N), a * 1 = a

Tactic:
by simp

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✝¹ : DivisionMonoid G
inst✝ : DivisionMonoid H
⊢ ∀ (x : G × H), x⁻¹⁻¹ = x

Tactic:
by simp

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✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x✝¹ * x) x✝ = (fun x ↦ x✝¹ * x) a₂ → x✝ = a₂

Tactic:
by simp

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✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x * x✝¹) x✝ = (fun x ↦ x * x✝¹) a₂ → x✝ = a₂

Tactic:
by simp

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✝¹ : CancelCommMonoid M
inst✝ : CancelCommMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x✝¹ * x) x✝ = (fun x ↦ x✝¹ * x) a₂ → x✝ = a₂

Tactic:
by simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
Q : Type u_6
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
by simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x✝ : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x✝ = f x✝

Tactic:
by simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
Q : Type u_6
inst✝ : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
by simp

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
u : Mˣ × Nˣ
⊢ (↑u.1, ↑u.2) * (↑u.1⁻¹, ↑u.2⁻¹) = 1

Tactic:
by simp

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
u : Mˣ × Nˣ
⊢ (↑u.1⁻¹, ↑u.2⁻¹) * (↑u.1, ↑u.2) = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
⊢ 1 ≠ 0

Tactic:
by
  intro h
  rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
  apply hx
  calc
    x = 1 * x := by rw [one_mul]
    _ = 0 := by rw [h, zero_mul]
    _ = 1 * y := by rw [h, zero_mul]
    _ = y := by rw [one_mul]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ a * a = 0 ↔ a = 0

Tactic:
by simp

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ 0 = a * a ↔ a = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m * σ ^ n) x = (σ ^ n * σ ^ m) x

Tactic:
zpow_mul_comm

Goal state after:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ n * σ ^ m) x = (σ ^ n * σ ^ m) x
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) ((fun x ↦ ⟨f ↑x, ⋯⟩) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f ↑x, ⋯⟩) ((fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.ofNat n = Equiv.mulLeft (a ^ Int.ofNat n)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.negSucc n = Equiv.mulLeft (a ^ Int.negSucc n)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.ofNat n = Equiv.mulRight (a ^ Int.ofNat n)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.negSucc n = Equiv.mulRight (a ^ Int.negSucc n)

Tactic:
by simp

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ (⇑hnp ∘ ⇑hmn) 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ ∀ (x y : α), (⇑hnp ∘ ⇑hmn) (x * y) = (⇑hnp ∘ ⇑hmn) x * (⇑hnp ∘ ⇑hmn) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (if 0 = 0 then 0 else 1) = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (if 1 = 0 then 0 else 1) = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
n : ℕ
⊢ (n + 1).binCast = n.binCast + 1

Tactic:
let : AddMonoidWithOne R := AddMonoidWithOne.unary
      rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a✝ : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : M₀
⊢ f (a • 0) = f 0

Tactic:
simp [smul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a✝ : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : A'
⊢ f (0 • a) = f 0

Tactic:
simp [smul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
inst✝ : Subsingleton M₀
x y : A
⊢ x = y

Tactic:
← one_smul M₀ x,

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
inst✝ : Subsingleton M₀
x y : A
⊢ 1 • x = y
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ 0 ^ Int.negSucc n = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : A
⊢ (if p then 1 else 0) • a = if p then a else 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ -1 • x = -x

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M : Type u_1
α✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : α
⊢ (unop ∘ ⇑f.symm ∘ MulOpposite.op) ((unop ∘ ⇑f ∘ MulOpposite.op) x) = x

Tactic:
by simp

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

Goal state before:
pp: case pos
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
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k 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 ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = Int.strongRec lt ge l

pp: case neg
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
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k 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 ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ (ge l ⋯ fun k_1 x ↦
      Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k 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 ⋯) k_1
        ⋯) =
    Int.strongRec lt ge l

Tactic:
· rw [strongRec_of_lt hlm]

Goal state after:
case neg
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
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k 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 ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ (ge l ⋯ fun k_1 x ↦
      Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k 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 ⋯) k_1
        ⋯) =
    Int.strongRec lt ge l
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M : Type u_1
α✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : β
⊢ (unop ∘ ⇑f ∘ MulOpposite.op) ((unop ∘ ⇑f.symm ∘ MulOpposite.op) x) = x

Tactic:
by simp

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

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

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a else 0) * b = if P then a * b else 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (a * if P then b else 0) = if P then a * b else 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (succ 0 + 1).sqrt ≤ succ 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 = 0 * 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)

Tactic:
by simp

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

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
H : (a :: l).TFAE
⊢ a ∈ a :: l

Tactic:
by simp

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✝¹ : One M
inst✝ : Monoid N
f : OneHom M N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by simp

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
f : M →* N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by simp

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✝¹ : One M
inst✝ : Group N
f : OneHom M N
n : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by simp

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✝ : CommGroup N
f : M →* N
n : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
⊢ f 0 = ↑0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_3
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : FunLike F ℕ R
inst✝ : RingHomClass F ℕ R
f g : F
⊢ f 1 = g 1

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
⊢ g (f 1) = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
a : R
⊢ SemiconjBy a (-1) (-1)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
x : R
⊢ SemiconjBy (-1) x x

Tactic:
by simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ (∃ x, x ≠ 0 ∧ x = a) ↔ a ≠ 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
u : αˣ
⊢ -↑u * -↑u⁻¹ = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
u : αˣ
⊢ -↑u⁻¹ * -↑u = 1

Tactic:
by simp

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

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

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

Goal state after: