mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ ComplementedLattice ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
disjoint_iff,

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
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ ComplementedLattice ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₁
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
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0

Tactic:
intros

Goal state after:
case h₁
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
i : Fin g.natDegree
a✝ : i ∉ Finset.univ
⊢ (monomial ↑i) (Pi.single i 1 i) = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f.natDegree ≤ q.natDegree

Tactic:
apply natDegree_le_of_dvd

Goal state after:
case refine_2.h1
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f ∣ q

case h2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0
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
hp₂ : Module.Finite R ↥p
⊢ f x = 0 x

Tactic:
simpa [LinearMap.restrict_apply, Subtype.ext_iff] using
    LinearMap.congr_fun (this p hp₁ hp₂) ⟨x, Submodule.subset_span ⟨0, k.zero_le, rfl⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝³ : Module.Finite K R
this✝² : Module.Finite R S
this✝¹ : Module.Finite K S
this✝ : IsArtinianRing R
this : IsReduced R
⊢ IsReduced (R[X] ⧸ Ideal.span {map (algebraMap K R) (minpoly K g)})

Tactic:
← Ideal.isRadical_iff_quotient_reduced,

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝³ : Module.Finite K R
this✝² : Module.Finite R S
this✝¹ : Module.Finite K S
this✝ : IsArtinianRing R
this : IsReduced R
⊢ (Ideal.span {map (algebraMap K R) (minpoly K g)}).IsRadical
Module: Mathlib.LinearAlgebra.Semisimple

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

Tactic:
have : K[f, g] ≤ φ.range := adjoin_le fun x ↦ by
    rintro (hx | hx) <;> rw [hx]
    · exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
    · exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩

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

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

Tactic:
apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ (x - -y) ^ n = 0
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 J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ l = k.succ ∨ l ≤ k

Tactic:
le_iff_eq_or_lt,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l = k + 1 ∨ l < k + 1
⊢ l = k.succ ∨ l ≤ k
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
this : ((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₁ = 0
⊢ ((bracket' R A L L) (z₁ + z₂)) (z₁ + z₂) = 0

Tactic:
by
      rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]

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

Goal state before:
pp: case succ
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
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x) ↑(⊤.lcs M (i + l)) ≤
      Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆ ∧
    ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆

Tactic:
refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩

Goal state after:
case succ.refine_1
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
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x) (Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆

case succ.refine_2
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
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ ↑⁅I, I.lcs M j⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (x y : A ⊗[R] L) (z : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
        z ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
          ⁅x, z⁆ ∈ Submodule.span A s → ⁅y, z⁆ ∈ Submodule.span A s → ⁅x + y, z⁆ ∈ Submodule.span A s

Tactic:
intros

Goal state after:
case refine_2.refine_2
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
x✝ y✝ : A ⊗[R] L
z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
a✝ : ⁅y✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝ + y✝, z✝⁆ ∈ Submodule.span A s
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✝⁷ : 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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (x : A ⊗[R] L) (y z : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
        z ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
          ⁅x, y⁆ ∈ Submodule.span A s → ⁅x, z⁆ ∈ Submodule.span A s → ⁅x, y + z⁆ ∈ Submodule.span A s

Tactic:
intros

Goal state after:
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✝⁷ : 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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
x✝ : A ⊗[R] L
y✝ z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
a✝ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, y✝ + z✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_4
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (r : A) (x : A ⊗[R] L) (y : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
        ⁅x, y⁆ ∈ Submodule.span A s → ⁅r • x, y⁆ ∈ Submodule.span A s

Tactic:
intros

Goal state after:
case refine_2.refine_4
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅r✝ • x✝, y✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_5
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (r : A) (x : A ⊗[R] L) (y : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
        ⁅x, y⁆ ∈ Submodule.span A s → ⁅x, r • y⁆ ∈ Submodule.span A s

Tactic:
intros

Goal state after:
case refine_2.refine_5
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
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, r✝ • y✝⁆ ∈ Submodule.span A s
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
⊢ False

Tactic:
have : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M :=
    le_inf_iff.mpr ⟨lowerCentralSeriesLast_le_of_not_isTrivial R L M contra,
      lowerCentralSeriesLast_le_max_triv R L M⟩

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 ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M
⊢ False
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : comap N.incl (ucs k ⊥) = ucs k ⊥
⊢ comap N.incl (ucs (k + 1) ⊥) = ucs (k + 1) ⊥

Tactic:
simp [← ih]

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₃
inst✝ : Normal F E
σ : Gal(E/F)
a✝ : E
⊢ (((toAlgHom F E K₁).comp ↑σ).restrictNormal E) a✝ = σ a✝

Tactic:
apply FaithfulSMul.algebraMap_injective E K₁

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₃
inst✝ : Normal F E
σ : Gal(E/F)
a✝ : E
⊢ (algebraMap E K₁) ((((toAlgHom F E K₁).comp ↑σ).restrictNormal E) a✝) = (algebraMap E K₁) (σ a✝)
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
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F α

Tactic:
by
  conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]
  rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]

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
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_toSubalgebra_of_isAlgebraic fun x h ↦
    IsAlgebraic.tower_top _ (isAlgebraic_iff.mp (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))

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 ↥E1 ↑E2).toSubalgebra = Algebra.adjoin ↥E1 ↑E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
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
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
⊢ K = K'

Tactic:
by
    ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
⊢ ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ

Tactic:
intros

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
μ✝ : K
⊢ Submodule.map ER.subtype (f'.maxGenEigenspace μ✝) ≤ f.maxGenEigenspace μ✝