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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' :
  (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ =
    0 ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
rw [assoc, zero_comp, X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃] at hx₂'

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂'✝ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯) ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) =
    0

Tactic:
rw [this]; simp

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) ≫
      hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) =
    0

Tactic:
rw [this]; simp

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (𝟙 i₁) f ⋯ n₁

Tactic:
rw [← cancel_epi (X.pOpcycles f (𝟙 _) n₁), p_fromOpcycles]
  dsimp [opcyclesIsoH]
  simp only [p_opcyclesIso_inv_assoc, homologyDataIdId_right_p, ← Functor.map_id,
    ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom]
  congr 1
  cat_disch

Goal state after:
Module: Mathlib.Order.Filter.Subsingleton

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝ : l.NeBot
hl : l.Subsingleton
⊢ ∃ a, l = pure a

Tactic:
rcases hl with ⟨s, hsl, hs⟩
  rcases exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨nonempty_of_mem hsl, hs⟩ with ⟨a, rfl⟩
  refine ⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩
  rwa [le_pure_iff]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ EventuallyConst (⇑f) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (page X data r hr).d pq pq' ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0

pp: case neg
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq pq'
⊢ (page X data r hr).d pq pq' ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0

Tactic:
· dsimp
    rw [pageD_eq X data r hr pq pq' h (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
      (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
      (homOfLE (data.le₃₃' hrr' hr pq' hi₃ hi₃'))
      (homOfLE (by simpa only [hi₃', data.i₃_next r r' _ _ h] using data.le₂₃ r pq))
      hi₀ hi₁ (by rw [hi₂, data.hc₀₂ r _ _ h])
      (by rw [hi₃, data.hc₁₃ r _ _ h]) (by rw [hi₃', data.i₃_next r r' _ _ h]) rfl
      (n₀ - 1) n₀ n₁ n₂ (by have := data.hc r pq pq' h; lia) (by simp) hn₁ hn₂,
      Category.assoc, Category.assoc, Iso.inv_hom_id_assoc,
      d_map_fourδ₄Toδ₃ .., comp_zero]
    rfl

Goal state after:
case neg
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq pq'
⊢ (page X data r hr).d pq pq' ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
n : N
⊢ ((↑f).inverse g h₁ h₂).toFun ⁅x, n⁆ = ⁅x, ((↑f).inverse g h₁ h₂).toFun n⁆

Tactic:
calc
        g ⁅x, n⁆ = g ⁅x, f (g n)⁆ := by rw [h₂]
        _ = g (f ⁅x, g n⁆) := by rw [map_lie]
        _ = ⁅x, g n⁆ := h₁ _

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x : M
⊢ ∃ y, (f ^ (m + n)) y = (⇑f)^[m] x

Tactic:
← f.pow_apply m,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x : M
⊢ ∃ y, (f ^ (m + n)) y = (f ^ m) x
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n ↦ (r ^ n • LinearMap.id).range) m
y : M
hy : r ^ m • y = x
⊢ (r ^ n * r ^ (m - n)) • y = x

Tactic:
← pow_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n ↦ (r ^ n • LinearMap.id).range) m
y : M
hy : r ^ m • y = x
⊢ r ^ (n + (m - n)) • y = x
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆

Tactic:
simp only [Ring.lie_def, right_distrib, left_distrib]; abel

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆

Tactic:
simp only [Ring.lie_def, right_distrib, left_distrib]; abel

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
intros
    apply SetCoe.ext
    apply lie_add

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆

Tactic:
have : e.toEquiv.toFun = e := rfl

Goal state after:
R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = ⇑e
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case add_left
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝ y✝ x y z : L
hx✝ : x ∈ span R s
hy✝ : y ∈ span R s
hz✝ : z ∈ span R s
hx : ⁅x, z⁆ ∈ span R s
hy : ⁅y, z⁆ ∈ span R s
⊢ ⁅x + y, z⁆ ∈ span R s

Tactic:
| add_left x y z _ _ _ hx hy =>

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Subsingleton ↥N → ∀ m ∈ N, m = 0

Tactic:
rintro ⟨h⟩ m hm

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
h : ∀ (a b : ↥N), a = b
m : M
hm : m ∈ N
⊢ m = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

Tactic:
rwa [(monic ⟨1, monic_one, by simp [eq_iff_true_of_subsingleton]⟩ :
           (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ ¬IsIntegral A (-x)

Tactic:
· exact IsIntegral.neg_iff.not.mpr hx

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ I
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0

Tactic:
rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : (Ideal.Quotient.mk I) (coeff n a) = 0
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ R[B.gen] = ⊤

Tactic:
by
  rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
  rintro x ⟨i, rfl⟩
  rw [B.basis_eq_pow i]
  exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n - (of (X ^ n - C a)) a = eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n - C a)

Tactic:
eval₂_sub,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n - (of (X ^ n - C a)) a =
    eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n) - eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (C a)
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) (X ^ p - C a) = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree

Tactic:
eval₂_sub,

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) (X ^ p) - eval₂ (of g) (root g) (C a) = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ #(f.aroots K).toFinset = (map (algebraMap F K) f).natDegree ↔ f.Separable

Tactic:
h.natDegree_eq_card_roots,

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ #(f.aroots K).toFinset = (map (algebraMap F K) f).roots.card ↔ f.Separable
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (of f) x = (of f) (a • x)

Tactic:
of,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • ((mk f).comp C) x = ((mk f).comp C) (a • x)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2, ∃ (h : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), a_2 ≤ p ∧ ⟨a ⊓ a_2, ⋯⟩ = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
exists_and_left,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2 ≤ p, ∃ (x : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), ⟨a ⊓ a_2, ⋯⟩ = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map (of f) I = Ideal.map (mk f) (Ideal.map C I)

Tactic:
of,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map ((mk f).comp C) I = Ideal.map (mk f) (Ideal.map C I)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsSemisimple
⊢ IsSemisimple (LinearMap.restrict f hp)

Tactic:
by
  rw [IsSemisimple] at hf ⊢
  let e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o
      Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
    (Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans <|
      Submodule.mapIic _
  exact (isSemisimpleModule_iff ..).mpr (e.complementedLattice_iff.mpr inferInstance)

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
x : L
⊢ (fun x ↦ (IsNilpotent.exp (-↑D)) x) ((IsNilpotent.exp ↑D).toFun x) = x

Tactic:
by
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply,
        ← Module.End.mul_eq_comp, h.exp_neg_mul_exp_self, Module.End.one_apply]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2.hfg
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := ⋯
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := ⋯
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := ⋯
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ ∀ i ∈ RN.sigma fun i ↦ RN,
    ((↑i.fst !)⁻¹ * (↑i.snd !)⁻¹) • (a ^ i.fst * b ^ i.snd) =
      ((↑(match i with
                  | ⟨i, j⟩ => (i, j)).1!)⁻¹ *
          (↑(match i with
                  | ⟨i, j⟩ => (i, j)).2!)⁻¹) •
        (a ^
            (match i with
              | ⟨i, j⟩ => (i, j)).1 *
          b ^
            (match i with
              | ⟨i, j⟩ => (i, j)).2)

Tactic:
simp only [implies_true]

Goal state after:
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x + ((bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) + ((bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
intro y₁

Goal state after:
case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
y₁ : A ⊗[R] L
⊢ ∀ (y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y₁ + ((bracket' R A L L) y₁) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (y₁ + y) + ((bracket' R A L L) (y₁ + y)) (a₁ ⊗ₜ[R] l₁) = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) z₂ + ((bracket' R A L L) z₂) x = 0 →
      ((bracket' R A L L) y) z₂ + ((bracket' R A L L) z₂) y = 0 →
        ((bracket' R A L L) (x + y)) z₂ + ((bracket' R A L L) z₂) (x + y) = 0

Tactic:
intro y₁

Goal state after:
case refine_3.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
y₁ : A ⊗[R] L
⊢ ∀ (y : A ⊗[R] L),
    ((bracket' R A L L) y₁) z₂ + ((bracket' R A L L) z₂) y₁ = 0 →
      ((bracket' R A L L) y) z₂ + ((bracket' R A L L) z₂) y = 0 →
        ((bracket' R A L L) (y₁ + y)) z₂ + ((bracket' R A L L) z₂) (y₁ + y) = 0
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ IsSolvable (A ⊗[R] L)

Tactic:
isSolvable_iff A

Goal state after:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ ∃ k, derivedSeries A (A ⊗[R] L) k = ⊥