mathlib-initiative/mathlib-tactics huggingface dataset:
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    (mapBifunctorRightUnitor F Y e p hp X).inv j ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) j

Tactic:
mapBifunctorRightUnitor_inv_apply,

Goal state after:
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    (e.inv.app (X j) ≫
        (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯) ≫
      mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) j
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₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst✝ : X₁.HasTensor X₂
⊢ Y₁.HasTensor Y₂

Tactic:
let e : ((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂ ≅
    ((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂ := isoMk _ _
      (fun ⟨i, j⟩ ↦ (eval i).mapIso e₁ ⊗ᵢ (eval j).mapIso e₂)
  exact hasMap_of_iso e _

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 (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
⊢ ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
    ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂ j hi ≫ f =
      ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂ j hi ≫ g

Tactic:
intro i₁ i₂₃₄ h'

Goal state after:
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 (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
⊢ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁

Tactic:
Category.comp_id

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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ f₂ n₀ n₁ ⋯ = X.δ f₁ f₂ n₀ n₁ hn₁
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

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

Tactic:
· dsimp
    convert! (inferInstance : Mono ((X.H n₃).map (𝟙 (mk₁ f₁))))
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : Square C
φ : X✝ ⟶ Y✝
⊢ (X✝.map F).f₂₄ ≫ F.map φ.τ₄ = F.map φ.τ₂ ≫ (Y✝.map F).f₂₄

Tactic:
by simpa only [Functor.map_comp] using! F.congr_map φ.comm₂₄

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₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ ≫ 𝟙 ((X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) = 0
⊢ x = 0

Tactic:
Category.comp_id

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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x = 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos.refine_2
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''
⊢ (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ =
    (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ ≫
        𝟙 (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)

Tactic:
Category.comp_id

Goal state after:
case pos.refine_2
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''
⊢ (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ =
    (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ =
    (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ ≫
        𝟙 (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)

Tactic:
Category.comp_id

Goal state after:
case pos
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ =
    (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: 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
⊢ { toFun := fun m ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    ⁅{ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ },
      { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }⁆

Tactic:
ext m; apply lie_lie

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

Goal state before:
pp: 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
x : L
y : ↥N
n : ℕ
⊢ ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y

Tactic:
induction n generalizing y with
  | zero => rfl
  | succ n ih => simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]

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
⊢ ⇑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R

Tactic:
ext a b

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
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 - y * x ∈ A'

Tactic:
have hxy := A'.mul_mem hx hy

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'
hxy : x * 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'
h : Function.Surjective ⇑f
⊢ f.idealRange = ⊤

Tactic:
by
  rw [← f.range_eq_top] at h
  rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, LieSubmodule.top_toSubmodule,
    LieSubalgebra.top_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
  use ⊤
  exact LieSubmodule.top_toSubmodule

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
x : L'
y : L
hy₁ : y ∈ ↑(toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule
hy₂ : ↑f y = x
⊢ ↑f y ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
LieSubmodule.mem_sup

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
x : L'
y : L
hy₁ : ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y
hy₂ : ↑f y = x
⊢ ↑f y ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
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 I₂ : LieIdeal R L
⊢ Submodule.comap (↑I).subtype ↑I₂ = ⊤ ↔ I ≤ I₂

Tactic:
rw [Submodule.comap_subtype_eq_top, LieSubmodule.toSubmodule_le_toSubmodule]

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 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
⊢ m ∈ ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
LieSubmodule.mem_sup

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
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'
hn : ∃ y ∈ N, ∃ z ∈ N', y + z = n
h : ⁅↑x, ↑⟨n, hn✝⟩⁆ = m
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
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 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
⊢ m ∈ ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
LieSubmodule.mem_sup

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
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
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
n : ↥N
h : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
⊢ -x ≡ -y [SMOD U]

Tactic:
simpa only [SModEq.def, Quotient.mk_neg, neg_inj]

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
⊢ (algebraMap A B) y = x

Tactic:
by
  have key : minpoly A x = X - C y := eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
    (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
      (dvd_iff_isRoot.2 h))
  have := aeval A x
  rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ ((Ideal.Quotient.mk (Ideal.map C I)).comp C) i = 0

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ C i ∈ Ideal.map C I
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:
rw [mul_assoc] at hz

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.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)

Tactic:
by
  apply_fun (frobeniusEquiv S p)^[n]
  · simp only [coe_frobeniusEquiv, ← map_iterate_frobenius]
    · rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
      · simp
      all_goals rw [← coe_frobeniusEquiv]; simp [Function.Commute, Function.Semiconj]
  apply Function.Injective.iterate
  simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
hp : ExpChar K p
⊢ PerfectRing K p

Tactic:
by
  refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
  rcases hp with _ | hp
  · simp [frobenius]
  rw [← not_forall_not]
  apply mt (X_pow_sub_C_irreducible_of_prime hp)
  apply mt separable_of_irreducible
  simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero,
    derivative_X_pow, degree_X_pow_sub_C hp.pos, hp.ne_zero]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
  induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih
  rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
  · refine ⟨0, f, h, ?_⟩
    rw [pow_zero, expand_one]
  · rcases N with - | N
    · rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
      rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
      have hf0 : f ≠ 0 := hf.ne_zero
      rw [h1, C_0] at hn
      exact absurd hn hf0
    have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
    have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
    have hg3 : g.natDegree < N.succ := by
      rw [← mul_one g.natDegree, ← hg1]
      exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
    rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
    refine ⟨n + 1, g, hg4, ?_⟩
    rw [← hgf, expand_expand, pow_succ']

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ¬∀ (a : F), Multiset.count a f.roots ≤ 1

Tactic:
not_forall,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ∃ x, ¬Multiset.count x f.roots ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ { val := (map i h).roots, nodup := ?nodup✝ } = {i x}

Tactic:
Finset.eq_singleton_iff_unique_mem

Goal state after:
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ i x ∈ { val := (map i h).roots, nodup := ?nodup✝ } ∧ ∀ x_1 ∈ { val := (map i h).roots, nodup := ?nodup✝ }, x_1 = i x
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ (lift i a h) (root f) = a

Tactic:
rw [root, lift_mk, eval₂_X]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ f.aroots L ↔ (Equiv.refl L) x ∈ f.aroots L

pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0

Tactic:
Equiv.refl_apply

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ f.aroots L ↔ x ∈ f.aroots L

R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2.hst
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := ⋯
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := ⋯
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := ⋯
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ ∀ (i : (_ : ℕ) × ℕ),
    (i ∈ RN.sigma fun i ↦ RN) ↔
      (match i with
        | ⟨i, j⟩ => (i, j)) ∈
        RN ×ˢ RN

Tactic:
simp only [mem_sigma, mem_product, implies_true]

Goal state after: