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
ι' : 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
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)))
⊢ 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)

Tactic:
rw [kerCompPreimage, map_finsuppSum, Finsupp.sum]

Premises used: Finsupp.sum, map_finsuppSum, Algebra.Generators.kerCompPreimage
-- 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 ι
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)))

Tactic:
Finset.sum_congr rfl fun j _ ↦ ?_

Premises used: Finset.sum_congr, 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
ι' : 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
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)
⊢ 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:
refine Finset.sum_congr rfl fun j _ ↦ ?_

Premises used: Finset.sum_congr, 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
ι' : 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)
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))
⊢ 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:
simp only [map_mul, Hom.toAlgHom_monomial]

Premises used: map_mul, Algebra.Generators.Hom.toAlgHom_monomial
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
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))
⊢ 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:
rw [one_smul, Finsupp.prod_mapDomain_index_inj Sum.inl_injective]

Premises used: Sum.inl_injective, Finsupp.prod_mapDomain_index_inj, one_smul
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
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))
⊢ 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 [rename, ← AlgHom.comp_apply, comp_aeval]

Premises used: AlgHom.comp_apply, MvPolynomial.comp_aeval, MvPolynomial.rename
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
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)
⊢ 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:
simp only [ofComp_val, Sum.elim_inr, Function.comp_apply,
    Sum.elim_inl, monomial_eq, Hom.toAlgHom_X]

Premises used: Algebra.Generators.ofComp_val, Algebra.Generators.Hom.toAlgHom_X, Sum.elim_inr, MvPolynomial.monomial_eq, Sum.elim_inl, Function.comp_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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
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)
⊢ 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:
congr 1
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
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)
⊢ 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:
rw [aeval_def, IsScalarTower.algebraMap_eq R S, ← MvPolynomial.algebraMap_eq,
    ← coe_eval₂Hom, ← map_aeval, P.aeval_val_σ]

Premises used: MvPolynomial.map_aeval, MvPolynomial.aeval_def, MvPolynomial.coe_eval₂Hom, Algebra.Generators.aeval_val_σ, IsScalarTower.algebraMap_eq, MvPolynomial.algebraMap_eq
-- 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 ι
x : ↥Q.ker
j : ι' →₀ ℕ
h : j ∈ support (↑x : Q.Ring)
⊢ 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:
simp [coeff]

Premises used: MvPolynomial.coeff
-- 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 ι
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
⊢ 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

Tactic:
ext x
-- 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 ι
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
⊢ 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:
rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]

Premises used: Algebra.Generators.toAlgHom_ofComp_surjective, Ideal.mem_map_iff_of_surjective
-- 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 ι
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
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
⊢ (∃ (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
-- 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 ι
x : Generators.Ring (Q.comp P)
hx : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
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)
⊢ Membership.mem (α := Q.Ring) Q.ker ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)

Tactic:
simp only [ker_eq_ker_aeval_val,
      RingHom.mem_ker] at hx ⊢

Premises used: RingHom.mem_ker, 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
ι' : 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)
h₂ 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)
⊢ 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:
rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_apply]

Premises used: Algebra.algebraMap_self_apply, Algebra.Generators.Hom.algebraMap_toAlgHom
-- 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 ι
x : Q.Ring
hx : 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:
⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

Premises used: Subtype.mk, Algebra.Generators.ofComp_kerCompPreimage, And.intro, Algebra.Generators.kerCompPreimage, Exists.intro, Subtype.property
-- 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 ι
x : Q.Ring
hx : 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:
exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩
-- 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 ι
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)) ⊥)
⊢ 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

Tactic:
rw [← map_ofComp_ker Q P,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective Q P)]

Premises used: Algebra.Generators.map_ofComp_ker, Algebra.Generators.toAlgHom_ofComp_surjective, Ideal.comap_map_of_surjective
-- 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 ι
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))
⊢ 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 [← sup_assoc, Algebra.Generators.map_toComp_ker, ← RingHom.ker_eq_comap_bot]

Premises used: Algebra.Generators.map_toComp_ker, sup_assoc, RingHom.ker_eq_comap_bot
-- 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 ι
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)
⊢ 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:
apply le_antisymm (le_trans le_sup_right le_sup_left)

Premises used: le_sup_left, le_sup_right, le_antisymm, le_trans
-- 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 ι
simp : 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) ⊔
      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]

Premises used: le_refl, and_true, le_sup_left, sup_le_iff, sup_of_le_left
-- 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 ι
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
⊢ 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

Premises used: RingHom.mem_ker