mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure → Φ.op.IsRightDerivabilityStructure

Tactic:
rintro ⟨_, _⟩

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
hasLeftResolutions✝ : Φ.HasLeftResolutions
guitartExact'✝ : TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).inv
⊢ Φ.op.IsRightDerivabilityStructure
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr.inl
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
this✝² : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
q : ℤ
inst✝ : K.IsStrictlyGE q
h✝ : L.IsStrictlyGE (q - 1)
this✝¹ : L.IsGE q
this✝ : QuasiIso (L.πTruncGE q)
this : Injective (opcycles L q)
⊢ Injective ((L.truncGE q).X q)

Tactic:
exact Injective.of_iso (L.truncGEXIsoOpcycles q).symm inferInstance

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
⊢ ∀ (X : DifferentialObject S C),
    { f := F.map (𝟙 X).f, comm := ⋯ } = 𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ }

Tactic:
intros

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ { f := F.map (𝟙 X✝).f, comm := ⋯ } = 𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
⊢ ∀ {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { f := F.map (f ≫ g).f, comm := ⋯ } = { f := F.map f.f, comm := ⋯ } ≫ { f := F.map g.f, comm := ⋯ }

Tactic:
intros

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { f := F.map (f✝ ≫ g✝).f, comm := ⋯ } = { f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝ : HasZeroObject C
this : (S.sc hS (k + 1) ⋯).HasHomology
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
let h := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝ : HasZeroObject C
this : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)

Tactic:
apply liftHomotopy (f ≫ g) <;> simp

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
n : ℕ
⊢ QuasiIsoAt (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩) n

Tactic:
by
    cases n
    · rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros']
      · dsimp
        refine (ShortComplex.exact_and_epi_g_iff_of_iso ?_).2
          ⟨exact_d_f (Projective.π Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
          (by simp [ofComplex]) (by simp)
      all_goals rfl
    · rw [quasiIsoAt_iff_exactAt']
      · apply ofComplex_exactAt_succ
      · apply ChainComplex.exactAt_succ_single_obj

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom =
    (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ

Tactic:
← cancel_mono (mapBifunctorLeftUnitor F X e p hp Y').inv,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ (mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom) ≫
      (mapBifunctorLeftUnitor F X e p hp Y').inv =
    ((mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ) ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: case h₁
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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ app' (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') 1 homMk₁._proof_5 =
    app' (twoδ₂Toδ₁ f g fg h ≫ β) 1 homMk₁._proof_5

Tactic:
· dsimp
    rw [hβ₁]
    exact (naturality' α 1 2).symm

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₀ i₁ : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
⊢ i₀ ≤ i₁

Tactic:
have := data.le₀₁ r pq'

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₀ i₁ : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
this : data.i₀ r pq' ⋯ ≤ data.i₁ pq'
⊢ i₀ ≤ i₁
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 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
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ IsZero ((E.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
by
    have : (coreE₂CohomologicalFin l).i₀ r' pq =
        (coreE₂CohomologicalFin l).i₀ r pq := by
      subst hrr'
      obtain ⟨k, rfl⟩ := Int.le.dest hr
      obtain ⟨p, q, hq⟩ := pq
      ext
      have h : q ≤ k := by
        by_contra!
        simp only [ComplexShape.spectralSequenceFin_rel_iff, not_and, Prod.forall] at hpq
        obtain ⟨t, rfl⟩ := Nat.le.dest (Nat.add_one_le_of_lt this)
        exact hpq _ ⟨t, by lia⟩ rfl (by simp; lia)
      simp_all
      lia
    have := isIso_homOfLE this
    apply E.isZero_H_map_mk₁_of_isIso

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.cyclesIsoH f n₀ n₁ hn₁).hom ≫ X.toCycles (𝟙 i₀) f f ⋯ n₀ = 𝟙 (X.cycles (𝟙 i₀) f n₀)

Tactic:
simpa using (X.cyclesIsoH f n₀ n₁ hn₁).hom_inv_id

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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv

Tactic:
rw [← cancel_mono (X.cyclesIso ..).hom,
      Category.assoc, Iso.inv_hom_id, Category.comp_id,
      ← cancel_mono (X.iCycles ..), Category.assoc, cyclesIso_hom_i ..,
      h.cyclesIso_inv_comp_iCycles, toCycles_i]

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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ h.i = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_5 + 1} → Submodule R P} [∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
intros

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
M✝ : PEmpty.{u_5 + 1} → Submodule R P
inst✝ : ∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)
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, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
intros

Goal state after:
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✝, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑z✝⁆, ⋯⟩
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

Goal state after:
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✝⁆, ⋯⟩
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 : ↥L'), ⟨⁅↑x, ↑x⁆, ⋯⟩ = 0

Tactic:
intros

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : ↥L'
⊢ ⟨⁅↑x✝, ↑x✝⁆, ⋯⟩ = 0
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⁆, ⋯⟩, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑⟨⁅↑x, ↑z⁆, ⋯⟩⁆, ⋯⟩

Tactic:
intros

Goal state after:
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✝⁆, ⋯⟩, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑⟨⁅↑x✝, ↑z✝⁆, ⋯⟩⁆, ⋯⟩
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
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
intros

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : ↥L'
⊢ ⁅x✝, t✝ • y✝⁆ = t✝ • ⁅x✝, y✝⁆
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)
⊢ ∀ (K K' : LieSubalgebra R L), ↑K ⊆ ↑K' ↔ K ≤ K'

Tactic:
intros

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
K✝ K'✝ : LieSubalgebra R L
⊢ ↑K✝ ⊆ ↑K'✝ ↔ K✝ ≤ K'✝
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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
⊢ (lieSpan R L s).toSubmodule = span R s

Tactic:
by
  suffices ∀ {x y}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s by
    refine le_antisymm ?_ submodule_span_le_lieSpan
    change _ ≤ ({ span R s with lie_mem' := this } : LieSubalgebra R L)
    rw [lieSpan_le]
    exact subset_span
  intro x y hx hy
  induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]

Goal state after:
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
x y : LieSubmodule R L M
h : ↑x = ↑y
⊢ x = y

Tactic:
cases x; cases y; congr

Goal state after:
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 N' : LieSubmodule R L M
⊢ Disjoint ↑N ↑N' ↔ Disjoint N N'

Tactic:
disjoint_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 N' : LieSubmodule R L M
⊢ ↑N ⊓ ↑N' = ⊥ ↔ Disjoint N N'
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 N' : LieSubmodule R L M
⊢ ↑N ⊓ ↑N' = ⊥ ↔ Disjoint N N'

Tactic:
disjoint_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 N' : LieSubmodule R L M
⊢ ↑N ⊓ ↑N' = ⊥ ↔ N ⊓ N' = ⊥
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ comap I.incl I₂ = ⊥ ↔ Disjoint I I₂

Tactic:
disjoint_iff,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ comap I.incl I₂ = ⊥ ↔ I ⊓ I₂ = ⊥
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
s : Set M
⊢ Submodule.span R s ≤ ↑(lieSpan R L s)

Tactic:
by
  rw [Submodule.span_le]
  apply subset_lieSpan

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

Goal state before:
pp: case refine_1
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
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ ⁅⊤, N⁆ = ⊥

pp: case refine_2
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
N : LieSubmodule R L M
h : ⁅⊤, N⁆ = ⊥
m : M
hm : m ∈ N
⊢ m ∈ maxTrivSubmodule R L M

Tactic:
· rw [← le_bot_iff, ← ideal_oper_maxTrivSubmodule_eq_bot R L M ⊤]
    exact LieSubmodule.mono_lie_right ⊤ h

Goal state after:
case refine_2
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
N : LieSubmodule R L M
h : ⁅⊤, N⁆ = ⊥
m : M
hm : m ∈ N
⊢ m ∈ maxTrivSubmodule R L M
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
⊢ root (X ^ Nat.succ 0 - C a) ≠ 0

Tactic:
rw [pow_one]
    intro e
    refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
    trans AdjoinRoot.mk (X - C a) (X - (X - C a))
    · rw [sub_sub_cancel]
    · rw [map_sub, mk_self, sub_zero, mk_X, e]

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

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
← normalize_normalized_factor _ hmem

Goal state after:
case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ ¬f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]

Goal state after:
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 = C (f.coeff 0)
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
rw [h1, C_0] at hn

Goal state after:
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
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
n : ℕ
⊢ (⇑(frobeniusEquiv R p).symm)^[n] x ^ p ^ n = x

Tactic:
induction n generalizing x with

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots).toFinset = f.roots.toFinset

Tactic:
roots_expand_pow_map_iterateFrobenius,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (p ^ n • f.roots).toFinset = f.roots.toFinset
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : 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 : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ Ideal.span {p} = ⊥

Tactic:
Ideal.span_singleton_eq_bot.mpr

Goal state after:
case pos
𝕜 : 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 : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ ⊥ = ⊥

case pos
𝕜 : 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 : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ p = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommSemiring S
inst✝² : Semiring T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
f g : AdjoinRoot p →ₐ[S] T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : f (root p) = g (root p)
⊢ f = g

Tactic:
apply AlgHom.coe_ringHom_injective; exact ringHom_ext congr(($hAlg).toRingHom) hRoot

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit ((toMatrix v v') ↑f).det

Tactic:
apply isUnit_det_of_left_inverse
  simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

Goal state after: