awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_4} (M := W) fun (x_2 : Γ) ↦ (f x_2 : (a : V) → W) x)
x x_1 : V
h :
  ∀ (x_2 : Γ),
    Eq.{u_4 + 1} (α := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
            { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x + x_1), isPWO_support' := ⋯ }))
        x_2)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
          (HAdd.hAdd (α := HahnModule Γ R W) (β := HahnModule Γ R W)
            ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
                { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x, isPWO_support' := ⋯ } :
              HahnModule Γ R W)
            ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
                { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ } :
              HahnModule Γ R W)))
        x_2)
⊢ (of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
      { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x + x_1), isPWO_support' := ⋯ } =
    HAdd.hAdd (α := HahnModule Γ R W) (β := HahnModule Γ R W)
      ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
          { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x, isPWO_support' := ⋯ : HahnSeries Γ W } :
        HahnModule Γ R W)
      ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
          { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ : HahnSeries Γ W } :
        HahnModule Γ R W)

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_4} (M := W) fun (x_3 : Γ) ↦ (f x_3 : (a : V) → W) x)
x x_1 : V
x_2 : Γ
⊢ Eq.{u_4 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
        ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
          { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x + x_1), isPWO_support' := ⋯ }))
      x_2)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
        (HAdd.hAdd (α := HahnModule Γ R W) (β := HahnModule Γ R W)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
              { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x, isPWO_support' := ⋯ } :
            HahnModule Γ R W)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
              { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ } :
            HahnModule Γ R W)))
      x_2)

Tactic:
simp
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_4} (M := W) fun (x_2 : Γ) ↦ (f x_2 : (a : V) → W) x)
x : R
x_1 : V
h :
  ∀ (x_2 : Γ),
    Eq.{u_4 + 1} (α := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
            { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x • x_1), isPWO_support' := ⋯ }))
        x_2)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
          (HSMul.hSMul (α := R) (β := HahnModule Γ R W) ((RingHom.id R : (a : R) → R) x : R)
            ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
                { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ } :
              HahnModule Γ R W)))
        x_2)
⊢ (of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
      { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x • x_1), isPWO_support' := ⋯ } =
    HSMul.hSMul (α := R) (β := HahnModule Γ R W) ((RingHom.id R : (a : R) → R) x : R)
      ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
          { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ : HahnSeries Γ W } :
        HahnModule Γ R W)

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_4} (M := W) fun (x_3 : Γ) ↦ (f x_3 : (a : V) → W) x)
x : R
x_1 : V
x_2 : Γ
⊢ Eq.{u_4 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
        ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
          { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) (x • x_1), isPWO_support' := ⋯ }))
      x_2)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
        (HSMul.hSMul (α := R) (β := HahnModule Γ R W) ((RingHom.id R : (a : R) → R) x : R)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
              { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := ⋯ } :
            HahnModule Γ R W)))
      x_2)

Tactic:
simp
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_4} (M := W) fun (g : Γ) ↦ (f g : (a : V) → W) x)
⊢ (coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) (of_coeff f hf) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst_1 : CommRing R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddCommGroup W
inst_5 : Module R W
A : HVertexOperator Γ R V W
⊢ of_coeff ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) A) ⋯ = A

Tactic:
rfl

Premises used: HVertexOperator.of_coeff, HahnModule, rfl
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
⊢ Set.IsPWO.{u_6} (α := Γ')
    (Function.support (M := HahnSeries Γ W) fun (g' : Γ') ↦
      (A : (a : V) → HahnModule Γ R W)
        ((((coeff : (a : HVertexOperator Γ' R U V) → Γ' → U →ₗ[R] V) B g' : U →ₗ[R] V) : (a : U) → V) u))

Tactic:
Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_

Premises used: HahnSeries.isPWO_support', HahnModule.of, Equiv.symm, Set.IsPWO.mono, DFunLike.coe
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
refine :
  Subset.{u_6} (α := Set Γ')
    (Function.support (M := HahnSeries Γ W) fun (g' : Γ') ↦
      (A : (a : V) → HahnModule Γ R W)
        ((((coeff : (a : HVertexOperator Γ' R U V) → Γ' → U →ₗ[R] V) B g' : U →ₗ[R] V) : (a : U) → V) u))
    (Function.support.{u_6, u_9} (M := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))))
⊢ Set.IsPWO.{u_6} (α := Γ')
    (Function.support (M := HahnSeries Γ W) fun (g' : Γ') ↦
      (A : (a : V) → HahnModule Γ R W)
        ((((coeff : (a : HVertexOperator Γ' R U V) → Γ' → U →ₗ[R] V) B g' : U →ₗ[R] V) : (a : U) → V) u))

Tactic:
refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_

Premises used: HahnSeries.isPWO_support', HahnModule.of, Equiv.symm, Set.IsPWO.mono, DFunLike.coe
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
simp :
  ∀ (x : Γ'),
    ¬Eq (α := HahnSeries Γ W)
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))
          0 →
      ¬Eq.{u_9 + 1} (α := V)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x)
          0
⊢ Subset.{u_6} (α := Set Γ')
    (Function.support (M := HahnSeries Γ W) fun (g' : Γ') ↦
      (A : (a : V) → HahnModule Γ R W)
        ((((coeff : (a : HVertexOperator Γ' R U V) → Γ' → U →ₗ[R] V) B g' : U →ₗ[R] V) : (a : U) → V) u))
    (Function.support.{u_6, u_9} (M := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))))

Tactic:
simp only [coeff_apply_apply, Function.support_subset_iff, ne_eq, Function.mem_support]

Premises used: ne_eq, Function.support_subset_iff, Function.mem_support, HVertexOperator.coeff_apply_apply
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' :
  ¬Eq (α := HahnSeries Γ W)
      ((A : (a : V) → HahnModule Γ R W)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) g'))
      0
hAB :
  Eq.{u_9 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) g')
    0
⊢ Eq (α := HahnSeries Γ W)
    ((A : (a : V) → HahnModule Γ R W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) g'))
    0

Tactic:
simp [hAB]
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' :
  ¬Eq (α := HahnSeries Γ W)
      ((A : (a : V) → HahnModule Γ R W)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) g'))
      0
hAB :
  Eq.{u_9 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) g')
    0
⊢ False

Tactic:
exact hg' (by simp [hAB])
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
coeff :
  ∀ (x : Γ') (x_1 : Γ),
    ((A.compHahnSeries B (u + v)).coeff x).coeff x_1 = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x).coeff x_1
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x : Γ'
x_1 : Γ
coeff :
  (HAdd.hAdd (α := HahnModule Γ R W)
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v))
              x))).coeff
      x_1 =
    HAdd.hAdd (α := W)
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x))
        x_1)
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v)) x))
        x_1)
⊢ ((A.compHahnSeries B (u + v)).coeff x).coeff x_1 = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x).coeff x_1

Tactic:
simp only [compHahnSeries_coeff, map_add, coeff_apply_apply, HahnSeries.coeff_add', Pi.add_apply]

Premises used: map_add, Pi.add_apply, HVertexOperator.compHahnSeries_coeff, HVertexOperator.coeff_apply_apply, HahnSeries.coeff_add'
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x : Γ'
x_1 : Γ
coeff coeff₁ :
  (HAdd.hAdd (α := HahnModule Γ R W)
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v))
              x))).coeff
      x_1 =
    (HAdd.hAdd (α := HahnSeries Γ W)
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v))
              x))).coeff
      x_1
⊢ (HAdd.hAdd (α := HahnModule Γ R W)
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v))
              x))).coeff
      x_1 =
    HAdd.hAdd (α := W)
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x))
        x_1)
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) v)) x))
        x_1)

Tactic:
rw [← HahnSeries.coeff_add]

Premises used: HahnSeries.coeff_add
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
coeff :
  ∀ (x : Γ') (x_1 : Γ),
    ((A.compHahnSeries B (r • u)).coeff x).coeff x_1 = ((r • A.compHahnSeries B u).coeff x).coeff x_1
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x : Γ'
x_1 : Γ
coeff :
  (HSMul.hSMul (β := HahnModule Γ R W) r
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))).coeff
      x_1 =
    HSMul.hSMul (β := W) r
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x))
        x_1)
⊢ ((A.compHahnSeries B (r • u)).coeff x).coeff x_1 = ((r • A.compHahnSeries B u).coeff x).coeff x_1

Tactic:
simp only [compHahnSeries_coeff, map_smul, coeff_apply_apply, HahnSeries.coeff_smul]

Premises used: HahnSeries.coeff_smul, HVertexOperator.compHahnSeries_coeff, HVertexOperator.coeff_apply_apply, map_smul
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x : Γ'
x_1 : Γ
coeff coeff₁ :
  (HSMul.hSMul (β := HahnModule Γ R W) r
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))).coeff
      x_1 =
    (HSMul.hSMul (β := HahnSeries Γ W) r
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))).coeff
      x_1
⊢ (HSMul.hSMul (β := HahnModule Γ R W) r
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))).coeff
      x_1 =
    HSMul.hSMul (β := W) r
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x))
        x_1)

Tactic:
rw [← HahnSeries.coeff_smul]

Premises used: HahnSeries.coeff_smul
-- Module: Mathlib.Algebra.Vertex.HVertexOperator
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
h :
  ∀ (g : Lex (Γ' × Γ)),
    Eq.{u_10 + 1} (α := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
          ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
            (A.compHahnSeries B (u + v)).ofIterate))
        g)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
          (HAdd.hAdd (α := HahnModule (Lex (Γ' × Γ)) R W) (β := HahnModule (Lex (Γ' × Γ)) R W)
            ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
                (A.compHahnSeries B u).ofIterate :
              HahnModule (Lex (Γ' × Γ)) R W)
            ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
                (A.compHahnSeries B v).ofIterate :
              HahnModule (Lex (Γ' × Γ)) R W)))
        g)
⊢ (of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B (u + v)).ofIterate =
    HAdd.hAdd (α := HahnModule (Lex (Γ' × Γ)) R W) (β := HahnModule (Lex (Γ' × Γ)) R W)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B u).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B v).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)

Tactic:
ext g