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
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
have obtain : ∀ (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)),
  IsAlmostIntegral R q.leadingCoeff
Tactic: obtain ⟨p, hp, hp'⟩ := hq
Cleared hypotheses: hq
-- 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
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)
⊢ IsAlmostIntegral R q.leadingCoeff
have refine : ∀ (n : ℕ),
  Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (p.leadingCoeff • q.leadingCoeff ^ n)
Tactic: refine ⟨p.leadingCoeff, by simpa using hp, fun n ↦ ?_⟩
-- 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
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 : ℕ
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (p.leadingCoeff • q.leadingCoeff ^ n)
have 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)
Tactic: obtain ⟨r, hr⟩ := hp' n
-- 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
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
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (p.leadingCoeff • q.leadingCoeff ^ n)
have 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))
Tactic: simp only [Algebra.smul_def, algebraMap_def, coe_mapRingHom] at hr ⊢
Cleared hypotheses: hr
-- 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
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
⊢ 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))
have 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))
Tactic: by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0
-- 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
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))
⊢ 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))
have 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))
Tactic: by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0
-- 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
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))
have h' : q.leadingCoeff ^ n ≠ 0
Tactic: have h' : q.leadingCoeff ^ n ≠ 0 := 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
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
⊢ 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))
have 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)
Tactic: use r.leadingCoeff
-- 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
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
⊢ ((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)
have 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
Tactic: simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢
Cleared hypotheses: 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
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
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * q.leadingCoeff ^ n
have 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
Tactic: rw [← leadingCoeff_pow' h'] at h ⊢
Cleared hypotheses: 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
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
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff
have h₁ : leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff =
  leadingCoeff (map (algebraMap R S) p) * (q ^ n).leadingCoeff
Tactic: rw [leadingCoeff_mul' 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
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
i : ℕ
⊢ IsAlmostIntegral R (p.coeff i)
have H : ∀ {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]
-- 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
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
⊢ IsAlmostIntegral R (p.coeff i)
have pos : ∀ (hp' : p.natDegree = 0), IsAlmostIntegral R (p.coeff i)
Tactic: by_cases hp' : p.natDegree = 0
-- 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
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)
⊢ IsAlmostIntegral R (p.coeff i)
have neg : ∀ (hp' : ¬p.natDegree = 0), IsAlmostIntegral R (p.coeff i)
Tactic: by_cases hp' : p.natDegree = 0
-- 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
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
⊢ IsAlmostIntegral R (p.coeff i)
have 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)
Tactic: obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
Cleared hypotheses: p, hp, hn, hp'
-- 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
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
⊢ IsAlmostIntegral.{u_1, u_2} R (S := S) (Polynomial.coeff ((C : (a : S) → S[X]) p) i)
have pos : IsAlmostIntegral R (if i = 0 then p else 0)
Tactic: simp only [coeff_C]
-- 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
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
⊢ IsAlmostIntegral R (if i = 0 then p else 0)
have pos : ∀ (h : i = 0), IsAlmostIntegral R p
Tactic: split_ifs with 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
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
⊢ IsAlmostIntegral R (if i = 0 then p else 0)
have neg : ∀ (h : ¬i = 0), IsAlmostIntegral.{u_1, u_2} R (S := S) 0
Tactic: split_ifs with 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
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
⊢ IsAlmostIntegral R (p.coeff i)
have pos : ∀ (hi : i = p.natDegree), IsAlmostIntegral R (p.coeff i)
Tactic: by_cases hi : i = p.natDegree
-- 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
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)
⊢ IsAlmostIntegral R (p.coeff i)
have neg : ∀ (hi : ¬i = p.natDegree), IsAlmostIntegral R (p.coeff i)
Tactic: by_cases hi : i = p.natDegree
-- 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
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.{u_1, u_2} R[X] p.eraseLead
have 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)))
Tactic: rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]
-- 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
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)))
have 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])
Tactic: refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))
-- 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
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 (α := 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])
have 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])
Tactic: obtain ⟨r, hr, hr'⟩ := H hp
-- 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
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 (α := 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])
have refine : ∀ (n : ℕ),
  Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
    (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))
Tactic: refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
-- 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
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_1 : ℕ
IH :
  ∀ m < n_1,
    ∀ {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_1
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)
n : ℕ
⊢ Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
    (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))
have obtain : ∀ (s : R) (hs : ((algebraMap R S : R →+* S) : (a : R) → S) s = r • p.leadingCoeff ^ n),
  Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X]))
    (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) n))
Tactic: obtain ⟨s, hs⟩ := hr' n