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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
refine :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (p.leadingCoeff • q.leadingCoeff ^ n)
⊢ IsAlmostIntegral R q.leadingCoeff

Tactic:
refine ⟨p.leadingCoeff, by simpa using hp, fun n ↦ ?_⟩
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
obtain :
  ∀ (r : R[X]) (hr : (algebraMap R[X] S[X] : (a : R[X]) → S[X]) r = p • q ^ n),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (p.leadingCoeff • q.leadingCoeff ^ n)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (p.leadingCoeff • q.leadingCoeff ^ n)

Tactic:
obtain ⟨r, hr⟩ := hp' n
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : (algebraMap R[X] S[X] : (a : R[X]) → S[X]) r = p • q ^ n
simp :
  ∀ (hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (p.leadingCoeff • q.leadingCoeff ^ n)

Tactic:
simp only [Algebra.smul_def, algebraMap_def, coe_mapRingHom] at hr ⊢

Premises used: Polynomial.algebraMap_def, Polynomial.coe_mapRingHom, Algebra.smul_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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
pos :
  ∀ (h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))
neg :
  ∀ (h : ¬HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))

Tactic:
by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0

Premises used: Algebra.algebraMap, Polynomial.leadingCoeff, DFunLike.coe
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))

Tactic:
simp [h]
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : ¬HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0
⊢ q.leadingCoeff ^ n ≠ 0

Tactic:
aesop
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : ¬HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0
⊢ q.leadingCoeff ^ n ≠ 0

Tactic:
have h' : q.leadingCoeff ^ n ≠ 0 := by aesop
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : ¬HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0
h' : q.leadingCoeff ^ n ≠ 0
h₁ :
  ((algebraMap R S : R →+* S) : (a : R) → S) r.leadingCoeff =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n))

Tactic:
use r.leadingCoeff

Premises used: Polynomial.leadingCoeff
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : ¬HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n) = 0
h' : q.leadingCoeff ^ n ≠ 0
h₁ :
  ∀ (h : ¬leadingCoeff (map (algebraMap R S) p) * q.leadingCoeff ^ n = 0),
    (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * q.leadingCoeff ^ n
⊢ ((algebraMap R S : R →+* S) : (a : R) → S) r.leadingCoeff =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p.leadingCoeff : S) (q.leadingCoeff ^ n)

Tactic:
simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢

Premises used: Polynomial.leadingCoeff_map_of_injective, FaithfulSMul.algebraMap_injective
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h' : q.leadingCoeff ^ n ≠ 0
h : ¬leadingCoeff (map (algebraMap R S) p) * q.leadingCoeff ^ n = 0
h₁ :
  ∀ (h : ¬leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff = 0),
    (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * q.leadingCoeff ^ n

Tactic:
rw [← leadingCoeff_pow' h'] at h ⊢

Premises used: Polynomial.leadingCoeff_pow'
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h' : q.leadingCoeff ^ n ≠ 0
h : ¬leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff = 0
h₁ h₂ :
  leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff =
    leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff

Tactic:
rw [leadingCoeff_mul' h]

Premises used: Polynomial.leadingCoeff_mul'
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
i : ℕ
⊢ ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff

Tactic:
have H {q : S[X]} (hq : IsAlmostIntegral R[X] q) : IsAlmostIntegral R q.leadingCoeff := by
    obtain ⟨p, hp, hp'⟩ := hq
    refine ⟨p.leadingCoeff, by simpa using hp, fun n ↦ ?_⟩
    obtain ⟨r, hr⟩ := hp' n
    simp only [Algebra.smul_def, algebraMap_def, coe_mapRingHom] at hr ⊢
    by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0
    · simp [h]
    have h' : q.leadingCoeff ^ n ≠ 0 := by aesop
    use r.leadingCoeff
    simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢
    rw [← leadingCoeff_pow' h'] at h ⊢
    rw [leadingCoeff_mul' h]
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
pos : ∀ (hp' : p.natDegree = 0), IsAlmostIntegral R (p.coeff i)
neg : ∀ (hp' : ¬p.natDegree = 0), IsAlmostIntegral R (p.coeff i)
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
by_cases hp' : p.natDegree = 0

Premises used: Polynomial.natDegree
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : p.natDegree = 0
pos :
  ∀ (p : S) (hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X]))
    (hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n)
    (hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0),
    IsAlmostIntegral.{u_1, u_2} R (S := S) (Polynomial.coeff ((C : (a : S) → S[X]) p) i)
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X])
hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n
hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0
pos : IsAlmostIntegral R (if i = 0 then p else 0)
⊢ IsAlmostIntegral.{u_1, u_2} R (S := S) (Polynomial.coeff ((C : (a : S) → S[X]) p) i)

Tactic:
simp only [coeff_C]

Premises used: Polynomial.coeff_C
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X])
hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n
hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0
pos : ∀ (h : i = 0), IsAlmostIntegral R p
neg : ∀ (h : ¬i = 0), IsAlmostIntegral.{u_1, u_2} R (S := S) 0
⊢ IsAlmostIntegral R (if i = 0 then p else 0)

Tactic:
split_ifs with h
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X])
hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n
hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0
h : i = 0
⊢ IsAlmostIntegral R p

Tactic:
simpa using H hp
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X])
hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n
hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0
h : ¬i = 0
⊢ IsAlmostIntegral.{u_1, u_2} R (S := S) 0

Tactic:
(completeIntegralClosure R S).zero_mem

Premises used: Set.Mem, Subalgebra.zero_mem, setOf, IsAlmostIntegral, completeIntegralClosure
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral.{u_1, u_2} R[X] (S := S[X]) ((C : (a : S) → S[X]) p : S[X])
hn : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = n
hp' : natDegree.{u_2} (R := S) ((C : (a : S) → S[X]) p) = 0
h : ¬i = 0
⊢ IsAlmostIntegral.{u_1, u_2} R (S := S) 0

Tactic:
exact (completeIntegralClosure R S).zero_mem

Premises used: Subalgebra.zero_mem, completeIntegralClosure
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
pos : ∀ (hi : i = p.natDegree), IsAlmostIntegral R (p.coeff i)
neg : ∀ (hi : ¬i = p.natDegree), IsAlmostIntegral R (p.coeff i)
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
by_cases hi : i = p.natDegree

Premises used: Polynomial.natDegree
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : i = p.natDegree
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
simp [hi, H hp]
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
rw :
  Membership.mem (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    (p -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
        (map (algebraMap R S) (HPow.hPow (α := R[X]) X p.natDegree)))
⊢ IsAlmostIntegral.{u_1, u_2} R[X] p.eraseLead

Tactic:
rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]

Premises used: Algebra.algebraMap, Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.map_pow, mem_completeIntegralClosure, Polynomial.map_X
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ Membership.mem (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    (p -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
        (map (algebraMap R S) (HPow.hPow (α := R[X]) X p.natDegree)))

Tactic:
sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))

Premises used: Set.Mem, setOf, sub_mem, algebraMap_mem, MulMemClass.mul_mem
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
refine :
  Membership.mem (α := S[X]) (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
⊢ Membership.mem (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    (p -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
        (map (algebraMap R S) (HPow.hPow (α := R[X]) X p.natDegree)))

Tactic:
refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))

Premises used: sub_mem, algebraMap_mem, MulMemClass.mul_mem
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
obtain :
  ∀ (r : R) (hr : Membership.mem (γ := Submonoid R) R⁰ r)
    (hr' :
      ∀ (n : ℕ),
        Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)),
    Membership.mem (α := S[X]) (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
      ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
⊢ Membership.mem (α := S[X]) (γ := Subalgebra.{u_1, u_2} R[X] S[X]) (completeIntegralClosure R[X] S[X])
    ((C : (a : S) → S[X]) p.leadingCoeff : S[X])

Tactic:
obtain ⟨r, hr, hr'⟩ := H hp
-- 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]} (hq : IsAlmostIntegral.{u_1, u_2} R[X] q), IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH :
  ∀ m < n, ∀ {p : S[X]} (hp : IsAlmostIntegral.{u_1, u_2} R[X] p) (hn : p.natDegree = m), IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • p.leadingCoeff ^ n)
⊢ Membership.mem (α := R[X]) (γ := Submonoid R[X]) R[X]⁰ ((C : (a : R) → R[X]) r : R[X])

Tactic:
simpa using hr