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

Goal state before:
pp: b : Bool
n : Nat
⊢ b.toNat / 2 + n = n

pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
div_eq_of_lt,

Goal state after:
b : Bool
n : Nat
⊢ 0 + n = n

b : Bool
n : Nat
⊢ b.toNat < 2

case H
b : Bool
n : Nat
⊢ 0 < 2
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b

Tactic:
by
  rw [mul_comm, mul_inv_cancel_right]

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

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
⊢ (if h : P then f h else g h) x = if h : P then (f h) x else (g h) x

Tactic:
split_ifs <;> rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ LeftInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
rintro ⟨a⟩; simp only [Quot.map, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h 1

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h 1

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d

Tactic:
smul_assoc,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • b • c • d = (a • c) • b • d
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • b • c • d = (a • c) • b • d

Tactic:
smul_assoc,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ a • b • c • d = a • c • b • d
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • (r • 1) • x = s • r • x

Tactic:
smul_assoc,

Goal state after:
M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • r • 1 • x = s • r • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (s • 1) • (r • 1) • x = s • r • 1 • x

Tactic:
smul_assoc,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • 1 • (r • 1) • x = s • r • 1 • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • (r • 1) • x = s • r • 1 • x

Tactic:
smul_assoc,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • r • 1 • x = s • r • 1 • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ (x • 1) • y = x • y

Tactic:
smul_assoc,

Goal state after:
α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ x • 1 • y = x • y
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ (m • n • 1) • q = m • n • q

Tactic:
smul_assoc,

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ m • (n • 1) • q = m • n • q
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ ((m • 1) • p) • q = m • p • q

Tactic:
smul_assoc,

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ (m • 1) • p • q = m • p • q
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
α : Sort u_1
x : α
p : x ≍ x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯

Tactic:
exact h rfl

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

Goal state before:
pp: case isFalse
n m : Nat
h : n ≤ m
hn : ¬n = 0
x✝ : Decidable (m = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq m 0 with

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl
  exact (hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≠ aᶜ

Tactic:
by
  intro h
  cases le_compl_self.1 (le_of_eq h)
  simp at h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
⊢ GeneralizedHeytingAlgebra α

Tactic:
let lattice := e.lattice
  let top := e.top
  let himp := e.himp
  apply e.injective.generalizedHeytingAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val (if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) = a

Tactic:
split_ifs <;> rfl

Goal state after:
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.domRestrict (extend f g g') = g' ∘ Subtype.val

Tactic:
exact domRestrict_dite_compl _ _

Goal state after:
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s <;> [left; right] <;> use x

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise f g x

case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise f g x
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ (if h : ∃ a, f a = x then r • g (Classical.choose ⋯) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x

Tactic:
split_ifs <;> rfl

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
⊢ uniqueElim ⁻¹' univ.pi t = t default

Tactic:
ext; simp [Unique.forall_iff]

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩
    choose! f hf using this
    rw [forall_mem_image] at hf
    use f
    rw [graphOn, image_image, EqOn.image_eq_self]
    exact fun x hx ↦ h (hf hx) hx rfl

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
by
  obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <|
    by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [Set.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
  exact ⟨
  { toFun := e₁
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

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

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ cast ⋯
      (match ↑((z - b).toNat + 1) with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] => inductionOn'.neg b zero pred n) =
    succ z hz
      (cast ⋯
        (match ↑(z - b).toNat with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
grind [inductionOn'.pos, show b + (z - b).toNat = z by lia]

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Tactic:
exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
⊢ (a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
⊢ (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n : ℕ
hn : n ≠ 0
ha : a ^ n ≠ 0
⊢ a ≠ 0

Tactic:
rintro rfl; exact ha <| zero_pow hn

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n

Tactic:
split_ifs <;> rfl

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

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

Tactic:
simpa only [one_div] using inv_ne_zero h

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✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ f (r * s) • m = f r • f s • m

Tactic:
simp [mul_smul]

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

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

Tactic:
← neg_add_rev,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = -(↑(n + 1) + ↑(m + 1))
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
mul_add,

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

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

Tactic:
mul_add,

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

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

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

Tactic:
mul_zero,

Goal state after:
α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: z : ℤ
⊢ IsSquare z.sign ↔ 0 ≤ z

Tactic:
induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩

Goal state after:
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 + 1)

Tactic:
Nat.cast_succ,

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ a * ↑n + a = a * (↑n + 1)
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 + 1)

Tactic:
mul_add,

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ a * ↑n + a = a * ↑n + a * 1
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 + y)) = f (x + y) * f (x + y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
mul_add,

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 + 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 * 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

Tactic:
mul_add,

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 x * f y + f y * (f x + f 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 x + f x * f y + f y * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
mul_add,

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 x * f y + (f y * f x + f y * f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Units

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

Tactic:
mul_add,

Goal state after:
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * 1 + ↑a * (↑a⁻¹ * b)
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x

Tactic:
induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

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:
mul_add,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑(n + 1) = f (↑n + 1)

Tactic:
Nat.cast_succ,

Goal state after:
R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = f (↑n + 1)
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑↑n = ↑n

Tactic:
intCast,

Goal state after:
R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑↑n = ↑n
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑(n + 1) • b = (n + 1) • b

Tactic:
Nat.cast_succ,

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ (↑n + 1) • b = (n + 1) • b
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = f (-↑(n + 1))

Tactic:
intCast,

Goal state after:
R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑(Int.negSucc n) = f (-↑(n + 1))