mathlib-initiative/mathlib-tactics huggingface dataset:
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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + i₂₃ = j

Tactic:
← h',

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + (i₂ + i₃) = 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₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ⊗ₘ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯) ≫
      (f₁ i₁ ⊗ₘ tensorHom f₂ f₃ (i₂ + i₃)) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      (𝟙 (Y₁ i₁) ⊗ₘ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯

Tactic:
MonoidalCategory.tensorHom_comp_tensorHom_assoc,

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₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ≫ f₁ i₁ ⊗ₘ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ tensorHom f₂ f₃ (i₂ + i₃)) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      (𝟙 (Y₁ i₁) ⊗ₘ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) 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₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ≫ f₁ i₁ ⊗ₘ (f₂ i₂ ⊗ₘ f₃ i₃) ≫ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      (𝟙 (Y₁ i₁) ⊗ₘ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯

Tactic:
MonoidalCategory.tensorHom_comp_tensorHom_assoc,

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₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ≫ f₁ i₁ ⊗ₘ (f₂ i₂ ⊗ₘ f₃ i₃) ≫ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ≫ 𝟙 (Y₁ i₁) ⊗ₘ (f₂ i₂ ⊗ₘ f₃ i₃) ≫ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) 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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ i₁₂ + i₃ = j

Tactic:
← h',

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ i₁ + i₂ + i₃ = 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₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (X₃ i₃)) ≫
      (tensorHom f₁ f₂ (i₁ + i₂) ⊗ₘ f₃ i₃) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      (ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (Y₃ i₃)) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯

Tactic:
MonoidalCategory.tensorHom_comp_tensorHom_assoc,

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₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ≫ tensorHom f₁ f₂ (i₁ + i₂) ⊗ₘ 𝟙 (X₃ i₃) ≫ f₃ i₃) ≫
      ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      (ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (Y₃ i₃)) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ 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₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ((f₁ i₁ ⊗ₘ f₂ i₂) ≫ ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ f₃ i₃) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      (ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (Y₃ i₃)) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯

Tactic:
MonoidalCategory.tensorHom_comp_tensorHom_assoc,

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₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ((f₁ i₁ ⊗ₘ f₂ i₂) ≫ ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ f₃ i₃) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ≫ ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ f₃ i₃ ≫ 𝟙 (Y₃ i₃)) ≫
      ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯
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
n : ℤ
h : IsZero ((X.H n).obj (mk₁ g))
⊢ IsZero (X.cycles f g n)

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_mono (X.iCycles ..)]

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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero ((X.H n).obj (mk₁ g))
⊢ 𝟙 (X.cycles f g n) ≫ X.iCycles f g n = 0 ≫ X.iCycles f g n
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
⊢ ((if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0) ≫
      if hpq : (c r).Rel pq' pq'' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq' - 1) (data.deg pq')
            (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₀ r pq' ⋯) (data.i₁ pq') ⋯ ⋯ ⋯ ⋯
              (data.deg pq') (data.deg pq' + 1) (data.deg pq' + 2) ⋯ ⋯ ⋯).inv
      else 0) =
    0

Tactic:
dif_neg hpq',

Goal state after:
case neg
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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : ¬(c r).Rel pq' pq''
⊢ (if hpq : (c r).Rel pq pq' then
        X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ ≫
          (pageXIso X data r hr pq' (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯ (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯).inv
      else 0) ≫
      0 =
    0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
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''
⊢ (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).Exact

Tactic:
rw [ShortComplex.exact_iff_epi _ ((page X data r hr).shape _ _ h)]
    have := isIso_mapFourδ₁Toδ₀' X data r r' hrr' hr pq' pq'' hpq'
      i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' h
    dsimp
    infer_instance

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x m : L
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]

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

Goal state before:
pp: L : Type v
inst✝ : LieRing L
x y z : L
⊢ -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0

Tactic:
abel

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m✝ n✝ : M
x : L
f : M →ₗ[R] N
m n : M
⊢ ⁅x, f m⁆ + ⁅x, f n⁆ - (f ⁅x, m⁆ + f ⁅x, n⁆) = ⁅x, f m⁆ - f ⁅x, m⁆ + (⁅x, f n⁆ - f ⁅x, n⁆)

Tactic:
abel

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n✝ : M
x y : L
f : M →ₗ[R] N
n : M
⊢ ⁅x, f n⁆ + ⁅y, f n⁆ - (f ⁅x, n⁆ + f ⁅y, n⁆) = ⁅x, f n⁆ - f ⁅x, n⁆ + (⁅y, f n⁆ - f ⁅y, n⁆)

Tactic:
abel

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m n✝ : M
x : L
f g : M →ₗ[R] N
n : M
⊢ ⁅x, f n⁆ + ⁅x, g n⁆ - (f ⁅x, n⁆ + g ⁅x, n⁆) = ⁅x, f n⁆ - f ⁅x, n⁆ + (⁅x, g n⁆ - g ⁅x, n⁆)

Tactic:
abel

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n✝ : M
x y : L
f : M →ₗ[R] N
n : M
⊢ ⁅x, ⁅y, f n⁆⁆ - ⁅x, f ⁅y, n⁆⁆ - (⁅y, f ⁅x, n⁆⁆ - f ⁅y, ⁅x, n⁆⁆) =
    ⁅x, ⁅y, f n⁆⁆ - ⁅y, ⁅x, f n⁆⁆ - (f ⁅x, ⁅y, n⁆⁆ - f ⁅y, ⁅x, n⁆⁆) +
      (⁅y, ⁅x, f n⁆⁆ - ⁅y, f ⁅x, n⁆⁆ - (⁅x, f ⁅y, n⁆⁆ - f ⁅x, ⁅y, n⁆⁆))

Tactic:
abel

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝ + x✝¹ * x✝ - (x✝ * x✝² + x✝ * x✝¹) = x✝² * x✝ - x✝ * x✝² + (x✝¹ * x✝ - x✝ * x✝¹)

Tactic:
abel

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝¹ + x✝² * x✝ - (x✝¹ * x✝² + x✝ * x✝²) = x✝² * x✝¹ - x✝¹ * x✝² + (x✝² * x✝ - x✝ * x✝²)

Tactic:
abel

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

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * (x✝¹ * x✝) - x✝² * (x✝ * x✝¹) - (x✝¹ * (x✝ * x✝²) - x✝ * (x✝¹ * x✝²)) =
    x✝² * (x✝¹ * x✝) - x✝¹ * (x✝² * x✝) - (x✝ * (x✝² * x✝¹) - x✝ * (x✝¹ * x✝²)) +
      (x✝¹ * (x✝² * x✝) - x✝¹ * (x✝ * x✝²) - (x✝² * (x✝ * x✝¹) - x✝ * (x✝² * x✝¹)))

Tactic:
abel

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
inst✝ : IsFaithful R L M
x : L
⊢ (toEnd R L M) x = ↑(toEnd R L M) 0 ↔ x = 0

Tactic:
exact toEnd_eq_iff R L M

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

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

Tactic:
abel

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
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier

Tactic:
suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
      exact K₂.lie_mem hx hy

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

Tactic:
by
  apply le_antisymm
  · 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]
  · rw [← SetLike.coe_subset_coe, ← h]; exact LieSubmodule.subset_lieSpan

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
N N' : LieSubmodule R L M
⊢ ∀ (x : L) (m n : ↥N), ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩

Tactic:
intro x m n

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
x : L
m n : ↥N
⊢ ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ comap f (map f N) = N

Tactic:
rw [SetLike.ext'_iff]
  exact (N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

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
m : M
⊢ IsCompactElement (lieSpan R L {m})

Tactic:
CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le

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
m : M
⊢ ∀ (s : Set (LieSubmodule R L M)),
    s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆

Tactic:
have hf : ⁅x, f.val⁆ m = 0 := by rw [f.property x, LinearMap.zero_apply]

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
hf : ⁅x, ↑f⁆ m = 0
⊢ (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f ⊥ = ⊥

Tactic:
by
  ext m; simp [eq_comm]

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✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x).leadingCoeff = p.leadingCoeff

Tactic:
(monic hx).leadingCoeff,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ 1 = p.leadingCoeff
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:
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.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p q : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
⊢ p ∣ q → (Polynomial.aeval b) q = 0

Tactic:
· rintro ⟨g, rfl⟩
    simp [hfa]

Goal state after:
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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit (C (c.coeff 0))

Tactic:
← Nat.eq_zero_of_le_zero h,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit (C (c.coeff c.natDegree))
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ P ∈ Ideal.span {C (X - C a), X - C b} ↔ eval a (eval b P) = 0

Tactic:
by
  rw [Ideal.mem_span_pair]
  constructor <;> intro h
  · rcases h with ⟨_, _, rfl⟩
    simp
  · rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩
    rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩
    exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩

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

Goal state before:
pp: case mp.add
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
ha : a ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
hb : b ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
ha' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑a
hb' : ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑b
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a + b)

Tactic:
obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩

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

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

Tactic:
abel

Goal state after: