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

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ p.degree ≠ 0

Tactic:
exact ne_of_gt (degree_pos_of_irreducible hp)

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
⊢ (σ a).Nonempty

Tactic:
by
  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
  have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p; rw [h_eval_p]; simp
  rw [(IsAlgClosed.splits p).eq_prod_roots_of_monic h_mon] at nu
  obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
  exact ⟨k, hk⟩

Goal state after:
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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : ↑S ⊆ ↑θ.carrier
⊢ False

Tactic:
← adjoin_le_iff

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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : adjoin F ↑S ≤ θ.carrier
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: 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
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, (Polynomial.map (algebraMap K ↥(t i)) (p i)).Splits ∧ t i = adjoin K ((p i).rootSet L)
i : ι
hi : i ∈ s
⊢ (Polynomial.map (algebraMap K ↥(⨆ i ∈ s, t i)) (p i)).Splits

Tactic:
by
    simpa [Polynomial.map_map] using (h i hi).1.map (inclusion (hF i hi)).toRingHom

Goal state after:
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 ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → y ∉ {ϕ | ϕ.IsExtendible}
⊢ False

Tactic:
simp_rw [Set.mem_ofPred, IsExtendible] at ϕ_max

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
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ¬∀ (S : Finset E), ∃ τ ≥ y, ↑S ⊆ ↑τ.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
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ S ⊆ ↑(adjoin E S)

Tactic:
← adjoin_le_iff

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ adjoin E S ≤ adjoin E S
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
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
φ : Module.End R M := (toEnd R L M) x
y : L
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = m
k : ℕ
⊢ ∃ y_1, (φ ^ k) y_1 = ⁅y, m⁆

Tactic:
obtain ⟨N, hN⟩ := LieAlgebra.nilpotent_ad_of_nilpotent_algebra R L

Goal state after:
K : Type u_1
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
φ : Module.End R M := (toEnd R L M) x
y : L
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = m
k N : ℕ
hN : ∀ (x : L), (LieAlgebra.ad R L) x ^ N = 0
⊢ ∃ y_1, (φ ^ k) y_1 = ⁅y, 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
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
n✝ : ℕ
a✝ : n✝ ≤ n → ((toEnd R L M) f ^ n✝) m = 0 → False
hi : n✝ + 1 ≤ n
H : ((toEnd R L M) f ^ (n✝ + 1)) m = 0
⊢ False

Tactic:
· next i IH =>
    have : ((i + 1) * (n - i) : ℤ) • (toEnd R L M f ^ i) m = 0 := by
      have := congr_arg (⁅e, ·⁆) H
      simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this
    rw [← Int.cast_smul_eq_zsmul R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero,
      Nat.cast_inj, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this
    simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this
    exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_gt i.lt_succ_self

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
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ (b : ℕ),
    l ≤ b →
      ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
        ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
          ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b
hl₁ : ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) l
hl₂ : ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) l
hl₃ : ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l
⊢ LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) =
    posFittingComp R L M

Tactic:
← iInf_lowerCentralSeries_eq_posFittingComp,

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
N₁ N₂ : LieSubmodule R L M
h : Codisjoint N₁ N₂
l : ℕ
hl :
  ∀ (b : ℕ),
    l ≤ b →
      ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) b ∧
        ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) b ∧
          ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b
hl₁ : ⨅ k, lowerCentralSeries R L (↥N₁) k = lowerCentralSeries R L (↥N₁) l
hl₂ : ⨅ k, lowerCentralSeries R L (↥N₂) k = lowerCentralSeries R L (↥N₂) l
hl₃ : ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l
⊢ LieSubmodule.map N₁.incl (⨅ k, lowerCentralSeries R L (↥N₁) k) ⊔
      LieSubmodule.map N₂.incl (⨅ k, lowerCentralSeries R L (↥N₂) k) =
    ⨅ k, lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.f)
hy✝ : v ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, u + v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
rw [lie_add]; exact add_mem hu hv

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Tactic:
rintro _ ⟨x, y, rfl⟩

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
⊢ ⁅↑x, ↑y⁆ ∈ ↑⊥
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a.left
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₁

pp: case a.right
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₂

Tactic:
· apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _
    · exact (hS.mono hX).isAtom I hI
    · exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_left)

Goal state after:
case a.right
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₂
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
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 : I ∈ {I | IsAtom I}
⊢ ∀ b ∈ {I | IsAtom I} \ {I}, b ≤ orthogonal Φ hΦ_inv I

Tactic:
simp only [Set.mem_sdiff, Set.mem_ofPred_eq, Set.mem_singleton_iff, and_imp]

Goal state after:
case refine_2
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 : I ∈ {I | IsAtom I}
⊢ ∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
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 : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(orthogonal Φ hΦ_inv I)

Tactic:
rintro _ ⟨x, y, rfl⟩

Goal state after:
case refine_2
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 : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
⊢ ⁅↑x, ↑y⁆ ∈ ↑(orthogonal Φ hΦ_inv I)
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
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
⊢ (B.restrict (B.orthogonal (K ∙ x))).Nondegenerate

Tactic:
refine ⟨fun m hm => Submodule.coe_eq_zero.1 (b₁.1 m fun n ↦ ?_),
    fun m hm => Submodule.coe_eq_zero.1 (b₁.2 m fun n ↦ ?_)⟩ <;>
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.1 <| this n

Goal state after:
case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B ↑m) (y + z) = 0

case refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (x_1 : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) x_1) m = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B (y + z)) ↑m = 0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn ↦ (subProdXSubC fn.1).coeff fn.2) v = 1
⊢ False

Tactic:
replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv

Goal state after:
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv :
  (toSplittingField (Finset.image Prod.fst v.support))
      ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn ↦ (subProdXSubC fn.1).coeff fn.2) v) =
    (toSplittingField (Finset.image Prod.fst v.support)) 1
⊢ False
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : ∀ (x y z : L), x ∈ killingCompl K L I → y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0
⊢ ⁅I ⊓ killingCompl K L I, I ⊓ killingCompl K L I⁆ = ⊥

Tactic:
LieSubmodule.lie_eq_bot_iff

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : ∀ (x y z : L), x ∈ killingCompl K L I → y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0
⊢ ∀ x ∈ I ⊓ killingCompl K L I, ∀ m ∈ I ⊓ killingCompl K L I, ⁅x, m⁆ = 0
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ (∀ (m : ι → R), ∃ n, (toLin' (A ^ n)) m = 0) ↔ ∀ (v : ι → R), ∃ n, A ^ n *ᵥ v = 0

Tactic:
toLin'_apply

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

Goal state before:
pp: R : Type u_1
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
⊢ LinearMap.BilinForm.lieInvariant L (traceForm R L M)

Tactic:
intro x y z
  rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ map (↑e).flip p.dualCoannihilator = (map (↑e.symm) p).dualAnnihilator

Tactic:
suffices
      (p.map (e.symm : Dual R M →ₗ[R] N)).dualAnnihilator.map (e.flip.symm : Dual R N →ₗ[R] M) =
        (p.dualCoannihilator.map (e.flip : M →ₗ[R] Dual R N)).map (e.flip.symm : Dual R N →ₗ[R] M)
    from (Submodule.map_injective_of_injective e.flip.symm.injective this).symm

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ map (↑e.flip.symm) (map (↑e.symm) p).dualAnnihilator = map (↑e.flip.symm) (map (↑e.flip) p.dualCoannihilator)
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : ↑S i ∈ ↑S '' Set.Iio m
⊢ (↑S i).degree < ↑m

Tactic:
S.degree_eq i,

Goal state after:
case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : ↑S i ∈ ↑S '' Set.Iio m
⊢ ↑i < ↑m
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
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
B : LinearMap.BilinForm R M
m₀ : M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
m₁ : M
hm₁ : m₁ ∈ posFittingCompOf R M x
hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0
⊢ (B m₀) m₁ = 0

Tactic:
obtain ⟨k, hk⟩ := hm₀ x

Goal state after:
R : Type u_1
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
B : LinearMap.BilinForm R M
m₀ : M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
m₁ : M
hm₁ : m₁ ∈ posFittingCompOf R M x
hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0
k : ℕ
hk : (φ x ^ k) m₀ = 0
⊢ (B m₀) m₁ = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
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
B : LinearMap.BilinForm R M
hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
⊢ (B m₀) m₁ = 0

Tactic:
replace hB : ∀ x (k : ℕ) m n, B m ((φ x ^ k) n) = (-1 : R) ^ k • B ((φ x ^ k) m) n := by
    intro x k
    induction k with
    | zero => simp
    | succ k ih =>
    intro m n
    replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
    have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ (-1 : R), smul_eq_mul]
    conv_lhs => rw [pow_succ, Module.End.mul_eq_comp, LinearMap.comp_apply, ih, hB,
      ← (φ x).comp_apply, ← Module.End.mul_eq_comp, ← pow_succ', ← smul_assoc, this]
  suffices ∀ (x : L) m, m ∈ posFittingCompOf R M x → B m₀ m = 0 by
    refine LieSubmodule.iSup_induction (motive := fun m ↦ (B m₀) m = 0) _ hm₁ this (map_zero _) ?_
    simp_all
  clear hm₁ m₁; intro x m₁ hm₁
  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm₀
  obtain ⟨k, hk⟩ := hm₀ x
  obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k
  simp [hB, hk]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' = 0

Tactic:
← Submodule.mem_bot (R := K),

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ ⊥
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
apply lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ ∀ (h : ↥H), ⁅h, e⁆ = α h • e
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)

Tactic:
have neg' (n : ℤ) (h : motive (-n)) : motive n := by
    convert! neg (-n) h; rw [neg_neg]

Goal state after:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ), motive (-n) → motive n
⊢ ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
⊢ (U R ↑n).degree = ↑n

Tactic:
induction n using Nat.twoStepInduction with

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
this : leadingCoeff 2 = 2
⊢ (U R ↑n).leadingCoeff = 2 ^ n

Tactic:
induction n using Nat.twoStepInduction with

Goal state after: