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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ (fun s ↦ s • (linearCombination R i) ↑x = 0) = fun s ↦ s • (linearCombination R i) ↑x = s • 0

pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ ∃ s, s • (linearCombination R i) ↑x = s • 0

Tactic:
· simp only [smul_zero]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ ∃ s, s • (linearCombination R i) ↑x = s • 0
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ π ↑x = 0

Tactic:
← LinearMap.mem_ker,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
x : ↥τ
⊢ ↑x ∈ π.ker
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ f.range ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker

Tactic:
rw [LinearMap.range_eq_map, ← hg₁, Submodule.map_span, Submodule.span_le,
            Set.image_subset_iff]

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Set.range g₁ ⊆ ⇑f ⁻¹' ↑(⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
x : R
⊢ ↑((supportedEquivMvPolynomial s).symm (C x)) = ↑((algebraMap R ↥(supported R s)) x)

Tactic:
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]

Goal state after:
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
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
h' : Module.Finite R M
⊢ ∃ d k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)

Tactic:
obtain ⟨d, s, hs⟩ := @Module.Finite.exists_fin _ _ _ _ _ h'

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
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
h' : Module.Finite R M
d : ℕ
s : Fin d → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ d k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ((LinearMap.toSpanSingleton R M ⋯.choose) 1)) =
    (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) (Submodule.Quotient.mk 1)

Tactic:
LinearMap.toSpanSingleton_apply_one,

Goal state after:
case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ⋯.choose) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) (Submodule.Quotient.mk 1)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
s : Fin d → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)

Tactic:
induction d generalizing M with

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (mkDerivation R) 1 = derivative'

Tactic:
ext : 1
  simp [derivative']

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case zero
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
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ ∀ (i : ι), x • 1 ∈ R ∙ p i ^ n i

Tactic:
← Quotient.mk_eq_zero

Goal state after:
case zero
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
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ ∀ (i : ι), Submodule.Quotient.mk (x • 1) = 0
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case succ
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
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin (m + 1)),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ 0 ∈ annihilator R M

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
r : R
hrp : r ∈ S
H : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) f)
⊢ Submonoid.powers r ≤ S

Tactic:
simpa [Submonoid.powers_le]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m) * C ((algebraMap R S) ↑m) = C ((algebraMap R S) a)

Tactic:
← map_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
m : ↥M
⊢ C (IsLocalization.mk' S a m * (algebraMap R S) ↑m) = C ((algebraMap R S) a)
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
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:
· intro p q _ _ hp hq
      simp [hp, hq]

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),
    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 h
σ : 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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := ⋯
⊢ (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X ()) = 1

Tactic:
← map_mul,

Goal state after:
case h
σ : 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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r * X ()) = 1
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
⊢ (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) 1 =
    (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x)

Tactic:
← map_mul,

Goal state after:
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
⊢ (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) 1 = (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r * X x)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mem.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
χ : Weight K (↥H) L
x_χ : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
m_α : L
hm_α : m_α ∈ sl2SubmoduleOfRoot ⋯
⊢ ⁅x_χ, m_α⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
| mem α m_α hm_α =>

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

Goal state before:
pp: case mem.add
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
χ : Weight K (↥H) L
x_χ : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
m₁ m₂ : L
hx✝ : m₁ ∈ ⨆ i, sl2SubmoduleOfRoot ⋯
hy✝ : m₂ ∈ ⨆ i, sl2SubmoduleOfRoot ⋯
ih₁ : ⁅x_χ, m₁⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
ih₂ : ⁅x_χ, m₂⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
⊢ ⁅x_χ, m₁⁆ + ⁅x_χ, m₂⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)

Tactic:
exact add_mem ih₁ ih₂

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

Goal state before:
pp: case add
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
x₁ x₂ : L
hx✝ : x₁ ∈ ⨆ i, genWeightSpace L ⇑i
hy✝ : x₂ ∈ ⨆ i, genWeightSpace L ⇑i
ih₁ : ⁅x₁, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
ih₂ : ⁅x₂, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
⊢ ⁅x₁, m⁆ + ⁅x₂, m⁆ ∈ ↑(⨆ α, sl2SubmoduleOfRoot ⋯)

Tactic:
exact add_mem ih₁ ih₂

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

Goal state before:
pp: 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 := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
χ : Weight K (↥H) L
hχ : Weight.toLinear K (↥H) L χ ∈ q
heq : ⇑χ = ⇑↑α
⊢ (rootSystem H).root α ∈ q

Tactic:
simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ

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

Goal state before:
pp: 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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ ⨆ α ∈ J.rootSet, sl2SubmoduleOfRoot ⋯ = LieSubmodule.restr I H

Tactic:
I.restr_eq_iSup_sl2SubmoduleOfRoot

Goal state after:
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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ ⨆ α ∈ J.rootSet, sl2SubmoduleOfRoot ⋯ = ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
a : MvPolynomial ι T
ha : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
b : MvPolynomial ι T
hb : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) b = y
⊢ x + (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) b = x + y

Tactic:
hb

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
a : MvPolynomial ι T
ha : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
b : MvPolynomial ι T
hb : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) b = y
⊢ x + y = x + y
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M ↔ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
by
  constructor
  · intro
    obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (finite_def.1 (inferInstance : Module.Finite A M))
    obtain ⟨R : Type w₁, _, relation, hR⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var) (by
          rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))
    exact
     ⟨{ G := G
        R := R
        relation := relation
        var := var
        linearCombination_var_relation := fun r ↦ by
          rw [Submodule.ext_iff] at hR
          exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
        toIsPresentation := by
          rw [Relations.Solution.isPresentation_iff]
          exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩
  · rintro ⟨pres, _, _⟩
    exact pres.finitePresentation

Goal state after:
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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x : P.Ring
⊢ (aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((aeval P.val) x)

Tactic:
by
  suffices ((MvPolynomial.aeval P'.val).restrictScalars R).comp f.toAlgHom =
      (IsScalarTower.toAlgHom R S S').comp (MvPolynomial.aeval P.val) from
    DFunLike.congr_fun this x
  apply MvPolynomial.algHom_ext
  intro i
  simp [Hom.toAlgHom]

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

Goal state before:
pp: case refine_1.refine_2
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
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
⊢ ∀ (hy : b ∈ P.ker • P.ker), 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 0

Tactic:
hb

Goal state after:
case refine_1.refine_2
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
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 0