mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ ((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

Tactic:
classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
T : Type u_3
inst✝¹ : CommRing R
inst✝ : Semiring T
p : R[X]
f g : AdjoinRoot p →+* T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : f (root p) = g (root p)
⊢ f = g

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u_1
T : Type u_3
inst✝¹ : CommRing R
inst✝ : Semiring T
p : R[X]
f g : AdjoinRoot p →+* T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : f (root p) = g (root p)
⊢ f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case ih
R : Type u_1
inst✝ : CommRing R
f p : R[X]
⊢ (mk f) p ∈ R[root f]

Tactic:
exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ RingHom.ker (aeval f)
⊢ X ∈ RingHom.ker (aeval f)

Tactic:
← AEval.annihilator_eq_ker_aeval (M := M)

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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: 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
⊢ exp (a + b) = exp a * exp b

Tactic:
rw [exp_eq_sum (k := 2 * N + 1)
    (Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero h₁ h₄ h₅ (by lia)),
    exp_eq_sum h₄, exp_eq_sum h₅]

Goal state after:
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
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i =
    (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * ∑ i ∈ range (N + 1), (↑i !)⁻¹ • b ^ i
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        ((quotEquivOfEq ⋯).symm
          ((Polynomial.quotQuotEquivComm I f)
            ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}))
              (Polynomial.map (Ideal.Quotient.mk I) p))))) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
Polynomial.quotQuotEquivComm_mk,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        ((quotEquivOfEq ⋯).symm
          ((Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f}))
            ((Ideal.Quotient.mk (Ideal.map C I)) p)))) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotEquivQuotMap f I).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)

Tactic:
rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
    AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: 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

Tactic:
· simp [pow_eq_zero_of_le (by lia : n ≤ j) hy]

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

Goal state before:
pp: case refine_2.refine_2.refine_2
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
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆

Tactic:
mul_left_comm a₂ a₁ a₃,

Goal state after:
case refine_2.refine_2.refine_2
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
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_1
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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
⊢ ⁅a ⊗ₜ[R] y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N

Tactic:
change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _

Goal state after:
case refine_1
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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
⊢ ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (a ⊗ₜ[R] y)) ((Finsupp.linearCombination A Subtype.val) c) ∈
    Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)

Tactic:
h.eq_bot,

Goal state after:
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✝ : IsNilpotent L M
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this : lowerCentralSeriesLast R L M ≤ ⊥
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := ⋯
⊢ (Basis.ofVectorSpaceIndex K V).Finite → IsNoetherian K V

Tactic:
intro hbfinite
    refine
      @isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)
    refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩
    rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ LieModule.lowerCentralSeries R L M k = ⊥ ↔ ucs k ⊥ = ⊤

Tactic:
simp [ucs_eq_top_iff]

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
h : F ≤ E
x✝ : Algebra ↥F ↥E := (inclusion h).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ∣ finrank (↥F) L

Tactic:
exact Module.finrank_dvd_finrank_left F E L

Goal state after:
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
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Tactic:
rw [Set.union_eq_right]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑S ∪ ↑T
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
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ Set.range ⇑(algebraMap F E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
rw [Set.union_eq_right]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ Set.range ⇑(algebraMap F E) ⊆ ⋃₀ (SetLike.coe '' S)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

Tactic:
rw [adjoin_subset_adjoin_iff]

Goal state after:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap (↥(adjoin F S)) E) ⊆ ↑(adjoin F (S ∪ T)) ∧ T ⊆ ↑(adjoin F (S ∪ T))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

Tactic:
rw [adjoin_subset_adjoin_iff]

Goal state after:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T) ∧ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L'
h : S ≤ f.fieldRange
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Goal state after:
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
⊢ n.succ = f.natDegree

Tactic:
unfold f

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
⊢ n.succ = (X ^ (n + 1) - 1).natDegree
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝² : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝¹ : Algebra S R := hSR.toRingHom.toAlgebra
this✝ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this : IsScalarTower R S L
⊢ ∀ (x : S), (algebraMap S L) x = (algebraMap R L) ((algebraMap S R) x)

Tactic:
by simp [RingHom.algebraMap_toAlgebra]

Goal state after:
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
inst✝ : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥⊤
hn : n < finrank F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
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 : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
this : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra
⊢ IsIntegral (↥L') s ∧ (Polynomial.map f'.toRingHom (minpoly (↥L') s)).Splits

Tactic:
have : IsScalarTower L L' E := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
case refine_1
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 : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower L (↥L') E
⊢ IsIntegral (↥L') s ∧ (Polynomial.map f'.toRingHom (minpoly (↥L') s)).Splits
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
⊢ { toFun := fun m ↦ ⟨⁅↑(t • x), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) t • { toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
simp only [RingHom.id_apply]

Goal state after:
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
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
⊢ { toFun := fun m ↦ ⟨⁅↑(t • x), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    t • { toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
hx : x ∈ rootSpace H α
⊢ MapsTo ⇑((toEnd R L M) x) ↑(genWeightSpace M χ) ↑(genWeightSpace M (α + χ))

Tactic:
intro m hm
  let x' : rootSpace H α := ⟨x, hx⟩
  let m' : genWeightSpace M χ := ⟨m, hm⟩
  exact (rootSpaceWeightSpaceProduct R L H M α χ (α + χ) rfl (x' ⊗ₜ m')).property

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
⊢ (B x) y = (B y) x

Tactic:
obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
⊢ (B x) y = (B y) x
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, (Φ n) y = 0
a : M
⊢ a ∈ N → (Φ a) ⁅x, y⁆ = 0

Tactic:
ha

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, (Φ n) y = 0
a : M
ha : a ∈ N
⊢ (Φ a) ⁅x, y⁆ = 0
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case h.right
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ sSup C = sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
· apply le_antisymm
    · apply _root_.sSup_le
      intro c hc
      rw [hT₂ c (hC _ hc) ((le_sSup hc).trans ha)]
      apply sSup_le_sSup
      apply _root_.le_sSup
      use c, hc, hC _ hc, (le_sSup hc).trans ha
    · simp only [Set.sSup_eq_sUnion, sSup_le_iff, Set.mem_sUnion, Set.mem_ofPred_eq,
        forall_exists_index, and_imp]
      rintro a T b hbC hb hbS rfl haT
      apply (le_sSup haT).trans
      rw [← hT₂]
      exact le_sSup hbC

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
⊢ a ∈ X → a ∈ Y

Tactic:
ha

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ a ∈ Y
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + 0

Tactic:
rw [← finrank_bot K V, ← this, finrank_sup_add_finrank_inf_eq,
    finrank_add_finrank_orthogonal b₁]

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ a ∈ {a | IsAtom a} → a ∈ S

Tactic:
ha

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ∈ S
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card = 0
⊢ (filter (fun a_1 ↦ a = a_1.1) s.val).card ≤ count a m

Tactic:
ha

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card = 0
⊢ 0 ≤ count a m
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ IsCompl ↑I ↑(killingCompl K L I)

Tactic:
I.toSubmodule_killingCompl,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ IsCompl (↑I) ((killingForm K L).orthogonal ↑I)