mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
    ((P.isoLeftDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙
                HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
            g ≫
          (Q.isoLeftDerivedObj F n).inv) ≫
      (Q.isoLeftDerivedObj F n).hom

Tactic:
ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,

Goal state after:
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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        g =
    ((P.isoLeftDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙
                HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
            g ≫
          (Q.isoLeftDerivedObj F n).inv) ≫
      (Q.isoLeftDerivedObj F n).hom

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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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

Tactic:
dsimp
    rw [hβ₀]
    exact naturality' α 0 1

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂'✝ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
obtain ⟨A₁, π₁, _, x₁, hx₁⟩ :=
    ((X.sequenceΨ_exact f₂ f₃ f₄ _ rfl f₃₄ h₃₄ n₁ n₂).exact 1).exact_up_to_refinements
      (x₂ ≫ X.ιE ..) (by simp [sequenceΨ, Precomp.map, hx₂'])

Goal state after:
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₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂'✝ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
x₁ : A₁ ⟶ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ = x₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
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₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom = (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia
  simp [πE, cyclesIsoH, EIsoH]

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
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).toNat l

Tactic:
Fin.clamp_eq_last _ _ (by lia),

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.last l = Fin.clamp (↑q + r).toNat l
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:
by
    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.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ EventuallyConst p l ↔ (p =ᶠ[l] fun x ↦ False) ∨ p =ᶠ[l] fun x ↦ True

Tactic:
by
  simp only [eventuallyConst_iff_exists_eventuallyEq, Prop.exists_iff]

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

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

Tactic:
have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0 := by rw [← lie_add]; apply lie_self
  simpa [neg_eq_iff_add_eq_zero] using h

Goal state after:
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 • ⁅x, y⁆

Tactic:
LieRing.of_associative_ring_bracket,

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

Tactic:
LieRing.of_associative_ring_bracket,

Goal state after:
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)
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = ⇑e
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆

Tactic:
LieRing.of_associative_ring_bracket,

Goal state after:
R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = ⇑e
⊢ e.toFun (x * y - y * x) = e.toFun x * e.toFun y - e.toFun y * e.toFun 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
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
s : Set L
⊢ map f (lieSpan R L s) = lieSpan R L₂ (⇑f '' s)

Tactic:
refine le_antisymm ?_ (lieSpan_le.mpr <| Set.image_mono subset_lieSpan)
  rw [map_le_iff_le_comap, lieSpan_le]
  change s ⊆ f ⁻¹' (lieSpan R L₂ (f '' s))
  exact image_subset_iff.mp <| subset_lieSpan

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
⊢ ↑{ toSubmodule := p, lie_mem := h } = p

Tactic:
by cases p; rfl

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 + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (c * a) + L (c * b) + L (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)⁆

Tactic:
mul_comm c a,

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (a * c) + L (c * b) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (a * c) + 2 • L (b * c)⁆
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
S : Set (LieSubmodule R L M)
⊢ sSup (toSubmodule '' S) = ⨆ N ∈ S, ↑N

Tactic:
sSup_image

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ⨆ a ∈ S, ↑a = ⨆ N ∈ S, ↑N
Module: Mathlib.Algebra.Lie.Abelian

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
x : L
⊢ x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0

Tactic:
simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    toEnd_apply_apply]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
x : L
m : M
hm : m ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
y : L
⊢ ⁅y, ⁅x, m⁆⁆ = 0

Tactic:
by rw [hm, lie_zero]

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

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

Tactic:
by
  have h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆ := by
    rw [sup_le_iff]; constructor <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_right]
  suffices ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆ by exact le_antisymm this h
  rw [lieIdeal_oper_eq_span, lieSpan_le]
  rintro m ⟨x, ⟨n, hn⟩, h⟩
  simp only [SetLike.mem_coe]
  rw [LieSubmodule.mem_sup] at hn ⊢
  rcases hn with ⟨n₁, hn₁, n₂, hn₂, hn'⟩
  use ⁅(x : L), (⟨n₁, hn₁⟩ : N)⁆; constructor; · apply lie_coe_mem_lie
  use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆; constructor; · apply lie_coe_mem_lie
  simp [← h, ← hn']

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0

Tactic:
· exact aeval_zero _

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ degree 1
⊢ minpoly A x = 1

Tactic:
rw [degree_one] at this

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
ha : (Polynomial.aeval x) a = 0
⊢ a.natDegree < (minpoly A x).natDegree

Tactic:
obtain ⟨_, c, hu, he⟩ := hdvd

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ a.natDegree < (minpoly A x).natDegree
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Tactic:
rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ minpoly K σ.toLinearMap = X ^ orderOf σ - C 1

Tactic:
have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by
    rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
    exact (AlgEquiv.algHomUnitsEquiv K L).injective
  rw [this, ← minpoly_algEquiv_toLinearMap]
  · apply congr_arg
    ext
    simp
  · rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Free R S
n : ℕ
⊢ (norm R) ↑n = ↑n ^ finrank R S

Tactic:
rw [← map_natCast (algebraMap R S), Algebra.norm_algebraMap]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

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

Tactic:
have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X ^ n - C 0) = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
⊢ x ^ n ∣ x

Tactic:
by
  by_cases hu : IsUnit x
  · exact (hu.pow n).dvd
  · rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl <;> simp

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

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Goal state after:
case mul.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

case mul.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : ¬p ∣ y
⊢ Squarefree (p * y)

Tactic:
exact squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = ((toMatrix b b) f).det

Tactic:
← det_toMatrix (b.map e),

Goal state after:
case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ ((toMatrix (b.map e) (b.map e)) (↑e ∘ₗ f ∘ₗ ↑e.symm)).det = ((toMatrix b b) f).det
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map ⇑(iterateFrobeniusEquiv R p n).symm {y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
Multiset.map_singleton,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (Polynomial.map (of f) f).IsRoot (root f)

Tactic:
rw [IsRoot, eval_map, eval₂_root]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = ((LinearMap.toMatrix e e) f).det * (e.toMatrix v).det

Tactic:
← Matrix.det_mul,

Goal state after:
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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = ((LinearMap.toMatrix e e) f * e.toMatrix v).det
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q

Tactic:
IsSemisimple,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ IsSemisimpleModule R[X] (AEval' f) ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
IsSemisimple,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp)) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ f.IsSemisimple ↔ g.IsSemisimple

Tactic:
IsSemisimple,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ IsSemisimpleModule R[X] (AEval' f) ↔ IsSemisimpleModule R[X] (AEval' g)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)

Tactic:
e.isSemisimple_iff ((LinearMap.restrict f hp).restrict hq₁) (LinearMap.restrict f this) rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple (LinearMap.restrict f this)