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
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ (ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p', q') (p, q)

Tactic:
constructor

Goal state after:
case left
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
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').1 + (r, 1 - r).1 = ↑(p, q).1

case right
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
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : ↑q + r - 1 ≤ ↑p + ↑q - 1
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q - 1 + r = ↑q'
⊢ ↑(p', q').2 + (r, 1 - r).2 = ↑(p, q).2
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) (p', q')

Tactic:
constructor

Goal state after:
case left
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).1 + (-r, r - 1).1 = ↑(p', q').1

case right
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
this : -↑p - ↑q + 1 < -↑q - r + 2
p' : ℕ
hp' : ↑p - r = ↑p'
q' : ℕ
hq' : ↑q + r - 1 = ↑q'
⊢ ↑(p, q).2 + (-r, r - 1).2 = ↑(p', q').2
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₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.fromOpcycles f (𝟙 i₁) f ⋯ n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = 𝟙 (X.opcycles f (𝟙 i₁) n₁)

Tactic:
by
  simpa using (X.opcyclesIsoH f n₀ n₁ hn₁).hom_inv_id

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ (ComplexShape.spectralSequenceNat (-r, r - 1)).Rel (p', q') (p, q)

Tactic:
constructor

Goal state after:
case left
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p', q').1 + (-r, r - 1).1 = ↑(p, q).1

case right
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
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (-r, r - 1)).Rel pq' (p, q)
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_11
this : -↑q + r - 1 ≤ 0
p' : ℕ
hp' : ↑p + r = ↑p'
q' : ℕ
hq' : ↑q + 1 - r = ↑q'
⊢ ↑(p', q').2 + (-r, r - 1).2 = ↑(p, q).2
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ h.π ≫ (X.homologyDataIdId f (n₁ - 1) n₁ n₂ ⋯ ⋯).left.homologyIso.inv =
    h.π ≫ X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
h.π_comp_homologyIso_inv

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ h.cyclesIso.inv ≫ (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).homologyπ =
    h.π ≫ X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
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).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''
⊢ i₀' = data.i₁ pq''

Tactic:
simpa [← data.i₀_prev r r' _ _ h]

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

Goal state before:
pp: case e_a
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₂
⊢ 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) ⋯ =
    homMk₁ (β.app 0) (β.app 1) ⋯ ≫
      homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯

Tactic:
ext

Goal state after:
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

case 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) ⋯)
      1 homMk₁._proof_5 =
    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) ⋯)
      1 homMk₁._proof_5
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
y z : L
n : M
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
        { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ })
      n

Tactic:
exact add_lie y z n

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

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₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x
h₃ :
  ∀ {x y : L₁},
    { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
        { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆
⊢ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f

Tactic:
ext

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₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x
h₃ :
  ∀ {x y : L₁},
    { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
        { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆
x✝ : L₁
⊢ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } x✝ = f x✝
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup 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)
m : ℕ
hm : n ≤ m
x : M
⊢ (f ^ m) x ∈ range (f ^ n)

Tactic:
hn _ hm

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup 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)
m : ℕ
hm : n ≤ m
x : M
⊢ (f ^ m) x ∈ range (f ^ m)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
⊢ IsUnit.submonoid R = R⁰

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
⊢ IsUnit.submonoid R = R⁰

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
⊢ IsUnit.submonoid R = nonZeroDivisorsRight R

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsRight R
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
⊢ IsUnit.submonoid R = nonZeroDivisorsLeft R

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsLeft R
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ ∃ b, x * b = 1

Tactic:
rw [mul_eq_zero, sub_eq_zero] at hy

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y = 1
⊢ ∃ b, x * b = 1
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₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
hn₁ : data.deg pq' - 1 + 1 = data.deg pq'
hn₂ : data.deg pq' + 1 = data.deg pq' + 1
⊢ (X.spectralSequence data).iso r r' pq' ⋯ ⋯ =
    ((X.spectralSequence data).page r ⋯).homologyIsoSc' ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯ ≪≫
      (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯ (data.i₀ r' pq' ⋯)
              (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯).left.homologyIso ≪≫
        (X.spectralSequencePageXIso data r' ⋯ pq' (data.i₀ r' pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r' pq' ⋯) ⋯ ⋯
            ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯).symm

Tactic:
ext

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₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
hn₁ : data.deg pq' - 1 + 1 = data.deg pq'
hn₂ : data.deg pq' + 1 = data.deg pq' + 1
⊢ ((X.spectralSequence data).iso r r' pq' ⋯ ⋯).hom =
    (((X.spectralSequence data).page r ⋯).homologyIsoSc' ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯ ≪≫
        (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯ (data.i₀ r' pq' ⋯)
                (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯).left.homologyIso ≪≫
          (X.spectralSequencePageXIso data r' ⋯ pq' (data.i₀ r' pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r' pq' ⋯) ⋯
              ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯).symm).hom
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case refine_1
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
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
⊢ x = 0

Tactic:
replace hx : toEnd R L M x = 0 := by ext m; simpa using hx m
    simpa using hx

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₂
⊢ Function.Surjective ⇑f.rangeRestrict

Tactic:
rintro ⟨y, hy⟩
  rw [mem_range] at hy; obtain ⟨x, rfl⟩ := hy
  use x
  simp only [rangeRestrict_apply]

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
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
constructor

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p
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₂
hf : Function.Injective ⇑f
x y : ↥K
⊢ (↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun ⁅x, y⁆ =
    ⁅(↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun x,
      (↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun y⁆

Tactic:
ext

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₂
hf : Function.Injective ⇑f
x y : ↥K
⊢ ↑((↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun ⁅x, y⁆) =
    ↑⁅(↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun x,
        (↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun y⁆
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₂
⊢ f.range = map f ⊤

Tactic:
ext

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₂
x✝ : L₂
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤
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₂
S : Set (LieSubalgebra R L)
x y : L
hx : x ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier
hy : y ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier
⊢ ⁅x, y⁆ ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier

Tactic:
simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_ofPred_eq,
          forall_apply_eq_imp_iff₂, exists_imp, and_imp] at hx hy ⊢

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx : ∀ a ∈ S, x ∈ ↑a.toSubmodule
hy : ∀ a ∈ S, y ∈ ↑a.toSubmodule
⊢ ∀ a ∈ S, ⁅x, y⁆ ∈ ↑a.toSubmodule
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
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ (toEnd R L M₂) x ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x

Tactic:
ext

Goal state after:
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
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
x✝ : M
⊢ ((toEnd R L M₂) x ∘ₗ ↑f) x✝ = (↑f ∘ₗ (toEnd R L M) x) 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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) ↔ ↑x ∈ K

Tactic:
constructor

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) → ↑x ∈ K

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ ↑x ∈ K → ∃ 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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ ofLe h = comap K'.incl K

Tactic:
ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x✝ : ↥K'
⊢ x✝ ∈ ofLe h ↔ x✝ ∈ comap K'.incl K
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

Goal state after:
case mp
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

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
K : LieSubalgebra R L
⊢ s ⊆ ↑K → lieSpan R L s ≤ K
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
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
constructor

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → (lieSpan R L ↑p).toSubmodule = p