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

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝⁵ : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝⁴ : Algebra S R := hSR.toRingHom.toAlgebra
this✝³ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this✝² : IsScalarTower R S L
this✝¹ : IsScalarTower S R L
this✝ : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
⊢ (equivOfAlgebraic' R S L M) ((algebraMap R L) (hSR x)) = (algebraMap R M) (hSR x)

Tactic:
rw [AlgEquiv.commutes]

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

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ (minpoly F x1).rootSet E

Tactic:
rw [mem_rootSet_of_ne, minpoly.aeval]
    exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))

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

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ((insert χ₂ s).sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂

Goal state after:
case insert
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ((insert χ₂ s).sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert.refine_1
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ₁ i))

Tactic:
refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
    simp only [Submodule.coe_iInf]
    exact h l χ₁

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

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ f * C 1⁻¹ = f

Tactic:
inv_one,

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ f * C 1 = f
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
⊢ Irreducible (f.comp g)

Tactic:
have hg' : natDegree g ≠ 0 := by
    have := Fact.mk hf
    intro e
    apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
    -- Needed to specialize `map_sub` to avoid a timeout https://github.com/leanprover-community/mathlib4/pull/8386
    rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
    apply hg (AdjoinRoot f)
    rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
⊢ Irreducible (f.comp g)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: 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)
⊢ F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)

Tactic:
ext m₁ m₂

Goal state after:
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)
m₁ : M₁
m₂ : M₂
⊢ ((AlgebraTensorModule.curry (F ∘ₗ ↑g)) m₁) m₂ = ((AlgebraTensorModule.curry (↑g ∘ₗ (f₁ + f₂))) m₁) m₂
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: 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
⊢ Commute f₁ f₂

Tactic:
ext m₁ m₂

Goal state after:
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
m₁ : M₁
m₂ : M₂
⊢ ((AlgebraTensorModule.curry (f₁ * f₂)) m₁) m₂ = ((AlgebraTensorModule.curry (f₂ * f₁)) m₁) m₂
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case mk
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
χ₂ : Weight R L M
toFun✝ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M toFun✝ ≠ ⊥
h : (fun χ ↦ χ.toFun) { toFun := toFun✝, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } = (fun χ ↦ χ.toFun) χ₂
⊢ { toFun := toFun✝, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } = χ₂

Tactic:
cases χ₂

Goal state after:
case mk.mk
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
toFun✝¹ : L → R
genWeightSpace_ne_bot'✝¹ : genWeightSpace M toFun✝¹ ≠ ⊥
toFun✝ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M toFun✝ ≠ ⊥
h :
  (fun χ ↦ χ.toFun) { toFun := toFun✝¹, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } =
    (fun χ ↦ χ.toFun) { toFun := toFun✝, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ }
⊢ { toFun := toFun✝¹, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } =
    { toFun := toFun✝, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ }
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
k N : ℕ
hN : ∀ (x : L), (LieAlgebra.ad R L) x ^ N = 0
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
x✝¹ : L
x✝ : M
⊢ ((AlgebraTensorModule.curry (f₁ ^ N)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝

Tactic:
simp [f₁, hN]

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
this : ⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ x ∈ corootSpace α ↔ ↑x ∈ Submodule.span R (⇑H.subtype '' s)

Tactic:
mem_corootSpace,

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
this : ⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ ↑x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x} ↔
    ↑x ∈ Submodule.span R (⇑H.subtype '' s)
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁.comp l r = B₂.comp l r
x' y' : M
⊢ ((B₁.comp l r) x') y' = ((B₂.comp l r) x') y'

Tactic:
h

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁.comp l r = B₂.comp l r
x' y' : M
⊢ ((B₂.comp l r) x') y' = ((B₂.comp l r) x') y'
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁ = B₂
⊢ B₁.comp l r = B₂.comp l r

Tactic:
h

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁ = B₂
⊢ B₂.comp l r = B₂.comp l r
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : flipHom B = B
x y : M
⊢ ((flipHom B) y) x = (B y) x

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : flipHom B = B
x y : M
⊢ (B y) x = (B y) x
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h : ∀ (x : M), (B x) x = (C x) x
x y : M
⊢ ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2 = ((C (x + y)) (x + y) - (C x) x - (C y) y) / 2

Tactic:
h

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : b i ∈ tx
j : ι
h₂ : b j ∈ ty
⊢ fx (b i) * (fy (b j) * (B (b i)) (b j)) = fx (b i) * (fy (b j) * (B (b j)) (b i))

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : b i ∈ tx
j : ι
h₂ : b j ∈ ty
⊢ fx (b i) * (fy (b j) * (B (b j)) (b i)) = fx (b i) * (fy (b j) * (B (b j)) (b i))
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : 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 y : L
hx : x ∈ H
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
hv' : ⁅x, v⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆ ∈ lieSpan R L (range b.e)

Tactic:
exact sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ∀ (i j : ι), (B (v i)) (b j) = if j = i then 1 else 0
x✝¹ x✝ : ι
⊢ (if x✝ = x✝¹ then 1 else 0) = (B (v x✝¹)) (b x✝)

Tactic:
h

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ∀ (i j : ι), (B (v i)) (b j) = if j = i then 1 else 0
x✝¹ x✝ : ι
⊢ (if x✝ = x✝¹ then 1 else 0) = if x✝ = x✝¹ then 1 else 0
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: 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
a✝ : ∀ (y : LieIdeal K L), InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ finrank K ↥x) y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ False

Tactic:
apply hJ.1

Goal state after:
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
a✝ : ∀ (y : LieIdeal K L), InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ finrank K ↥x) y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := ⋯
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J = ⊥
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ LieModule.IsIrreducible R L L

Tactic:
by
  suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩
  rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial]
  have _i : ¬ IsLieAbelian L := IsSimple.non_abelian R
  contrapose _i
  infer_instance

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
hI : IsLieAbelian ↥⊤
⊢ False

Tactic:
lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
hI : IsLieAbelian L
⊢ False
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 χ ≠ ⊥
t : R
x : L
⊢ finrank R ↥(genWeightSpace M χ) • χ (t • x) = finrank R ↥(genWeightSpace M χ) • t • χ x

Tactic:
smul_comm,

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 χ ≠ ⊥
t : R
x : L
⊢ finrank R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank R ↥(genWeightSpace M χ) • χ x
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case inr
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
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain ⟨J, hJs, hJI⟩ : ∃ J ∈ s, ¬ J ≤ I := by
    by_contra! H
    exact hI.ne (le_antisymm hI.le (s.sup_le H))

Goal state after:
case inr
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
hJI : ¬J ≤ I
⊢ ∃ t ⊆ s, I = t.sup id
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h : ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
⊢ ¬(f = 0 ∧ g = 0)

pp: case refine_2
K : Type v
inst✝ : Field K
f g : K[X]
h : ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
⊢ x ∣ f → ¬x ∣ g

Tactic:
· replace h := @h K _ _ _ 0
    contrapose! h
    rw [h.left, h.right, map_zero, and_self]

Goal state after:
case refine_2
K : Type v
inst✝ : Field K
f g : K[X]
h : ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
⊢ x ∣ f → ¬x ∣ g
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
h

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : 0 = n.succ
h : f.natDegree = 0
⊢ False
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian ↥⊤
⊢ IsLieAbelian L

Tactic:
lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv

Goal state after:
case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian L
⊢ IsLieAbelian L