mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
pow_succ',

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a

Tactic:
simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a]

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
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr ((pi fun i ↦ f i ∘ₗ proj i) (Pi.single j₂ (b j₁)))) ⟨i₂, i₁⟩ =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Pi.basis_repr,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((pi fun i ↦ f i ∘ₗ proj i) (Pi.single j₂ (b j₁)) i₂)) i₁ = if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ h = C h.leadingCoeff * (X - C x)

Tactic:
suffices (map i h).roots = {i x} from
    map_injective i i.injective (by simpa using h_splits.eq_X_sub_C_of_single_root this)

Goal state after:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ (map i h).roots = {i x}
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f₁ f₂ : AdjoinRoot g
i : Fin g.natDegree
⊢ ((modByMonicHom hg) (f₁ + f₂)).coeff ↑i =
    ((fun i ↦ ((modByMonicHom hg) f₁).coeff ↑i) + fun i ↦ ((modByMonicHom hg) f₂).coeff ↑i) i

Tactic:
simp only [(modByMonicHom hg).map_add, coeff_add, Pi.add_apply]

Goal state after:
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.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
⊢ f x = 0 x

Tactic:
obtain ⟨k : ℕ, hk : f ^ k = 0⟩ := hn

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
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
⊢ f x = 0 x
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
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 ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
h✝ : i.1 < N + 1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
pow_eq_zero_of_le (by linarith) h₅,

Goal state after:
case inr
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 ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
h✝ : i.1 < N + 1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * 0) = 0
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x m : L
n : M
⊢ ((↑(toEnd R L M)).toFun ⁅x, m⁆) n = ⁅x, (↑(toEnd R L M)).toFun m⁆ n

Tactic:
simp [LieRing.of_associative_ring_bracket]

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
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Tactic:
change sInf s = 0 ↔ _

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ 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
⊢ baseChange A ⊤ = ⊤

Tactic:
simp only [baseChange, top_toSubmodule, Submodule.baseChange_top]

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
⊢ { toSubmodule := ⊤, lie_mem := ⋯ } = ⊤
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 = ⊥}
hs : s.Nonempty
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Tactic:
change sInf s = 0 ↔ _

Goal state after:
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 = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Subsingleton M
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 = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ ⊥ = lowerCentralSeries ℤ L M 0

Tactic:
@eq_comm (LieSubmodule ℤ L M)

Goal state after:
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 = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ lowerCentralSeries ℤ L M 0 = ⊥
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
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
this : ∀ i ∈ s, l i ∈ subfield G F
⊢ False

Tactic:
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

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩

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
⊢ (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Tactic:
by
  rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]
  simp_rw [sup_def, adjoin_toSubfield, coe_toSubfield]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  exact Set.mem_union_left _ (algebraMap_mem S x)

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

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R L) (minpoly R x)).Splits
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

Tactic:
rw [IsScalarTower.algebraMap_eq R K L] at h
  exact int.minpoly_splits_tower_top' h

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 : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈
    map (AlgHom.restrictScalars A (Algebra.ofId B C)) A⟮b⟯

Tactic:
use x

Goal state after:
case h
F : Type u_1
inst✝⁹ : Field F
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑x ∈ ↑A⟮b⟯.toSubsemiring ∧
    ↑(AlgHom.restrictScalars A (Algebra.ofId B C)) ↑x = ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x
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 = Fintype.card ↑(f.rootSet K)

Tactic:
card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)

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 = f.natDegree
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
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hx : x ∈ ⨆ a, ↑a
this : Nonempty ↑s
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Tactic:
← SetLike.mem_coe,

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)
hne : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hx : x ∈ ↑(⨆ a, ↑a)
this : Nonempty ↑s
⊢ ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.refine_2
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
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
x : L
y : ↥(IsScalarTower.toAlgHom F L E).range := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x
⊢ f (↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm y) = f x

Tactic:
exact congr_arg f (AlgEquiv.symm_apply_apply _ _)

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case e'_5
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
e_3✝ : CommRing.toCommSemiring.toSemiring = Field.toSemifield.toDivisionSemiring.toSemiring
x✝ : L
⊢ f (↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm ((algebraMap L ↥L') x✝)) = f x✝

Tactic:
exact congr_arg f (AlgEquiv.symm_apply_apply _ _)

Goal state after:
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} (max #↑(Set.range ⇑(algebraMap F E) ∪ s) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
rw [lift_max, sup_le_iff, 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.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
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
have h_inj : Function.Injective p.subtype := Subtype.coe_injective

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, p ⊓ (f.genEigenspace μ) k)
h_inj : Injective ⇑p.subtype
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅f, e⁆ = -h

Tactic:
rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]

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

Goal state before:
pp: case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ((toEnd R L M) f ^ (n + 1)) m⁆ = (μ - 2 * ↑(n + 1)) • ((toEnd R L M) f ^ (n + 1)) m

Tactic:
pow_succ',

Goal state after:
case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ((toEnd R L M) f * (toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑(n + 1)) • ((toEnd R L M) f * (toEnd R L M) f ^ n) m
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h.inl
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
⊢ (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0

Tactic:
rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁,
      map_zero]

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

Goal state before:
pp: case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅e, ((toEnd R L M) f ^ (n + 1 + 1)) m⁆ = ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m

Tactic:
pow_succ',

Goal state after:
case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅e, ((toEnd R L M) f * (toEnd R L M) f ^ (n + 1)) m⁆ =
    ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ((toEnd R L M) e ^ (n + 1)) m⁆ = (μ + 2 * ↑(n + 1)) • ((toEnd R L M) e ^ (n + 1)) m

Tactic:
pow_succ',

Goal state after:
case succ
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ((toEnd R L M) e * (toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑(n + 1)) • ((toEnd R L M) e * (toEnd R L M) e ^ n) m
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
this : ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ posFittingCompOf R M x ≤ lowerCentralSeries R L M k

Tactic:
by
    intro m hm
    obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
    exact this n k

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

Goal state before:
pp: case mem
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
j : ι
⊢ ⁅b.e i, b.f j⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
rcases eq_or_ne i j with rfl | hij

Goal state after:
case mem.inl
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
⊢ ⁅b.e i, b.f i⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

case mem.inr
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
j : ι
hij : i ≠ j
⊢ ⁅b.e i, b.f j⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint ↑I ↑(orthogonal Φ hΦ_inv I)

Tactic:
LieSubmodule.disjoint_toSubmodule

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)