mathlib-initiative/mathlib-tactics huggingface dataset:
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)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
this : (toMatrix b b) e = fromBlocks A B 0 D
⊢ (fromBlocks A B 0 D).det = ((toMatrix bW bW) (e.restrict he)).det * ((toMatrix bQ bQ) (W.mapQ W e he)).det

Tactic:
Matrix.det_fromBlocks_zero₂₁

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)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
this : (toMatrix b b) e = fromBlocks A B 0 D
⊢ A.det * D.det = ((toMatrix bW bW) (e.restrict he)).det * ((toMatrix bQ bQ) (W.mapQ W e he)).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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun i ↦ (f ^ i) x
x✝ : M
⊢ x✝ ∈ {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1} ↔ x✝ ∈ g '' Iic k

Tactic:
simp [g]

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

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
x : L
⊢ ⁅D, (ad R L) x⁆ = (ad R L) (D x)

Tactic:
rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ (quotEquivQuotMap (minpoly R pb.gen) I)
      ((Ideal.Quotient.mk (Ideal.map (of (minpoly R pb.gen)) I))
        ((pb.lift (root (minpoly R pb.gen)) ⋯) ((aeval pb.gen) g))) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
PowerBasis.lift_aeval,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ (quotEquivQuotMap (minpoly R pb.gen) I)
      ((Ideal.Quotient.mk (Ideal.map (of (minpoly R pb.gen)) I)) ((aeval (root (minpoly R pb.gen))) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case e'_4
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))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P + -(1 * (aeval (P.newtonMap^[n] x)) P) = 0

Tactic:
one_mul,

Goal state after:
case e'_4
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))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P + -(aeval (P.newtonMap^[n] x)) P = 0
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: 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 : 0 = (aeval r₁) P + (aeval r₁) (derivative P) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂

Tactic:
hr₁',

Goal state after:
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 : 0 = 0 + (aeval r₁) (derivative P) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i =
    ∑ i ∈ RN, ∑ j ∈ RN, ((↑i !)⁻¹ * (↑j !)⁻¹) • (a ^ i * b ^ j)

Tactic:
rw [sum_mul_sum]
      refine sum_congr rfl fun _ _ ↦ sum_congr rfl fun _ _ ↦ ?_
      rw [smul_mul_assoc, mul_smul_comm, smul_smul]

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

Goal state before:
pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) x) z) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x)) z +
          ((bracket' R A L M) x) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x + y)) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y))) z +
            ((bracket' R A L M) (x + y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
· grind [LinearMap.add_apply]

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

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)

Tactic:
· grind [LinearMap.add_apply]

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

Goal state before:
pp: case a
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
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
simp only [← ih]
      exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian
    ↥(match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
rcases h : derivedLengthOfIdeal R L I with - | k

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian
    ↥(match 0 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
⊢ baseChange A ⁅I, N⁆ = ⁅baseChange A I, baseChange A N⁆

Tactic:
rw [← toSubmodule_inj, coe_baseChange, lieIdeal_oper_eq_linear_span',
    Submodule.baseChange_span, this, lieIdeal_oper_eq_linear_span']

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
⊢ Submodule.span A s = Submodule.span A {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}
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✝ : Nontrivial M
⊢ nilpotencyLength L M = 1 ↔ IsTrivial L M

Tactic:
by
  rw [nilpotencyLength_eq_succ_iff ℤ, ← trivial_iff_lower_central_eq_bot]
  simp

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

Goal state before:
pp: case succ
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
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match n✝ + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
exact h.2

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 (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ F

Tactic:
← mem_extendScalars (le_refl F),

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 (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ extendScalars ⋯
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro.right.a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
simp only [← coe_type_toSubalgebra] at this

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1.toSubalgebra ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have := sup_toSubalgebra_of_isAlgebraic_right E2 E1

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
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
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[F] L)

Tactic:
have : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule

Goal state after:
case refine_2
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
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this : FiniteDimensional F ↥Ks
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[F] L)
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
this : (aeval x) (1 * X + C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
one_mul,

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
this : (aeval x) (X + C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ IsCompactElement F⟮x⟯

Tactic:
isCompactElement_iff_le_of_directed_sSup_le,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ ∀ (s : Set (IntermediateField F E)),
    s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → F⟮x⟯ ≤ sSup s → ∃ x_1 ∈ s, F⟮x⟯ ≤ x_1
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ IsCompactElement F⟮x⟯

Tactic:
by
  simp_rw [isCompactElement_iff_le_of_directed_sSup_le,
    adjoin_simple_le_iff, sSup_eq_iSup', ← exists_prop]
  intro s hne hs hx
  have := hne.to_subtype
  rwa [← SetLike.mem_coe, coe_iSup_of_directed hs.directed_val, mem_iUnion, Subtype.exists] at hx

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
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
⊢ ∃ φ, AlgHom.domRestrict (↥L) φ = f

Tactic:
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl

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
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ ∃ φ, AlgHom.domRestrict (↥L) φ = f
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank K ↥K⟮x⟯

Tactic:
mul_comm,

Goal state after:
case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank K ↥K⟮x⟯ * finrank (↥K⟮x⟯) L
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
⊢ ∃ φ, φ.comp (inclusion hL) = f

Tactic:
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl

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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ ∃ φ, φ.comp (inclusion hL) = f
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case ind
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
| ind n ih =>

Goal state after:
case ind
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule

Tactic:
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ((toEnd R L M) x ^ 0) m ∈ genWeightSpace M (0 • χ₁ + χ₂)

Tactic:
simpa using hm

Goal state after: