awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have contrapose! : ∀
  (h :
    Ne.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)),
  p ∣ (m : (a : σ) → ℕ) i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
⊢ p ∣ (m : (a : σ) → ℕ) i
have h₁ : Ne.{u_3 + 1} (α := R)
  (∑ᶠ (d : σ →₀ ℕ),
    HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R))
  0
Tactic: simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R)
      (0 : R)
have by_contra! : ∀
  (hc :
    ∀ (d : σ →₀ ℕ),
      Eq.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R)
        (0 : R)),
  False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
hc :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R)
      (0 : R)
⊢ False
have h₁ : Ne.{u_3 + 1} (α := R) 0 0
Tactic: rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
⊢ p ∣ (m : (a : σ) → ℕ) i
have obtain : ∀ (d : σ →₀ ℕ)
  (hd :
    Ne.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R)
      (0 : R)),
  p ∣ (m : (a : σ) → ℕ) i
Tactic: obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
      R)
    (0 : R)
⊢ p ∣ (m : (a : σ) → ℕ) i
have this : Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
  ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
Tactic: have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
      R)
    (0 : R)
this :
  Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
⊢ p ∣ (m : (a : σ) → ℕ) i
have hd₁ : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
Tactic: rw [this, coeff_monomial] at hd
Cleared hypotheses: hd, this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
this :
  Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
⊢ m = p • d
have by_contra : ∀ (hc : ¬m = p • d), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
this :
  Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
hc : ¬m = p • d
⊢ False
have hd₁ : Ne.{u_3 + 1} (α := R) 0 0
Tactic: rw [if_neg hc] at hd
Cleared hypotheses: hd, this, hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
this :
  Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
⊢ p ∣ (m : (a : σ) → ℕ) i
have meq : m = p • d
Tactic: have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have contrapose! : ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
  Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
Tactic: classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have contrapose!₂ : Ne.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R) →
  p ∣ (m : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
          R)
        (0 : R)),
    p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have contrapose!₅ : ∀
  (h :
    Ne.{u_3 + 1} (α := R)
      (∑ᶠ (d : σ →₀ ℕ),
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff m : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R))
      0),
  p ∣ (m : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
          R)
        (0 : R)),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₅ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0),
    p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have contrapose!₆ : ∀
  (h :
    Ne.{u_3 + 1} (α := R)
      (∑ᶠ (d : σ →₀ ℕ),
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff m : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R))
      0)
  (d : σ →₀ ℕ)
  (hd :
    Ne.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R)
      (0 : R)),
  p ∣ (m : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d
have this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
Tactic: have : ∀ i, p ∣ d i := fun _ => by_contra fun hc => hd (coeff_expand_of_not_dvd p hp φ hc)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d
have eq_aux : p • m = d
Tactic: have eq_aux : p • m = d := (Finsupp.ext fun a => Nat.eq_mul_of_div_eq_right (this a) rfl).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
eq_aux : p • m = d
this₁ : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d
have hd₁ : let m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) sorry d;
φ m ≠ 0
Tactic: rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd
Cleared hypotheses: hd, this, m, eq_aux
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine : Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
  (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
Tactic: refine (support_expand_subset p hp φ).antisymm ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
have obtain : ∀ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
Tactic: obtain ⟨n, hn₁, hn₂⟩ := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
have simp : Ne.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)
Tactic: simp only [← hn₂, Function.mem_support]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d
hc : Eq.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)
⊢ False
have hn₃ : Ne.{u_3 + 1} (α := R) 0 0
Tactic: rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
Cleared hypotheses: hn₁, hn₂, hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine : Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
  (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
Tactic: classical
  refine (support_expand_subset p hp φ).antisymm ?_
  intro d hd
  obtain ⟨n, hn₁, hn₂⟩ := hd
  simp only [← hn₂, Function.mem_support]
  by_contra hc
  rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
  contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
refine :
  Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine₁ : ∀ ⦃d : σ →₀ ℕ⦄ (hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d),
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
Tactic: classical
  refine (support_expand_subset p hp φ).antisymm ?_
  intro d hd
  obtain ⟨n, hn₁, hn₂⟩ := hd
  simp only [← hn₂, Function.mem_support]
  by_contra hc
  rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
  contradiction
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
refine :
  Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
refine₁ :
  ∀ ⦃d : σ →₀ ℕ⦄ (hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d),
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine₂ : ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
Tactic: classical
  refine (support_expand_subset p hp φ).antisymm ?_
  intro d hd
  obtain ⟨n, hn₁, hn₂⟩ := hd
  simp only [← hn₂, Function.mem_support]
  by_contra hc
  rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
  contradiction