mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_1
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))

Tactic:
have eq := s.ι.naturality
        (CostructuredArrow.homMk f : CostructuredArrow.mk (L.map f ≫ φ) ⟶ CostructuredArrow.mk φ)
      dsimp at eq hφ ⊢
      rw [comp_id] at eq
      rw [assoc] at hφ
      rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]

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

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X

Tactic:
hasPointwiseRightDerivedFunctorAt_iff F W.Q W

Goal state after:
C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.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
K : Plus (InjectiveObject C)
⊢ IsKInjective (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K.obj)

Tactic:
obtain ⟨K, n, hn⟩ := K

Goal state after:
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
K : CochainComplex (InjectiveObject C) ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ IsKInjective (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj { obj := K, property := ⋯ }.obj)
Module: Mathlib.Algebra.Homology.GrothendieckAbelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
emb : (K ⟶ L) → (i : Shrink.{w, t} ι) → Shrink.{w, v} (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i)) :=
  fun f i ↦ (equivShrink (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i))) (f.f ((equivShrink ι).symm i))
f g : K ⟶ L
h : emb f = emb g
i : ι
⊢ f.f i = g.f i

Tactic:
obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
emb : (K ⟶ L) → (i : Shrink.{w, t} ι) → Shrink.{w, v} (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i)) :=
  fun f i ↦ (equivShrink (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i))) (f.f ((equivShrink ι).symm i))
f g : K ⟶ L
h : emb f = emb g
i : Shrink.{w, t} ι
⊢ f.f ((equivShrink ι).symm i) = g.f ((equivShrink ι).symm i)
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| 𝟙 (F.obj P) ≫ φ.app P

Tactic:
← F.map_id

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
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
| F.map (𝟙 P) ≫ φ.app P
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
⊢ δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (K.d p' p ≫ f) h'

Tactic:
by
  by_cases hp : p' + 1 = p
  · dsimp only [toSingleMk]
    rw [δ_single _ n n' (by lia) p' (q + 1) (by lia) rfl]
    simp
  · simp [δ_shape n n' (by lia), HomologicalComplex.shape K p' p (by simp; lia)]

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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f

Tactic:
have h' := F.congr_map (comp_p f)

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 : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f
h' : F.map (f.f ≫ x✝.p) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
⊢ ∃ f, ∃ (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α

Tactic:
obtain ⟨f, hf⟩ := Cochain.fromSingleMk_surjective α.1 q h
  have hα := α.δ_eq_zero (n + 1)
  rw [← hf, Cochain.δ_fromSingleMk _ _ _ q' (by lia)] at hα
  replace hα := Cochain.congr_v hα p q' (by lia)
  exact ⟨f, by simpa using hα, by ext : 1; assumption⟩

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:
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.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝²⁵ : AddMonoid I
C : Type u_1
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝²² : X₁.HasTensor X₂
inst✝²¹ : X₂.HasTensor X₃
inst✝²⁰ : X₃.HasTensor X₄
inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄
inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄
inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄
inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)
inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)
inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄
inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄
inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄
inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄
inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄
inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)
inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄
⊢ tensorHom (associator X₁ X₂ X₃).hom (𝟙 X₄) ≫
      (associator X₁ (tensorObj X₂ X₃) X₄).hom ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).hom =
    (associator (tensorObj X₁ X₂) X₃ X₄).hom ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).hom

Tactic:
by
  rw [← cancel_epi (associator (tensorObj X₁ X₂) X₃ X₄).inv,
    ← cancel_epi (associator X₁ X₂ (tensorObj X₃ X₄)).inv, Iso.inv_hom_id_assoc,
    Iso.inv_hom_id, ← pentagon_inv_assoc]
  simp [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom_assoc]

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

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

Tactic:
hi₀',

Goal state after:
ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
⊢ data.i₀ r' pq' ⋯ ≤ i₀
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₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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:
hi₀',

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₀
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₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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''
⊢ data.i₀ r' pq' ⋯ = data.i₁ pq''
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).next pq' = pq''
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' ⋯
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:
hi₀',

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₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
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' ⋯
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''
⊢ data.i₀ r' pq' ⋯ = data.i₁ pq''
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 : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f j = f i

Tactic:
eq_comm

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
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⁆ +
      ∑ 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⁆

Tactic:
add_comm,

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 ^ x_1.1) y, (φ x) ((φ x ^ x_1.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.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: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
p✝ : (x : L) → x ∈ lieSpan R L s → Prop
mem : ∀ (x : L) (h : x ∈ s), p✝ x ⋯
zero : p✝ 0 ⋯
add : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p✝ x hx → p✝ y hy → p✝ (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : x ∈ lieSpan R L s), p✝ x hx → p✝ (a • x) ⋯
x : L
lie : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p✝ x hx → p✝ y hy → p✝ ⁅x, y⁆ ⋯
hx : x ∈ lieSpan R L s
p : LieSubalgebra R L :=
  { carrier := {x | ∃ (hx : x ∈ lieSpan R L s), p✝ x hx}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }
⊢ p✝ x hx

Tactic:
exact lieSpan_le (K := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

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'
h : f.range = ⊤
⊢ f.idealRange = ⊤

Tactic:
rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, LieSubmodule.top_toSubmodule,
    LieSubalgebra.top_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'
h : f.range = ⊤
⊢ ∃ N, ↑N = ⊤
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
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1

Tactic:
simpa only [map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)

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✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : x = (algebraMap A B) y
⊢ (algebraMap A B) y = x

Tactic:
eq_comm

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : (algebraMap A B) y = x
⊢ (algebraMap A B) y = x
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ ¬q.natDegree < orderOf σ

Tactic:
intro H

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
H : q.natDegree < orderOf σ
⊢ False
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp
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]
⊢ y ∈ Ideal.map (algebraMap R ↥R[x]) I → ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

Tactic:
intro H

Goal state after:
case mp
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]
H : y ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
⊢ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
refine ⟨f, ?_, hy⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
⊢ f.natDegree < d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
refine ⟨f, ?_, hy⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ f.degree < ↑d
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
⊢ (aeval pb.gen) (X ^ pb.dim) -
      ∑ x, (aeval pb.gen) (C ((pb.basis.repr (pb.gen ^ pb.dim)) x)) * (aeval pb.gen) (X ^ ↑x) =
    0

Tactic:
map_pow,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) X ^ pb.dim - ∑ x, (aeval pb.gen) (C ((pb.basis.repr (pb.gen ^ pb.dim)) x)) * (aeval pb.gen) X ^ ↑x = 0
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
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (minpoly A pb.gen).natDegree = pb.dim

Tactic:
rw [← minpolyGen_eq, natDegree_minpolyGen]

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
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = (aeval pb.gen) pb.minpolyGen

Tactic:
add_comm,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x + pb.gen ^ pb.dim = (aeval pb.gen) pb.minpolyGen
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ (norm R) s = ((leftMulMatrix b) s).det

Tactic:
by
  rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]; rfl

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible ((X ^ k) ^ m - C (b ^ m))
q : K[X]
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False

Tactic:
map_pow,

Goal state after:
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible ((X ^ k) ^ m - C b ^ m)
q : K[X]
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ False
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree (∏ x ∈ s, f x)

Tactic:
refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩

Goal state after:
case cons.refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
i : ι
hi : i ∈ s
⊢ IsRelPrime (f a) (f i)

case cons.refine_2
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (∏ x ∈ s, f x)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N * M').det = N.det

Tactic:
by
  rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R M) then detAux (Trunc.mk ⋯.some) else 1) f = 1

Tactic:
dif_neg,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ 1 f = 1

case hnc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ s, Nonempty (Basis (↥s) R M)
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x = (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))

Tactic:
add_comm,

Goal state after:
R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x = (iterateFrobeniusEquiv R p (n + m)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = ⇑((RingAut.toPerm R) (frobeniusEquiv R p ^ n))

Tactic:
map_pow,

Goal state after:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = ⇑((RingAut.toPerm R) (frobeniusEquiv R p) ^ n)