mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case e_s
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 : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
⊢ {α | rootSpace H ⇑↑α ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q) hq) H} = {i | (rootSystem H).root i ∈ ↑q}

Tactic:
;

Goal state after:
case e_s
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 : ↥(rootSystem H).invtRootSubmodule
hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
⊢ {α | rootSpace H ⇑↑α ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q) hq) H} = {i | (rootSystem H).root i ∈ ↑q}
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 ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
i✝ : I
⊢ (aeval (⇑f ∘ X)) (X i✝) = f (X i✝)

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
i✝ : I
⊢ (aeval (⇑f ∘ X)) (X i✝) = f (X i✝)
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₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.map (Submodule.subtype pres.ker) (Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩)) =
    Submodule.map (Submodule.subtype pres.ker) ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span,
      Submodule.coe_subtype, Ideal.submodule_span_eq]

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₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Ideal.span (Subtype.val '' Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = pres.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 ι σ
r : σ
a✝ : ι
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R ι).repr ((D R (MvPolynomial ι R)) (pres.relation r))))))
      a✝

Tactic:
;

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 ι σ
r : σ
a✝ : ι
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R ι).repr ((D R (MvPolynomial ι R)) (pres.relation r))))))
      a✝
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.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ mk x ∈ Submodule.restrictScalars P.Ring (map f).ker

Tactic:
suffices f.toRingHom x ∈ P'.ker ^ 2 by simpa [mk_eq_zero_iff]

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.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ f.toRingHom ↑x ∈ P'.ker ^ 2
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁷ : Ring A
ι : Type w
inst✝⁶ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (M i)
inst✝⁴ : (i : ι) → Module A (M i)
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
solution : (i : ι) → (relations i).Solution (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N✝ : Type w'
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (Relations.directSum relations).Solution N✝
i : ι
g : (relations i).G
⊢ ((directSum solution).postcomp (toModule A ι N✝ fun i ↦ ⋯.desc (directSumEquiv s i))).var ⟨i, g⟩ = s.var ⟨i, g⟩

Tactic:
;

Goal state after:
A : Type u
inst✝⁷ : Ring A
ι : Type w
inst✝⁶ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (M i)
inst✝⁴ : (i : ι) → Module A (M i)
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
solution : (i : ι) → (relations i).Solution (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N✝ : Type w'
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (Relations.directSum relations).Solution N✝
i : ι
g : (relations i).G
⊢ ((directSum solution).postcomp (toModule A ι N✝ fun i ↦ ⋯.desc (directSumEquiv s i))).var ⟨i, g⟩ = s.var ⟨i, g⟩
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

Goal state after:
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
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
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
s : P.Ring
hs : s ∈ P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨r • s, ⋯⟩ = 1 ⊗ₜ[P.Ring] (r • ⟨s, hs⟩)

Tactic:
;

Goal state after:
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
s : P.Ring
hs : s ∈ P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨r • s, ⋯⟩ = 1 ⊗ₜ[P.Ring] (r • ⟨s, hs⟩)
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators 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✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) ((fun f ↦ ⟨f.toAlgHom, ⋯⟩) f)).val x✝) =
    coeff m✝ (f.val x✝)

Tactic:
;

Goal state after:
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators 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✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) ((fun f ↦ ⟨f.toAlgHom, ⋯⟩) f)).val x✝) =
    coeff m✝ (f.val x✝)
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators 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✝ : IsScalarTower R S S'
f : { f // ∀ (x : P.Ring), (aeval P'.val) (f x) = (algebraMap S S') ((aeval P.val) x) }
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (↑((fun f ↦ ⟨f.toAlgHom, ⋯⟩) ((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) f)) (X i✝)) =
    coeff m✝ (↑f (X i✝))

Tactic:
;

Goal state after:
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹¹ : CommRing R''
inst✝¹⁰ : CommRing S''
inst✝⁹ : Algebra R'' S''
P'' : Generators 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✝ : IsScalarTower R S S'
f : { f // ∀ (x : P.Ring), (aeval P'.val) (f x) = (algebraMap S S') ((aeval P.val) x) }
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (↑((fun f ↦ ⟨f.toAlgHom, ⋯⟩) ((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) f)) (X i✝)) =
    coeff m✝ (↑f (X i✝))
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ False

Tactic:
;

Goal state after:
A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ False
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
relations : Relations A
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module A M
inst✝² : IsEmpty relations.R
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (relations.G →₀ A) →ₗ[A] N✝
h : relations.solutionFinsupp.postcomp f✝ = relations.solutionFinsupp.postcomp f'✝
a✝ : relations.G
⊢ (f✝ ∘ₗ Finsupp.lsingle a✝) 1 = (f'✝ ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
;

Goal state after:
A : Type u
inst✝⁵ : Ring A
relations : Relations A
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module A M
inst✝² : IsEmpty relations.R
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (relations.G →₀ A) →ₗ[A] N✝
h : relations.solutionFinsupp.postcomp f✝ = relations.solutionFinsupp.postcomp f'✝
a✝ : relations.G
⊢ (f✝ ∘ₗ Finsupp.lsingle a✝) 1 = (f'✝ ∘ₗ Finsupp.lsingle a✝) 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 ι
i✝ : ι
⊢ (Hom.id P).toAlgHom (X i✝) = (AlgHom.id R P.Ring) (X i✝)

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
i✝ : ι
⊢ (Hom.id P).toAlgHom (X i✝) = (AlgHom.id R P.Ring) (X i✝)
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 1}

Tactic:
;

Goal state after:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 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 ι
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✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)

Tactic:
;

Goal state after:
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✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)
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 S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val x✝)

Tactic:
;

Goal state after:
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 S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val x✝)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case mul_X
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators 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 R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial ι R
i : ι
hp : (g.comp f).toAlgHom p = g.toAlgHom (f.toAlgHom p)
⊢ g.toAlgHom (f.toAlgHom p) * (aeval g.val) (f.val i) = g.toAlgHom (f.toAlgHom p) * g.toAlgHom (f.val i)

Tactic:
;

Goal state after:
case mul_X
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' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators 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 R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial ι R
i : ι
hp : (g.comp f).toAlgHom p = g.toAlgHom (f.toAlgHom p)
⊢ g.toAlgHom (f.toAlgHom p) * (aeval g.val) (f.val i) = g.toAlgHom (f.toAlgHom p) * g.toAlgHom (f.val i)
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
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.toComp P).toAlgHom = aeval (X ∘ Sum.inr)

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.toComp P).toAlgHom = aeval (X ∘ Sum.inr)
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

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

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
r : presM.R
⊢ ∀ (b : B) (f : presM.R →₀ B),
    r ∉ f.support →
      b ≠ 0 →
        f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r b + f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 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
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
p : P.Ring
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Q.ofComp P).toAlgHom.comp (rename Sum.inr)) (X i✝)) =
    coeff m✝ (((IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i✝))

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
p : P.Ring
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Q.ofComp P).toAlgHom.comp (rename Sum.inr)) (X i✝)) =
    coeff m✝ (((IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i✝))
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 ι
x✝ : P.toExtension.Ring
⊢ (Hom.id P).toExtensionHom.toRingHom x✝ = (Extension.Hom.id P.toExtension).toRingHom x✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
x✝ : P.toExtension.Ring
⊢ (Hom.id P).toExtensionHom.toRingHom x✝ = (Extension.Hom.id P.toExtension).toRingHom x✝