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

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := H (p * C (leadingCoeff p)⁻¹) (monic_mul_leadingCoeff_inv hp.ne_zero)
      (irreducible_mul_leadingCoeff_inv.mpr hp)

Goal state after:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ ∃ x, eval x p = 0
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 = (↑j).emb ((inclusion h) x)

Tactic:
rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]

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 _

Goal state after:
k : Type u
inst✝¹⁶ : Field k
K : Type u
inst✝¹⁵ : Field K
L : Type v
M : Type w
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : Field M
inst✝¹¹ : Algebra K M
inst✝¹⁰ : IsAlgClosed M
inst✝⁹ : Algebra.IsAlgebraic K L
R : Type u
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type v
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
inst✝³ : Algebra R M
inst✝² : IsTorsionFree R S
inst✝¹ : IsTorsionFree R M
inst✝ : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (FaithfulSMul.algebraMap_injective R S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.inl
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 = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
x : E
hx : x ∈ ↑(↑π₁).carrier
⊢ (θ π₂).emb ((inclusion ⋯) ((inclusion ⋯) ⟨x, hx⟩)) = (↑π₁).emb ⟨x, hx⟩

Tactic:
(ge π₂).2,

Goal state after:
case refine_2.inl
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 = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
x : E
hx : x ∈ ↑(↑π₁).carrier
⊢ (↑π₂).emb ((inclusion ⋯) ⟨x, hx⟩) = (↑π₁).emb ⟨x, hx⟩
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₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
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 : ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
⊢ (↑g ∘ₗ (f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0

Tactic:
LinearMap.comp_apply,

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₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
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 : ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
⊢ ↑g (((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂)) = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (B (r • x)) y = r • (B x) y

Tactic:
by
  rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
⊢ y ∈ (Φ.orthogonal ↑N).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal ↑N).carrier

Tactic:
suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
      simpa only [
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
⊢ (∀ n ∈ N, (Φ n) y = 0) → ∀ n ∈ N, (Φ n) ⁅x, y⁆ = 0
Module: Mathlib.Algebra.Lie.Weights.Linear

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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) ⁅x, y⁆ = 0

Tactic:
LinearMap.comp_apply,

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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ)) (↑(toEnd R L ↥(genWeightSpace M χ)) ⁅x, y⁆) = 0
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:
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.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
⊢ 1 ∉ Ideal.span (Set.range fun fn ↦ (subProdXSubC fn.1).coeff fn.2)

Tactic:
Ideal.span,

Goal state after:
k : Type u
inst✝ : Field k
⊢ 1 ∉ Submodule.span (MvPolynomial (Vars k) k) (Set.range fun fn ↦ (subProdXSubC fn.1).coeff fn.2)
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule

Tactic:
simp only [ad_apply_lieDerivation, LieHom.range_toSubmodule, neg_mem_iff]
  exact (rangeAdOrthogonal R L).lie_mem hD

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 (-α + ⇑(chainBot α β)) = ⊥

Tactic:
by
  rw [← chainTop_neg, genWeightSpace_add_chainTop _ _ (by simpa using hα)]

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
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
hB : ∀ (m : M), (B m) ((φ x) n) = -1 • (B ((φ x) m)) n
this : (-1) ^ k • -1 = (-1) ^ (k + 1)
| (B m) (((φ x ^ k) ∘ₗ φ x) n)

Tactic:
LinearMap.comp_apply,

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₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
hB : ∀ (m : M), (B m) ((φ x) n) = -1 • (B ((φ x) m)) n
this : (-1) ^ k • -1 = (-1) ^ (k + 1)
| (B m) ((φ x ^ k) ((φ x) n))
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
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Tactic:
have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z

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
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
h : iSupIndep fun i ↦ ↑(genWeightSpaceOf M i z)
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y
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 • ↑α' ∈ LinearMap.ker (killingForm K L)

Tactic:
apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))

Goal state after:
case hx
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 := ⋯
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ rootSpace H 0

case hx'
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 := ⋯
⊢ ∀ y ∈ rootSpace H (-0), ((killingForm K L) (⁅e, f⁆ - ((killingForm K L) e) f • ↑α')) y = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
χ : Weight K L M
hχ : χ ∈ {χ | χ.IsZero}
⊢ Weight.toLinear K L M χ = 0

Tactic:
simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ

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
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : α x = 0
⊢ x = 0

Tactic:
exact eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

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

Goal state before:
pp: case refine_1.refine_2
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✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₂ • f ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

Tactic:
exact mem_sup_left <| mem_sup_right <| smul_mem _ _ hfα

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) -
      ((⇑derivative)^[k + 2] (T R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (T R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (T R n)) =
    (⇑derivative)^[k + 1] (T R n) * X + k • (⇑derivative)^[k] (T R n) - ↑(n ^ 2) * (⇑derivative)^[k] (T R n)
⊢ (⇑derivative)^[k] (T R n) * ↑k + (⇑derivative)^[k] (T R n) * ↑k * ↑(k - 1) - (⇑derivative)^[k] (T R n) * ↑k ^ 2 = 0

Tactic:
cases k <;> grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1

Tactic:
simpa using congr_arg transpose hAB

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) -
      ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (U R n)) =
    ↑3 * ((⇑derivative)^[k + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)
⊢ (⇑derivative)^[k] (U R n) * ↑k + (⇑derivative)^[k] (U R n) * ↑k * ↑(k - 1) - (⇑derivative)^[k] (U R n) * ↑k ^ 2 = 0

Tactic:
cases k <;> grind

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
⊢ f.range = g.ker

Tactic:
LinearMap.exact_iff.mp H

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
⊢ f.range = f.range
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : AdicCompletion I M → Prop
x : AdicCompletion I M
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
⊢ p x

Tactic:
obtain ⟨f, rfl⟩ := mk_surjective I M x
  exact h f

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]

Tactic:
let u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), fun c ↦ (hmn c).symm⟩

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
⊢ ?m.97

Tactic:
refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
⊢ ∀ x ∈ Multiset.replicate m p, Irreducible x

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
⊢ ∀ x ∈ Multiset.replicate n q, Irreducible x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ emultiplicity (Classical.choose ⋯) r = ↑n

Tactic:
hr,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ emultiplicity (Classical.choose ⋯) (↑u * ϖ ^ n) = ↑n
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : ¬y ∣ x
⊢ toWithBotNat x < toWithBotNat y

Tactic:
exact lt_iff_not_ge.mpr (mt (dvd_of_toWithBotNat_le_toWithBotNat _ _ hy) hyx)

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ¬IsField R
this : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ¬IsField R
this✝ : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1
this : maximalIdeal R ≠ ⊥
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE