mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
g : Y ⟶ X
hg : mk (f ≫ g) = mk (𝟙 X)
⊢ mk (f ≫ g ≫ f) = mk f

Tactic:
mk_eq_mk_iff,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
g : Y ⟶ X
hg : RightHomotopyRel (f ≫ g) (𝟙 X)
⊢ RightHomotopyRel (f ≫ g ≫ f) f
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝¹ x✝ : FibrantObject C
f : x✝¹ ⟶ x✝
⊢ f ≫ { hom := iResolutionObj (ι.obj x✝) } = { hom := iResolutionObj (ι.obj x✝¹) } ≫ homMk (resolutionMap (ι.map f))

Tactic:
by
    ext : 1
    exact (HoCat.resolutionMap_fac f.hom).symm

Goal state after:
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
⊢ (quotient (InjectiveObject C)).IsLocalization
    ((CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus)

Tactic:
rw [inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectι]
  infer_instance

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

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : K.IsKProjective
this : HasDerivedCategory C := ⋯
e_2✝ :
  ((HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
      (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    (Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶
      Qh.obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
          ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
⊢ ⇑(((quotientCompQhIso C).symm.app K).homCongr
          ((Functor.commShiftIso Q n).symm.app L ≪≫
            (quotientCompQhIso C).symm.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))) ∘
      ⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) ∘ toSmallShiftedHom =
    Qh.map ∘ ⇑toHom

Tactic:
ext x

Goal state after:
case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : K.IsKProjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
e_2✝ :
  ((HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
      (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    (Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶
      Qh.obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
          ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
x : CohomologyClass K L n
⊢ (⇑(((quotientCompQhIso C).symm.app K).homCongr
            ((Functor.commShiftIso Q n).symm.app L ≪≫
              (quotientCompQhIso C).symm.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))) ∘
        ⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) ∘ toSmallShiftedHom)
      x =
    (Qh.map ∘ ⇑toHom) x
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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
⊢ mapExactFunctor F = ⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀

Tactic:
ext x

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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
x : Ext X Y 0
⊢ mapExactFunctor F x = (⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀) x
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : X✝ ⟶ Y✝
⊢ { f := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.f, ⋯⟩, comm := ⋯ } = x✝

Tactic:
ext; simp [ConcreteCategory.ofHom_hom]

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

Goal state before:
pp: case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
hmp : -1 + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = -1
⊢ h.d (Int.negSucc (0 + 1)) (-1) ≫ h.d (-1) p = 0

Tactic:
obtain rfl : p = 0 := by lia

Goal state after:
case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
hnm : Int.negSucc (0 + 1) + 1 = -1
hmp : -1 + 1 = 0
⊢ h.d (Int.negSucc (0 + 1)) (-1) ≫ h.d (-1) 0 = 0
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 ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
X' : C
g : X ⟶ X'
⊢ (toSingleEquiv h) (toSingleMk (f ≫ g) h) =
    (toSingleEquiv h) ((toSingleMk f h).comp (ofHom ((singleFunctor C q).map g)) ⋯)

Tactic:
simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]

Goal state after:
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 : C ⥤ Karoubi D
⊢ FunctorExtension₁.map (𝟙 F) = 𝟙 (FunctorExtension₁.obj F)

Tactic:
ext P
    exact comp_p (F.map P.p)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ (Iso.refl
          { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
              g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.X₁).hom ≫
      { X₁ := syzygies (Projective.π Z), X₂ := over Z, X₃ := Z, f := d (Projective.π Z), g := Projective.π Z,
          zero := ⋯ }.f =
    { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
          g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.f ≫
      (Iso.refl
          { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
              g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.X₂).hom

Tactic:
by simp [ofComplex]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ (a • φ₁).τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + (a • φ₂).τ₃

Tactic:
by
    dsimp
    rw [h.comm₃]
    simp only [smul_add, Linear.smul_comp]

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

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₃
⊢ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
      X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
by
  simp [← cancel_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂), ← cancel_epi (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁),
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl f₃₄ h₃₄ n₀ n₁ n₂ n₃,
    X.πE_map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) (𝟙 _) n₁ n₂ n₃]

Goal state after:
Module: Mathlib.Order.WithBotTop

Goal state before:
pp: ι : Type u_1
⊢ Function.Injective coe

Tactic:
rintro _ _ ⟨⟩; rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₀ (r + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ r pq ⋯

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hr

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
pq : ℤ × Fin l
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
k : ℕ
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (2 + ↑k, 1 - (2 + ↑k))).Rel pq pq'
hr : 2 ≤ 2 + ↑k
⊢ (coreE₂CohomologicalFin l).i₀ (2 + ↑k + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ (2 + ↑k) pq ⋯
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h :
  (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } =
    (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }

Tactic:
simp at h

Goal state after:
case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h : toLinearMap✝¹ = toLinearMap✝
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
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
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
h :
  (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } =
    (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }

Tactic:
simp at h

Goal state after:
case mk.mk
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
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
h : toLinearMap✝¹ = toLinearMap✝
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
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 (LieSubalgebra R L)
⊢ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p = ⋂ s ∈ S, ↑s

Tactic:
ext x

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p ↔ x ∈ ⋂ s ∈ S, ↑s
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
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
⊢ comap K.incl (lieSpan R L (range (Subtype.val ∘ f))) = lieSpan R (↥K) (range f)

Tactic:
by
  apply le_antisymm
  · intro ⟨x, hx⟩ hx'
    simp only [mem_comap, coe_incl] at hx'
    suffices x ∈ (lieSpan R K (range f)).map K.incl by aesop
    clear hx
    induction hx' using lieSpan_induction with
    | mem u hu =>
      have (i : ι) : f i ∈ lieSpan R K (range f) := subset_lieSpan <| mem_range_self i
      aesop
    | zero => exact zero_mem _
    | add u v _ _ hu hv => revert hu hv; exact add_mem
    | smul t u _ hu => revert hu; exact LieSubalgebra.smul_mem _ _
    | lie u v _ _ hu hv => revert hu hv; exact lie_mem _
  · rw [lieSpan_le]
    rintro - ⟨i, rfl⟩
    simp only [SetLike.mem_coe, mem_comap, coe_incl]
    exact subset_lieSpan <| by simp

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

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
⊢ L₁'.toSubmodule = L₁''.toSubmodule

Tactic:
ext x

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
x : L₁
⊢ x ∈ L₁'.toSubmodule ↔ x ∈ L₁''.toSubmodule
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
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 : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ f x = 0

Tactic:
apply h x hx

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

Goal state before:
pp: case a
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ↑⁅I, N⁆

Tactic:
· rw [lieIdeal_oper_eq_span]; apply submodule_span_le_lieSpan

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

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ minpoly A (f x) = minpoly A x

Tactic:
by
  classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : (Polynomial.aeval x) p = 0
⊢ (Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0

Tactic:
simp [hp]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (Polynomial.aeval x) (minpoly A x - p) = 0

Tactic:
simp [hp]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range

Tactic:
rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one]
  exact degree_eq_one_iff

Goal state after:
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
⊢ map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆

Tactic:
rw [map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
  intro x hx
  obtain ⟨⟨y₁, hy₁⟩, ⟨y₂, hy₂⟩, hx⟩ := hx
  rw [← hx]
  let fy₁ : ↥(map f I₁) := ⟨f y₁, mem_map hy₁⟩
  let fy₂ : ↥(map f I₂) := ⟨f y₂, mem_map hy₂⟩
  change _ ∈ comap f ⁅map f I₁, map f I₂⁆
  simp only [mem_comap, LieHom.map_lie]
  exact LieSubmodule.lie_coe_mem_lie fy₁ fy₂

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

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p q : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
hga : (Polynomial.aeval b) q = 0
⊢ p ∣ p * C p.leadingCoeff⁻¹

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : ∑ i ∈ Finset.range (orderOf σ), q.coeff i • σ.toLinearMap ^ i = 0
H : q.natDegree < orderOf σ
⊢ False

Tactic:
← Fin.sum_univ_eq_sum_range

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : ∑ i, q.coeff ↑i • σ.toLinearMap ^ ↑i = 0
H : q.natDegree < orderOf σ
⊢ False
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
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
x : S
⊢ f x = g x
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ p = 0

Tactic:
rw [p.as_sum_range' _ hlt, Finset.sum_range]

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ ∑ i, (monomial ↑i) (p.coeff ↑i) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ f.coeff n ∈ comap C I

Tactic:
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ((Quotient.mk I).comp C) (f.coeff n) = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < pb.dim

Tactic:
rw [← pb.natDegree_minpoly]

Goal state after:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < (minpoly A pb.gen).natDegree
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ (pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) = AlgHom.id A S'

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
x : S'
⊢ ((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) x = (AlgHom.id A S') x
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ (pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) = AlgHom.id A S

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
x : S
⊢ ((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂)) x = (AlgHom.id A S) x