mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
x : Ext X Y 0
⊢ mapExactFunctor F x = (⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀) x

Tactic:
rcases (Ext.mk₀_bijective X Y).2 x with ⟨y, hy⟩

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
x : Ext X Y 0
y : X ⟶ Y
hy : mk₀ y = x
⊢ mapExactFunctor F x = (⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀) x
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m✝ : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc 0) (Int.ofNat m) = 0

Tactic:
obtain _ | m := m

Goal state after:
case zero.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m : ℤ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0
⊢ h.d (Int.negSucc 0) (Int.ofNat 0) = 0

case zero.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m✝ : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat (m + 1)
⊢ h.d (Int.negSucc 0) (Int.ofNat (m + 1)) = 0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj))
    ext._auto_1

Tactic:
rw [Functor.map_id]

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
dif_neg h₀

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
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₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃ + i₄) = j

Tactic:
by rw [← h, ← add_assoc, ← add_assoc]

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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (mk₁ f).obj' 1 homMk₁._proof_5 ⟶ (mk₁ f').obj' 1 homMk₁._proof_5

Tactic:
by exact α.app 1

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₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
| (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃ ⊗ X₄ i₄)).inv ≫
    (α_ (X₁ i₁ ⊗ X₂ i₂) (X₃ i₃) (X₄ i₄)).inv ≫
      (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫ ιTensorObj (tensorObj X₁ X₂) X₃ (i₁ + i₂) i₃ (i₁ + i₂ + i₃) ⋯) ▷
          X₄ i₄ ≫
        ιTensorObj (tensorObj (tensorObj X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯

Tactic:
← ιTensorObj₃'_eq X₁ X₂ X₃ i₁ i₂ i₃ _ rfl _ rfl

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 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₄
j i₁ i₂ i₃ i₄ : I
h : i₁ + i₂ + i₃ + i₄ = j
| (α_ (X₁ i₁) (X₂ i₂) (X₃ i₃ ⊗ X₄ i₄)).inv ≫
    (α_ (X₁ i₁ ⊗ X₂ i₂) (X₃ i₃) (X₄ i₄)).inv ≫
      ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫
        ιTensorObj (tensorObj (tensorObj X₁ X₂) X₃) X₄ (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
n : ℕ
⊢ Finite ↑((fun i ↦ i.1 + i.2) ⁻¹' {n})

Tactic:
by
  refine Finite.of_injective (fun ⟨⟨i₁, i₂⟩, (hi : i₁ + i₂ = n)⟩ =>
    ((⟨i₁, by lia⟩, ⟨i₂, by lia⟩) : Fin (n + 1) × Fin (n + 1))) ?_
  rintro ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ h
  simpa using h

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

Goal state before:
pp: 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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
by
  have := X.map_ιE _ _ _ _ _ _ α (𝟙 _) n₀ n₁ n₂
  rw [opcyclesMap_id, comp_id] at this
  exact mono_of_mono_fac this

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

Goal state before:
pp: case e_a.h₀
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₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ app'
      (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
        homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2) ⋯)
      0 homMk₁._proof_4 =
    app'
      (homMk₁ (β.app 0) (β.app 1) ⋯ ≫
        homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯)
      0 homMk₁._proof_4

Tactic:
simpa [h₀] using naturality' α 0 1

Goal state after:
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 : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ m, (f ^ m).range = (f ^ n).range

Tactic:
refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

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 : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : n ≤ l
m : ℕ
⊢ (f ^ l).range ≤ (f ^ m).range
Module: Mathlib.Algebra.Lie.Basic

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

Tactic:
by
  rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]
  abel

Goal state after:
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).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'
⊢ data.i₃ r' pq' ⋯ = data.i₂ pq

Tactic:
data.i₃_next r r' pq pq' h

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).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'
⊢ data.i₂ pq = data.i₂ pq
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 : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤

Tactic:
LieSubalgebra.mem_bot

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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ ⟨x, hx✝⟩ ∈ ⊥ ↔ ⟨x, hx✝⟩ ∈ ⊤
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
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule

Tactic:
rw [Submodule.span_le, coe_toSubmodule]
  apply subset_lieSpan

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:
apply le_antisymm

Goal state after:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I ≤ J

case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ J ≤ map f I
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤

Tactic:
eq_top_iff

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ ⊤ ≤ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
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
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
⊢ comap K.incl (lieSpan R L (range (Subtype.val ∘ f))) = lieSpan R (↥K) (range f)

Tactic:
apply le_antisymm

Goal state after:
case a
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
⊢ comap K.incl (lieSpan R L (range (Subtype.val ∘ f))) ≤ lieSpan R (↥K) (range f)

case a
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
⊢ lieSpan R (↥K) (range f) ≤ comap K.incl (lieSpan R L (range (Subtype.val ∘ f)))
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ↑⁅I, N⁆
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
z₁ : L
⊢ ∃ x ∈ (toLieSubalgebra R L I).toSubmodule, f x = ⁅f z₁, f z₂⁆

Tactic:
use ⁅z₁, z₂⁆

Goal state after:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ (Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule).carrier
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧ f ⁅z₁, z₂⁆ = ⁅f z₁, f z₂⁆
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'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) = f.idealRange ⊓ J

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) ≤ f.idealRange ⊓ J

case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ f.idealRange ⊓ J ≤ map f (comap f J)
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
S : Set (LieSubmodule R L M)
⊢ ∀ {x : L} {m : M}, m ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier → ⁅x, m⁆ ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier

Tactic:
by
        intro x m (hm : m ∈ sSup {(p : Submodule R M) | p ∈ S})
        change ⁅x, m⁆ ∈ sSup {(p : Submodule R M) | p ∈ S}
        obtain ⟨s, hs, hsm⟩ := Submodule.mem_sSup_iff_exists_finset.mp hm
        clear hm
        induction s using Finset.induction_on generalizing m with
        | empty =>
          replace hsm : m = 0 := by simpa using hsm
          simp [hsm]
        | insert q t hqt ih =>
          rw [Finset.iSup_insert] at hsm
          obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm
          rw [lie_add]
          refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)
          obtain ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)
          suffices p ≤ sSup {(p : Submodule R M) | p ∈ S} by exact this (p.lie_mem hm')
          exact le_sSup ⟨p, hp, rfl⟩

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
this : ⁅⊥, N⁆ ≤ ⊥
⊢ ⁅⊥, N⁆ = ⊥

Tactic:
exact le_bot_iff.mp this

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 J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
⊢ ⁅I, N⁆ ≤ ⁅J, N'⁆

Tactic:
intro m h
  rw [lieIdeal_oper_eq_span, mem_lieSpan] at h; rw [lieIdeal_oper_eq_span, mem_lieSpan]
  intro N hN; apply h; rintro m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩; rw [← hm]; apply hN
  use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩

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 : LieSubmodule R L M
⊢ Nontrivial ↥N ↔ N ≠ ⊥

Tactic:
constructor
  · rintro ⟨⟨m₁, h₁⟩, ⟨m₂, h₂⟩, h₁₂⟩ rfl
    simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂
  · contrapose!
    rw [LieSubmodule.eq_bot_iff]
    rintro ⟨h⟩ m hm
    simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩

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
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p

Tactic:
p.exists_lieSubmodule_coe_eq_iff L

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
p : Submodule R M
⊢ ↑(lieSpan R L ↑p) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
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
x y : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
hy : y ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
z : L
⊢ ⁅z, x + y⁆ = 0

Tactic:
by rw [lie_add, hx, hy, add_zero]

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
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ ¬2 ≤ (minpoly A x).natDegree

Tactic:
not_le

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
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ ⁅I₁, I₂⁆ ≤ comap f ⁅map f I₁, map f I₂⁆

Tactic:
LieSubmodule.lieIdeal_oper_eq_span,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ LieSubmodule.lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ comap f ⁅map f I₁, map f I₂⁆
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
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
⊢ p * C p.leadingCoeff⁻¹ = minpoly A x

Tactic:
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
  apply eq_of_irreducible_of_monic
  · exact Associated.irreducible ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff,
      by rwa [← C_mul, inv_mul_cancel₀, C_1], by rwa [← C_mul, mul_inv_cancel₀, C_1]⟩, rfl⟩ hp1
  · rw [aeval_mul, hp2, zero_mul]
  · rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]

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
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
apply lt_add_of_pos_right

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
⊢ 0 < c.natDegree
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
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ U

Tactic:
Submodule.Quotient.eq

Goal state after:
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
⊢ x - y ∈ U ↔ x - y ∈ U