mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : ¬c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

Tactic:
· simp only [leftUnitor'_inv, assoc, mapBifunctor.d_eq,
      Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
      unit_tensor_d₁, comp_zero, zero_add]
    rw [mapBifunctor.d₂_eq _ _ _ _ _ hij _ (by simp)]
    dsimp
    simp only [ComplexShape.ε_zero, one_smul, ← whisker_exchange_assoc,
      id_whiskerLeft, assoc, Iso.inv_hom_id_assoc]

Goal state after:
case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : ¬c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯ ≫ (X.H n₂).map (𝟙 (mk₁ f))
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0

Tactic:
rw [Functor.map_id, comp_id] at eq

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
⊢ X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0
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₃
⊢ Mono (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₃

Tactic:
dsimp
    convert! (inferInstance : Mono ((X.H n₃).map (𝟙 (mk₁ f₁))))
    cat_disch

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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26
⊢ ⟨(↑↑(a, ⟨a', isLt✝⟩).2 - (r' - 2)).toNat, ⋯⟩ ≤ ⟨(↑↑(a, ⟨a', isLt✝⟩).2 - (r - 2)).toNat, ⋯⟩

Tactic:
rw [Fin.mk_le_mk]

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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_24
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_26
⊢ (↑↑(a, ⟨a', isLt✝⟩).2 - (r' - 2)).toNat ≤ (↑↑(a, ⟨a', isLt✝⟩).2 - (r - 2)).toNat
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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_34
⊢ Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r - 1)).toNat l ≤ Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r' - 1)).toNat l

Tactic:
rw [Fin.mk_le_mk]

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₀ : ℤ
l : ℕ
r r' a : ℤ
a' : ℕ
isLt✝ : a' < l
hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32
hrr' : autoParam (r ≤ r') SpectralSequenceDataCore._auto_34
⊢ ↑(Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r - 1)).toNat l) ≤ ↑(Fin.clamp (↑↑(a, ⟨a', isLt✝⟩).2 + (r' - 1)).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
E : SpectralObject C EInt
r r' : ℤ
pq : ℤ × ℤ
hpq : ∀ (pq' : ℤ × ℤ), ¬(ComplexShape.up' (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = coreE₂Cohomological.deg pq - 1
hrr' : r + 1 = r'
hr : 2 ≤ r
⊢ IsZero ((E.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
exfalso
    exact hpq (pq - (r, 1 - r)) (by simp)

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

Goal state before:
pp: case refine_1
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

Tactic:
exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r : ℤ
hr : r₀ ≤ r
pq : κ
n : ℤ
hn : n = data.deg pq
i₁ i₂ : ι
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h : IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))
⊢ IsZero (((X.spectralSequence data).page r ⋯).X pq)

Tactic:
X.isZero_spectralSequence_page_X_iff data r hr pq
    _ i₁ i₂ _ rfl h₁ h₂ rfl (n - 1) n (n + 1) hn

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 : ℤ
hr : r₀ ≤ r
pq : κ
n : ℤ
hn : n = data.deg pq
i₁ i₂ : ι
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h : IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))
⊢ IsZero (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n - 1) n (n + 1) ⋯ ⋯)
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieRing L'
inst✝⁹ : LieAlgebra R L'
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : LieRingModule L M'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier
this : ⁅f x, f y⁆ ∈ J
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
by
        simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          Submodule.mem_toAddSubmonoid, Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie,
          LieSubalgebra.mem_toSubmodule]
        exact this

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
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : x ∈ span R s
hy : y ∈ span R s
⊢ ⁅x, y⁆ ∈ span R s

Tactic:
induction hx, hy using span_induction₂ with

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'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
rw [f.idealRange_eq_map]

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'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤
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'
I : LieIdeal R L
⊢ I ≤ f.ker ↔ ∀ x ∈ I, f x = 0

Tactic:
constructor <;> intro h x hx

Goal state after:
case mp
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'
I : LieIdeal R L
h : I ≤ f.ker
x : L
hx : x ∈ I
⊢ f x = 0

case mpr
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'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ x ∈ f.ker
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
rw [lieIdeal_oper_eq_linear_span]

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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
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 J : LieIdeal R L
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
suffices ∀ I J : LieIdeal R L, ⁅I, J⁆ ≤ ⁅J, I⁆ by exact le_antisymm (this I J) (this J I)

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
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 J : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⁅J, I⁆

Tactic:
rintro x ⟨y, z, h⟩

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ x ∈ ↑⁅J, I⁆
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 t : Set M
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)

Tactic:
exact Subset.trans h subset_lieSpan

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ I
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0

Tactic:
by
    rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
    simp only [this, C_0]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : ∑ x_1, (algebraMap K S) (g x_1) * x ^ ↑x_1 = 0
⊢ g i = 0

Tactic:
← aeval_monomial,

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : ∑ x_1, (aeval x) ((monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
    (Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

Tactic:
rw [Ideal.Quotient.lift_mk] at hp hq ⊢

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) p) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) q) =
    (Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) (p + q)) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p + q)
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_cases hu : IsUnit x

Goal state after:
case pos
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

case neg
R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
⊢ x ^ n ∣ x
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N).det = (N * M).det

Tactic:
nontriviality A
  -- Although `m` and `n` are different a priori, we will show they have the same cardinality.
  -- This turns the problem into one for square matrices, which is easy.
  let e := indexEquivOfInv hMM' hM'M
  rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis (↥s) A M), P ((toMatrix b b) f).det
h1 : P 1
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ P (LinearMap.det f)

Tactic:
rwa [LinearMap.det_def, dif_neg H]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
by
  replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
  induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih
  rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
  · refine ⟨0, f, h, ?_⟩
    rw [pow_zero, expand_one]
  · rcases N with - | N
    · rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
      rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
      have hf0 : f ≠ 0 := hf.ne_zero
      rw [h1, C_0] at hn
      exact absurd hn hf0
    have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
    have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
    have hg3 : g.natDegree < N.succ := by
      rw [← mul_one g.natDegree, ← hg1]
      exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
    rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
    refine ⟨n + 1, g, hg4, ?_⟩
    rw [← hgf, expand_expand, pow_succ']

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
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
⊢ Module.Finite R M

Tactic:
simp [finite_of_det_ne_one (f := f), hf]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case e'_3.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p

Tactic:
apply pow_one

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p

Tactic:
apply pow_one

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ p ^ 1 = p

Tactic:
apply pow_one

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
· rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
· rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
    rw [eq_comm]
    apply eq_of_monic_of_associated p_monic _ p_gen
    apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
⊢ IsUnit (e.det v)

Tactic:
set v' := Basis.mk hli hspan.ge

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli ⋯
⊢ IsUnit (e.det v)
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.det f * (e.toMatrix v).det

Tactic:
← f.det_toMatrix e,

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).det * (e.toMatrix v).det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ p✝ %ₘ g - p✝

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ p✝ - g * (p✝ /ₘ g) - p✝
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
g : R[X]
hg : g.Monic
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ f - f %ₘ g

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ f - (f - g * (f /ₘ g))
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 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)
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)

Tactic:
let B : Matrix m n R := Matrix.of fun i l ↦
    ((sumQuot bW bQ).repr (e ((sumQuot bW bQ) (Sum.inr l)))) (Sum.inl i)

Goal state after:
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)
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)
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
μ : R
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

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
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p