mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case mp.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
hx : (linearCombination R Subtype.val) x = 0
⊢ f (b.repr.symm (mapDomain σ x)) = x

Tactic:
simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]

Goal state after:
case mp.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
hx : (linearCombination R Subtype.val) x = 0
⊢ mapDomain π (mapDomain σ x) = x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
h : a * b ∈ I ^ 0
⊢ a ∈ I ∨ b ∈ I ^ 0

pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
· simp

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Field K
ι✝ : ?m.1
inst✝¹ : IsDedekindDomain R
ι : Type u_4
inst✝ : Fintype ι
I : Ideal R
P : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), Prime (P i)
coprime : Pairwise fun i j ↦ P i ≠ P j
prod_eq : ∏ i, P i ^ e i = I
⊢ Pairwise fun i j ↦ { asIdeal := P i, isPrime := ⋯, ne_bot := ⋯ } ≠ { asIdeal := P j, isPrime := ⋯, ne_bot := ⋯ }

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ supported R s = (rename Subtype.val).range

Tactic:
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename_eq_aeval]

Goal state after:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ (aeval fun x ↦ X ↑x).range = (aeval (X ∘ Subtype.val)).range
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : ↥(factors ⊤.annihilator).toFinset
⊢ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Tactic:
← torsionBySet_span_singleton_eq,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : ↥(factors ⊤.annihilator).toFinset
⊢ torsionBySet R M ↑(R ∙ IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ D (p * X i) + D (q * X i) = (p + q) • D (X i) + X i • (D p + D q)

Tactic:
hp,

Goal state after:
case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ p • D (X i) + X i • D p + D (q * X i) = (p + q) • D (X i) + X i • (D p + D q)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu : IsUnit ((algebraMap R Rₛ) ↑⟨t, ⋯⟩)
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ↑s₂ • ↑s₀ • (↑hu₀.unit⁻¹ • lₛ') ∘ₗ lₛ = ↑s₂ • ↑s₀ • LinearMap.id

Tactic:
rw [LinearMap.smul_comp, ← smul_assoc s₀.1, Algebra.smul_def s₀.1, IsUnit.mul_val_inv, one_smul]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu : IsUnit ((algebraMap R Rₛ) ↑⟨t, ⋯⟩)
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ↑s₂ • lₛ' ∘ₗ lₛ = ↑s₂ • ↑s₀ • LinearMap.id
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case refine_3
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (fun a_1 b ↦ (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) =
    (monomial (s - single i 1)) (a * ↑(s i))

Tactic:
· simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : ¬n = m + single i 1
hn : ¬n i = 0
x✝ : σ
⊢ (single i 1) x✝ ≤ n x✝

Tactic:
by grind

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ (aeval fun x ↦ invSelf r) 0 = 0

pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (x y : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      y ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
        (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) y = 0 → (aeval fun x ↦ invSelf r) (x + y) = 0

pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
· simp

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (x y : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      y ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
        (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) y = 0 → (aeval fun x ↦ invSelf r) (x + y) = 0

case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
intro a x _ hx

Goal state after:
case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
a x : MvPolynomial Unit R
hx✝ : x ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
hx : (aeval fun x ↦ invSelf r) x = 0
⊢ (aeval fun x ↦ invSelf r) (a • x) = 0
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
⊢ ∀ (a x : MvPolynomial Unit R),
    x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
· intro a x _ hx
      simp [hx]

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

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : ¬Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
w_chi : ¬Weight.toLinear K (↥H) L χ = 0
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)
y : ↥H.toLieSubmodule
hy : y ∈ ↑↑(corootSpace ⇑α)
hm_eq : m_αneg + ↑H.toLieSubmodule.incl y = m_α
hm_α_decomp : m_α = m_pos + m_neg + ↑H.toLieSubmodule.incl y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑H.toLieSubmodule.incl y⁆
h_chi_in_q : Weight.toLinear K (↥H) L χ ∉ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
· exact chi_not_in_q_aux q hq χ x_χ m_α hx_χ α hαq hα₀ w_plus w_minus w_chi m_pos m_neg y hy
      h_bracket_sum h_pos_containment h_neg_containment h_chi_in_q

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))) (X x) =
    ((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x)

Tactic:
simp only [auxInv, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
      Function.comp_apply, auxHom_mk, aeval_X, RingHomCompTriple.comp_eq, invSelf, Away.lift,
      lift_mk'_spec]
    simp only [map_one]
    rw [← map_one (Ideal.Quotient.mk _), ← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem,
      ← Ideal.neg_mem_iff, neg_sub]
    exact Ideal.mem_span_singleton_self (C r * X x - 1)

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

Goal state before:
pp: case mem
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
χ : Weight K (↥H) L
x_χ : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
⊢ ⁅x_χ, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂

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

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
J : LieIdeal K L := ⋯
⊢ α ∈ J.rootSet → (rootSystem H).root α ∈ q

Tactic:
intro hα_mem
    by_contra hα_not
    have hα_nz := H.isNonZero_coe_root α
    have hne (χ : Weight K H L) (hχ : ↑χ ∈ q) : (χ : H → K) ≠ ((α : Weight K H L) : H → K) :=
      fun heq ↦ hα_not (by simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ)
    have h_le : J.restr H ≤ ⨆ (χ : H → K) (_ : χ ≠ (α : Weight K H L)), genWeightSpace L χ := by
      refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_
      rw [sl2SubmoduleOfRoot_eq_sup]
      refine sup_le (sup_le ?_ ?_) ?_
      · exact le_iSup₂_of_le _ (hne β hβ_mem) le_rfl
      · have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
        exact le_iSup₂_of_le _ (hne (-β) this) le_rfl
      · apply (LieSubmodule.map_incl_le.trans (rootSpace_zero_eq K L H).symm.le).trans
        exact le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl
    have h_disj := ((iSupIndep_genWeightSpace K H L _).mono_right h_le).mono_right hα_mem
    exact (α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ Finsupp.single () 1 ≠ 0

pp: case refine_2
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ ∀ (f : Unit →₀ ℕ), (rename Sum.inr) (P.σ 0) * (monomial (Finsupp.mapDomain Sum.inl f)) 1 = 0

pp: case refine_3
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (rename Sum.inr) (P.σ g) * (monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1))) 1 +
      (rename Sum.inr) (P.σ (-1)) * (monomial (Finsupp.mapDomain Sum.inl 0)) 1 =
    (rename Sum.inr) (P.σ g) * X (Sum.inl ()) + C (-1)

Tactic:
· simp

Goal state after:
case refine_2
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ ∀ (f : Unit →₀ ℕ), (rename Sum.inr) (P.σ 0) * (monomial (Finsupp.mapDomain Sum.inl f)) 1 = 0

case refine_3
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (rename Sum.inr) (P.σ g) * (monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1))) 1 +
      (rename Sum.inr) (P.σ (-1)) * (monomial (Finsupp.mapDomain Sum.inl 0)) 1 =
    (rename Sum.inr) (P.σ g) * X (Sum.inl ()) + C (-1)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
s : Set S
hs : adjoin R s = ⊤
⊢ Function.Surjective ⇑(aeval Subtype.val)

Tactic:
rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
    Subtype.range_coe_subtype, Set.ofPred_mem_eq]

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

Goal state before:
pp: case refine_1.refine_1
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
⊢ ∀ (r : P.Ring) (hr : r ∈ P.ker) (n : P.Ring) (hn : n ∈ P.ker), 1 ⊗ₜ[P.Ring] ⟨r • n, ⋯⟩ = 0

Tactic:
intro r hr s hs
      trans (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩
      · rw [smul_tmul]; rfl
      · simp_all [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case zero
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ 0 ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

pp: case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ ∀ (a : presM.R) (b : B) (f : presM.R →₀ B),
    a ∉ f.support →
      b ≠ 0 →
        f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single a b + f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
· simp

Goal state after:
case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ ∀ (a : presM.R) (b : B) (f : presM.R →₀ B),
    a ∉ f.support →
      b ≠ 0 →
        f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single a b + f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)