awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f
n : β →₀ ℕ
h :
  Eq (α := MvPolynomial β R →+* MvPolynomial β S)
    (RingHom.comp (β := MvPolynomial α R)
      (RingHom.comp (β := MvPolynomial α S) (AlgHom.toRingHom (rename (⇑e : (a : α) → β)))
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)))
      (AlgHom.toRingHom (rename (⇑e.symm : (a : β) → α))))
    (algebraMap (MvPolynomial β R) (MvPolynomial β S))
⊢ RingHom.IsIntegralElem (R := MvPolynomial β R) (A := MvPolynomial β S)
    (RingHom.comp (β := MvPolynomial α R)
        (RingHom.comp (β := MvPolynomial α S) (AlgHom.toRingHom (rename (⇑e : (a : α) → β)))
          (algebraMap (MvPolynomial α R) (MvPolynomial α S)))
        (AlgHom.toRingHom (rename (⇑e.symm : (a : β) → α))) :
      MvPolynomial β R →+* MvPolynomial β S)
    ((AlgHom.toRingHom (rename (⇑e : (a : α) → β)) : (a : MvPolynomial α S) → MvPolynomial β S)
        ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f) :
      MvPolynomial β S)
have h₁ : (AlgHom.toRingHom (rename (⇑e : (a : α) → β)) : (a : MvPolynomial α S) → MvPolynomial β S)
    ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f) =
  f
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f
n : β →₀ ℕ
⊢ IsIntegral R (coeff n f)
have this : IsIntegral.{u_1, u_2} R (A := S)
  (coeff (Finsupp.embDomain e.symm.toEmbedding n)
    ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f))
Tactic: have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert! H <;> aesop)) (n.embDomain e.symm)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f
n : PEmpty.{w + 1} →₀ ℕ
⊢ IsIntegral R (coeff n f)
have refine : RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R) (A := MvPolynomial PEmpty.{w + 1} S)
  (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
        (algebraMap R S))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))) :
    MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
  ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff n f) :
    MvPolynomial PEmpty.{w + 1} S)
Tactic: refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f
n : PEmpty.{w + 1} →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R) (A := MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
          (algebraMap R S))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))) :
      MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
          (a : S) → MvPolynomial PEmpty.{w + 1} S)
        (coeff n f) :
      MvPolynomial PEmpty.{w + 1} S)
have h : Eq (α := MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
  (RingHom.comp
    (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
      (algebraMap R S))
    (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))))
  (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S))
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f
n : PEmpty.{w + 1} →₀ ℕ
h :
  Eq (α := MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
        (algebraMap R S))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))))
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S))
⊢ RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R) (A := MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
          (algebraMap R S))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))) :
      MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
          (a : S) → MvPolynomial PEmpty.{w + 1} S)
        (coeff n f) :
      MvPolynomial PEmpty.{w + 1} S)
have h₁ : (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
      (a : S) → MvPolynomial PEmpty.{w + 1} S)
    (coeff n f) =
  f
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff n f) =
    f
have h : (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
      (a : S) → MvPolynomial PEmpty.{w + 1} S)
    (coeff 0 f) =
  f
Tactic: obtain rfl := Subsingleton.elim n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f
⊢ (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff 0 f) =
    f
have this : Eq (α := MvPolynomial PEmpty.{w + 1} S →+* S) constantCoeff
  (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv S PEmpty.{w + 1})))
Tactic: have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R) (A := MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
          (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
      MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
          (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
        ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) :
      MvPolynomial.{w, u_2} (Option α) S)
have h : Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
  (RingHom.comp
    (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
      (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
    (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
  (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
h :
  Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
        (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))
⊢ RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R) (A := MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
          (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
      MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
          (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
        ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) :
      MvPolynomial.{w, u_2} (Option α) S)
have h₁ : (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
      (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
    ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) =
  f
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
⊢ Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
        (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))
have h : ∀ (i : R) (m : Option α →₀ ℕ),
  Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp
              (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
            C :
          (a : R) → MvPolynomial (Option α) S)
        i))
    (coeff m
      ((RingHom.comp (β := MvPolynomial.{w, u_1} (Option α) R)
            (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) C :
          (a : R) → MvPolynomial (Option α) S)
        i))
Tactic: ext i m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
h :
  ∀ (i : R) (m : Option α →₀ ℕ),
    Eq.{u_2 + 1} (α := S)
      (coeff m
        ((RingHom.comp
              (RingHom.comp
                (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                  (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
                (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
              C :
            (a : R) → MvPolynomial (Option α) S)
          i))
      (coeff m
        ((RingHom.comp (β := MvPolynomial.{w, u_1} (Option α) R)
              (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) C :
            (a : R) → MvPolynomial (Option α) S)
          i))
⊢ Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
        (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))
have h₁ : ∀ (i : Option α) (m : Option α →₀ ℕ),
  Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
Tactic: ext i m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
have h : Eq.{u_2 + 1} (α := S)
  (coeff m
    ((RingHom.comp
          (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
            (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
        (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
      (X none)))
  (coeff m
    ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
        (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
      (X none)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
h :
  Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
have h₁ : ∀ (val : α),
  Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X (some val))))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X (some val))))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
⊢ IsIntegral R (coeff n f)
have this : IsIntegral.{u_1, u_2} R (A := S)
  (coeff n.some
    (Polynomial.coeff ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f)
      ((n : (a : Option α) → ℕ) none)))
Tactic: have := IH (IsIntegral.coeff (R := MvPolynomial α R)
      (p := optionEquivLeft _ _ f) (.of_map
      (g := (optionEquivLeft _ _).symm.toRingHom) (optionEquivLeft _ _).symm.injective
      (.of_comp (f := (optionEquivLeft _ _).toRingHom) (by
        convert! H
        · ext i m
          · aesop
          · cases i <;> aesop
        · aesop))) (n .none)) n.some
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
this :
  IsIntegral.{u_1, u_2} R (A := S)
    (coeff n.some
      (Polynomial.coeff ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f)
        ((n : (a : Option α) → ℕ) none)))
⊢ IsIntegral R (coeff n f)
have rwa : ∀ (this : IsIntegral R (coeff n f)), IsIntegral R (coeff n f)
Tactic: rwa [optionEquivLeft_coeff_some_coeff_none] at this
Cleared hypotheses: this