awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
⊢ 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'

Premises used: Set.range_comp, Ideal.submodule_span_eq, Ideal.map_span
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)))
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)
⊢ 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))

Premises used: Ideal.mem_map_of_mem, Eq.le, PowerSeries.constantCoeff, Ideal.mem_span_range_iff_exists_fun, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
n : ℕ
H : G n ∈ I
⊢ 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)

Tactic:
simpa [hT _ H] using sub_const_eq_X_mul_shift (G n - ∑ i, C (T (G n) i) * F i)

Premises used: HMul.hMul, Finset.univ, HSub.hSub, PowerSeries.sub_const_eq_X_mul_shift, PowerSeries.C, DFunLike.coe, Finset.sum
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ ∀ (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)
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)
⊢ ∀ (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
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ ∀ (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)
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ g - ∑ i : Fin n, (↑((trunc 0 : (a : R⟦X⟧) → Polynomial R) (H i)) : R⟦X⟧) * F i =
    HPow.hPow (α := R⟦X⟧) (β := ℕ) X 0 * G 0

Tactic:
simp [G]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 : ℕ
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:
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 _)]

Premises used: add_mul, Finset.mul_sum, mul_sub, Finset.sum_add_distrib, pow_succ, mul_assoc, mul_left_comm, PowerSeries.C, sub_sub, PowerSeries.monomial_eq_C_mul_X_pow, PowerSeries.trunc_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
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)
⊢ 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

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 _)]

Premises used: add_mul, Finset.mul_sum, mul_sub, Finset.sum_add_distrib, pow_succ, mul_assoc, mul_left_comm, PowerSeries.C, sub_sub, PowerSeries.monomial_eq_C_mul_X_pow, PowerSeries.trunc_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ ∀ (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 _)]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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 :
  ∀ (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)
⊢ g = ∑ i : Fin n, H i * F i

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
h₁ :
  ∀ (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
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) g : R) ((coeff n : (a : R⟦X⟧) → R) (∑ i : Fin n_1, H i * F i) : R)

Tactic:
simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)

Premises used: PowerSeries.coeff_trunc, sub_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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

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)
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
rw : Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) (∑ i : Fin n, H i * F i)
⊢ Membership.mem (γ := Submodule R⟦X⟧ R⟦X⟧) (Submodule.span R⟦X⟧ (Set.range F)) g

Tactic:
rw [h₂]
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)) (∑ i : Fin n, H i * F i)

Tactic:
Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _ (subset_span (Set.mem_range_self _))

Premises used: Set.mem_range_self, Ideal.subset_span, Set.Mem, Ideal.sum_mem, Submodule.span, Set.range, PowerSeries, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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)) (∑ i : Fin n, H i * F i)

Tactic:
exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _ (subset_span (Set.mem_range_self _))

Premises used: Set.mem_range_self, Ideal.subset_span, Ideal.sum_mem, Ideal.span, Set.range, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
r : R
hr : r ∈ S
⊢ Membership.mem (γ := Set R) ((⇑constantCoeff : (a : R⟦X⟧) → R) '' (↑I : Set R⟦X⟧)) r

Tactic:
simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr

Premises used: Ideal.subset_span, PowerSeries.constantCoeff_surj, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.PowerSeries.Ideal
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
⊢ 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