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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((NatTrans.leftDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq α P,

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
          (P.isoLeftDerivedToHomotopyCategoryObj G).inv) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv
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
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (F.leftDerived 0).map f ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        (ChainComplex.isoHomologyι₀
              ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as)).hom ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    ((HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
        (ChainComplex.isoHomologyι₀
              ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as)).hom ≫
          (projectiveResolution X).fromLeftDerivedZero' F) ≫
      F.map f

Tactic:
dsimp [leftDerived]

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
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).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) ≫
      F.map f
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ (GradedObject.Monoidal.leftUnitor K.X).inv i ≫ GradedObject.Monoidal.tensorHom (tensorUnitIso C c).hom (𝟙 K.X) i =
    (λ_ (K.X i)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ (tensorUnit C c).ιTensorObj K 0 i i ⋯

Tactic:
GradedObject.Monoidal.leftUnitor_inv_apply,

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ ((λ_ (K.X i)).inv ≫
        GradedObject.Monoidal.tensorUnit₀.inv ▷ K.X i ≫
          GradedObject.Monoidal.ιTensorObj GradedObject.Monoidal.tensorUnit K.X 0 i i ⋯) ≫
      GradedObject.Monoidal.tensorHom (tensorUnitIso C c).hom (𝟙 K.X) i =
    (λ_ (K.X i)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ (tensorUnit C c).ιTensorObj K 0 i i ⋯
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.δ f₁ f₂ n₀ n₁ (CategoryTheory.Abelian.SpectralObject.d._proof_1 n₀ n₁ hn₁) ≫ X.pOpcycles f₁ f₂ n₁ = 0

Tactic:
δ_pOpcycles ..

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₁
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₂.IsPushout

Tactic:
refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
  all_goals simp

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₃
f : L₂ →ₗ⁅R⁆ L₃
g : L₁ →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L₁}, (↑f ∘ₗ ↑g).toFun ⁅x, y⁆ = ⁅(↑f ∘ₗ ↑g).toFun x, (↑f ∘ₗ ↑g).toFun y⁆

Tactic:
by
      simp

Goal state after:
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
f : N →ₗ⁅R,L⁆ P
g : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M}, (↑f ∘ₗ ↑g).toFun ⁅x, m⁆ = ⁅x, (↑f ∘ₗ ↑g).toFun m⁆

Tactic:
by
      simp

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

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
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
⊢ x = 0

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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy : (toEnd R L M) x = (toEnd R L M) y
⊢ x = y

Tactic:
· replace hx : toEnd R L M x = 0 := by ext m; simpa using hx m
    simpa using hx

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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy : (toEnd R L M) x = (toEnd R L M) y
⊢ x = y
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * a = a * (b * a)

Tactic:
mul_assoc

Goal state after:
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * (b * a) = a * (b * a)
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * (a * (a * b)) = a * (a * a * b)

Tactic:
mul_assoc

Goal state after:
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * (a * (a * b)) = a * (a * (a * b))
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
mul_assoc

Goal state after:
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * (b * (a * a)) = a * (b * (a * a))
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
    use ⟨(x : L), h⟩

Goal state after:
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
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K

Tactic:
by
  constructor
  · exact Set.Subset.trans subset_lieSpan
  · intro hs m hm
    rw [mem_lieSpan] at hm
    exact hm _ hs

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

Goal state before:
pp: case a
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
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I ≤ J

pp: case a
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
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ J ≤ map f I

Tactic:
· rw [map, LieSubmodule.lieSpan_le, Submodule.map_coe]
    /- I'm uncertain how to best resolve this `erw`.
    ```
    have : (↑(toLieSubalgebra R L I).toSubmodule : Set L) = I := rfl
    rw [this]
    simp [h]
    ```
    works, but still feels awkward. There are missing `simp` lemmas here.`
    -/
    erw [h]

Goal state after:
case a
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
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ J ≤ map f I
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
⊢ ∃ y_1, f y_1 = ⁅x, y⁆

Tactic:
obtain ⟨w, hw⟩ := h x z

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 y : L'
z : L
hz : f z = y
w : L
hw : ⁅x, f z⁆ = f w
⊢ ∃ y_1, f y_1 = ⁅x, y⁆
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [add_mul, add_mul]
  iterate 6 rw [mul_add]
  iterate 10 rw [map_add]
  rw [mul_comm b a, mul_comm c a, mul_comm c b]
  iterate 3 rw [two_smul]
  simp only [add_lie]
  abel_nf

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
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(LieSubmodule.lieSpan R L' ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)) = Submodule.map ↑f ↑I

Tactic:
toLieSubalgebra_toSubmodule,

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 := ⋯ }
⊢ ↑(LieSubmodule.lieSpan R L' ↑(Submodule.map ↑f ↑I)) = Submodule.map ↑f ↑I
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case empty
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
S : Set (LieSubmodule R L M)
x : L
m : M
hs : ↑∅ ⊆ {x | ∃ p ∈ S, ↑p = x}
hsm : m ∈ ⨆ i ∈ ∅, i
⊢ ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
| empty =>

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

Goal state before:
pp: case insert
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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
m' u : M
hu : u ∈ ⨆ x ∈ t, x
p : LieSubmodule R L M
hp : p ∈ S
hqt : ↑p ∉ t
hs : ↑(insert (↑p) t) ⊆ {x | ∃ p ∈ S, ↑p = x}
hm' : m' ∈ ↑p
hsm : m' + u ∈ ↑p ⊔ ⨆ x ∈ t, x
⊢ ↑p ≤ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
exact le_sSup ⟨p, hp, rfl⟩

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 : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ ⁅I, N⁆

Tactic:
rw [lieIdeal_oper_eq_span]; apply subset_lieSpan; use x, m

Goal state after:
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⁆ ≤ I ∧ ⁅I, J⁆ ≤ J

Tactic:
exact ⟨lie_le_left I J, lie_le_right J I⟩

Goal state after:
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 : LieIdeal R L
⊢ ↑(LieSubmodule.lieSpan R L ↑(toLieSubalgebra R L I).toSubmodule) = ↑I

Tactic:
toLieSubalgebra_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ↑(LieSubmodule.lieSpan R L ↑↑I) = ↑I
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
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N

Tactic:
· intro hs m hm; rw [mem_lieSpan] at hm; exact hm _ hs

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
y : L
⊢ y ∈ LieModule.ker R L L ↔ y ∈ center R L

Tactic:
simp only [LieModule.mem_maxTrivSubmodule, LieModule.mem_ker, ← lie_skew _ y, neg_eq_zero]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ (if h : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B') (f x) x_1 = 0) ⋯ else 0) =
    if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0

Tactic:
← Polynomial.aeval_def,

Goal state after:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ (if h : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (aeval (f x)) x_1 = 0) ⋯ else 0) =
    if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (aeval x) x_1 = 0) ⋯ else 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ 0 < (minpoly A x).natDegree

Tactic:
rw [pos_iff_ne_zero]

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ (minpoly A x).natDegree ≠ 0
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case empty
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
hxy : ∀ i ∈ ∅, x i ≡ y i [SMOD U]
⊢ ∑ i ∈ ∅, x i ≡ ∑ i ∈ ∅, y i [SMOD U]

Tactic:
| empty =>

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case empty
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
hxy : ∀ i ∈ ∅, x i ≡ y i [SMOD I]
⊢ ∏ i ∈ ∅, x i ≡ ∏ i ∈ ∅, y i [SMOD I]

Tactic:
| empty =>

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type u_4
B✝ : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : Algebra A B✝
K : Type u_6
inst✝¹ : Field K
ι : Type u_7
inst✝ : Fintype ι
B : Basis ι R S
x : S
e : ι ≃ Fin (Fintype.card ι)
hx : ∀ (i : ι), B i = x ^ ↑(e i)
i : Fin (Fintype.card ι)
⊢ (B.reindex e) i = x ^ ↑i

Tactic:
by simp [hx]

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
inst✝ : StrongRankCondition R
pb : PowerBasis R S
⊢ Fintype.card (Fin pb.dim) = pb.dim

Tactic:
Fintype.card_fin

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
pb : PowerBasis R S
⊢ pb.dim = pb.dim
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
  rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
  exact mem_map_of_mem _ ha

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (f * g) =
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) f *
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) g

Tactic:
by simp only [coe_eval₂RingHom, eval₂_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ IsUnit y

Tactic:
mul_assoc

Goal state after:
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
⊢ x ^ n ∣ x

Tactic:
by_cases hu : IsUnit x
  · exact (hu.pow n).dvd
  · rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
mul_assoc

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y
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
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ b = d * c

Tactic:
rw [hc, ← eq, mul_comm]

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

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
hs : (↑∅).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ ∅, Squarefree (f i)
⊢ Squarefree (∏ i ∈ ∅, f i)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ p - C a)

Tactic:
by
  -- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
  have : ¬ IsUnit (X ^ p - C a) := by
    rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
    exact hp.ne_zero
  have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
  -- It suffices to show that `deg g = p`.
  suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
  -- Suppose `deg g ≠ p`.
  by_contra h
  -- Let `r` be a root of `g`, then `N_K(r) ^ p = N_K(r ^ p) = N_K(a) = a ^ (deg g)`.
  have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree := by
    have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
  -- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
  -- also a `p`-power, contradicting the hypothesis
  have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
  exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ (filter (fun a ↦ s ^ p ^ n = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots).card ≤
    (filter (fun x ↦ s = x) ((expand R (p ^ n)) f).roots).card

Tactic:
exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)

Goal state after: