awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R S S'
inst_17 : Algebra R R''
inst_18 : Algebra R S''
inst_19 : IsScalarTower R R'' S''
inst_20 : IsScalarTower R S S''
inst_21 : IsScalarTower R' R'' S''
inst_22 : IsScalarTower R' S' S''
inst_23 : IsScalarTower S S' S''
inst_24 : IsScalarTower R R' R''
inst_25 : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
toRingHom :
  ∀ (x : P.toExtension.Ring),
    Eq (α := P''.toExtension.Ring)
      ((Extension.Hom.toRingHom (toExtensionHom (f.comp g)) : (a : P.toExtension.Ring) → P''.toExtension.Ring) x :
        P''.toExtension.Ring)
      ((Extension.Hom.toRingHom (Extension.Hom.comp f.toExtensionHom g.toExtensionHom) :
            (a : P.toExtension.Ring) → P''.toExtension.Ring)
          x :
        P''.toExtension.Ring)
⊢ Eq (α := P.toExtension.Hom P''.toExtension) (toExtensionHom (f.comp g))
    (Extension.Hom.comp f.toExtensionHom g.toExtensionHom)

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R S S'
inst_17 : Algebra R R''
inst_18 : Algebra R S''
inst_19 : IsScalarTower R R'' S''
inst_20 : IsScalarTower R S S''
inst_21 : IsScalarTower R' R'' S''
inst_22 : IsScalarTower R' S' S''
inst_23 : IsScalarTower S S' S''
inst_24 : IsScalarTower R R' R''
inst_25 : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
x : P.toExtension.Ring
⊢ Eq (α := P''.toExtension.Ring)
    ((Extension.Hom.toRingHom (toExtensionHom (f.comp g)) : (a : P.toExtension.Ring) → P''.toExtension.Ring) x :
      P''.toExtension.Ring)
    ((Extension.Hom.toRingHom (Extension.Hom.comp f.toExtensionHom g.toExtensionHom) :
          (a : P.toExtension.Ring) → P''.toExtension.Ring)
        x :
      P''.toExtension.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
x : P.toExtension.Ring
⊢ Eq (α := P'.toExtension.Ring)
    ((Extension.Hom.toAlgHom f.toExtensionHom : (a : P.toExtension.Ring) → P'.toExtension.Ring) x : P'.toExtension.Ring)
    ((f.toAlgHom : (a : P.Ring) → P'.Ring) x : P'.Ring)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
simp :
  Eq (α := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (↑(aeval P.val) : MvPolynomial ι R →+* S))
    (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))
⊢ P.ker = RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)

Tactic:
simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq]

Premises used: Algebra.Generators.ker, Algebra.Extension.ker, Algebra.Generators.algebraMap_eq, Algebra.Generators.toExtension_Ring
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
⊢ Eq (α := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (↑(aeval P.val) : MvPolynomial ι R →+* S))
    (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
ι : Type w
inst : CommRing R
⊢ Eq (α := Ideal (Generators.Ring (S := MvPolynomial ι R) (mvPolynomial R ι))) (ker (mvPolynomial R ι)) ⊥

Tactic:
simp [ker_eq_ker_aeval_val, SetLike.ext_iff, aeval_X_left]

Premises used: MvPolynomial.aeval_X_left, SetLike.ext_iff, Algebra.Generators.ker_eq_ker_aeval_val
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
x : P.Ring
hx : x ∈ P.ker
rwa rwa₁ rwa₂ rwa₃ : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
⊢ Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) (0 : S)

Tactic:
rwa [← algebraMap_apply]

Premises used: Algebra.Generators.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
inst : CommRing R
σ : Type u_8
I : Ideal (MvPolynomial σ R)
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
⊢ (naive s hs).ker = I

Tactic:
I.mk_ker

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, AddMonoidAlgebra, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
change :
  Eq (α := Ideal (ofAlgHom f h).toExtension.Ring)
    (RingHom.ker (F := (ofAlgHom f h).toExtension.Ring →+* S) (algebraMap (ofAlgHom f h).toExtension.Ring S))
    (RingHom.ker f.toRingHom)
⊢ (ofAlgHom f h).ker = RingHom.ker f.toRingHom

Tactic:
change RingHom.ker _ = _

Premises used: RingHom.ker
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
e_f : algebraMap (ofAlgHom f h).toExtension.Ring S = f.toRingHom
⊢ Eq (α := Ideal (ofAlgHom f h).toExtension.Ring)
    (RingHom.ker (F := (ofAlgHom f h).toExtension.Ring →+* S) (algebraMap (ofAlgHom f h).toExtension.Ring S))
    (RingHom.ker f.toRingHom)

Tactic:
congr
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ ∀ (r : R),
    Eq.{v + 1} (α := S)
      ((algebraMap (ofAlgHom f h).toExtension.Ring S : (a : MvPolynomial I R) → S)
          ((C : (a : R) → MvPolynomial I R) r : MvPolynomial I R) :
        S)
      ((f.toRingHom : (a : MvPolynomial I R) → S) ((C : (a : R) → MvPolynomial I R) r : MvPolynomial I R) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ ∀ (i : I),
    Eq.{v + 1} (α := S) ((algebraMap (ofAlgHom f h).toExtension.Ring S : (a : MvPolynomial I R) → S) (X i) : S)
      ((f.toRingHom : (a : MvPolynomial I R) → S) (X i) : S)

Tactic:
simp [ofAlgHom]

Premises used: Algebra.Generators.ofAlgHom
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ algebraMap (ofAlgHom f h).toExtension.Ring S = f.toRingHom

Tactic:
exact MvPolynomial.ringHom_ext (by simp) (by simp [ofAlgHom])

Premises used: MvPolynomial.ringHom_ext
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
rw : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval (P.ofAlgEquiv e).val) = P.ker
rw₁ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval ((⇑e : (a : S) → T) ∘ P.val)) = P.ker
rw₂ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval fun (x : ι) ↦ (e : (a : S) → T) (P.val x)) = P.ker
rw₃ :
  RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval fun (x : ι) ↦ ((↑e : S →ₐ[R] T) : (a : S) → T) (P.val x)) = P.ker
rw₄ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (AlgHom.comp (↑e : S →ₐ[R] T) (aeval P.val)) = P.ker
rw₅ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →ₐ[R] T) (↑e : S →ₐ[R] T)) = P.ker
rw₆ :
  Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →+* T) (↑(↑e : S →ₐ[R] T) : S →+* T)) =
    P.ker
rw₇ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →+* T) (↑e : S →+* T)) = P.ker
rw₈ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) ⊥ = P.ker
rw₉ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) = P.ker
rw₁₀ rw₁₁ : P.ker = P.ker
⊢ (P.ofAlgEquiv e).ker = P.ker

Tactic:
rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
    ← MvPolynomial.comp_aeval, ← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom,
    AlgHomClass.toRingHom_toAlgHom, AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot,
    ← ker_eq_ker_aeval_val]

Premises used: AlgHomClass.toRingHom_toAlgHom, AlgHom.coe_coe, AlgHom.comap_ker, AlgHom.ker_coe_equiv, MvPolynomial.comp_aeval, RingHom.ker_coe_toRingHom, Function.comp_def, RingHom.ker_eq_comap_bot, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Generators.ofAlgEquiv_val
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
a :
  LE.le (α := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker)
    (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)))
a₁ :
  LE.le (α := Ideal (Generators.Ring (Q.comp P)))
    (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker)
⊢ Eq (α := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker)
    (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
a :
  P.ker ≤
    Ideal.comap (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P))
      (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)))
⊢ LE.le (α := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker)
    (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)))

Tactic:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
hf :
  ∀ (i : ι),
    Eq (α := Q.Ring)
      ((AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (Hom.toAlgHom (Q.toComp P)) :
            (a : MvPolynomial ι R) → Q.Ring)
          (X i) :
        Q.Ring)
      ((IsScalarTower.toAlgHom R P.Ring Q.Ring : (a : MvPolynomial ι R) → Q.Ring) (X i) : Q.Ring)
⊢ Eq (α := P.Ring →ₐ[R] Q.Ring)
    (AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (Hom.toAlgHom (Q.toComp P)))
    (IsScalarTower.toAlgHom R P.Ring Q.Ring)

Tactic:
ext1
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
i : ι
⊢ Eq (α := Q.Ring)
    ((AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (Hom.toAlgHom (Q.toComp P)) :
          (a : MvPolynomial ι R) → Q.Ring)
        (X i) :
      Q.Ring)
    ((IsScalarTower.toAlgHom R P.Ring Q.Ring : (a : MvPolynomial ι R) → Q.Ring) (X i) : Q.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
this :
  Eq (α := P.Ring →ₐ[R] Q.Ring)
    (AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (Hom.toAlgHom (Q.toComp P)))
    (IsScalarTower.toAlgHom R P.Ring Q.Ring)
a : Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
⊢ Membership.mem (γ := Submodule P.Ring P.Ring)
    (Ideal.comap (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P))
      (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P))))
    x

Tactic:
simp only [Ideal.mem_comap,
      RingHom.mem_ker, ← AlgHom.comp_apply, this, IsScalarTower.toAlgHom_apply]

Premises used: AlgHom.comp_apply, RingHom.mem_ker, Ideal.mem_comap, IsScalarTower.toAlgHom_apply
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
this :
  Eq (α := P.Ring →ₐ[R] Q.Ring)
    (AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (Hom.toAlgHom (Q.toComp P)))
    (IsScalarTower.toAlgHom R P.Ring Q.Ring)
a :
  Eq (α := Q.Ring) ((algebraMap S Q.Ring : (a : S) → Q.Ring) ((algebraMap P.Ring S : (a : P.Ring) → S) x) : Q.Ring)
    (0 : Q.Ring)
a₁ : Eq (α := Q.Ring) ((algebraMap S Q.Ring : (a : S) → Q.Ring) 0) 0
a₂ a₃ : Eq (α := Q.Ring) 0 0
⊢ Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)

Tactic:
rw [IsScalarTower.algebraMap_apply P.Ring S, hx, map_zero]

Premises used: Algebra.Generators.Ring, map_zero, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
this :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ v ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x),
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) x))
⊢ Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) x

Tactic:
simpa only [AlgHom.toRingHom_eq_coe, Finset.sum_map, Equiv.coe_toEmbedding,
        EquivLike.coe_coe, AddEquiv.symm_apply_apply, support_sum_monomial_coeff] using this

Premises used: Equiv.coe_toEmbedding, Finset.sum_map, AddEquiv.symm_apply_apply, AlgHom.toRingHom_eq_coe, MvPolynomial.support_sum_monomial_coeff, EquivLike.coe_coe
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
a :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ v ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x),
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) x))
⊢ Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker) x

Tactic:
suffices ∑ v ∈ (support x).map e, (monomial (e.symm v)) (coeff (e.symm v) x) ∈
        Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker by
      simpa only [AlgHom.toRingHom_eq_coe, Finset.sum_map, Equiv.coe_toEmbedding,
        EquivLike.coe_coe, AddEquiv.symm_apply_apply, support_sum_monomial_coeff] using this
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
a :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ j ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)),
      ∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = j,
        (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ v ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x),
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) x))

Tactic:
rw [← Finset.sum_fiberwise_of_maps_to (fun i ↦ Finset.mem_image_of_mem Prod.fst)]

Premises used: Finset.sum_fiberwise_of_maps_to, Prod.fst, Finset.mem_image_of_mem
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ j ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)),
      ∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = j,
        (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))

Tactic:
sum_mem fun i hi ↦ ?_

Premises used: Set.Mem, sum_mem