awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
refine_1 : Ne (α := Unit →₀ ℕ) (Finsupp.single () 1) 0
refine_2 :
  ∀ (f : Unit →₀ ℕ),
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ 0) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl f) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) =
      0
refine_3 :
  HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1)) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) +
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ (-1)) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl 0) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
⊢ (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)

Tactic:
refine (Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_

Premises used: Unit.unit, Finsupp.sum_single_add_single, OfNat.ofNat, Neg.neg, Eq.trans, Finsupp.single
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ Ne (α := Unit →₀ ℕ) (Finsupp.single () 1) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ ∀ (f : Unit →₀ ℕ),
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ 0) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl f) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) =
      0

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1)) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) +
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ (-1)) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl 0) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)

Tactic:
simp [h1, ← X_pow_eq_monomial]

Premises used: MvPolynomial.X_pow_eq_monomial
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
rw :
  Eq (α := Ideal (P.reindex e).Ring)
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation)))
    (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
      (Ideal.span (Set.range P.relation)))
⊢ Ideal.span
      (Set.range (ι := σ')
        ((⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R) ∘
          P.relation ∘ (⇑f : (a : σ') → σ))) =
    (P.reindex e).ker

Tactic:
rw [Generators.ker_eq_ker_aeval_val, Generators.reindex_val, ← aeval_comp_rename,
      ← AlgHom.comap_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker,
      Set.range_comp, Set.range_comp, Equiv.range_eq_univ, Set.image_univ,
      ← Ideal.map_span (rename ⇑e.symm)]

Premises used: Set.range_comp, Set.image_univ, AlgHom.comap_ker, Ideal.map_span, Algebra.Presentation.span_range_relation_eq_ker, MvPolynomial.rename, Algebra.Generators.reindex_val, Algebra.Generators.ker_eq_ker_aeval_val, Equiv.range_eq_univ, MvPolynomial.aeval_comp_rename, Equiv.symm, DFunLike.coe, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)

Tactic:
have hf : Function.Bijective (MvPolynomial.rename e.symm) := (renameEquiv R e.symm).bijective
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf :
  Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
a :
  Eq (α := Ideal (MvPolynomial ι R))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
        (Ideal.span (Set.range P.relation))))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
        (Ideal.span (Set.range P.relation))))
⊢ Eq (α := Ideal (P.reindex e).Ring)
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.span (Set.range P.relation)))
    (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
      (Ideal.span (Set.range P.relation)))

Tactic:
apply Ideal.comap_injective_of_surjective _ hf.2

Premises used: And.right, Ideal.comap_injective_of_surjective
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf :
  Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
a :
  Eq (α := Ideal (MvPolynomial ι R))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
        (Ideal.span (Set.range P.relation))))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι R) (rename _root_.id) (Ideal.span (Set.range P.relation)))
⊢ Eq (α := Ideal (MvPolynomial ι R))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
        (Ideal.span (Set.range P.relation))))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.comap (F := MvPolynomial ι' R →ₐ[R] MvPolynomial ι R) (rename (⇑e : (a : ι') → ι))
        (Ideal.span (Set.range P.relation))))

Tactic:
simp_rw [Ideal.comap_comapₐ, rename_comp_rename, Equiv.self_comp_symm]

Premises used: Ideal.comap_comapₐ, Equiv.self_comp_symm, MvPolynomial.rename_comp_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf :
  Function.Bijective (α := MvPolynomial ι R) (β := MvPolynomial ι' R)
    (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
⊢ Eq (α := Ideal (MvPolynomial ι R))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' R) (rename (⇑e.symm : (a : ι) → ι'))
        (Ideal.span (Set.range P.relation))))
    (Ideal.comap (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι R) (rename _root_.id) (Ideal.span (Set.range P.relation)))

Tactic:
simp [Ideal.comap_map_of_bijective _ hf, rename_id]

Premises used: Ideal.comap_map_of_bijective, MvPolynomial.rename_id
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ (P.reindex e f).dimension = P.dimension

Tactic:
simp [dimension, Nat.card_congr e, Nat.card_congr f]

Premises used: Nat.card_congr, Algebra.Presentation.dimension
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
ι : Type w
σ : Type t
inst : CommRing R
v : ι → MvPolynomial σ R
s :
  HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v)) → MvPolynomial σ R
hs :
  ∀ (x : HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v))),
    (Ideal.Quotient.mk (Ideal.span (Set.range v)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ Ideal.span (Set.range v))
        (s x) =
      x
⊢ (naive s hs).relation = v

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
ι : Type w
σ : Type t
inst : CommRing R
v : ι → MvPolynomial σ R
s :
  HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v)) → MvPolynomial σ R
hs :
  ∀ (x : HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v))),
    (Ideal.Quotient.mk (Ideal.span (Set.range v)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ Ideal.span (Set.range v))
        (s x) =
      x
i : ι
⊢ (naive s hs).relation i = v i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
ι : Type w
σ : Type t
inst : CommRing R
v : ι → MvPolynomial σ R
s :
  HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v)) → MvPolynomial σ R
hs :
  ∀ (x : HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v))),
    (Ideal.Quotient.mk (Ideal.span (Set.range v)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ Ideal.span (Set.range v))
        (s x) =
      x
i : ι
⊢ v i ∈ (naive s hs).ker

Tactic:
relation_mem_ker _ i

Premises used: Set.Mem, Algebra.Presentation.relation_mem_ker
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst_4 : Finite α
rw : Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))
⊢ P.ker.FG

Tactic:
rw [Generators.ker_eq_ker_aeval_val]

Premises used: Algebra.Generators.ker_eq_ker_aeval_val
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst_4 : Finite α
⊢ Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))

Tactic:
Algebra.FinitePresentation.ker_fG_of_surjective _ P.aeval_val_surjective

Premises used: Algebra.Generators.aeval_val_surjective, MvPolynomial.aeval, MvPolynomial.eval₂Hom, Algebra.FinitePresentation.ker_fG_of_surjective, Ideal.comap, RingHom.ker
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_1
P : Generators R S α
inst_4 : Finite α
⊢ Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))

Tactic:
exact Algebra.FinitePresentation.ker_fG_of_surjective _ P.aeval_val_surjective

Premises used: Algebra.Generators.aeval_val_surjective, Algebra.FinitePresentation.ker_fG_of_surjective
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
x : σ
⊢ (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆ (↑(MvPolynomial.coeffs (P.relation x)) : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
inst_3 : Finite σ
⊢ P.coeffs.Finite

Tactic:
Set.finite_iUnion fun _ ↦ Finset.finite_toSet _

Premises used: Set.finite_iUnion, Algebra.Presentation.coeffs, MvPolynomial.coeffs, Algebra.Presentation.relation, Finset.finite_toSet
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ P.coeffs ⊆ (↑P.core : Set R)

Tactic:
Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
x : σ
⊢ (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆ (↑P.core : Set R)

Tactic:
subset_trans (P.coeffs_relation_subset_coeffs x) P.coeffs_subset_core

Premises used: subset_trans, Algebra.Presentation.coeffs_relation_subset_coeffs, Algebra.Presentation.coeffs_subset_core
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ FaithfulSMul P.Core R

Tactic:
inferInstanceAs <| FaithfulSMul P.core R

Premises used: _private.0.Algebra.Presentation.instFaithfulSMulCore._proof_1
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ IsScalarTower P.Core R S

Tactic:
inferInstanceAs <| IsScalarTower P.core R S

Premises used: _private.0.Algebra.Presentation.instIsScalarTowerCore._proof_1
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
inst_3 : Finite σ
⊢ FiniteType.{0, u_1} ℤ P.Core

Tactic:
.adjoin_of_finite P.finite_coeffs

Premises used: Algebra.FiniteType.adjoin_of_finite, Set.Mem, Algebra.Presentation.Core, RingHom.codRestrict, Algebra.Presentation.finite_coeffs
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ P.coeffs ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)

Tactic:
subset_trans P.coeffs_subset_core ?_

Premises used: subset_trans, Algebra.Presentation.coeffs_subset_core
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
refine : (↑P.core : Set R) ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)
⊢ P.coeffs ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)

Tactic:
refine subset_trans P.coeffs_subset_core ?_

Premises used: subset_trans, Algebra.Presentation.coeffs_subset_core
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
⊢ (↑P.core : Set R) ⊆ Set.range (ι := P.Core) (⇑(algebraMap P.Core R) : (a : P.Core) → R)

Tactic:
simp [Core, Subalgebra.algebraMap_eq]

Premises used: Algebra.Presentation.Core, Subalgebra.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
⊢ P.coeffs ⊆ Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)

Tactic:
HasCoeffs.coeffs_subset_range

Premises used: Algebra.Presentation.HasCoeffs.coeffs_subset_range
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
R₁ : Type u_6
inst_8 : CommRing R₁
inst_9 : Algebra R₀ R₁
inst_10 : Algebra R₁ R
inst_11 : IsScalarTower R₀ R₁ R
inst_12 : Algebra R₁ S
inst_13 : IsScalarTower R₁ R S
⊢ P.HasCoeffs R₁

Tactic:
⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩

Premises used: subset_trans, Algebra.Presentation.coeffs_subset_range, Algebra.Presentation.HasCoeffs.mk
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
R₁ : Type u_6
inst_8 : CommRing R₁
inst_9 : Algebra R₀ R₁
inst_10 : Algebra R₁ R
inst_11 : IsScalarTower R₀ R₁ R
inst_12 : Algebra R₁ S
inst_13 : IsScalarTower R₁ R S
refine :
  Subset.{u_1} (α := Set R) (Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R))
    (Set.range.{u_1, u_6 + 1} (ι := R₁) (⇑(algebraMap R₁ R) : (a : R₁) → R))
⊢ P.HasCoeffs R₁

Tactic:
refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
R₁ : Type u_6
inst_8 : CommRing R₁
inst_9 : Algebra R₀ R₁
inst_10 : Algebra R₁ R
inst_11 : IsScalarTower R₀ R₁ R
inst_12 : Algebra R₁ S
inst_13 : IsScalarTower R₁ R S
⊢ Subset.{u_1} (α := Set R) (Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R))
    (Set.range.{u_1, u_6 + 1} (ι := R₁) (⇑(algebraMap R₁ R) : (a : R₁) → R))

Tactic:
simp [IsScalarTower.algebraMap_eq R₀ R₁ R, RingHom.coe_comp, Set.range_comp]

Premises used: Set.range_comp, IsScalarTower.algebraMap_eq, RingHom.coe_comp
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
s : Set R
⊢ P.HasCoeffs ↥(adjoin R₀ s)

Tactic:
HasCoeffs.of_isScalarTower R₀

Premises used: Algebra.Presentation.HasCoeffs.of_isScalarTower
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
x : σ
⊢ (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆
    Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)

Tactic:
subset_trans (P.coeffs_relation_subset_coeffs x) HasCoeffs.coeffs_subset_range

Premises used: subset_trans, Algebra.Presentation.coeffs_relation_subset_coeffs, Algebra.Presentation.HasCoeffs.coeffs_subset_range
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
x : σ
rw :
  (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆
    Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)
⊢ Membership.mem (γ := Set (MvPolynomial ι R))
    (Set.range (ι := MvPolynomial ι R₀)
      (⇑(MvPolynomial.map (algebraMap R₀ R)) : (a : MvPolynomial ι R₀) → MvPolynomial ι R))
    (P.relation x)

Tactic:
rw [MvPolynomial.mem_range_map_iff_coeffs_subset]

Premises used: MvPolynomial.mem_range_map_iff_coeffs_subset