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

Goal state before:
pp: case hP₀
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))

Tactic:
convert! hP₀

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
⊢ (structuredArrowEquiv W W.Q L) (StructuredArrow.mk (𝟙 (W.Q.obj X))) = StructuredArrow.mk (𝟙 (L.obj X))
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
inst✝ : F.HasPointwiseRightDerivedFunctorAt W X
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
rwa [← hasPointwiseRightDerivedFunctorAt_iff F L W]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
e : W₂.Q.obj (Φ.functor.obj X) ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).app X
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor.obj X))

Tactic:
(Φ.functor ⋙ F).hasPointwiseRightDerivedFunctorAt_iff W₁.Q W₁ X,

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
X : C₁
e : W₂.Q.obj (Φ.functor.obj X) ≅ (Φ.localizedFunctor W₁.Q W₂.Q).obj (W₁.Q.obj X) :=
  (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).app X
⊢ W₁.Q.HasPointwiseLeftKanExtensionAt (Φ.functor ⋙ F) (W₁.Q.obj X) ↔
    W₂.Q.HasPointwiseLeftKanExtensionAt F (W₂.Q.obj (Φ.functor.obj 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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (quotient C ⋙ L).IsLocalization (CochainComplex.Plus.quasiIso C)

Tactic:
by
  refine Functor.IsLocalization.comp _ _
    ((homotopyEquivalences C (.up ℤ)).inverseImage (CochainComplex.Plus.ι C))
    (quasiIso C) _ ?_ ?_ ?_
  · intro _ _ f hf
    refine Localization.inverts L (quasiIso C) _ ?_
    simpa [quasiIso, quotient_map_mem_quasiIso_iff]
  · intro K L f hf
    exact homotopyEquivalences_le_quasiIso _ _ _ hf
  · rintro K L f hf
    obtain ⟨K, rfl⟩ := Plus.quotient_obj_surjective K
    obtain ⟨L, rfl⟩ := Plus.quotient_obj_surjective L
    obtain ⟨f, rfl⟩ := (Plus.quotient C).map_surjective f
    apply MorphismProperty.map_mem_map
    simpa [quasiIso, quotient_map_mem_quasiIso_iff] using! hf

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

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ K.IsStrictlySupportedOutside e → IsZero (K.stupidTrunc e)

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ IsZero (K.stupidTrunc e)
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
        (projectiveResolution X).fromLeftDerivedZero' F =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F

Tactic:
have h₁ := ProjectiveResolution.fromLeftDerivedZero'_naturality
    (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F ≫ F.map (𝟙 X)
⊢ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
        (projectiveResolution X).fromLeftDerivedZero' F =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ (∃ i, True ∧ ∀ y ∈ Ici i, f y = f i) ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i

Tactic:
by
    simp only [true_and, mem_Ici]

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
Module: Mathlib.RingTheory.Jacobson.Semiprimary

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝¹ : RingHomSurjective τ₁₂
inst✝ : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f ⊥ ≤ Submodule.comap f ⊥

Tactic:
le_rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
n : ℕ
⊢ f.range ≠ ⊤

Tactic:
rwa [Ne, LinearMap.range_eq_top]

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

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq

Tactic:
rw [hi₃', data.i₃_next r r' _ _ h]

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

Goal state before:
pp: 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₃
x y : L₁ →ₗ⁅R⁆ L₂
h : (fun f ↦ (↑f).toFun) x = (fun f ↦ (↑f).toFun) y
⊢ x = y

Tactic:
cases x

Goal state after:
case 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₃
y : L₁ →ₗ⁅R⁆ L₂
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) y
⊢ { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = y
Module: Mathlib.Algebra.Lie.Basic

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

Tactic:
cases x

Goal state after:
case 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
y : M →ₗ⁅R,L⁆ N
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) y
⊢ { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = y
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq

Tactic:
rw [hi₃', data.i₃_next r r' _ _ h]

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

Goal state before:
pp: case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ (φ x ^ (n + 1)) ⁅y, z⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ (ij.2 + 1)) z⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅((ad R L) x ^ (ij.1 + 1)) y, (φ x ^ ij.2) z⁆

Tactic:
simp only [pow_succ', Module.End.mul_apply, ih, map_sum, map_nsmul,
      toEnd_lie, nsmul_add, sum_add_distrib]

Goal state after:
case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆ +
      ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x ^ x_1.1) y, (φ x) ((φ x ^ x_1.2) z)⁆ =
    ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x ^ x_1.1) y, (φ x) ((φ x ^ x_1.2) z)⁆ +
      ∑ x_1 ∈ antidiagonal n, n.choose x_1.2 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p

Tactic:
intro h

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ ∀ x_1 ∈ antidiagonal n,
    n.choose x_1.1 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆ =
      n.choose x_1.2 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆

Tactic:
rintro ⟨i, j⟩ hij

Goal state after:
case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).1 • ⁅((ad R L) x) (((ad R L) x ^ (i, j).1) y), (φ x ^ (i, j).2) z⁆ =
    n.choose (i, j).2 • ⁅((ad R L) x) (((ad R L) x ^ (i, j).1) y), (φ x ^ (i, j).2) 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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ 0 ∈ N

Tactic:
exact N.zero_mem'

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

Goal state before:
pp: case mpr
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 : ↥K'
⊢ ↑x ∈ K → ∃ y, ⟨↑y, ⋯⟩ = x

Tactic:
intro h

Goal state after:
case mpr
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 : ↥K'
h : ↑x ∈ K
⊢ ∃ y, ⟨↑y, ⋯⟩ = x
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
intro h

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → (lieSpan R L ↑p).toSubmodule = p

Tactic:
intro h

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑p).toSubmodule = p
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

Goal state after:
case mk
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
y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
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'
⊢ (∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆) → ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z

Tactic:
intro h

Goal state after:
case mp
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'
h : ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆
⊢ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
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'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z) → ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆

Tactic:
intro h

Goal state after:
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
⊢ ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
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
⊢ I ≤ f.ker → ∀ x ∈ I, f x = 0

Tactic:
intro h

Goal state after:
case mp
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 : I ≤ f.ker
⊢ ∀ x ∈ I, f x = 0
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
⊢ (∀ x ∈ I, f x = 0) → I ≤ f.ker

Tactic:
intro h

Goal state after:
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
⊢ I ≤ f.ker
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p

Tactic:
intro h

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p
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 : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
  refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
  rintro h _ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩
  exact h x hx m hm

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

Goal state before:
pp: case mp
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
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
intro h

Goal state after:
case mp
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
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
⊢ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ↑(lieSpan R L ↑p) = p

Tactic:
intro h

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ↑(lieSpan R L ↑p) = p
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.smul
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⁅⟨u, hx✝⟩, ⟨y, hy⟩⁆ = 0
⊢ ⁅⟨t • u, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
      simp [Subtype.ext_iff, hu]

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

Goal state before:
pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : I ≤ LieModule.ker R L ↥I
x✝¹ x✝ : ↥I
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ⁅⟨x, hx⟩, ⟨y, hy⟩⁆ = 0

Tactic:
· simpa using LinearMap.congr_fun (h hx) ⟨y, hy⟩

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

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
c : R
x : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
y : L
⊢ ⁅y, c • x⁆ = 0

Tactic:
by rw [lie_smul, hx, smul_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
⊢ ↑(sSup s) = ↑(⨆ i, ↑i)

Tactic:
SetLike.coe_set_eq,

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
⊢ sSup s = ⨆ i, ↑i