mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
refine fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ f.coeff n ∈ comap C I
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 : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
⊢ (∑ x_1, (monomial ↑x_1) (g x_1)).degree < (minpoly K x).degree

Tactic:
simp_rw [← C_mul_X_pow_eq_monomial]
    exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case h
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_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
⊢ (detAux (Trunc.mk b)) f = ((toMatrix b' b') f).det

Tactic:
detAux_def',

Goal state after:
case h
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_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
⊢ ((toMatrix b b) f).det = ((toMatrix b' b') f).det
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
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
by
  have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩
  rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ b]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : ¬Nontrivial R
⊢ M ≃ₗ[R] M

Tactic:
exact 1

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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((e.toMatrix v)ᵀ.updateRow i ⇑(e.repr (v j))).det = 0

Tactic:
← e.toMatrix_transpose_apply

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mpr
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
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤

Tactic:
have : ⇑v' = v := by
      ext i
      rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]

Goal state after:
case mpr
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
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : ⇑v' = v
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₀
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
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
⊢ j ≠ i → (monomial ↑j) (Pi.single i 1 j) = 0

Tactic:
hj

Goal state after:
case h₀
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
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ (monomial ↑j) (Pi.single i 1 j) = 0
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
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
let e : Submodule R[X] (AEval' (f.restrict hp)) ≃o Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
    (Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans
      (Submodule.mapIic _)
  simp_rw [IsSemisimple, isSemisimpleModule_iff, e.complementedLattice_iff, disjoint_iff,
    ← (OrderIso.Iic _ _).complementedLattice_iff, Iic.complementedLattice_iff, Subtype.forall,
    Subtype.exists, Subtype.mk_le_mk, Sublattice.mk_inf_mk, Sublattice.mk_sup_mk, Subtype.mk.injEq,
    exists_and_left, exists_and_right, invtSubmodule.mk_eq_bot_iff, exists_prop, and_assoc]
  rfl

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:
rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]
    simp only [Function.iterate_succ_apply', ih, map_sum, map_nsmul, apply_lie_eq_add, smul_add,
      sum_add_distrib, add_right_inj]
    refine sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_
    rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]

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

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
inst✝ : LieModule R L M
I J : LieIdeal R L
⊢ L ⧸ I → L ⧸ I → L ⧸ I

Tactic:
by
    intro x y
    apply Quotient.liftOn₂' x y fun x' y' => mk ⁅x', y'⁆
    intro x₁ x₂ y₁ y₂ h₁ h₂
    apply (Submodule.Quotient.eq I.toSubmodule).2
    rw [Submodule.quotientRel_def] at h₁ h₂
    have h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ := by
      simp [-lie_skew, sub_eq_add_neg, add_assoc]
    rw [h]
    apply Submodule.add_mem
    · apply lie_mem_right R L I x₁ (x₂ - y₂) h₂
    · apply lie_mem_left R L I (x₁ - y₁) y₂ h₁

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ (exp D) (x * y) = (exp D) x * (exp D) y

Tactic:
have h₁ : exp D (x * y) = m (exp (DL + DR) (x ⊗ₜ[R] y)) := by
    suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using! LinearMap.congr_fun this (x ⊗ₜ[R] y)
    apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil
    ext
    simp [DL, DR, hm, h_der]

Goal state after:
R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ : (exp D) (x * y) = m ((exp (DL + DR)) (x ⊗ₜ[R] y))
⊢ (exp D) (x * y) = (exp D) x * (exp D) y
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L k ≤ ⊤

Tactic:
simp only [le_top]

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

Goal state before:
pp: L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k : ℕ
hk : lowerCentralSeries ℤ L M k = ⊥
⊢ s.Nonempty

Tactic:
exact ⟨k, hk⟩

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E

Tactic:
apply eq_of_le_of_finrank_le h_le

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ finrank K ↥E ≤ finrank K ↥F
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s : Finset F
⊢ LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s

Tactic:
have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'
  conv_lhs =>
    rw [Finset.sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  change
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ finrank (↥(subfield G F)) F ≤ Fintype.card G

Tactic:
by
  rw [← @Nat.cast_le Cardinal, finrank_eq_rank]
  apply rank_le_card

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
⊢ (adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

Tactic:
have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits ↔ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
refine ⟨?_, IntermediateField.splits_of_splits h⟩

Goal state after:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits → ∀ x ∈ p.rootSet L, x ∈ F
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
exact Set.union_subset
      (fun x hx ↦ Subfield.subset_closure <| .inl ⟨⟨x, Subfield.subset_closure (.inr hx)⟩, rfl⟩)
      (fun x hx ↦ Subfield.subset_closure <| .inr hx)

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ (σ a).Nonempty

Tactic:
exact ⟨k, hk⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, f.HasEigenvalue c

Tactic:
simp_rw [hasEigenvalue_iff_mem_spectrum]

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ (aeval a) (x * w✝¹) = 0 ∧ (aeval a) (x * w✝) = 0

Tactic:
simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
have : Nontrivial V := finrank_pos_iff.1 (by rw [h_dim]; apply Nat.zero_lt_succ)

Goal state after:
case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → y ∉ {ϕ | ϕ.IsExtendible}
⊢ False

Tactic:
Set.mem_ofPred,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ¬y.IsExtendible
⊢ False
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : ↑{α} ⊆ ↑θ.carrier ∧ ↑(Finset.univ.biUnion S) ⊆ ↑θ.carrier
⊢ False

Tactic:
Finset.coe_singleton,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : {α} ⊆ ↑θ.carrier ∧ ↑(Finset.univ.biUnion S) ⊆ ↑θ.carrier
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := ⋯
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
⊢ finrank (↥K⟮(aeval (root p)) g⟯) Kx = (minpoly (↥K⟮(aeval (root p)) g⟯) (root p)).natDegree

Tactic:
have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝¹ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this✝ : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
this : (↥K⟮(aeval (root p)) g⟯)⟮root p⟯ = ⊤
⊢ finrank (↥K⟮(aeval (root p)) g⟯) Kx = (minpoly (↥K⟮(aeval (root p)) g⟯) (root p)).natDegree