mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w.hComp' w' eT eB).GuitartExact

Tactic:
dsimp only [TwoSquare.hComp']

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₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ ((w ≫ₕ w').whiskerHorizontal eT.inv eB.hom).GuitartExact
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
⊢ IsZero ((K.stupidTrunc e).X i')

Tactic:
by_cases hi'' : ∃ i, e.f i = i'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ IsZero ((K.stupidTrunc e).X i')
Module: Mathlib.Algebra.Homology.Embedding.Connect

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

Tactic:
obtain _ | n := n

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

case 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 n : ℕ
hnm : Int.negSucc (n + 1) + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc (n + 1)) (Int.ofNat m) = 0
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy
    (if hj : ∃ k, c.Rel j k then double (𝟙 X) ⋯ else (single C c j).obj X)

Tactic:
split_ifs with h

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy (double (𝟙 X) ⋯)

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c j).obj X)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.sc₂ f g fg h n₀).Exact

Tactic:
by
  subst h
  exact (X.exact₂' n₀ (mk₂ f g)).exact 0

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

Goal state before:
pp: case h₂
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₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₂

Tactic:
dsimp
    convert! (inferInstance : IsIso ((X.H n₁).map (𝟙 _)))
    cat_disch

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
z₀ :
  A✝ ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A✝
w✝ : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
⊢ z₁ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).g = 0

Tactic:
dsimp
    have H := X.p_opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) (𝟙 _) n₁ (by cat_disch)
    rw [Functor.map_id, id_comp] at H
    rw [← H, ← reassoc_of% hz₁, hz₀, comp_zero]

Goal state after:
Module: Mathlib.Order.Filter.Subsingleton

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

Tactic:
rcases eq_or_neBot l with rfl | hbot

Goal state after:
case inl
α : Type u_1
inst✝ : Nonempty α
⊢ ⊥.Subsingleton ↔ ∃ a, ⊥ ≤ pure a

case inr
α : Type u_1
l : Filter α
inst✝ : Nonempty α
hbot : l.NeBot
⊢ l.Subsingleton ↔ ∃ a, l ≤ pure a
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.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]

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.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).Exact
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
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : ↥s), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : ↥s) → M ⧸ ↑↑m := LinearMap.pi fun m ↦ (↑↑m).mkQ
x : M
hx : x ∈ f.ker
⊢ x ∈ ⊥

Tactic:
rw [← h, Module.jacobson, Submodule.mem_sInf]

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
h : Module.jacobson R M = ⊥
s : Finset { m // IsCoatom m }
hs : ∀ (a : { m // IsCoatom m }), s.inf Subtype.val ≤ ↑a
x✝ : ∀ (m : ↥s), IsSimpleModule R (M ⧸ ↑↑m)
f : M →ₗ[R] (m : ↥s) → M ⧸ ↑↑m := LinearMap.pi fun m ↦ (↑↑m).mkQ
x : M
hx : x ∈ f.ker
⊢ ∀ p ∈ {m | IsCoatom m}, x ∈ p
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 y : M
hy : (f ^ m) ((f ^ n) y) = (f ^ m) x
⊢ x - (f ^ n) y ∈ (f ^ m).ker

Tactic:
by simp [hy]

Goal state after:
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 ≤ (LinearMap.toSpanSingleton R R x).range

Tactic:
exact LinearMap.map_le_range

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'
⊢ f.idealRange = LieIdeal.map f ⊤

Tactic:
by
  ext
  simp only [idealRange, range_eq_map]
  rfl

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

Goal state before:
pp: 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
⊢ range f ⊆ ↑(comap K.incl (lieSpan R L (range (Subtype.val ∘ f))))

Tactic:
rintro - ⟨i, rfl⟩

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
i : ι
⊢ f i ∈ ↑(comap K.incl (lieSpan R L (range (Subtype.val ∘ f))))
Module: Mathlib.Algebra.Lie.Abelian

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₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅f u, y⁆ = 0

Tactic:
obtain ⟨v, rfl⟩ := h₁ y

Goal state after:
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₂
h₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅f u, f v⁆ = 0
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'
J₁ J₂ : LieIdeal R L'
⊢ ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆

Tactic:
by
  rw [← map_le_iff_le_comap]
  exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

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

Tactic:
mem_bot,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ x - y = 0 ↔ x = y
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
by
    rw [comap_bracket_incl]; rw [← inf_eq_right] at h₁ h₂; rw [h₁, h₂]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
unfold minpolyGen

Goal state after:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (X ^ pb.dim - ∑ i, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree = ↑pb.dim
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
split_ifs with h

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ Subalgebra.toSubmodule R[B.gen] = ⊤

Tactic:
_root_.eq_top_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ ⊤ ≤ Subalgebra.toSubmodule R[B.gen]
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ R[x]
⊢ R[x] = ⊤

Tactic:
_root_.eq_top_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ R[x]
⊢ ⊤ ≤ R[x]
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
by
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
  rintro rfl
  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) (derivative (X + C a))

Tactic:
derivative_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) (derivative X + derivative (C a))
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f (a * p + b * derivative p) = 1

Tactic:
H,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f 1 = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hMM'
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ c.toMatrix ⇑b * b.toMatrix ⇑c = 1

Tactic:
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hM'M
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ b.toMatrix ⇑c * c.toMatrix ⇑b = 1

Tactic:
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
rw [iterateFrobeniusEquiv_eq_pow]

Goal state after:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
⊢ f.roots.Nodup ↔ f.Separable

Tactic:
classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((f i₂) (if i₂ = j₂ then b j₁ else 0))) i₁ = if i₂ = j₂ then (b.repr ((f i₂) (b j₁))) i₁ else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : i₂ = j₂
⊢ (b.repr ((f i₂) (b j₁))) i₁ = (b.repr ((f i₂) (b j₁))) i₁

case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : ¬i₂ = j₂
⊢ (b.repr ((f i₂) 0)) i₁ = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g

Tactic:
rw [sub_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ (ad R A) a * (ad R A) b - (ad R A) b * (ad R A) a = 0

Tactic:
← Ring.lie_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ ⁅(ad R A) a, (ad R A) b⁆ = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ (algEquivOfAssociated R f g hfg) (root f) = root g

Tactic:
rw [coe_algEquivOfAssociated, algHomOfDvd_root]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (toAdjoin R x).range = ⊤

Tactic:
_root_.eq_top_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ ⊤ ≤ (toAdjoin R x).range
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
i k : m
⊢ (toMatrix b b) e (Sum.inl i) (Sum.inl k) = fromBlocks A B 0 D (Sum.inl i) (Sum.inl k)

Tactic:
| inl k =>

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ span {(Ideal.Quotient.mk (Ideal.map C I)) f} =
    Ideal.map (↑I.polynomialQuotientEquivQuotientPolynomial) (span {Polynomial.map (Ideal.Quotient.mk I) f})

Tactic:
by
      rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f]

Goal state after: