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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
      (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
    restrict_commute h_comm.symm _ _

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (e * a + e * b) * e = e * a * e + e * b * e

Tactic:
add_mul

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
restrict_comp hf' hg',

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) (restrict g hg' ∘ₗ restrict f hf') = 0
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
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ ((mapBilinear (RingHom.id R) M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M)
      (dualTensorHom R N N) =
    ((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)

Tactic:
ext f m g n

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : Dual R M
m : M
g : Dual R N
n : N
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((mapBilinear (RingHom.id R) M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M)
                  (dualTensorHom R N N)))
              f)
            m))
        g)
      n =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)))
              f)
            m))
        g)
      n
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Tactic:
have h :=
    calc
      Submodule.comap ((f - μ • 1) ^ finrank K V)
        (f.genEigenspace μ (finrank K V)) =
          LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
            (f - algebraMap K (End K V) μ) ^ finrank K V) := by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
      _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
              simp_rw [← pow_add, genEigenspace_nat]; rfl
      _ = f.genEigenspace μ (finrank K V) := by
              rw [genEigenspace_eq_genEigenspace_finrank_of_le]; lia

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))
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:
by simp

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

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

Tactic:
by 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₁
⊢ comp 1 1 = i₁.comp 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)

Tactic:
exact reduce_replicate _ _

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:
by simp

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

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

Tactic:
by 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:
by 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₂
y : M₃
⊢ 1 y = 1 ↔ y ∈ Set.range ⇑f₂

Tactic:
by simpa using hf₂ y

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

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

Tactic:
by 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:
by 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:
by 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:
by 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₂
y : M₃
⊢ 0 y = 0 ↔ y ∈ Set.range ⇑f₂

Tactic:
by simpa using hf₂ y

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:
by 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:
by 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:
by 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:
by 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:
by simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
⊢ ↑↑0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
⊢ ∀ (n : ℕ), ↑↑(n + 1) = ↑↑n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  ∑ i ∈ insert (Polynomial.map (algebraMap R S) f).natDegree (range (Polynomial.map (algebraMap R S) f).natDegree),
      (Polynomial.map (algebraMap R S) f).coeff i * x ^ i =
    0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
sum_insert notMem_range_self,

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  (Polynomial.map (algebraMap R S) f).coeff (Polynomial.map (algebraMap R S) f).natDegree *
        x ^ (Polynomial.map (algebraMap R S) f).natDegree +
      ∑ x_1 ∈ range (Polynomial.map (algebraMap R S) f).natDegree,
        (Polynomial.map (algebraMap R S) f).coeff x_1 * x ^ x_1 =
    0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
intro i hi
    obtain ⟨k, hk⟩ := exists_add_of_le hi
    rw [hk, pow_add]
    exact mul_mem_right _ _ this

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₃]
⊢ (fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK })
      ((fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }) x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₃,c₁]
⊢ (fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK })
      ((fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }) x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n) %ₘ q + r * (C h.leadingCoeff * q ^ n) %ₘ q +
        C g.leadingCoeff * q ^ m * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q

Tactic:
rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ 0 + r * (C h.leadingCoeff * q ^ n) %ₘ q + C g.leadingCoeff * q ^ m * s %ₘ q + r * s %ₘ q = r * s %ₘ q

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
R : Type u_3
c₁ c₃ : R
inst✝² : CommRing R
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
s : S
a : ℍ[R,c₁,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
b : Option α
⊢ 1 • b = b

Tactic:
cases b
    exacts [rfl, congr_arg some (one_smul _ _)]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y✝ : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x y : ℍ[R,c₁,c₂,c₃]
⊢ (op ∘ star) (x * y) = (op ∘ star) x * (op ∘ star) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r✝ x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
r : R
⊢ (op ∘ star) ((algebraMap R ℍ[R,c₁,c₂,c₃]) r) = (algebraMap R ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ) r

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im * a.im = -(-a.im * a.im)

Tactic:
neg_mul,

Goal state after:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im * a.im = - -(a.im * a.im)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker (algebraMap R (R ⧸ P)) = P

Tactic:
ext a; simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) 1 x = x

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ (-1) ^ (k + 1) * a * b = (-1) ^ (k + 1) * (a * b)

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(s * t) ≤ #↑s * #↑t

Tactic:
by
  rw [← image2_mul]; exact Cardinal.mk_image2_le

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ Nat.card ↑s⁻¹ = Nat.card ↑s

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) = ∏ i, f i ^ a i

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: R : Type u_4
inst✝ : Ring R
k : ℤ
⊢ (fun x ↦ x • 1) k = ↑k

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) = ∏ i, f i ^ a i

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ ∀ s ∈ toSubmonoid '' f, s.MulSaturated

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
hs : s.saturation.toSubmonoid ≤ s
⊢ s.saturation.MulSaturated

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ IsMulIndecomposable.baseOf v f ⊆ univ

Tactic:
by simp

Goal state after: