mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x : E
h : x ∈ adjoin F s
⊢ p 1 ⋯

Tactic:
simp_rw [← (Algebra.algebraMap F E).map_one]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x : E
h : x ∈ adjoin F s
⊢ p ((Algebra.algebraMap F E) 1) ⋯
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
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (⨆ i, S i).FG

Tactic:
simp_rw [← hs, ← adjoin_iUnion]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (adjoin F (⋃ i, ↑(s i))).FG
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

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

Tactic:
aeval_add,

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
this : (aeval x) X + (aeval x) (C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = 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
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb ((inclusion ⋯) ((inclusion h) x))

Tactic:
inclusion_inclusion,

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₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb ((inclusion ⋯) x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case inl
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
h✝ : IsEmpty ι
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Tactic:
simp_rw [iSup_of_empty, bot_toSubalgebra]

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

Goal state before:
pp: case h.succ
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
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀

Goal state after:
case h.succ
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
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this : ϕ.carrier ≠ ⊤
⊢ False

Tactic:
obtain ⟨α, -, hα⟩ := SetLike.exists_of_lt this.lt_top

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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
⊢ False
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
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
⊢ K' = K

Tactic:
have hsub : K' ≤ K := by
    refine adjoin_le_iff.mpr fun x ↦ ?_
    rw [Finset.mem_coe, mem_coeffs_iff]
    rintro ⟨n, -, rfl⟩
    rw [coeff_map]
    apply Subtype.mem

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ K' = K
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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

Tactic:
finrank_mul_finrank

Goal state after:
case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank K L
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type u
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ #↥(adjoin F s) ≤ max (max #F #↑s) ℵ₀

Tactic:
by
  simpa using lift_cardinalMk_adjoin_le F s

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

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.toLieSubmodule.IsUcsLimit → H.IsCartanSubalgebra

Tactic:
rintro ⟨k, hk⟩
    exact
      { nilpotent := by
          dsimp only [LieRing.IsNilpotent]
          -- The instance for the second `H` in the goal is `lieRingSelfModule`
          -- but `rw` expects it to be `H.toLieSubmodule.instLieRingModuleSubtypeMem`,
          -- and these are not reducibly defeq.
          erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
          use k
          rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
        self_normalizing := by
          have hk' := hk (k + 1) k.le_succ
          rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
          rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.coe_toLieSubmodule] }

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

Goal state before:
pp: case h
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₃ := ⋯
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := ⋯
f₂ : Module.End R (M₁ ⊗[R] M₂) := ⋯
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
⊢ ((f₁ + f₂) ^ (k₁ + k₂ - 1)) (m₁ ⊗ₜ[R] m₂) = 0

Tactic:
have hf_comm : Commute f₁ f₂ := by
    ext m₁ m₂
    simp only [f₁, f₂, Module.End.mul_apply, LinearMap.rTensor_tmul, LinearMap.lTensor_tmul,
      AlgebraTensorModule.curry_apply, LinearMap.lTensor_tmul, TensorProduct.curry_apply,
      LinearMap.coe_restrictScalars]

Goal state after:
case h
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₂
⊢ ((f₁ + f₂) ^ (k₁ + k₂ - 1)) (m₁ ⊗ₜ[R] m₂) = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: 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 μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : ⁅e, ((toEnd R L M) f ^ (i + 1)) m⁆ = ⁅e, 0⁆
⊢ ((↑i + 1) * (↑n - ↑i)) • ((toEnd R L M) f ^ i) m = 0

Tactic:
simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this

Goal state after:
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
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅x, y⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
rw [← lie_skew, map_neg, neg_eq_zero] at hk

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
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: 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 μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (↑i + 1 = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
← @Nat.cast_one ℤ,

Goal state after:
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 μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (↑i + ↑1 = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ x ∈ corootSpace α ↔ ↑x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}

Tactic:
have : x ∈ corootSpace α ↔
      (x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α) := by
    rw [corootSpace]
    simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map,
      LieSubmodule.incl_apply, SetLike.coe_eq_coe, exists_eq_right]
    rfl
  simp_rw [this, corootSpace, ← LieModuleHom.map_top, ← LieSubmodule.mem_toSubmodule,
    LieSubmodule.toSubmodule_map, LieSubmodule.top_toSubmodule, ← TensorProduct.span_tmul_eq_top,
    LinearMap.map_span, Set.image, Set.mem_ofPred_eq, exists_exists_exists_and_eq]
  change (x : L) ∈ Submodule.span R
    {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _
  simp

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m
⊢ m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)

Tactic:
simp only [LieSubmodule.mem_comap, mem_posFittingCompOf]

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m
⊢ ∀ (k : ℕ), ∃ n, ((toEnd R L M₂) y ^ k) n = f m
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
⊢ ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩

Goal state after:
ι : 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 i, b.h j⁆ = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

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

Tactic:
(b.sl2 i).lie_e_f

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.h i ∈ H.toLieSubmodule ⊔ b.borelLower
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
hB₀ : B.IsRefl
⊢ IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)

Tactic:
refine ⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩
  rw [codisjoint_iff]
  apply (eq_top_of_finrank_eq <| (finrank_le _).antisymm _)
  calc
    finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) := le_self_add
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W) := ?_
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) := by simp [h.eq_bot]
  rw [finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal hB₀ W]

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f x.fst ↑x.snd

Tactic:
by
  rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]
  · rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]
  · intro x
    rfl

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

Goal state before:
pp: case inr.right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
hJI : J ⊓ I = J
⊢ J ≤ I

Tactic:
← hJI

Goal state after:
case inr.right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
hJI : J ⊓ I = J
⊢ J ⊓ I ≤ I
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0

Tactic:
by
  constructor
  · rintro rfl μ hμ
    by_contra hμ0
    obtain ⟨x, hx, hx_ne⟩ := (Submodule.ne_bot_iff _).mp hμ
    rw [mem_eigenspace_iff] at hx
    exact hx_ne ((smul_eq_zero.mp hx.symm).resolve_left hμ0)
  · intro h
    suffices f.eigenspace 0 = ⊤ by rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
    rw [← hf.iSup_eigenspace_eq_top]
    refine le_antisymm (le_iSup _ 0) (iSup_le fun μ ↦ ?_)
    rcases eq_or_ne μ 0 with rfl | hμ
    · exact le_refl _
    · have : f.eigenspace μ = ⊥ := not_not.mp (hasEigenvalue_iff.not.mp fun he ↦ hμ (h μ he))
      simp [this]

Goal state after:
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
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e ∪ range b.f)
hy✝ : v ∈ lieSpan R L (range b.e ∪ range b.f)
hu : u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ∃ yc ∈ H, ∃ yl ∈ lieSpan R L (range b.f), ∃ yu ∈ lieSpan R L (range b.e), yc + yl + yu = u

Tactic:
simpa [LieSubmodule.mem_sup] using! hu

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((↑(chainTopCoeff α β) + 1) • α + ⇑β) = ⊥

Tactic:
by
  rw [← genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα, ← Nat.cast_smul_eq_nsmul ℤ,
    Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: case neg
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (-⇑α) ≠ ⊥

Tactic:
intro e
      obtain ⟨x, hx, x_ne0⟩ := α.exists_ne_zero
      have := mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H hx
        (fun y hy ↦ by rw [rootSpace, e] at hy; rw [hy, map_zero])
      rw [ker_killingForm_eq_bot] at this
      exact x_ne0 this

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (-↑n)) = ↑(if Even (-↑n) then ↑(-↑n / 2).negOnePow else 0)
ih2 : eval 0 (T R (-↑n + 1)) = ↑(if Even (-↑n + 1) then ↑((-↑n + 1) / 2).negOnePow else 0)
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

Tactic:
have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (-↑n)) = ↑(if Even (-↑n) then ↑(-↑n / 2).negOnePow else 0)
ih2 : eval 0 (T R (-↑n + 1)) = ↑(if Even (-↑n + 1) then ↑((-↑n + 1) / 2).negOnePow else 0)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)