mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
h : ↑l < ↑q + r
⊢ (coreE₂CohomologicalFin l).i₃ r (p, ⟨q, hq⟩) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯

Tactic:
dsimp

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₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
h : ↑l < ↑q + r
⊢ Fin.clamp (↑q + (r - 1)).toNat l = Fin.clamp (↑q + (r + 1 - 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 ι
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₂
⊢ Mono (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp

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₂
⊢ Mono (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂)
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'' : κ
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
        (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
      (page X data r hr).d pq' pq'' =
    0

Tactic:
dsimp

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'' : κ
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
        (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
      pageD X data r pq' pq'' ⋯ =
    0
Module: Mathlib.Order.Filter.Subsingleton

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝ : Nonempty α
⊢ l.Subsingleton ↔ ∃ a, {a} ∈ l

Tactic:
simp only [subsingleton_iff_exists_le_pure, le_pure_iff]

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' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (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₂).f

Tactic:
dsimp

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' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ ⋯ ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ ⋯).inv)
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₂
⊢ Mono (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp

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₂
⊢ Mono (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
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₂
⊢ Epi (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g

Tactic:
dsimp

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₂
⊢ Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
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₂
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f =
    (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f ≫
      𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂

Tactic:
dsimp

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₂
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)
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.dKernelSequence (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ n₀ n₁ n₂
          (n₂ + 1) ⋯ ⋯ ⋯).g =
    (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₂).g ≫
      (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯).hom

Tactic:
dsimp

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) ⋯ ⋯ ⋯ =
    pageD X data r pq' pq'' ⋯ ≫
      (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯).hom
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''
this : IsIso (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
⊢ Epi (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₂).f

Tactic:
dsimp

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 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''
this : IsIso (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
⊢ Epi
    (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ ⋯ ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ ⋯).inv)
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' : κ
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'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ (page X data r hr).d pq pq' ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0

Tactic:
dsimp

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' : κ
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'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ pageD X data r pq pq' ⋯ ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0
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' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).g

Tactic:
dsimp

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' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi
    ((pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
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.dCokernelSequence (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
          (have this := homOfLE ⋯;
          this)
          (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯).f =
    (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).f ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom

Tactic:
dsimp

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₂ ⋯ ⋯ ⋯ =
    pageD X data r pq pq' ⋯ ≫ (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
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).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'
this : IsIso (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
⊢ Mono (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).g

Tactic:
dsimp

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 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'
this : IsIso (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
⊢ Mono
    ((pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝² : Ring A
R : Type u
inst✝¹ : CommRing R
inst✝ : Algebra R A
t : R
x y : A
⊢ x * t • y - t • y * x = t • (x * y - y * x)

Tactic:
Algebra.mul_smul_comm,

Goal state after:
A : Type v
inst✝² : Ring A
R : Type u
inst✝¹ : CommRing R
inst✝ : Algebra R A
t : R
x y : A
⊢ t • (x * y) - t • y * x = t • (x * y - y * x)
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
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K

Tactic:
constructor
  · exact Set.Subset.trans subset_lieSpan
  · intro hs m hm
    rw [mem_lieSpan] at hm
    exact hm _ hs

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ ∀ (t : R) (x : L) (m : ↥N), ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
intro t x y; apply SetCoe.ext; apply lie_smul

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

Goal state before:
pp: case left
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
⊢ N ≤ N ⊔ N'

Tactic:
exact le_sup_left

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

Goal state before:
pp: case left
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
⊢ I ≤ I ⊔ J

Tactic:
exact le_sup_left

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
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1

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

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x) p = ↑y
this : y = ∑ i ∈ p.support, p.coeff i • ⟨(aeval x) (X ^ i), ⋯⟩
⊢ ∑ x_1 ∈ p.support, (algebraMap R ↥R[x]) (p.coeff x_1) * ⟨(aeval x) (X ^ x_1), ⋯⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
exact sum_mem fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ (hp i))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) (a.sum fun n a ↦ (monomial n) a) = 0

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (C.comp (Quotient.mk I)) X (a.sum fun n a ↦ (monomial n) a) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (fun n a ↦ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) n (a.coeff n) = 0

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) (a.coeff n)) = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
x : S'
⊢ ((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) x = (AlgHom.id A S') x

Tactic:
obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) ((aeval pb'.gen) f) = (AlgHom.id A S') ((aeval pb'.gen) f)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

pp: case inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y

Tactic:
· exact hu

Goal state after:
case inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
← not_exists

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r