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

Goal state before:
pp: case h2
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ snd (ε * x) = snd (x * ε)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
x y : A
⊢ (↑fe).1 x * (↑fe).2 * ((↑fe).1 y * (↑fe).2) = 0

Tactic:
rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case empty
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
⊢ μ₁ ∉ ∅ → Disjoint ((f.genEigenspace μ₁) k) (∅.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f⁻¹ * (↑f * g)) = (trace R M) g

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case intro.inl
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i : ι
⊢ (Matrix.single i i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b i)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Free.ChooseBasisIndex R M))

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).trace = x.trace

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
x✝ : M
⊢ (f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ) x✝ = (μ • f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)

Tactic:
surj,

Goal state after:
case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥⊤)
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_re
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x✝ * y✝).re =
    ({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK } *
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }).re +
      ({ re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK } *
          { re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK }).re

Tactic:
simp

Goal state after:
case h2.e_re
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK)
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imI
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x✝ * y✝).imI =
    ({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK } *
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }).imI +
      ({ re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK } *
          { re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK }).imI

Tactic:
simp

Goal state after:
case h2.e_imI
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ)
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imJ
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x✝ * y✝).imJ =
    ({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK } *
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }).imJ +
      ({ re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK } *
          { re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK }).imJ

Tactic:
simp

Goal state after:
case h2.e_imJ
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI)
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imK
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x✝ * y✝).imK =
    ({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK } *
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }).imK +
      ({ re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK } *
          { re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK }).imK

Tactic:
simp

Goal state after:
case h2.e_imK
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
← geom_sum_mul,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (∑ i ∈ range n, x ^ i) * (x - 1) / (x - 1)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ x * (x ^ Nat.zero)⁻¹ = (x ^ Nat.zero)⁻¹ * x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ -1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case succ.zero
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
ih : reduce (List.replicate 0 x) = List.replicate 0 x
⊢ (List.casesOn (List.replicate 0 x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate 0 x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Prop
L2 L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = L2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
cases L2

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

case cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
h : reduce [] = head✝ :: tail✝ ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ traverse (pure ∘ f) (x * y) = pure (f <$> (x * y))

Tactic:
by
        rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
⊢ comp 1 1 = i₁.comp 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
⊢ Function.Surjective ⇑i₁

Tactic:
by
  refine surjective_of_surjective_of_surjective_of_injective (1 : Unit →* M₁) f₁ f₂ (1 : Unit →* N₁)
    g₁ g₂ 1 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁ (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃
  simp only [Set.mem_range, one_apply, exists_const]
  exact ⟨fun h ↦ (hg₀ ((map_one _).trans h.symm)), fun h ↦ h ▸ (map_one _)⟩

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
⊢ reduce (a :: reduce L) = reduce (a :: L)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ traverse (pure ∘ f) (of x * y) = pure (f <$> (of x * y))

Tactic:
by
        rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
a : α
this : DecidableEq α := Classical.decEq α
⊢ toWord 1 ≠ (of a).toWord

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case h₂
α : Type u
inst✝ : Nonempty α
⊢ ℵ₀ ≤ #(FreeGroup α)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = max #α ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type u
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max #R #X) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
⊢ comp 1 i₃ = comp 1 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type u
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = #R

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
⊢ ∀ ⦃a₂ : Unit⦄, 1 () = 1 a₂ → () = a₂

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
⊢ Fintype.card α ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
⊢ 0 ∘ₗ 0 = i₁ ∘ₗ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
⊢ 0 ∘ₗ i₃ = 0 ∘ₗ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
⊢ ∀ ⦃a₂ : Unit⦄, 0 () = 0 a₂ → () = a₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case ih1
α : Type u_1
x✝ : α
⊢ toFreeMonoid (of x✝) ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case ih2
α : Type u_1
x✝ : α
y✝ : FreeSemigroup α
a✝¹ : toFreeMonoid (of x✝) ≠ 1
a✝ : toFreeMonoid y✝ ≠ 1
⊢ toFreeMonoid (of x✝ * y✝) ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
⊢ 1 = 1 ∨ ∃ y, toFreeMonoid y = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
b : α
⊢ toFreeMonoid (of b) = FreeMonoid.of b * 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
b : α
y : FreeSemigroup α
⊢ toFreeMonoid (of b * y) = FreeMonoid.of b * toFreeMonoid y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case one
α : Type u_1
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : FreeMonoid α),
    (lift fun x ↦ ↑(FreeSemigroup.of x)) (x * y) =
      (lift fun x ↦ ↑(FreeSemigroup.of x)) x * (lift fun x ↦ ↑(FreeSemigroup.of x)) y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℕ
p : ℕ
hf : ∀ k ∈ ∅, f k ≠ 0
⊢ (∅.lcm f).factorization p = ∅.sup fun a ↦ (f a).factorization p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case empty
ι : Type u_3
f : ι → ℚ
⊢ (∑ i ∈ ∅, f i).den ∣ ∅.lcm fun i ↦ (f i).den

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case empty
ι : Type u_3
f : ι → ℚ
⊢ (∏ i ∈ ∅, f i).den ∣ ∏ i ∈ ∅, (f i).den

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).re = (↑x + ↑y).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imI = (↑x + ↑y).imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imJ = (↑x + ↑y).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imK = (↑x + ↑y).imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).re = (-↑x).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imI = (-↑x).imI

Tactic:
simp

Goal state after: