mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2
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, ∑ j ∈ RN, ((↑i !)⁻¹ * (↑j !)⁻¹) • (a ^ i * b ^ j) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
rw [sum_sigma']
      apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))
      · exact ⟨fun ⟨i, j⟩ ⟨i', j'⟩ h ↦ by cases h; rfl, fun ⟨i, j⟩ ↦ ⟨⟨i, j⟩, rfl⟩⟩
      · simp only [mem_sigma, mem_product, implies_true]
      · simp only [implies_true]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a✝ b✝ : M
hm₁ : a✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
hm₂ : b✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, a✝ + b✝⁆ ∈ N

Tactic:
by rw [lie_add]; exact N.add_mem' (hm₁ x) (hm₂ x)

Goal state after:
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✝⁷ : 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
t : A
x : A ⊗[R] L
m : A ⊗[R] M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by simp only [bracket_def, map_smul, LinearMap.smul_apply]

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
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
this : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
⊢ k₂ ∈ s

Tactic:
exact eq_bot_iff.mpr this

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

Goal state before:
pp: case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = k✝.succ
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥

Tactic:
rename_i k h
    obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
    have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
    simp only [h₂, h₃]

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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
⊢ ∃ t, ∃ z ∈ I, y = t • x + z

Tactic:
have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : y ∈ ⊤
⊢ ∃ t, ∃ z ∈ I, y = t • x + z
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
⊢ lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)

Tactic:
by
  suffices
    ∀ l,
      ((⊤ : LieIdeal R L).lcs M (i + l) : Submodule R M) ≤
        (I.lcs M j : Submodule R M).map (toEnd R L M x ^ l) ⊔
          (I.lcs M (j + 1) : Submodule R M)
    by simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using! this n
  intro l
  induction l with
  | zero =>
    simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]
    exact le_sup_of_le_left hIM
  | succ l ih =>
    simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
    refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
    · rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
      grw [coe_map_toEnd_le]
    · norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p✝ p q : P[X]
ihp : map (↑g) (m • p) = (MonoidHom.id M) m • map (↑g) p
ihq : map (↑g) (m • q) = (MonoidHom.id M) m • map (↑g) q
⊢ map (↑g) (m • (p + q)) = (MonoidHom.id M) m • map (↑g) (p + q)

Tactic:
rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieRing.IsNilpotent L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
⊢ LieRing.IsNilpotent L

Tactic:
by
  rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢
  peel h₁ with k hk
  apply LieIdeal.bot_of_map_eq_bot h₂; rw [eq_bot_iff, ← hk]
  apply LieIdeal.map_lowerCentralSeries_le

Goal state after:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x✝ : ↥(toAlgHom F E K₁).range
x : K₂
y : K₁
hx : ↑ϕ y = x
z : E
hy : (toAlgHom F E K₁).toRingHom z = y
⊢ ↑ϕ y ∈ (toAlgHom F E K₂).range

Tactic:
← hy

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x✝ : ↥(toAlgHom F E K₁).range
x : K₂
y : K₁
hx : ↑ϕ y = x
z : E
hy : (toAlgHom F E K₁).toRingHom z = y
⊢ ↑ϕ ((toAlgHom F E K₁).toRingHom z) ∈ (toAlgHom F E K₂).range
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0

Tactic:
by
  rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]
  simp only [minpoly, Polynomial.map_toSubring]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ Algebra.EssFiniteType F ↥K ↔ K.FG

Tactic:
by
  suffices (∃ s : Finset E, (s : Set E) ⊆ K ∧ adjoin F ↑s = K) ↔
      ∃ t : Finset E, adjoin F ↑t = K by
    simpa [IntermediateField.FG, (Equiv.finsetSubtypeComm _).exists_congr_left,
      ← (IntermediateField.map_injective K.val).eq_iff, ← IntermediateField.fg_top_iff,
      adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using! this
  exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩

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

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

Tactic:
Algebra.restrictScalars_adjoin F E'.toSubalgebra

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Algebra.adjoin F (↑E'.toSubalgebra ∪ ↑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
S T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

Tactic:
adjoin_adjoin_left,

Goal state after:
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) = restrictScalars F (adjoin (↥(adjoin F T)) S)
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 : Set E
⊢ adjoin F (S ∪ T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

Tactic:
adjoin_adjoin_left,

Goal state after:
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 F (T ∪ S)
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
⊢ restrictScalars F (adjoin (↥(adjoin F ↑K)) S) = adjoin F (↑(adjoin F ↑K) ∪ S)

Tactic:
adjoin_adjoin_left,

Goal state after:
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
⊢ adjoin F (↑K ∪ S) = adjoin F (↑(adjoin F ↑K) ∪ S)
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₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
⊢ ∃ (h : L₁.carrier ≤ L₃.carrier), ∀ (x : ↥L₁.carrier), L₃.emb ((inclusion h) x) = L₁.emb x

Tactic:
refine ⟨h₁₂.trans h₂₃, fun _ ↦ ?_⟩

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₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
x✝ : ↥L₁.carrier
⊢ L₃.emb ((inclusion ⋯) x✝) = L₁.emb 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
ι : Type u_3
i : ι → E
x : E
⊢ x ∈ adjoin F (Set.range i) ↔ ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

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
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)

Tactic:
let : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain _
  let : Algebra (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R _
  have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
  have := (IsFractionRing.isAlgebraic_iff' R S (FractionRing S)).1 inferInstance
  exact ⟨fun _ ↦ (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    (Algebra.IsAlgebraic.isAlgebraic _)⟩

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
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
⊢ FiniteDimensional K ↥(⨆ i, t i)

Tactic:
← iSup_univ

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
⊢ FiniteDimensional K ↥(⨆ x ∈ Set.univ, t x)
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
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
⊢ ∃ τ ≥ union c hc, ↑S ⊆ ↑τ.carrier

Tactic:
have : IsChain (· ≤ ·) (Set.range θ) := by
    simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq
    rintro _ ⟨π₁, rfl⟩ _ ⟨π₂, rfl⟩ -
    wlog h : π₁ ≤ π₂ generalizing π₁ π₂
    · exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm
    refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
    · rw [eq, eq]; exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)
    rintro x (hx | hx)
    · change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
        (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
      rw [(ge π₁).2, (ge π₂).2, h.2]
    · change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
      rw [(hθ π₁).2, (hθ π₂).2]

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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
this : IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)
⊢ ∃ τ ≥ union c hc, ↑S ⊆ ↑τ.carrier
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
K : IntermediateField F E
⊢ Module.rank F ↥K = 1 ↔ K.toSubalgebra = ⊥.toSubalgebra

Tactic:
← rank_eq_rank_subalgebra,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ Module.rank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = ⊥.toSubalgebra
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✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
x : E
⊢ finrank F ↥F⟮x⟯ = 1

Tactic:
by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]

Goal state after:
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)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
⊢ restrictScalars K (↥K⟮(aeval (root p)) g⟯)⟮root p⟯ = ⊤

Tactic:
adjoin_adjoin_left,

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

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ e ≠ 0

Tactic:
have := t.h_ne_zero
  contrapose this
  simpa [this] using t.lie_e_f.symm

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

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ f ≠ 0

Tactic:
have := t.h_ne_zero
  contrapose this
  simpa [this] using t.lie_e_f.symm

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

Goal state before:
pp: case pos
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : v ∈ ⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂
hχ₂ : χ₂ ∈ s
⊢ ⁅u, v⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)

Goal state after:
case pos
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : v ∈ ⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂
hχ₂ : χ₂ ∈ s
⊢ ⁅u, v⁆ ∈ ⨆ (_ : χ₁ + χ₂ ∈ s), genWeightSpace 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
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ⁅y, m⁆ ∈ 𝕎(M, χ₁ + χ₂, x)

Tactic:
apply LieModule.weight_vector_multiplication L M M (toModuleHom R L M) χ₁ χ₂
  simp only [LieModuleHom.coe_toLinearMap, Function.comp_apply, LinearMap.coe_comp,
    TensorProduct.mapIncl, LinearMap.mem_range]
  use ⟨y, hy⟩ ⊗ₜ ⟨m, hm⟩
  simp only [Submodule.subtype_apply, toModuleHom_apply, TensorProduct.map_tmul]

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
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
⊢ (B (∑ a ∈ tx, fx a • a)) y = (B y) (∑ a ∈ tx, fx a • a)

Tactic:
← hy

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 (∑ a ∈ tx, fx a • a)) (∑ a ∈ ty, fy a • a) = (B (∑ a ∈ ty, fy a • a)) (∑ a ∈ tx, fx a • a)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : 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
i j : ι
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i

Tactic:
rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]

Goal state after:
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
this : P ⊤
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
let e := LieModuleEquiv.ofTop R L M

Goal state after:
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)