mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H✝ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H✝
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H✝
B : C ⥤ H✝
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ s, Nonempty (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
s₁ : S
f₁ : Z s₁ ⟶ A₁
P : Precylinder X₀
hP : T.map P.i₀ = T.map P.i₁
h : (P.map L).LeftHomotopy ↑s₀ ↑s₁
Z' : CostructuredArrowDownwards e.hom g := CostructuredArrowDownwards.mk e.hom g P.I (e₀.inv ≫ T.map P.i₀) h.h ⋯
⊢ (structuredArrowDownwards e.hom Y₀).map (StructuredArrow.homMk P.i₀ ⋯) ≫ CostructuredArrow.hom Z' =
    CostructuredArrow.hom (Z s₀)

Tactic:
by simp [Z, Z', dsimp% h.h₀]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), ∃ i, quasiIso C i

Tactic:
obtain ⟨L, i, _, _, _⟩ := modelCategoryQuillen.exists_quasiIso_injective K.obj n

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), ∃ i, quasiIso C i
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2
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 C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ((Plus.prepathObject { obj := K₂, property := ⋯ }).map
        (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy
    (ObjectProperty.homMk f₀) (ObjectProperty.homMk f₁)

Tactic:
refine PrepathObject.RightHomotopy.fullSubcategoryEquiv.symm
        { h := pathObject.lift f₀ f₁ (homotopyOfEq _ _
          ((HomotopyCategory.Plus.ι C).congr_map hf)) ≫
          (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C)
            (fun n ↦ ⟨n + 1, by simp⟩)).inv
          h₀ := ?_
          h₁ := ?_ }
      all_goals
        dsimp [Functor.mapCochainComplexPlus]
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((shiftFunctor C (m + n)).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
    (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d

pp: case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (m + n)).map f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom =
    (mkIso (shiftAdd X✝.obj m n) ⋯).hom ≫ (shiftFunctor C m ⋙ shiftFunctor C n).map f

Tactic:
· dsimp
    rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)]
    simp only [Category.assoc, Iso.inv_hom_id_app_assoc]
    rw [← NatTrans.naturality_assoc]
    dsimp
    simp only [Functor.map_comp, Category.assoc,
      shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj,
      Iso.inv_hom_id_app_assoc]

Goal state after:
case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (m + n)).map f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom =
    (mkIso (shiftAdd X✝.obj m n) ⋯).hom ≫ (shiftFunctor C m ⋙ shiftFunctor C n).map f
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m = e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩

Tactic:
by
      rw [← hm ⟨⟨j, 0⟩, hp j⟩, mapBifunctorRightUnitorCofan_inj, assoc, ← Functor.map_comp_assoc,
        Iso.inv_hom_id, Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]

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

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

Tactic:
exact (X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0

Goal state after:
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₁
⊢ f₁ ≫ f₂₃ = f₁ ≫ f₂ ≫ f₃

Tactic:
by rw [h₂₃]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.kernelSequenceOpcycles f g fg h n).Exact

Tactic:
by
  apply ShortComplex.exact_of_f_is_kernel
  exact IsLimit.ofIsoLimit (kernelIsKernel _)
    (Iso.symm (Fork.ext (X.opcyclesIsoKernel f g fg h n) (by
      simp [← cancel_epi (X.pOpcycles f g n)])))

Goal state after:
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₀ : ℤ
l : ℕ
⊢ ∀ (r r' : ℤ) (pq : ℤ × Fin l) (hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24)
    (hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26),
    ⟨(↑↑pq.2 - (r' - 2)).toNat, ⋯⟩ ≤ ⟨(↑↑pq.2 - (r - 2)).toNat, ⋯⟩

Tactic:
rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26
⊢ ⟨(↑↑(a, ⟨a', isLt✝⟩).2 - (r' - 2)).toNat, ⋯⟩ ≤ ⟨(↑↑(a, ⟨a', isLt✝⟩).2 - (r - 2)).toNat, ⋯⟩
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₀ : ℤ
l : ℕ
⊢ ∀ (r r' : ℤ) (pq : ℤ × Fin l),
    autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32 →
      autoParam (r ≤ r') SpectralSequenceDataCore._auto_34 →
        Fin.clamp (↑↑pq.2 + (r - 1)).toNat l ≤ Fin.clamp (↑↑pq.2 + (r' - 1)).toNat l

Tactic:
rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_34
⊢ Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r - 1)).toNat l ≤ Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r' - 1)).toNat l
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂

Tactic:
have : h.cyclesIso.inv =
      X.toCycles (𝟙 i) f f (by simp) n₁ ≫
        (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv := by
    rw [← cancel_mono (X.cyclesIso ..).hom,
      Category.assoc, Iso.inv_hom_id, Category.comp_id,
      ← cancel_mono (X.iCycles ..), Category.assoc, cyclesIso_hom_i ..,
      h.cyclesIso_inv_comp_iCycles, toCycles_i]
    dsimp [h]
    rw [← Functor.map_id]
    congr 1
    cat_disch

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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂
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 : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
n : N
⊢ g ⁅x, n⁆ = g ⁅x, f (g n)⁆

Tactic:
h₂

Goal state after:
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 : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
n : N
⊢ g ⁅x, n⁆ = g ⁅x, n⁆
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n.succ • y

Tactic:
simp [Nat.succ_eq_add_one, pow_add, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ Jac * Jac ^ n = Jac ^ n

Tactic:
rw [← Ideal.IsTwoSided.pow_succ]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ Jac ^ (n + 1) = Jac ^ n
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₂
y : L₂
hy : y ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy⟩

Tactic:
rw [mem_range] at hy

Goal state after:
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₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩
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 * (a + b + c) + b * (a + b + c) + 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:
iterate 6 rw [mul_add]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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)⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
hv : ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
⊢ ⟨u + v, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
revert hu hv

Goal state after:
case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
      ⟨u + v, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case lie
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
hv : ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
⊢ ⟨⁅u, v⁆, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
revert hu hv

Goal state after:
case lie
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
      ⟨⁅u, v⁆, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case a.add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hy✝ : v ∈ lieSpan R L (range (Subtype.val ∘ f))
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
hv : v ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ u + v ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu hv

Goal state after:
case a.add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hy✝ : v ∈ lieSpan R L (range (Subtype.val ∘ f))
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f)) →
    v ∈ map K.incl (lieSpan R (↥K) (range f)) → u + v ∈ map K.incl (lieSpan R (↥K) (range f))
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case a.lie
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hy✝ : v ∈ lieSpan R L (range (Subtype.val ∘ f))
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
hv : v ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu hv

Goal state after:
case a.lie
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hy✝ : v ∈ lieSpan R L (range (Subtype.val ∘ f))
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f)) →
    v ∈ map K.incl (lieSpan R (↥K) (range f)) → ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
by
  rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]; rfl

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : x ∈ ↑(⨆ i, N i)
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x

Tactic:
LieSubmodule.iSup_toSubmodule

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, ↑(N i)
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x
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 I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
h₂

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I₁, I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Module: Mathlib.RingTheory.Polynomial.Quotient

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

Tactic:
eval₂_eq_eval_map,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ eval X (Polynomial.map (C.comp (Quotient.mk I)) f) = Polynomial.map (Quotient.mk I) f
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) f

Tactic:
← aeval_modByMonic_eq_self_of_root hy

Goal state after:
case inr
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)

Tactic:
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]

Goal state after:
case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ∑ x ∈ Finset.range pb.dim, ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x) =
    ∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i
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✝ : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ f, y = (aeval x) f
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i)

Tactic:
obtain ⟨f, rfl⟩ := hy
  apply mem_span_pow'.mpr _
  have := minpoly.monic hx
  refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩
  conv_lhs => rw [← modByMonic_add_div f (minpoly R x)]
  simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]

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

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

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

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsUnit q

Tactic:
apply isCoprime_self.mp

Goal state after:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime q q
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis (↥s) R M
⊢ Free R M
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✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis (↥s) A M)
⊢ Module.Finite A M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩

Goal state after:
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
s : Finset M
hs : Basis (↥s) A M
⊢ Module.Finite A M
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
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.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs
    simp only [← det_toMatrix (Module.finBasis A M), map_smul, Fintype.card_fin, Matrix.det_smul]

Goal state after: