awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₃ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval fun (x : ι) ↦ ((↑e : S →ₐ[R] T) : (a : S) → T) (P.val x)) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₄ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (AlgHom.comp (↑e : S →ₐ[R] T) (aeval P.val)) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₅ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →ₐ[R] T) (↑e : S →ₐ[R] T)) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₆ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →+* T) (↑(↑e : S →ₐ[R] T) : S →+* T)) =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₇ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) (RingHom.ker (F := S →+* T) (↑e : S →+* T)) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₈ : Ideal.comap (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) ⊥ = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₉ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₁₀ : P.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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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 (ι' →₀ ℕ)
⊢ 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)))
have 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)))
⊢ 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)))
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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 (ι' →₀ ℕ)
⊢ 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)))
have 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)))
Tactic: rw [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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
have a : Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
Tactic: simp only [Ideal.mem_comap,
      RingHom.mem_ker, ← AlgHom.comp_apply, this, IsScalarTower.toAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply P.Ring S, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
have a₁ : Eq (α := Q.Ring) ((algebraMap S Q.Ring : (a : S) → Q.Ring) 0) 0
Tactic: rw [IsScalarTower.algebraMap_apply P.Ring S, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ Eq (α := Q.Ring) ((algebraMap P.Ring Q.Ring : (a : P.Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
have a₂ : Eq (α := Q.Ring) 0 0
Tactic: rw [IsScalarTower.algebraMap_apply P.Ring S, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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 (γ := 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
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
    (∑ v ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x),
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) x))
have 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))
Tactic: rw [← Finset.sum_fiberwise_of_maps_to (fun i ↦ Finset.mem_image_of_mem Prod.fst)]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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))
have a : ∀ (i : ι' →₀ ℕ)
  (hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support 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)
    (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
Tactic: refine sum_mem fun i hi ↦ ?_