mathlib-initiative/mathlib-tactics huggingface dataset:
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
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F ≫ F.map (𝟙 X)
h₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution 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

Tactic:
simp only [Functor.map_id, comp_id] at h₁

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₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution X))
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F
⊢ (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.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯) = 0

Tactic:
zero₁ ..,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.iCycles f₂ f₃ n₀ ≫ 0 = 0
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
E : SpectralObject C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq pq'
n : ℤ
hn : n = coreE₂Cohomological.deg pq + 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ False

Tactic:
exact hpq _ rfl

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₃
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp at x₂ hx₂
  obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    (X.kernelSequenceE_exact f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂).exact_up_to_refinements
      (x₂ ≫ X.iCycles f₁ f₂₃ n₁) (by cat_disch)
  exact ⟨A₁, π₁, inferInstance, x₁, by simpa [← cancel_mono (X.iCycles ..)]⟩

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₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
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₂
⊢ (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).right.homologyIso =
    (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso

Tactic:
ext1

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 ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
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₂
⊢ (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
            n₀ n₁ n₂ hn₁' ⋯ ⋯).right.homologyIso.hom =
    (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
            n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso.hom
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆

Tactic:
by simp only [Ring.lie_def, right_distrib, left_distrib]; abel

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆

Tactic:
by simp only [Ring.lie_def, right_distrib, left_distrib]; abel

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'
h : ↑x ∈ K
⊢ ∃ y, ⟨↑y, ⋯⟩ = x

Tactic:
use ⟨(x : L), h⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ ⁅x, y⁆ ∈ A'

Tactic:
LieRing.of_associative_ring_bracket

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ x * y - y * x ∈ A'
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ∃ N, ↑N = Submodule.map ↑f ↑I
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_4
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
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R s, ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, a • x⁆ ∈ Submodule.span R s

Tactic:
· intro t m'' _ hm''; rw [lie_smul]; exact Submodule.smul_mem _ t hm''

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f (I ⊔ f.ker) ≤ map f I

Tactic:
apply LieSubmodule.lieSpan_mono

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ ↑(Submodule.map (↑f) (toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule) ⊆
    ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
Module: Mathlib.Algebra.Lie.IdealOperations

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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
m : M
⊢ (∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m) → ∃ x n, ⁅↑x, ↑n⁆ = m

Tactic:
rintro ⟨x, hx, n, hn, rfl⟩
    exact ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

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

Goal state before:
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:
mem_maxTrivSubmodule

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
⊢ ∀ (x : L), ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ ∈ ⁅I, N⁆

pp: case h.right
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ∃ z ∈ ⁅I, N'⁆, ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + z = m

Tactic:
· apply lie_coe_mem_lie

Goal state after:
case h.right
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ∃ z ∈ ⁅I, N'⁆, ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + z = m
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₂, hn₂⟩⁆ ∈ ⁅I, N'⁆

pp: case h.right
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + ⁅↑x, ↑⟨n₂, hn₂⟩⁆ = m

Tactic:
· apply lie_coe_mem_lie

Goal state after:
case h.right
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
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + ⁅↑x, ↑⟨n₂, hn₂⟩⁆ = m
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective ⇑f
⊢ ∀ {x : L} {m : ↥N},
    (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⁅x, m⁆ =
      ⁅x, (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun m⁆

Tactic:
rintro x ⟨m, hm : m ∈ N⟩; ext; exact f.map_lie x m

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

Goal state before:
pp: case h.left
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆

pp: case h.right
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m

Tactic:
· apply lie_coe_mem_lie

Goal state after:
case h.right
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆

pp: case h.right
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m

Tactic:
· apply lie_coe_mem_lie

Goal state after:
case h.right
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 J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m
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 a b : ↥R[x]
hb✝ : b ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
p : R[X]
hp : (aeval x) p = ↑a
⊢ (aeval x) (p * b') = ↑(a • b)

Tactic:
by simp [hp, hb']

Goal state after:
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
⊢ y = ∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩

Tactic:
ext1

Goal state after:
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
⊢ ↑y = ↑(∑ i ∈ p.support, ⟨(aeval x) (C (p.coeff i) * X ^ i), ⋯⟩)
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]

Tactic:
by
  rcases subsingleton_or_nontrivial B
  · exact ⟨0, by rw [SModEq, Subsingleton.eq_zero b, map_zero]⟩
  refine ⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩
  have H := pb.basis.sum_repr b
  rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (notMem_erase _ _)] at H
  rw [SModEq, ← add_zero (algebraMap _ _ _), Quotient.mk_add]
  nth_rewrite 1 [← H]
  rw [Quotient.mk_add]
  congr 1
  · simp [Algebra.algebraMap_eq_smul_one ((pb.basis.repr b) _)]
  · rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]
    refine sum_mem _ (fun i hi ↦ ?_)
    rw [Algebra.smul_def']
    refine Ideal.mul_mem_left _ _ <| Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ <|
      Nat.pos_of_ne_zero <| fun h ↦ notMem_erase i univ <| Fin.eq_mk_iff_val_eq.2 h ▸ hi

Goal state after:
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
⊢ pb.minpolyGen.Monic

Tactic:
by
  nontriviality A
  apply (monic_X_pow _).sub_of_left _
  rw [degree_X_pow]
  exact degree_sum_fin_lt _

Goal state after:
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
B : PowerBasis R S
⊢ R[B.gen] = ⊤

Tactic:
rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ Set.range ⇑B.basis ⊆ ↑(Subalgebra.toSubmodule R[B.gen])
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r

Tactic:
simp only [hr, not_true, false_or, and_false]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ^ 2 = a * b

Tactic:
by rw [sq, eq]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a : R
⊢ (X + C a).Separable

Tactic:
rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]
  exact isCoprime_one_right

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
⊢ ⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1)

Tactic:
ext
  rw [LinearMap.det_def]
  split_ifs
  · congr -- use the correct `DecidableEq` instance
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H

Goal state after:
case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis (↥s) A M)
this : finrank A M = 0
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
classical
      have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix b (b.map e)) ↑e * (toMatrix (b.map e) b) ↑e.symm = 1

Tactic:
← toMatrix_comp,

Goal state after:
case pos.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) (b.map e)) (↑e ∘ₗ ↑e.symm) = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) b) ↑e.symm * (toMatrix b (b.map e)) ↑e = 1

Tactic:
← toMatrix_comp,

Goal state after:
case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix b b) (↑e.symm ∘ₗ ↑e) = 1