mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : Nonempty m
⊢ (f x).det = x.det

pp: case neg
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).det = x.det

Tactic:
· exact det_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x

Goal state after:
case neg
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).det = x.det
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
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ p ∣ Polynomial.map (↑f.symm) q

Tactic:
by
      simpa [Polynomial.map_map] using map_dvd f.symm.toRingHom h.dvd

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
⊢ Function.LeftInverse ⇑(mk g) ⇑(modByMonicHom hg)

Tactic:
by
  intro f
  induction f using AdjoinRoot.induction_on
  rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div, sub_sub_cancel_left, dvd_neg]
  apply dvd_mul_right

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
x✝ : ℕ
h₂ : x✝ ∈ Ico (nilpotencyClass a) k
⊢ (↑x✝!)⁻¹ • a ^ x✝ = 0

Tactic:
rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

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✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))) =
    (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x

Tactic:
quotAdjoinRootEquivQuotPolynomialQuot_mk_of,

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
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) (C x)) =
    (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_6
S : Type u_7
T : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (tensorAlgEquiv p q h) (1 ⊗ₜ[R] root p) = root q

Tactic:
simp [tensorAlgEquiv]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_6
S : Type u_7
T : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x : S
⊢ (tensorAlgEquiv p q h) (1 ⊗ₜ[R] (of p) x) = (of q) (1 ⊗ₜ[R] x)

Tactic:
simp [tensorAlgEquiv]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_6
L : Type u_7
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

Tactic:
have h := hf.ne_zero

Goal state after:
K : Type u_6
L : Type u_7
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case inl
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : x = f
⊢ f ∈ ↑φ.range

pp: case inr
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : x ∈ {g}
⊢ g ∈ ↑φ.range

Tactic:
· exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩

Goal state after:
case inr
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : x ∈ {g}
⊢ g ∈ ↑φ.range
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))

Tactic:
rw [← sub_sub_sub_cancel_right r₂ r₁ x]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - x - (r₁ - x)))
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
rcases le_or_gt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)

Goal state after:
case inl
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

case inr
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : i + 1 ≤ m
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p * (-1) ^ p

Tactic:
apply dvd_mul_of_dvd_left

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p * (-1) ^ p

Tactic:
apply dvd_mul_of_dvd_left

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
⊢ (exp fN ∘ₗ g) m = (g ∘ₗ exp fM) m

Tactic:
have (i : ℕ) : (fN ^ i) (g m) = g ((fM ^ i) m) := by
    simpa using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h i) m

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
this : ∀ (i : ℕ), (fN ^ i) (g m) = g ((fM ^ i) m)
⊢ (exp fN ∘ₗ g) m = (g ∘ₗ exp fM) m
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ N₁.normalizer ≤ N₂.normalizer

Tactic:
by
  intro m hm
  rw [mem_normalizer] at hm ⊢
  exact fun x ↦ h (hm x)

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
⊢ LieModule.IsNilpotent (↥K) (↥L' ⧸ K.toLieSubmodule)

Tactic:
refine hK₁ _ fun x => ?_

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
⊢ IsNilpotent ((toEnd R (↥K) (↥L' ⧸ K.toLieSubmodule)) x)
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
I : LieIdeal R L
k : ℕ
⊢ ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)

Tactic:
by
  induction k with
  | zero =>
    simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    congr
    ext x
    constructor
    · rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
    · rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Goal state after:
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
f : K[X]
inst✝ : IsSplittingField K L f
⊢ FiniteDimensional K L

Tactic:
exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
      if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
      else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)

Tactic:
coe_empty,

Goal state after:
case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥F[] →ₐ[F] L)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ adjoin F S = adjoin F (↑K ∪ S)

Tactic:
exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

Goal state after:
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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
σ : Lifts F E K
hσ✝ : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
x : ↥σ.carrier
⊢ (union c hc).emb ((inclusion ⋯) x) = σ.emb x

Tactic:
dsimp only [union, AlgHom.comp_apply]
    exact Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)

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

Goal state before:
pp: case h.zero
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
ih :
  ∀ m < 0,
    ∀ {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 = 0
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

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:
· rw [← top_le_iff]
    simp only [Submodule.finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]

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
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card ↑(f.rootSet K)
⊢ (Fintype.card K).succ ≤ Fintype.card K

Tactic:
rw [hroot]

Goal state after:
k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card ↑(f.rootSet K)
⊢ Fintype.card ↑(f.rootSet K) ≤ Fintype.card K
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : derivative f = 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ derivative f * g

Tactic:
eq_C_of_derivative_eq_zero hdf0

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : derivative f = 0
⊢ (∀ (x : K), (C (f.coeff 0)).IsRoot x → g.IsRoot x) → C (f.coeff 0) ∣ derivative (C (f.coeff 0)) * g
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
i : ι
h✝ : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
this✝ : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo ⇑(f j) ↑p ↑p
this : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ j, (fun j ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ j, (f j).maxGenEigenspace (μ j)

Tactic:
rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
i : ι
h✝ : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
this✝ : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo ⇑(f j) ↑p ↑p
this : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)
⊢ ⨅ i_1, Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)) =
    ⨅ i, p ⊓ (f i).maxGenEigenspace (μ i)
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 := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
⊢ finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree

Tactic:
adjoin.finrank,

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)
⊢ (minpoly K ((aeval (root p)) g)).natDegree = f.natDegree

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)
⊢ IsIntegral K ((aeval (root p)) g)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀ ∧
    Cardinal.lift.{u, v} ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
lift_aleph0

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀ ∧
    ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ max (max (Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E))) (Cardinal.lift.{u, v} #↑s))
      (Cardinal.lift.{u, v} ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
lift_aleph0

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ max (max (Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E))) (Cardinal.lift.{u, v} #↑s)) ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case pos
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsZero
⊢ genWeightSpace L ⇑α ≤ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), rootSpace H ⇑α

Tactic:
simp [hα]

Goal state after: