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

Goal state before:
pp: 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₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasLeftResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
⊢ Φ.IsLeftDerivabilityStructure ↔ TwoSquare.GuitartExact e.inv

Tactic:
rw [isLeftDerivabilityStructure_iff_op,
    Φ.op.isRightDerivabilityStructure_iff L₁.op L₂.op F.op (NatIso.op e.symm),
    ← TwoSquare.guitartExact_op_iff e.inv]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
← hasPointwiseLeftKanExtensionAt_iff_of_equivalence W.Q L F
    (Localization.uniq W.Q L W) (Localization.compUniqFunctor W.Q L W) (W.Q.obj X) (L.obj X)
    ((Localization.compUniqFunctor W.Q L W).app X)

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
⊢ W₂
    (R.functor.preimage
      (iso.hom.app (L.functor.objPreimage ρ.X₁) ≫ B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w))

Tactic:
simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]
        refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
        exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso (L.functor.objObjPreimageIso ρ.X₁))
          (Iso.refl _)

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ φ.f k = φ'.f k

Tactic:
simp only [not_or] at h
    apply (isZero_double_X f hi₀₁ k h.1 h.2).eq_of_tgt

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''
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d i j =
        (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d i j ≫
          (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
rintro _ n rfl
    rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntLE (-1))) _
      (i' := Int.negSucc (n + 1)) (j' := Int.negSucc n) (by dsimp; lia) (by dsimp; lia),
      cochainComplex_d, d_negSucc]
    simp

Goal state after:
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬c.Rel i j
this : C.d i j = 0
⊢ (C.d i j).app t = 0

Tactic:
NatTrans.ext_iff,

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬c.Rel i j
this : (C.d i j).app = NatTrans.app 0
⊢ (C.d i j).app t = 0
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : C.d i j ≫ C.d j k = 0
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
NatTrans.ext_iff,

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : (C.d i j ≫ C.d j k).app = NatTrans.app 0
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0
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
P : Karoubi C
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ (φ.app P.X).f

Tactic:
have h := φ.naturality P.p
        have h' := F.congr_map P.idem
        simp only [hom_ext_iff, Karoubi.comp_f, F.map_comp] at h h'
        simp only [obj_obj_p, assoc, ← h]
        slice_lhs 1 3 => rw [h', h']

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
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
⊢ ((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
      { hom := { app := fun P ↦ { f := (Y.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
          inv := { app := fun P ↦ { f := (Y.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { app := fun P ↦ { f := (X.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
          inv := { app := fun P ↦ { f := (X.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (𝟭 (Karoubi C ⥤ Karoubi D)).map φ

Tactic:
by
      ext P
      dsimp
      rw [natTrans_eq φ P, P.decomp_p]
      simp only [Functor.map_comp, comp_f, assoc]
      rfl

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 G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : F.map ((toKaroubi C).map f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map ((toKaroubi C).map f.f)
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map X.decompId_i ≫ τ.app X.X ≫ G.map ((toKaroubi C).map f.f ≫ Y.decompId_p) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f

Tactic:
← h₃,

Goal state after:
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 : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : F.map ((toKaroubi C).map f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map ((toKaroubi C).map f.f)
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map X.decompId_i ≫ τ.app X.X ≫ G.map (X.decompId_p ≫ f) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case neg
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'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : ¬i = 0
⊢ IsInitial ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j ⟨(i, j'), h⟩)

Tactic:
exact mapBifunctorObjSingle₀ObjIsInitial _ _ _ _ hi

Goal state after:
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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (mk₁ f).obj' 0 homMk₁._proof_4 ⟶ (mk₁ f').obj' 0 homMk₁._proof_4

Tactic:
by exact α.app 0

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₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁ f₂ ⟶ mk₂ f₁' f₂'
n₀ n₁ n₂ : ℤ
hβ : β = homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ =
    X.cyclesMap f₁ f₂ f₁' f₂' β n₁ ≫ X.πE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂

Tactic:
by
  simp [πE, map, X.cyclesIso_inv_cyclesMap_assoc f₁ f₂ f₃ f₁' f₂' f₃' α β hβ n₀ n₁ n₂]

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
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ (b : ℕ),
    k ≤ b → IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ m, (f ^ m).range = (f ^ b).range ∧ ⨆ m, (f ^ m).ker = (f ^ b).ker
⊢ IsCompl (⨆ n, (f ^ n).ker) (⨅ n, (f ^ n).range)

Tactic:
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)

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
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ (b : ℕ),
    k ≤ b → IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ m, (f ^ m).range = (f ^ b).range ∧ ⨆ m, (f ^ m).ker = (f ^ b).ker
h₁ : IsCompl (f ^ k).ker (f ^ k).range
h₂ : ⨅ m, (f ^ m).range = (f ^ k).range
h₃ : ⨆ m, (f ^ m).ker = (f ^ k).ker
⊢ IsCompl (⨆ n, (f ^ n).ker) (⨅ n, (f ^ n).range)
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
⊢ ∀ (x : A), ⁅x, x⁆ = 0

Tactic:
simp only [Ring.lie_def, forall_const, sub_self]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + -⁅L (a * a), L b⁆ + -⁅L (b * b), L a⁆ = 0

Tactic:
lie_skew,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + ⁅L b, L (a * a)⁆ + -⁅L (b * b), L a⁆ = 0
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + ⁅L b, L (a * a)⁆ + -⁅L (b * b), L a⁆ = 0

Tactic:
lie_skew,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
intro h'

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
⊢ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s✝ s : Set L
x x✝ y✝ : L
hx✝ : x✝ ∈ lieSpan R L (-s)
hy✝ : y✝ ∈ lieSpan R L (-s)
hu : x✝ ∈ lieSpan R L s
hv : y✝ ∈ lieSpan R L s
⊢ x✝ + y✝ ∈ lieSpan R L s

Tactic:
| add _ _ _ _ hu hv =>

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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⨅ i, ↑(p i)

Tactic:
iInf,

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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(sInf (range fun i ↦ p i)) = ⨅ i, ↑(p 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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
iInf,

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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(sInf (range fun i ↦ p i)) = ⋂ i, ↑(p i)
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
by
  suffices ∀ I J : LieIdeal R L, ⁅I, J⁆ ≤ ⁅J, I⁆ by exact le_antisymm (this I J) (this J I)
  clear! I J; intro I J
  rw [lieIdeal_oper_eq_span, lieSpan_le]; rintro x ⟨y, z, h⟩; rw [← h]
  rw [← lie_skew, ← lie_neg, ← LieSubmodule.coe_neg]
  apply lie_coe_mem_lie

Goal state after:
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
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
⊢ IsMulCommutative A ↔ IsLieAbelian A

Tactic:
by
  have : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨(·.trivial), (⟨·⟩)⟩
  simp [this, isMulCommutative_iff, LieRing.of_associative_ring_bracket, sub_eq_zero]

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ⨆ a ∈ s, a = ⨆ i, ↑i

Tactic:
iSup_subtype

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ⨆ a ∈ s, a = ⨆ i, ⨆ (h : i ∈ s), ↑⟨i, h⟩
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ p.degree

Tactic:
simp only [degree_zero, bot_le]

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
⊢ RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x

Tactic:
ext p
  simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]

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
h : Function.Surjective ⇑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆

Tactic:
rw [← LieSubmodule.toSubmodule_le_toSubmodule, coe_map_of_surjective h,
    LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LinearMap.map_span]

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
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x})
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
⊢ ∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩ = ∑ i ∈ p.support, p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩

Tactic:
congr with i

Goal state after:
case e_f
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
i : ℕ
⊢ ↑⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩ = ↑(p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩)
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (a * a)),

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (a * a)),

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ a ∈ I, ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
intro a ha

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ((Quotient.mk (map C I)).comp C) a = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ f ∈ map C I, (eval₂RingHom (C.comp (Quotient.mk I)) X) f = 0

Tactic:
intro a ha

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) a = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg.e_a
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
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (pb.basis ⟨i, hi⟩) = y ^ ↑⟨i, hi⟩

Tactic:
Basis.constr_basis

Goal state after:
case neg.e_a
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
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ y ^ ↑⟨i, hi⟩ = y ^ ↑⟨i, hi⟩
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) (p * X i))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p * X i)

Tactic:
simp only [coe_eval₂Hom, Ideal.Quotient.lift_mk,
      eval₂_mul, map_mul, eval₂_X] at hp ⊢

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (C.comp (Ideal.Quotient.mk I)) X p) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
        (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (C.comp (Ideal.Quotient.mk I)) X p) *
      (Ideal.Quotient.mk (Ideal.map C I)) (X i) =
    (Ideal.Quotient.mk (Ideal.map C I)) p * (Ideal.Quotient.mk (Ideal.map C I)) (X i)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ IsUnit q

Tactic:
apply isUnit_of_self_mul_dvd_separable hsep

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p