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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
⊢ ι f n₀ ≫ π f n₀ = f

Tactic:
simp [π]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
        Q.map (CochainComplex.mappingCone.descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) ≫
          triangleOfSESδ ⋯ ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
descShortComplex_triangleOfSESδ_assoc

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
        Q.map (CochainComplex.mappingCone.triangle (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).f).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).X₁ ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
X✝ Y✝ : CochainComplex.Plus C
f✝ : X✝ ⟶ Y✝
⊢ (quasiIso C).inverseImage (R C).functor f✝ ↔ CochainComplex.Plus.quasiIso C f✝

Tactic:
apply quotient_map_mem_quasiIso_iff

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f ≫ g) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K))

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d n (n + 1) =
    (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).d n (n + 1) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom

Tactic:
restriction_d_eq (e := (ComplexShape.embeddingUpIntGE 0)) _ (i' := n)
      (j' := (n + 1 : ℕ)) (by simp) (by simp),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d n (n + 1) =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫
        h.cochainComplex.d ↑n ↑(n + 1) ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (φ.app x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (φ.app x✝.X).f

Tactic:
slice_rhs 1 2 => rw [h'']

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : δ n (n + 1) ↑((n + 1).negOnePow • α) = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
coe_units_smul,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : δ n (n + 1) ((n + 1).negOnePow • ↑α) = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0

Tactic:
← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),

Goal state after:
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₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩)

Tactic:
rintro ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ h

Goal state after:
I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n fst✝¹ snd✝¹ : ℕ
property✝¹ : (fst✝¹, snd✝¹) ∈ (fun i ↦ i.1 + i.2) ⁻¹' {n}
fst✝ snd✝ : ℕ
property✝ : (fst✝, snd✝) ∈ (fun i ↦ i.1 + i.2) ⁻¹' {n}
h :
  (fun x ↦
        match x with
        | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩))
      ⟨(fst✝¹, snd✝¹), property✝¹⟩ =
    (fun x ↦
        match x with
        | ⟨(i₁, i₂), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩))
      ⟨(fst✝, snd✝), property✝⟩
⊢ ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁

Tactic:
← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,

Goal state after:
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₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (𝟙 (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
Module: Mathlib.Order.Fin.Clamp

Goal state before:
pp: m a b : ℕ
h : a ≤ b
⊢ (fun n ↦ clamp n m) a ≤ (fun n ↦ clamp n m) b

Tactic:
le_iff_val_le_val

Goal state after:
m a b : ℕ
h : a ≤ b
⊢ ↑((fun n ↦ clamp n m) a) ≤ ↑((fun n ↦ clamp n m) b)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
N : Submodule S M
c : R
x : M
hx : x ∈ N.carrier
⊢ c • x ∈ N.carrier

Tactic:
obtain ⟨r, rfl⟩ := H c

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
⊢ (algebraMap S R) r • x ∈ N.carrier
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m✝ n : M
x y : L
m : M →ₗ[R] R
⊢ { toFun := fun m_1 ↦ -m ⁅x + y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m_1 ↦ -m ⁅y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n; simp [-neg_add_rev, neg_add]

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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L₂}, x ∈ (↑f).range.carrier → y ∈ (↑f).range.carrier → ⁅x, y⁆ ∈ (↑f).range.carrier

Tactic:
by
        rintro - - ⟨x, rfl⟩ ⟨y, rfl⟩
        exact ⟨⁅x, y⁆, f.map_lie x y⟩

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
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ ↑K
⊢ m ∈ K

Tactic:
exact hK hm

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I = ⊥

Tactic:
eq_bot_iff

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: 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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, ⊥⁆ = ⊥

Tactic:
eq_bot_iff

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∀ m ∈ ⁅I, ⊥⁆, m = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: 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
⊢ N = ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
eq_bot_iff

Goal state after:
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
⊢ N ≤ ⊥ ↔ ∀ m ∈ N, m = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: L : Type u_1
M : Type u_2
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Subsingleton M
x : L
m : M
⊢ ⁅x, m⁆ = 0

Tactic:
by simp_rw [Subsingleton.eq_zero m, lie_zero]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, x = 0

Tactic:
rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ = 0
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆

Tactic:
← LieSubmodule.toSubmodule_le_toSubmodule,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ↑⁅map f I₁, map f I₂⁆ ≤ ↑(map f ⁅I₁, I₂⁆)
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD I]
⊢ ∏ i ∈ Finset.cons i s h✝, x i ≡ ∏ i ∈ Finset.cons i s h✝, y i [SMOD I]

Tactic:
Finset.prod_cons,

Goal state after:
case cons
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD I]
⊢ x i * ∏ x_1 ∈ s, x x_1 ≡ ∏ i ∈ Finset.cons i s h✝, y i [SMOD I]
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD I]
⊢ x i * ∏ x_1 ∈ s, x x_1 ≡ ∏ i ∈ Finset.cons i s h✝, y i [SMOD I]

Tactic:
Finset.prod_cons,

Goal state after:
case cons
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD I]
⊢ x i * ∏ x_1 ∈ s, x x_1 ≡ y i * ∏ x ∈ s, y x [SMOD I]
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0

Tactic:
apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
⊢ (∑ x_1, (monomial ↑x_1) (g x_1)).degree < (minpoly K x).degree

S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : ∑ x_1, (monomial ↑x_1) (g x_1) = 0
⊢ g i = 0
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: case inl
K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ False

Tactic:
refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_

Goal state after:
case inl
K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ (mk (X - C a)) (C a) = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
⊢ Squarefree x

Tactic:
by
  rintro y ⟨z, hz⟩
  rw [mul_assoc] at hz
  rcases h.isUnit_or_isUnit hz with (hu | hu)
  · exact hu
  · apply isUnit_of_mul_isUnit_left hu

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
by
  simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm

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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (∏ i ∈ cons a s ha, f i)

Tactic:
Finset.prod_cons,

Goal state after:
case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (f a * ∏ x ∈ s, f x)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ x ∈ insert a s, (f x).Separable
⊢ (∏ x ∈ insert a s, f x).Separable

Tactic:
Finset.forall_mem_insert,

Goal state after:
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    ∀ x ∈ s, (x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x_1 ∈ s, x ≠ x_1 → IsCoprime (f x) (f x_1)
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
⊢ (∏ x ∈ insert a s, f x).Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
exact absurd hn hf0

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ (annIdealGenerator 𝕜 a).Monic

Tactic:
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ (C p).degree ≤ f.degree

Tactic:
degree_C h_contra,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ 0 ≤ f.degree
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
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
⊢ f = 0

Tactic:
by
  have (p) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite R p) : f.restrict hp₁ = 0 := by
    specialize hs p hp₁ hp₂
    replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
    exact eq_zero_of_isNilpotent_isSemisimple hn hs
  ext x
  obtain ⟨k : ℕ, hk : f ^ k = 0⟩ := hn
  let p := Submodule.span R {(f ^ i) x | (i : ℕ) (_ : i ≤ k)}
  have hp₁ : p ∈ f.invtSubmodule := by
    simp only [mem_invtSubmodule, p, Submodule.span_le]
    rintro - ⟨i, hi, rfl⟩
    apply Submodule.subset_span
    rcases lt_or_eq_of_le hi with hik | rfl
    · exact ⟨i + 1, hik, by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x⟩
    · exact ⟨i, by simp [hk]⟩
  have hp₂ : Module.Finite R p := by
    let g : ℕ → M := fun i ↦ (f ^ i) x
    have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
    exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)
  simpa [LinearMap.restrict_apply, Subtype.ext_iff] using
    LinearMap.congr_fun (this p hp₁ hp₂) ⟨x, Submodule.subset_span ⟨0, k.zero_le, rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D D1✝ D2✝ : LieDerivation R L M
a b : L
D1 D2 : LieDerivation R L M
h : (fun D ↦ D.toFun) D1 = (fun D ↦ D.toFun) D2
⊢ D1 = D2

Tactic:
by cases D1; cases D2; congr; exact DFunLike.coe_injective h

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑includeRight) (1 ⊗ₜ[R] root p) (Polynomial.map (↑(ofId S (AdjoinRoot p))) p) = 0

Tactic:
change Polynomial.eval₂ _ ((RingHomClass.toRingHom includeRight) (root p)) (p.map (of _)) = _

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑includeRight) (↑includeRight (root p)) (Polynomial.map (of p) p) = 0