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
ι' : 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 ι
x : ↥Q.ker
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring) : Q.Ring)
    (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring)) :
      MvPolynomial ι' S)
have rw : Eq (α := Q.Ring)
  (∑ a ∈ (↑x : Q.Ring).support,
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
      (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) a)) :
          MvPolynomial (ι' ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl a) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)))
  (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring)))
Tactic: rw [kerCompPreimage, map_finsuppSum, Finsupp.sum]
-- 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 ι
x : ↥Q.ker
⊢ Eq (α := Q.Ring)
    (∑ a ∈ (↑x : Q.Ring).support,
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
              (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) a)) :
            MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl a) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)))
    (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring)))
have refine : ∀ j ∈ support (↑x : Q.Ring),
  Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
              (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
            MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl j) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)) :
      Q.Ring)
    ((monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
Tactic: refine Finset.sum_congr rfl fun j _ ↦ ?_
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
              (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
            MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl j) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)) :
      Q.Ring)
    ((monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
have simp : HMul.hMul (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j))) :
      Q.Ring)
    (HSMul.hSMul (α := R) (β := Q.Ring) 1
      (Finsupp.prod (Finsupp.mapDomain Sum.inl j) fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
        Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2)) =
  (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
Tactic: simp only [map_mul, Hom.toAlgHom_monomial]
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ HMul.hMul (α := Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j))) :
        Q.Ring)
      (HSMul.hSMul (α := R) (β := Q.Ring) 1
        (Finsupp.prod (Finsupp.mapDomain Sum.inl j) fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
          Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2)) =
    (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
have rw : HMul.hMul (α := Q.Ring) (β := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j))) :
      Q.Ring)
    (j.prod fun (a : ι') (b : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) (Sum.inl a) ^ b : Q.Ring) =
  (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
Tactic: rw [one_smul, Finsupp.prod_mapDomain_index_inj Sum.inl_injective]
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ HMul.hMul (α := Q.Ring) (β := Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j))) :
        Q.Ring)
      (j.prod fun (a : ι') (b : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) (Sum.inl a) ^ b : Q.Ring) =
    (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
have rw : HMul.hMul (α := Q.Ring) (β := Q.Ring)
    ((aeval fun (i : ι) ↦ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) ((X ∘ Sum.inr) i) :
          (a : MvPolynomial ι R) → Q.Ring)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
      Q.Ring)
    (j.prod fun (a : ι') (b : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) (Sum.inl a) ^ b : Q.Ring) =
  (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
Tactic: rw [rename, ← AlgHom.comp_apply, comp_aeval]
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ HMul.hMul (α := Q.Ring) (β := Q.Ring)
      ((aeval fun (i : ι) ↦ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) ((X ∘ Sum.inr) i) :
            (a : MvPolynomial ι R) → Q.Ring)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
        Q.Ring)
      (j.prod fun (a : ι') (b : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) (Sum.inl a) ^ b : Q.Ring) =
    (monomial j : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring))
have simp : HMul.hMul (α := Q.Ring) (β := Q.Ring)
    ((aeval fun (i : ι) ↦ (C : (a : S) → MvPolynomial ι' S) (P.val i) : (a : MvPolynomial ι R) → Q.Ring)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
      Q.Ring)
    (j.prod fun (a : ι') (b : ℕ) ↦ HPow.hPow (α := Q.Ring) (X a) b : Q.Ring) =
  HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
    (j.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
Tactic: simp only [ofComp_val, Sum.elim_inr, Function.comp_apply,
    Sum.elim_inl, monomial_eq, Hom.toAlgHom_X]
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ HMul.hMul (α := Q.Ring) (β := Q.Ring)
      ((aeval fun (i : ι) ↦ (C : (a : S) → MvPolynomial ι' S) (P.val i) : (a : MvPolynomial ι R) → Q.Ring)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
        Q.Ring)
      (j.prod fun (a : ι') (b : ℕ) ↦ HPow.hPow (α := Q.Ring) (X a) b : Q.Ring) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
      (j.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
have e_a : Eq (α := Q.Ring)
  ((aeval fun (i : ι) ↦ (C : (a : S) → MvPolynomial ι' S) (P.val i) : (a : MvPolynomial ι R) → Q.Ring)
      (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
    Q.Ring)
  ((C : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
Tactic: congr 1
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ Eq (α := Q.Ring)
    ((aeval fun (i : ι) ↦ (C : (a : S) → MvPolynomial ι' S) (P.val i) : (a : MvPolynomial ι R) → Q.Ring)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j)) :
      Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
have e_a : Eq (α := Q.Ring) ((algebraMap S Q.Ring : (a : S) → Q.Ring) (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) j) : Q.Ring)
  ((algebraMap S (MvPolynomial ι' S) : (a : S) → MvPolynomial ι' S) (coeff j (↑x : Q.Ring)) : MvPolynomial ι' S)
Tactic: rw [aeval_def, IsScalarTower.algebraMap_eq R S, ← MvPolynomial.algebraMap_eq,
    ← coe_eval₂Hom, ← map_aeval, P.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 ι
⊢ Ideal.map (R := Generators.Ring (Q.comp P)) (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P))
      (ker (Q.comp P)) =
    Q.ker
have h : ∀ (x : Q.Ring),
  Membership.mem (γ := Ideal Q.Ring)
      (Ideal.map (R := Generators.Ring (Q.comp P)) (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring)
        (Hom.toAlgHom (Q.ofComp P)) (ker (Q.comp P)))
      x ↔
    x ∈ Q.ker
Tactic: ext x
-- 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 ι
x : Q.Ring
⊢ Membership.mem (γ := Ideal Q.Ring)
      (Ideal.map (R := Generators.Ring (Q.comp P)) (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring)
        (Hom.toAlgHom (Q.ofComp P)) (ker (Q.comp P)))
      x ↔
    x ∈ Q.ker
have h : (∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x) ↔
  x ∈ Q.ker
Tactic: rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
-- 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 ι
x : Q.Ring
⊢ (∃ (x_1 : Generators.Ring (Q.comp P)),
      Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
        (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x) ↔
    x ∈ Q.ker
have h : (∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x) →
  x ∈ Q.ker
Tactic: constructor
-- 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 ι
x : Q.Ring
h :
  (∃ (x_1 : Generators.Ring (Q.comp P)),
      Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
        (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x) →
    x ∈ Q.ker
⊢ (∃ (x_1 : Generators.Ring (Q.comp P)),
      Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
        (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x) ↔
    x ∈ Q.ker
have h₁ : x ∈ Q.ker →
  ∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x
Tactic: constructor
-- 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 ι
x : Generators.Ring (Q.comp P)
hx : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
⊢ Membership.mem (α := Q.Ring) Q.ker ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
have h : ∀ (hx : Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T) (0 : T)),
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    (0 : T)
Tactic: simp only [ker_eq_ker_aeval_val,
      RingHom.mem_ker] at hx ⊢
Cleared hypotheses: hx
-- 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 ι
x : Generators.Ring (Q.comp P)
hx : Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T) (0 : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    (0 : T)
have h : Eq.{u_7 + 1} (α := T)
  ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
  ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
Tactic: rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_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 ι
x : Generators.Ring (Q.comp P)
hx : Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T) (0 : T)
h :
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    (0 : T)
have h₁ : Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
  ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
Tactic: rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_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 ι
x : Generators.Ring (Q.comp P)
hx : Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T) (0 : T)
h :
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
h₁ :
  Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : Q.Ring) → T) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) : T)
    (0 : T)
have h₂ : Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T)
  ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T) x : T)
Tactic: rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_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 ι
⊢ ker (Q.comp P) =
    Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker ⊔
      Ideal.comap (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) Q.ker
have rw : ker (Q.comp P) =
  Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker ⊔
    (ker (Q.comp P) ⊔ Ideal.comap (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊥)
Tactic: rw [← map_ofComp_ker Q P,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
-- 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 ι
⊢ ker (Q.comp P) =
    Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) P.ker ⊔
      (ker (Q.comp P) ⊔ Ideal.comap (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊥)
have rw : ker (Q.comp P) =
  RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊔ ker (Q.comp P) ⊔
    RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P))
Tactic: rw [← sup_assoc, Algebra.Generators.map_toComp_ker, ← RingHom.ker_eq_comap_bot]
-- 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 ι
⊢ ker (Q.comp P) =
    RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊔ ker (Q.comp P) ⊔
      RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P))
have apply : RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊔ ker (Q.comp P) ⊔
    RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ≤
  ker (Q.comp P)
Tactic: apply le_antisymm (le_trans le_sup_right le_sup_left)
-- 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 ι
⊢ RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ⊔ ker (Q.comp P) ⊔
      RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ≤
    ker (Q.comp P)
have simp : RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P)) ≤ ker (Q.comp P)
Tactic: simp only [le_sup_left, sup_of_le_left, sup_le_iff, le_refl, and_true]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (hypothesis)
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 ι
x : Generators.Ring (Q.comp P)
hx :
  Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)))
    (RingHom.ker (F := Generators.Ring (Q.comp P) →ₐ[R] Q.Ring) (Hom.toAlgHom (Q.ofComp P))) x
⊢ Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
have hx₁ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
Tactic: simp only [RingHom.mem_ker] at hx
Cleared hypotheses: hx
-- 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 ι
x : Generators.Ring (Q.comp P)
hx : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
⊢ Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
have rw : Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
  (0 : T)
Tactic: rw [Generators.ker_eq_ker_aeval_val, RingHom.mem_ker,
    ← algebraMap_self_apply (MvPolynomial.aeval _ x)]
-- 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 ι
x : Generators.Ring (Q.comp P)
hx : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
⊢ Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    (0 : T)
have rw : Eq.{u_7 + 1} (α := T)
  ((aeval Q.val : (a : MvPolynomial ι' S) → T)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) :
    T)
  (0 : T)
Tactic: rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]