mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
⊢ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) ≤
    RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val)

pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
⊢ RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val) ≤
    Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
·

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
⊢ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) ≤
    RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val)
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

pp: case mpr
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 := ⋯
⊢ (rootSystem H).root α ∈ q → α ∈ J.rootSet

Tactic:
·

Goal state after:
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
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
⊢ RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val) ≤
    Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
·

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
⊢ RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val) ≤
    Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case refine_2
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
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ genWeightSpace L (-⇑↑⟨β, ⋯⟩) ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ

pp: case refine_3
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
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ corootSubmodule ↑⟨β, ⋯⟩ ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ

Tactic:
·

Goal state after:
case refine_2
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
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ genWeightSpace L (-⇑↑⟨β, ⋯⟩) ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case refine_3
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
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ corootSubmodule ↑⟨β, ⋯⟩ ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ

Tactic:
·

Goal state after:
case refine_3
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
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ corootSubmodule ↑⟨β, ⋯⟩ ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mpr
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 := ⋯
⊢ (rootSystem H).root α ∈ q → α ∈ J.rootSet

Tactic:
·

Goal state after:
case mpr
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 := ⋯
⊢ (rootSystem H).root α ∈ q → α ∈ J.rootSet
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝¹ : Ideal.span (Set.range s) = P.ker
hs✝ : Submodule.span P.Ring (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤
⊢ Submodule.span S (Set.range fun i ↦ mk ⟨s i, ⋯⟩) = ⊤

pp: case hs
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝ : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker

Tactic:
·

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝¹ : Ideal.span (Set.range s) = P.ker
hs✝ : Submodule.span P.Ring (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤
⊢ Submodule.span S (Set.range fun i ↦ mk ⟨s i, ⋯⟩) = ⊤
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case hs
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝ : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker

Tactic:
·

Goal state after:
case hs
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝ : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case mp
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) → x ∈ Set.range Q.relation

pp: case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)

Tactic:
·

Goal state after:
case mp
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) → x ∈ Set.range Q.relation
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)

Tactic:
·

Goal state after:
case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)
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:
·

Goal state after:
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
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
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:
·

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
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : P.Cotangent
hx : x ∈ Submodule.restrictScalars P.Ring (map f).ker
⊢ x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

pp: case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : P.Cotangent
hx : x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
⊢ x ∈ Submodule.restrictScalars P.Ring (map f).ker

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : P.Cotangent
hx : x ∈ Submodule.restrictScalars P.Ring (map f).ker
⊢ x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
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:
·

Goal state after:
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.Basic

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : P.Cotangent
hx : x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
⊢ x ∈ Submodule.restrictScalars P.Ring (map f).ker

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : P.Cotangent
hx : x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
⊢ x ∈ Submodule.restrictScalars P.Ring (map f).ker
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ Extension.Cotangent.mk ((fun r ↦ ⟨pres.relation r, ⋯⟩) r) ∈ φ.range

Tactic:
simp only [LinearMap.mem_range]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ ∃ y, φ y = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

pp: case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
·

Goal state after:
case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
·

Goal state after:
case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: case mp
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

pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M

Tactic:
·

Goal state after:
case mp
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
Module: Mathlib.Algebra.Module.Presentation.Finite

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

Tactic:
·

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M