awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
refine : ∀ n ∈ f.support, ∀ i ∈ n.support, IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S) (X i)
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ x ∈ f.support,
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((C : (a : S) → MvPolynomial σ S) (coeff x f) : MvPolynomial σ S)
        (x.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ S) (X n) e : MvPolynomial σ S))

Tactic:
refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)

Premises used: IsIntegral.mul, IsIntegral.pow, IsIntegral.prod, Algebra.ofId, HPow.hPow, IsIntegral.map, IsIntegral.tower_top, IsIntegral.sum
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
n : σ →₀ ℕ
h : n ∈ f.support
i : σ
h_1 : i ∈ n.support
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S) (X i) :
      MvPolynomial σ S)

Tactic:
isIntegral_algebraMap (x := MvPolynomial.X i)

Premises used: isIntegral_algebraMap
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
n : σ →₀ ℕ
h_1 : n ∈ f.support
i : σ
h_2 : i ∈ n.support
h :
  Eq (α := MvPolynomial σ S) (X i)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S) (X i))
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S) (X i)

Tactic:
convert! isIntegral_algebraMap (x := MvPolynomial.X i)

Premises used: isIntegral_algebraMap
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
n : σ →₀ ℕ
h : n ∈ f.support
i : σ
h_1 : i ∈ n.support
⊢ Eq (α := MvPolynomial σ S) (X i)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S) (X i))

Tactic:
simp only [algebraMap_def, map_X]

Premises used: MvPolynomial.map_X, MvPolynomial.algebraMap_def
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f

Tactic:
case mpr =>
    rw [← f.support_sum_monomial_coeff]
    simp_rw [monomial_eq]
    refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)
    convert! isIntegral_algebraMap (x := MvPolynomial.X i)
    simp only [algebraMap_def, map_X]

Premises used: IsIntegral.mul, IsIntegral.pow, IsIntegral.prod, Algebra.ofId, HPow.hPow, IsIntegral.map, MvPolynomial.support_sum_monomial_coeff, MvPolynomial.monomial_eq, IsIntegral.tower_top, IsIntegral.sum, MvPolynomial.map_X, MvPolynomial.algebraMap_def
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
mp :
  ∀
    (this :
      ∀ {σ : Type w} {f : MvPolynomial σ S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
        (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f))
    (hσ : ¬Finite σ), IsIntegral R (coeff n f)
wlog :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)

Tactic:
wlog hσ : Finite σ generalizing σ

Premises used: Finite
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
⊢ (↑f.vars : Set σ) ⊆ Set.range (ι := ↥f.vars) (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
mp :
  ∀ (g : MvPolynomial.{w, u_2} (↥f.vars) S)
    (hg :
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f),
    IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)

Tactic:
obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)

Premises used: Subtype.val_injective, MvPolynomial.exists_rename_eq_of_vars_subset_range
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
pos :
  ∀
    (hn :
      Membership.mem (γ := Set (σ →₀ ℕ))
        (Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))) n),
    IsIntegral R (coeff n f)
neg :
  ∀ (hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))),
    IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)

Tactic:
by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))

Premises used: Finsupp.mapDomain, Set.range, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))) n
pos : ∀ (n : ↥f.vars →₀ ℕ), IsIntegral R (coeff (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) n) f)
⊢ IsIntegral R (coeff n f)

Tactic:
obtain ⟨n, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
pos : IsIntegral R (coeff n g)
⊢ IsIntegral R (coeff (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) n) f)

Tactic:
simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]

Premises used: Subtype.val_injective, MvPolynomial.coeff_rename_mapDomain
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
simp :
  RingHom.IsIntegralElem
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    f
⊢ RingHom.IsIntegralElem (R := MvPolynomial σ R) (A := MvPolynomial σ S)
    (RingHom.comp (β := MvPolynomial.{w, u_1} (↥f.vars) R)
        (RingHom.comp (β := MvPolynomial.{w, u_2} (↥f.vars) S)
          (AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))))
          (algebraMap (MvPolynomial.{w, u_1} (↥f.vars) R) (MvPolynomial.{w, u_2} (↥f.vars) S)))
        (AlgHom.toRingHom (killCompl ⋯)) :
      MvPolynomial σ R →+* MvPolynomial σ S)
    ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) :
          (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S)
        g :
      MvPolynomial σ S)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe, MvPolynomial.algebraMap_def
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial σ R) (A := MvPolynomial σ S)
    (RingHom.comp
        (AlgHom.toRingHom
          (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
            (killCompl ⋯)))
        (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) :
      MvPolynomial σ R →+* MvPolynomial σ S)
    ((AlgHom.toRingHom
            (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
              (killCompl ⋯)) :
          (a : MvPolynomial σ S) → MvPolynomial σ S)
        f :
      MvPolynomial σ S)

Tactic:
H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom

Premises used: RingHom.IsIntegralElem.map, MvPolynomial.killCompl, Subtype.val_injective, MvPolynomial.rename, AlgHom.toRingHom, AlgHom.comp, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
h :
  Eq (α := MvPolynomial σ R →+* MvPolynomial σ S)
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    (RingHom.comp
      (AlgHom.toRingHom
        (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
          (killCompl ⋯)))
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)))
h₁ :
  f =
    (AlgHom.toRingHom
          (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
            (killCompl ⋯)) :
        (a : MvPolynomial σ S) → MvPolynomial σ S)
      f
⊢ RingHom.IsIntegralElem
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    f

Tactic:
convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom

Premises used: RingHom.IsIntegralElem.map, MvPolynomial.killCompl, Subtype.val_injective, MvPolynomial.rename, AlgHom.toRingHom, AlgHom.comp, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ ∀ (x : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S)
      ((RingHom.comp
              (RingHom.comp
                (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) :
                  MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
                (map (algebraMap R S)))
              (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R) :
            (a : MvPolynomial σ R) → MvPolynomial σ S)
          x :
        MvPolynomial σ S)
      ((RingHom.comp
              (AlgHom.toRingHom
                (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S)
                  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) (killCompl ⋯)))
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) :
            (a : MvPolynomial σ R) → MvPolynomial σ S)
          x :
        MvPolynomial σ S)

Tactic:
simp [MvPolynomial.killCompl_map]

Premises used: MvPolynomial.killCompl_map
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ S)
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    (RingHom.comp
      (AlgHom.toRingHom
        (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
          (killCompl ⋯)))
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)))

Tactic:
exact RingHom.ext (by simp [MvPolynomial.killCompl_map])

Premises used: RingHom.ext
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
h :
  Eq (α := MvPolynomial σ S)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g :
      MvPolynomial σ S)
    ((AlgHom.toRingHom
            (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
              (killCompl ⋯)) :
          (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g) :
      MvPolynomial σ S)
⊢ f =
    (AlgHom.toRingHom
          (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
            (killCompl ⋯)) :
        (a : MvPolynomial σ S) → MvPolynomial σ S)
      f

Tactic:
nth_rw 1 12 [← hg]
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ Eq (α := MvPolynomial σ S)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g :
      MvPolynomial σ S)
    ((AlgHom.toRingHom
            (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
              (killCompl ⋯)) :
          (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g) :
      MvPolynomial σ S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff n g)

Tactic:
exact this (f := g) (RingHom.IsIntegralElem.of_map
        (g := (rename ((↑) : f.vars → σ)).toRingHom) (rename_injective _ Subtype.val_injective)
        (.of_comp (f := (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective).toRingHom) <| by
        simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
        convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
        · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)

Premises used: RingHom.IsIntegralElem.of_map, RingHom.IsIntegralElem.of_comp, Finite.of_fintype
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
⊢ ∀ (u : ↥f.vars →₀ ℕ), Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) u = n → coeff u g = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
neg : IsIntegral.{u_1, u_2} R (A := S) 0
⊢ IsIntegral R (coeff n f)

Tactic:
rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]

Premises used: MvPolynomial.coeff_rename_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
⊢ IsIntegral.{u_1, u_2} R (A := S) 0

Tactic:
isIntegral_zero

Premises used: isIntegral_zero