awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have this : RingHomSurjective.{u_1, u_1} (R₁ := R⟦X⟧) constantCoeff
Tactic: have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have hfg₁ : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
Tactic: replace hfg : (Ideal.map constantCoeff I).FG := by
    have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
    exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have pos : spanFinrank (R := R⟦X⟧)
    (Ideal.span
      (insert X
        (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
Tactic: nth_rw 1 [eq_span_insert_X_of_X_mem_of_span_eq hI (I.map constantCoeff).span_generators]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ spanFinrank (R := R⟦X⟧)
      (Ideal.span
        (insert X
          (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have pos : Set.Finite (α := R⟦X⟧)
  (insert X (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))
Tactic: refine le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
pos :
  Set.Finite (α := R⟦X⟧)
    (insert X (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))
⊢ spanFinrank (R := R⟦X⟧)
      (Ideal.span
        (insert X
          (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have pos₁ : ncard (α := R⟦X⟧)
      (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) +
    1 ≤
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
Tactic: refine le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R⟦X⟧)
        (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) +
      1 ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have pos : ncard (α := R⟦X⟧)
    (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) ≤
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
Tactic: simp only [add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R⟦X⟧)
      (Set.image (α := R) (⇑C : (a : R) → R⟦X⟧) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I))) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have pos : ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)) ≤
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
Tactic: refine le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : Ideal.FG (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ ncard (α := R) (generators (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)) ≤
    spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
have pos : spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) ≤
  spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
Tactic: rw [FG.generators_ncard hfg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
⊢ I = J
have refine : I ≤ J
Tactic: refine hJI.antisymm' ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : LE.le (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
⊢ I ≤ J
have h'₁ : Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
Tactic: replace h' := h'.antisymm (Ideal.map_mono hJI)
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff J)
⊢ I ≤ J
have obtain : ∀ (n : ℕ) (F : Fin n → R⟦X⟧) (hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I) (hJ : FG (Submodule.span R⟦X⟧ (Set.range F)))
  (h' :
    Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
      (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Submodule.span R⟦X⟧ (Set.range F)))),
  I ≤ Submodule.span R⟦X⟧ (Set.range F)
Tactic: obtain ⟨n, F, rfl⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hJ
Cleared hypotheses: J, hJI, hJ, h'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (Submodule.span R⟦X⟧ (Set.range F)))
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)
have h'₁ : Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
  (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
Tactic: rw [submodule_span_eq, map_span, ← Set.range_comp] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)
have choose! : ∀ (T : (g : R⟦X⟧) → Fin n → R)
  (hT :
    ∀ (g : R⟦X⟧) (hg : g ∈ I),
      Eq (α := R) (∑ i : Fin n, T g i * ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F) i : R)
        ((constantCoeff : (a : R⟦X⟧) → R) g : R)),
  I ≤ Submodule.span R⟦X⟧ (Set.range F)
Tactic: choose! T hT using fun g (hg : g ∈ I) ↦
    mem_span_range_iff_exists_fun.mp (h'.le (Ideal.mem_map_of_mem _ hg))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have hG' : ∀ (n_1 : ℕ) (H : G n_1 ∈ I),
  G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
Tactic: have hG' (n : ℕ) (H : G n ∈ I) : G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1) := by
    simpa [hT _ H] using sub_const_eq_X_mul_shift (G n - ∑ i, C (T (G n) i) * F i)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG' :
  ∀ (n_1 : ℕ) (H : G n_1 ∈ I),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have hG : ∀ (n : ℕ), G n ∈ I
Tactic: have hG : ∀ n, G n ∈ I := Nat.rec hg fun n IH ↦
    (‹I.IsPrime›.mul_mem_iff_mem_or_mem.mp (hG' n IH ▸ I.sub_mem IH (I.sum_mem fun i _ ↦
      I.mul_mem_left _ (hJI (subset_span (Set.mem_range_self _)))))).resolve_left hXI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG' :
  ∀ (n_1 : ℕ) (H : G n_1 ∈ I),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
hG : ∀ (n : ℕ), G n ∈ I
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have hG'₁ : ∀ (n_1 : ℕ),
  G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
Tactic: replace hG' := fun n ↦ hG' n (hG n)
Cleared hypotheses: hG'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n_1 : ℕ
F : Fin n_1 → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n_1 → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n_1, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n_1, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n : ℕ), G n - ∑ i : Fin n_1, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n) i) : R⟦X⟧) (F i) = X * G (n + 1)
H : (i : Fin n_1) → R⟦X⟧ := fun (i : Fin n_1) ↦ mk fun (n : ℕ) ↦ T (G n) i
n : ℕ
⊢ g - ∑ i : Fin n_1, (↑((trunc n : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i = HPow.hPow (α := R⟦X⟧) X n * G n
have zero : g - ∑ i : Fin n_1, (↑((trunc 0 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
  HPow.hPow (α := R⟦X⟧) (β := ℕ) X 0 * G 0
Tactic: induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n_1 : ℕ
F : Fin n_1 → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n_1 → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n_1, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n_1, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n : ℕ), G n - ∑ i : Fin n_1, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n) i) : R⟦X⟧) (F i) = X * G (n + 1)
H : (i : Fin n_1) → R⟦X⟧ := fun (i : Fin n_1) ↦ mk fun (n : ℕ) ↦ T (G n) i
n : ℕ
zero :
  g - ∑ i : Fin n_1, (↑((trunc 0 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
    HPow.hPow (α := R⟦X⟧) (β := ℕ) X 0 * G 0
⊢ g - ∑ i : Fin n_1, (↑((trunc n : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i = HPow.hPow (α := R⟦X⟧) X n * G n
have succ : ∀ (n : ℕ)
  (IH :
    g - ∑ i : Fin n_1, (↑((trunc n : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i = HPow.hPow (α := R⟦X⟧) X n * G n),
  g - ∑ i : Fin n_1, (↑((trunc (n + 1) : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
    HPow.hPow (α := R⟦X⟧) X (n + 1) * G (n + 1)
Tactic: induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n_1 : ℕ),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
H : (i : Fin n) → R⟦X⟧ := fun (i : Fin n) ↦ mk fun (n : ℕ) ↦ T (G n) i
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have h₁ : ∀ (n_1 : ℕ),
  g - ∑ i : Fin n, (↑((trunc n_1 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i = HPow.hPow (α := R⟦X⟧) X n_1 * G n_1
Tactic: have h₁ (n : ℕ) : g - ∑ i, trunc n (H i) * F i = X ^ n * G n := by
    induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n_1 : ℕ),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
H : (i : Fin n) → R⟦X⟧ := fun (i : Fin n) ↦ mk fun (n : ℕ) ↦ T (G n) i
h₁ :
  ∀ (n_1 : ℕ),
    g - ∑ i : Fin n, (↑((trunc n_1 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
      HPow.hPow (α := R⟦X⟧) X n_1 * G n_1
⊢ g = ∑ i : Fin n, H i * F i
have h : ∀ (n_1 : ℕ),
  Eq (α := R) ((coeff n_1 : (a : R⟦X⟧) → R) g : R) ((coeff n_1 : (a : R⟦X⟧) → R) (∑ i : Fin n, H i * F i) : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n_1 : ℕ),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
H : (i : Fin n) → R⟦X⟧ := fun (i : Fin n) ↦ mk fun (n : ℕ) ↦ T (G n) i
h₁ :
  ∀ (n_1 : ℕ),
    g - ∑ i : Fin n, (↑((trunc n_1 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
      HPow.hPow (α := R⟦X⟧) X n_1 * G n_1
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have h₂ : g = ∑ i : Fin n, H i * F i
Tactic: have h₂ : g = ∑ i, H i * F i := by
    ext n; simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' :
  Eq (α := Ideal R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
    (span (Set.range ((⇑constantCoeff : (a : R⟦X⟧) → R) ∘ F)))
T : (g : R⟦X⟧) → Fin n → R
hT :
  ∀ (g : R⟦X⟧) (hg : g ∈ I),
    Eq (α := R) (∑ i : Fin n, HMul.hMul (β := R) (T g i) ((constantCoeff : (a : R⟦X⟧) → R) (F i) : R) : R)
      ((constantCoeff : (a : R⟦X⟧) → R) g : R)
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ R⟦X⟧) g
      (fun (x : ℕ) (G' : R⟦X⟧) ↦
        mk fun (p : ℕ) ↦
          HSub.hSub (α := R) (β := R) ((coeff (p + 1) : (a : R⟦X⟧) → R) G' : R)
            (∑ i : Fin n, HMul.hMul (β := R) (T G' i) ((coeff (p + 1) : (a : R⟦X⟧) → R) (F i) : R) : R))
      t
hG : ∀ (n : ℕ), G n ∈ I
hG' :
  ∀ (n_1 : ℕ),
    G n_1 - ∑ i : Fin n, HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (T (G n_1) i) : R⟦X⟧) (F i) = X * G (n_1 + 1)
H : (i : Fin n) → R⟦X⟧ := fun (i : Fin n) ↦ mk fun (n : ℕ) ↦ T (G n) i
h₁ :
  ∀ (n_1 : ℕ),
    g - ∑ i : Fin n, (↑((trunc n_1 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
      HPow.hPow (α := R⟦X⟧) X n_1 * G n_1
h₂ : g = ∑ i : Fin n, H i * F i
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g
have rw : Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) (∑ i : Fin n, H i * F i)
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
⊢ ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard
have this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
Tactic: have : SurjOn constantCoeff I S := by
    intro r hr
    simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
inst_1 : I.IsPrime
hI : X ∉ I
S : Set R
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
hS : S.Finite
this : SurjOn (⇑constantCoeff : (a : R⟦X⟧) → R) (↑I : Set R⟦X⟧) S
⊢ ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard
have obtain : ∀ (T : Set R⟦X⟧) (hTI : T ⊆ (↑I : Set R⟦X⟧)) (hinj : InjOn (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R) T)
  (hT : (⇑constantCoeff : (a : R⟦X⟧) → R) '' T = S), ∃ (T : Set R⟦X⟧), I = span T ∧ T.Finite ∧ T.ncard = S.ncard
Tactic: obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq