mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
inst✝ : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact

Tactic:
by
  rw [guitartExact_iff_final]
  intro X₂
  let e : costructuredArrowRightwards (w.whiskerHorizontal α.inv β.hom) X₂ ≅
      w.costructuredArrowRightwards X₂ ⋙ (CostructuredArrow.mapIso (β.app X₂)).functor :=
    NatIso.ofComponents (fun f ↦ CostructuredArrow.isoMk (α.symm.app f.left))
  rw [Functor.final_natIso_iff e]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact

Tactic:
← guitartExact_op_iff,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔ w.GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
← guitartExact_op_iff,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w ≫ₕ w'.hom).op.GuitartExact ↔ w.GuitartExact
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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

pp: 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

Tactic:
· simp at hnm

Goal state after:
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.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi (P.π.f (n✝ + 1))

Tactic:
· rw [π_f_succ]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ P.iso.inv ≫ (projectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv

Tactic:
by
  apply HomotopyCategory.eq_of_homotopy
  apply liftHomotopy f
  all_goals
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ

Tactic:
dsimp
    rw [← cancel_epi (P.isoLeftDerivedToHomotopyCategoryObj F).inv, Iso.inv_hom_id_assoc,
      isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc f P Q φ comm F,
      Iso.inv_hom_id, comp_id]

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₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
⊢ tensorHom e.hom e'.hom ≫ tensorHom e.inv e'.inv = 𝟙 (tensorObj X₁ Y₁)

Tactic:
simp [tensorHom_comp_tensorHom]

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₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
⊢ tensorHom e.inv e'.inv ≫ tensorHom e.hom e'.hom = 𝟙 (tensorObj X₂ Y₂)

Tactic:
simp [tensorHom_comp_tensorHom]

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
n : ℤ
h : IsZero ((X.H n).obj (mk₁ f))
⊢ 𝟙 (X.opcycles f g n) = 0

Tactic:
← cancel_epi (X.pOpcycles ..)

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₁ f))
⊢ X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n) = X.pOpcycles f g n ≫ 0
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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact

Tactic:
by
  obtain rfl : n₀ = n₁ - 1 := by lia
  apply ShortComplex.exact_cokernel

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

Tactic:
constructor <;> lia

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.IsFirstQuadrant
⊢ ∀ (r r' : ℤ) (pq : ℕ × ℕ),
    (∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel pq pq') →
      ∀ (n : ℤ),
        n = coreE₂CohomologicalNat.deg pq + 1 →
          ∀ (hrr' : autoParam (r + 1 = r') HasSpectralSequence._auto_1)
            (hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3), IsZero ((Y.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
    apply isZero₁_of_isFirstQuadrant
    simp only [coreE₂CohomologicalNat_i₀, WithBotTop.coe_le_coe]
    by_contra!
    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p + r by lia)
    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + 1 - r by lia)
    exact hpq ⟨p', q'⟩ (by constructor <;> lia)

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.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 <;> lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hβ : β = homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map α

Tactic:
by
  obtain rfl : α = homMk₁ (β.app 1) (β.app 2) (naturality' β 1 2) := by
    subst hβ
    exact hom_ext₁ rfl rfl
  exact (ShortComplex.LeftHomologyMapData.ofZeros
    (X.shortComplexMap _ _ _ _ _ _ β n₀ n₁ n₂ hn₁ hn₂) ..).homologyMap_comm

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 (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 <;> lia

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 <;> lia

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

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ = -⁅x, m⁆

Tactic:
by
  rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
  simp

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

Goal state before:
pp: case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
toLieHom✝¹ : L₁ →ₗ⁅R⁆ L₂
invFun✝¹ : L₂ → L₁
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieHom✝¹).toFun
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₁ :
  (↑{ toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toLieHom).toFun =
    (↑{ toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toLieHom).toFun
h₂ :
  { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simp at h₁ h₂

Goal state after:
case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
toLieHom✝¹ : L₁ →ₗ⁅R⁆ L₂
invFun✝¹ : L₂ → L₁
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieHom✝¹).toFun
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₂ : invFun✝¹ = invFun✝
h₁ : toLieHom✝¹ = toLieHom✝
⊢ { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
            right_inv := right_inv✝¹ }.toLieModuleHom).toFun =
    (↑{ toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝,
            right_inv := right_inv✝ }.toLieModuleHom).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simp at h₁ h₂

Goal state after:
case mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₂ : invFun✝¹ = invFun✝
h₁ : toLieModuleHom✝¹ = toLieModuleHom✝
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ R ∙ x

Tactic:
LinearMap.span_singleton_eq_range

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ (LinearMap.toSpanSingleton R R x).range
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ x ∈ N, I x = ⊥
⊢ N = ⊥

Tactic:
rw [← this, ← le_bot_iff, Ideal.mul_le]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ x ∈ N, I x = ⊥
⊢ ∀ r ∈ Jac ^ n, ∀ s ∈ N, r * 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
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
h :
  (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝

Tactic:
exact SetLike.coe_injective h

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

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

Tactic:
rw [mul_add]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * (a + b) + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [mul_add]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * a + a * b + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [mul_add]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * a + a * b + a * c + (b * (a + b) + b * c) + c * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [mul_add]

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * a + a * b + a * c + (b * a + b * b + b * c) + c * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
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:
by
      suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
      exact K₂.lie_mem hx hy

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

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

Tactic:
rw [mul_add]

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