awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
coeff :
  Eq.{u_8 + 1} (α := V)
    (∑
      gh ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      s.hsum.coeff gh.1 • t.hsum.coeff gh.2)
    (∑ ij ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯, s.hsum.coeff ij.1 • t.hsum.coeff ij.2)
⊢ (s.smul t).hsum.coeff g =
    HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) s.hsum
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) t.hsum : HahnModule Γ' R V)))
      g

Tactic:
rw [coeff_smul s t g, HahnModule.coeff_smul, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, HahnSeries.SummableFamily.coeff_smul, HahnModule.coeff_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
h : x ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯
⊢ s.hsum.coeff x.1 • t.hsum.coeff x.2 =
    s.hsum.coeff ((fun (a : Γ × Γ') ↦ a) x).1 • t.hsum.coeff ((fun (a : Γ × Γ') ↦ a) x).2

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
coeff :
  ∀ (x : Γ × Γ') (hgh : x ∈ (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))),
    (fun (a : Γ × Γ') ↦ a) x ∈
      (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
            ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
        Set (Γ × Γ'))
coeff₁ :
  ∀
    gh ∈
      VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
        ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
    ∀
      (hgh :
        gh ∉
          (fun (a : Γ × Γ') ↦ a) ''
            (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))),
      s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
⊢ Eq.{u_8 + 1} (α := V)
    (∑
      gh ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      s.hsum.coeff gh.1 • t.hsum.coeff gh.2)
    (∑ ij ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯, s.hsum.coeff ij.1 • t.hsum.coeff ij.2)

Tactic:
refine Eq.symm (sum_of_injOn (fun a ↦ a) (fun _ _ _ _ h ↦ h) (fun _ hgh => ?_)
    (fun gh _ hgh => ?_) fun _ _ => by simp)

Premises used: Finset.sum_of_injOn, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh : x ∈ (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))
coeff :
  ∀ (hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g),
    (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0) ∧
      ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
⊢ (fun (a : Γ × Γ') ↦ a) x ∈
    (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
      Set (Γ × Γ'))

Tactic:
simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]

Premises used: and_true, Finset.mem_vaddAntidiagonal, Set.mem_iUnion, ne_eq, Finset.mem_coe, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
coeff : ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0
coeff₁ : ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
⊢ (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0) ∧
    ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ ¬Eq.{u_7 + 1} (α := R) (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0 ∧
    ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g

Tactic:
rw [coeff_hsum_eq_sum] at hgh

Premises used: HahnSeries.SummableFamily.coeff_hsum_eq_sum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh :
  ¬Eq.{u_7 + 1} (α := R) (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0 ∧
    ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ ∃ a ∈ (s.coeff x.1).support, Ne.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) x.1) 0

Tactic:
have h' := Finset.exists_ne_zero_of_sum_ne_zero hgh.1
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh :
  ¬Eq.{u_7 + 1} (α := R) (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0 ∧
    ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
h' : ∃ a ∈ (s.coeff x.1).support, Ne.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) x.1) 0
⊢ ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0

Tactic:
simpa using h'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
coeff : ∀ (hi : ¬∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0), False
⊢ ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0

Tactic:
by_contra hi
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
hi : ¬∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
hgh :
  gh ∉ (fun (a : Γ × Γ') ↦ a) '' (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))
⊢ ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g

Tactic:
simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh

Premises used: Set.image_id', Finset.mem_vaddAntidiagonal, ne_eq, not_and, Finset.mem_coe, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
pos : ∀ (h : s.hsum.coeff gh.1 = 0), s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
neg : ∀ (h : ¬s.hsum.coeff gh.1 = 0), s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
by_cases h : s.hsum.coeff gh.1 = 0

Premises used: Prod.fst, HahnSeries.coeff, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h_1 :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
smul_eq_zero_of_left h (t.hsum.coeff gh.2)

Premises used: smul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h_1 :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)

Premises used: smul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h_1 :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : ¬s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
x : R⟦Γ⟧
t : SummableFamily Γ' V β
⊢ x • t = Equiv (Equiv.punitProd β) ((const Unit x).smul t)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
x : R⟦Γ⟧
s : SummableFamily Γ' V α
a : α
⊢ Eq (α := V⟦Γ'⟧) ((x • s : (a : α) → V⟦Γ'⟧) a : V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((s : (a : α) → V⟦Γ'⟧) a) : HahnModule Γ' R V)) :
      V⟦Γ'⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
x : R⟦Γ⟧
s : SummableFamily Γ' V α
rw :
  (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₁ :
  ((const Unit x).smul s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₂ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) (const Unit x).hsum
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
rw₃ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((const Unit x : (a : PUnit.{1}) → R⟦Γ⟧) default : R⟦Γ⟧)
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
rw₄ rw₅ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))

Tactic:
rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]

Premises used: HahnSeries.SummableFamily.smul_hsum, HahnSeries.SummableFamily.const_toFun, HahnSeries.SummableFamily.smul_eq, HahnSeries.SummableFamily.hsum_unique, HahnSeries.SummableFamily.hsum_equiv
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x x_1 : R⟦Γ⟧
x_2 : SummableFamily Γ' V α
x_3 : α
⊢ Eq (α := V⟦Γ'⟧) (((x * x_1) • x_2 : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧) ((x • x_1 • x_2 : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧)

Tactic:
simp [HahnModule.instModule.mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : SummableFamily Γ' V α
x_1 : α
rw :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) 1
          ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1) : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
rw₁ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1)) :
      V⟦Γ'⟧)
    ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
rw₂ rw₃ : Eq (α := V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (α := R⟦Γ⟧) 1 x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)

Tactic:
rw [smul_apply, HahnModule.one_smul', Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, HahnSeries.SummableFamily.smul_apply, HahnModule.one_smul'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : R⟦Γ⟧
x_1 : α
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (β := SummableFamily Γ' V α) x 0 : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
    ((0 : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : R⟦Γ⟧
x_1 x_2 : SummableFamily Γ' V α
x_3 : α
⊢ Eq (α := V⟦Γ'⟧) ((x • (x_1 + x_2) : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧) ((x • x_1 + x • x_2 : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x x_1 : R⟦Γ⟧
x_2 : SummableFamily Γ' V α
x_3 : α
⊢ Eq (α := V⟦Γ'⟧) (((x + x_1) • x_2 : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧)
    ((x • x_2 + x_1 • x_2 : (a : α) → V⟦Γ'⟧) x_3 : V⟦Γ'⟧)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : SummableFamily Γ' V α
x_1 : α
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (α := R⟦Γ⟧) 0 x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((0 : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
rw :
  (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) s.hsum : HahnModule Γ R R)) =
    x * s.hsum
rw₁ rw₂ : x * s.hsum = x * s.hsum
⊢ (x • s).hsum = x * s.hsum

Tactic:
rw [hsum_smul_module, of_symm_smul_of_eq_mul]

Premises used: HahnSeries.SummableFamily.hsum_smul_module, HahnSeries.of_symm_smul_of_eq_mul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst_3 : Ring R
s t : SummableFamily Γ R α
rw : (lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) (s - t) = s.hsum - t.hsum
rw₁ :
  HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) s : R⟦Γ⟧)
      ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) =
    s.hsum - t.hsum
rw₂ : HSub.hSub (β := R⟦Γ⟧) s.hsum ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) = s.hsum - t.hsum
rw₃ rw₄ : s.hsum - t.hsum = s.hsum - t.hsum
⊢ (s - t).hsum = s.hsum - t.hsum

Tactic:
rw [← lsum_apply, map_sub, lsum_apply, lsum_apply]

Premises used: map_sub, HahnSeries.SummableFamily.lsum_apply
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : α → R⟦Γ⟧
t : β → R⟦Γ⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_1} (α := Γ) (⋃ (b : β), (t b).support)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α × β), support.{u_1, u_3} (R := R) ((fun (a : α × β) ↦ s a.1 * t a.2) a))

Tactic:
isPWO_iUnion_support_prod_smul hs ht

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ Finite
    (↑{x : α × β |
          match (motive := α × β → Prop) x with
          | a =>
            Ne.{u_3 + 1} (α := R)
              (HahnSeries.coeff
                ((fun (a : α × β) ↦
                    HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a.1 : R⟦Γ⟧)
                      ((t : (a : β) → R⟦Γ⟧) a.2 : R⟦Γ⟧))
                  a)
                g)
              0} :
      Type (max u_5 u_6))

Tactic:
finite_co_support_prod_smul s t g

Premises used: setOf, HahnSeries.SummableFamily.finite_co_support_prod_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ s.mul t = s.smul t

Tactic:
rfl

Premises used: HahnSeries.SummableFamily.mul, HahnSeries.SummableFamily.smul, rfl