awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop x.sum = (map untrop x).inf
⊢ untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf

Tactic:
simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]

Premises used: Multiset.map_cons, Tropical.untrop_add, Multiset.inf_cons, Multiset.sum_cons
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Multiset (Tropical R)
empty : Eq.{u_1 + 1} (α := R) (untrop (sum 0)) (inf (map untrop 0))
cons :
  ∀ (s : Tropical R) (x : Multiset (Tropical R)) (IH : untrop x.sum = (map untrop x).inf),
    untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf
⊢ untrop s.sum = (map untrop s).inf

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]

Premises used: Multiset.map_cons, Multiset.cons, Tropical.untrop_add, Multiset.inf_cons, Multiset.sum_cons
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (Multiset.map f s.val).sum = (Multiset.map untrop (Multiset.map f s.val)).inf

Tactic:
Multiset.untrop_sum (s.val.map f)

Premises used: Multiset.map, Multiset.untrop_sum, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → Tropical R
h : s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf
⊢ untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)

Tactic:
convert! Multiset.untrop_sum (s.val.map f)

Premises used: Multiset.map, Multiset.untrop_sum, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → Tropical R
⊢ s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf

Tactic:
simp only [Multiset.map_map, Function.comp_apply, inf_def]

Premises used: Finset.inf_def, Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
inl : untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' (↑∅ : Set S))
inr : ∀ (h : s.Nonempty), untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' (↑∅ : Set S))

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]

Premises used: Finset.coe_empty, WithTop.sInf_empty, Finset.sum_empty, Tropical.untrop_zero, Set.image_empty
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
inr : untrop (∑ i ∈ s, f i) = s.inf' h (untrop ∘ f)
inr₁ : untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)
inr₂ inr₃ : s.inf (untrop ∘ f) = s.inf (untrop ∘ f)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))

Tactic:
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']

Premises used: Finset.untrop_sum', Finset.inf'_eq_csInf_image, Finset.inf'_eq_inf
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
inst_1 : Fintype S
f : S → Tropical (WithTop R)
rw : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf (Set.range fun (i : S) ↦ untrop (f i)))
rw₁ : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf ((fun (i : S) ↦ untrop (f i)) '' Set.univ))
rw₂ : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf ((fun (i : S) ↦ untrop (f i)) '' (↑univ : Set S)))
rw₃ : sInf (untrop ∘ f '' (↑univ : Set S)) = sInf ((fun (i : S) ↦ untrop (f i)) '' (↑univ : Set S))
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := WithTop R) (sInf ((fun (x : S) ↦ untrop (f x)) '' (↑univ : Set S)))
    (sInf ((fun (i : S) ↦ untrop (f i)) '' (↑univ : Set S)))
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]

Premises used: Set.image_univ, iInf, Finset.coe_univ, Function.comp_def, untrop_sum_eq_sInf_image
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i ∈ s, f i)) (⨅ (i : ↥s), untrop (f (↑i : S)))

Tactic:
simpa [← _root_.untrop_sum] using (sum_attach _ _).symm

Premises used: Finset.sum_attach, untrop_sum, Eq.symm
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
⊢ Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ

Tactic:
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
simp : sSup (untrop '' s) = sSup ∅
⊢ sSup s = sSup ∅

Tactic:
simp only [sSup, Set.image_empty, trop_inj_iff]

Premises used: Tropical.trop_inj_iff, SupSet.sSup, Set.image_empty
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs₁ : ¬BddAbove (untrop '' s)
⊢ sSup (untrop '' s) = sSup ∅

Tactic:
apply csSup_of_not_bddAbove

Premises used: csSup_of_not_bddAbove
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs₁ : ∀ (hs : BddAbove (untrop '' s)), BddAbove s
⊢ ¬BddAbove (untrop '' s)

Tactic:
contrapose hs
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddAbove (untrop '' s)
⊢ BddAbove (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)

Tactic:
change BddAbove (tropOrderIso.symm '' s) at hs

Premises used: Tropical.tropOrderIso, OrderIso.symm, BddAbove, Set.image, DFunLike.coe
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddAbove (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
⊢ BddAbove s

Tactic:
tropOrderIso.symm.bddAbove_image.1 hs

Premises used: OrderIso.bddAbove_image, Iff.mp
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddAbove (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
⊢ BddAbove s

Tactic:
exact tropOrderIso.symm.bddAbove_image.1 hs

Premises used: OrderIso.bddAbove_image, Iff.mp
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
⊢ Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ

Tactic:
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
simp : sInf (untrop '' s) = sInf ∅
⊢ sInf s = sInf ∅

Tactic:
simp only [sInf, Set.image_empty, trop_inj_iff]

Premises used: Tropical.trop_inj_iff, InfSet.sInf, Set.image_empty
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs₁ : ¬BddBelow (untrop '' s)
⊢ sInf (untrop '' s) = sInf ∅

Tactic:
apply csInf_of_not_bddBelow

Premises used: csInf_of_not_bddBelow
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs₁ : ∀ (hs : BddBelow (untrop '' s)), BddBelow s
⊢ ¬BddBelow (untrop '' s)

Tactic:
contrapose hs
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddBelow (untrop '' s)
⊢ BddBelow (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)

Tactic:
change BddBelow (tropOrderIso.symm '' s) at hs

Premises used: Tropical.tropOrderIso, OrderIso.symm, BddBelow, Set.image, DFunLike.coe
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddBelow (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
⊢ BddBelow s

Tactic:
tropOrderIso.symm.bddBelow_image.1 hs

Premises used: Iff.mp, OrderIso.bddBelow_image
-- Module: Mathlib.Algebra.Tropical.Lattice
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Eq.{u_1 + 1} (α := Set R) (Set.range untrop) Set.univ
hs : BddBelow (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
⊢ BddBelow s

Tactic:
exact tropOrderIso.symm.bddBelow_image.1 hs

Premises used: Iff.mp, OrderIso.bddBelow_image
-- 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 B : HVertexOperator Γ R V W
h :
  ∀ (v : V),
    Eq (α := HahnModule Γ R W) ((A : (a : V) → HahnModule Γ R W) v : HahnModule Γ R W)
      ((B : (a : V) → HahnModule Γ R W) v : HahnModule Γ R W)
⊢ A = B

Tactic:
LinearMap.ext h

Premises used: LinearMap.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
A : HVertexOperator Γ R V W
n : Γ
u v : V
⊢ HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) (u + v))) n =
    HAdd.hAdd (α := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) u)) n)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) v)) n)

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
A : HVertexOperator Γ R V W
n : Γ
r : R
v : V
⊢ HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) (r • v))) n =
    HSMul.hSMul (α := R) (β := W) ((RingHom.id R : (a : R) → R) r : R)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) v)) n)

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
x x_1 : HVertexOperator Γ R V W
h :
  ∀ (x_2 : Γ) (x_3 : V),
    Eq.{u_4 + 1} (α := W)
      (({
              toFun := fun (v : V) ↦
                HahnSeries.coeff
                  ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                    ((x + x_1 : (a : V) → HahnModule Γ R W) v))
                  x_2,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : V) → W)
          x_3 :
        W)
      ((HAdd.hAdd (α := Γ → V →ₗ[R] W) (β := Γ → V →ₗ[R] W)
              (fun (n : Γ) ↦
                {
                  toFun := fun (v : V) ↦
                    HahnSeries.coeff
                      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                        ((x : (a : V) → HahnModule Γ R W) v))
                      n,
                  map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
              (fun (n : Γ) ↦
                {
                  toFun := fun (v : V) ↦
                    HahnSeries.coeff
                      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                        ((x_1 : (a : V) → HahnModule Γ R W) v))
                      n,
                  map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
              x_2 :
            (a : V) → W)
          x_3 :
        W)
⊢ (fun (n : Γ) ↦
      {
        toFun := fun (v : V) ↦
          HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x + x_1 : (a : V) → HahnModule Γ R W) v))
            n,
        map_add' := ⋯, map_smul' := ⋯ }) =
    HAdd.hAdd (α := Γ → V →ₗ[R] W)
      (fun (n : Γ) ↦
        {
          toFun := fun (v : V) ↦
            HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x : (a : V) → HahnModule Γ R W) v)) n,
          map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
      fun (n : Γ) ↦
      {
        toFun := fun (v : V) ↦
          HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x_1 : (a : V) → HahnModule Γ R W) v)) n,
        map_add' := ⋯, map_smul' := ⋯ : V →ₗ[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
x x_1 : HVertexOperator Γ R V W
x_2 : Γ
x_3 : V
⊢ Eq.{u_4 + 1} (α := W)
    (({
            toFun := fun (v : V) ↦
              HahnSeries.coeff
                ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                  ((x + x_1 : (a : V) → HahnModule Γ R W) v))
                x_2,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : V) → W)
        x_3 :
      W)
    ((HAdd.hAdd (α := Γ → V →ₗ[R] W) (β := Γ → V →ₗ[R] W)
            (fun (n : Γ) ↦
              {
                toFun := fun (v : V) ↦
                  HahnSeries.coeff
                    ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x : (a : V) → HahnModule Γ R W) v))
                    n,
                map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
            (fun (n : Γ) ↦
              {
                toFun := fun (v : V) ↦
                  HahnSeries.coeff
                    ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                      ((x_1 : (a : V) → HahnModule Γ R W) v))
                    n,
                map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
            x_2 :
          (a : V) → W)
        x_3 :
      W)

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
x : R
x_1 : HVertexOperator Γ R V W
h :
  ∀ (x_2 : Γ) (x_3 : V),
    Eq.{u_4 + 1} (α := W)
      (({
              toFun := fun (v : V) ↦
                HahnSeries.coeff
                  ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                    ((x • x_1 : (a : V) → HahnModule Γ R W) v))
                  x_2,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : V) → W)
          x_3 :
        W)
      ((HSMul.hSMul (α := R) (β := Γ → V →ₗ[R] W) ((RingHom.id R : (a : R) → R) x : R)
              (fun (n : Γ) ↦
                {
                  toFun := fun (v : V) ↦
                    HahnSeries.coeff
                      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                        ((x_1 : (a : V) → HahnModule Γ R W) v))
                      n,
                  map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
              x_2 :
            (a : V) → W)
          x_3 :
        W)
⊢ (fun (n : Γ) ↦
      {
        toFun := fun (v : V) ↦
          HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x • x_1 : (a : V) → HahnModule Γ R W) v))
            n,
        map_add' := ⋯, map_smul' := ⋯ }) =
    HSMul.hSMul (α := R) (β := Γ → V →ₗ[R] W) ((RingHom.id R : (a : R) → R) x : R) fun (n : Γ) ↦
      {
        toFun := fun (v : V) ↦
          HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((x_1 : (a : V) → HahnModule Γ R W) v)) n,
        map_add' := ⋯, map_smul' := ⋯ : V →ₗ[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
x : R
x_1 : HVertexOperator Γ R V W
x_2 : Γ
x_3 : V
⊢ Eq.{u_4 + 1} (α := W)
    (({
            toFun := fun (v : V) ↦
              HahnSeries.coeff
                ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                  ((x • x_1 : (a : V) → HahnModule Γ R W) v))
                x_2,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : V) → W)
        x_3 :
      W)
    ((HSMul.hSMul (α := R) (β := Γ → V →ₗ[R] W) ((RingHom.id R : (a : R) → R) x : R)
            (fun (n : Γ) ↦
              {
                toFun := fun (v : V) ↦
                  HahnSeries.coeff
                    ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W)
                      ((x_1 : (a : V) → HahnModule Γ R W) v))
                    n,
                map_add' := ⋯, map_smul' := ⋯ : V →ₗ[R] W })
            x_2 :
          (a : V) → W)
        x_3 :
      W)

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
A : HVertexOperator Γ R V W
v : V
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support.{u_1, u_4} (M := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((A : (a : V) → HahnModule Γ R W) v))))

Tactic:
((of R).symm (A v)).isPWO_support'

Premises used: HahnSeries.isPWO_support', HahnModule.of, Equiv.symm, DFunLike.coe
-- 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
_ :
  ∀ ⦃a₂ : HVertexOperator Γ R V W⦄,
    Eq (α := Γ → V →ₗ[R] W) ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₁ : Γ → V →ₗ[R] W)
        ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₂ : Γ → V →ₗ[R] W) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : HVertexOperator Γ R V W⦄,
    Eq (α := Γ → V →ₗ[R] W) ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₁ : Γ → V →ₗ[R] W)
        ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₂ : Γ → V →ₗ[R] W) →
      a₁ = a₂

Tactic:
_
-- 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₁ a₂ : HVertexOperator Γ R V W
h :
  Eq (α := Γ → V →ₗ[R] W) ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₁ : Γ → V →ₗ[R] W)
    ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₂ : Γ → V →ₗ[R] W)
h₁ :
  ∀ (v : V) (n : Γ),
    Eq.{u_4 + 1} (α := W)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₁ : (a : V) → HahnModule Γ R W) v)) n)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₂ : (a : V) → HahnModule Γ R W) v)) n)
⊢ a₁ = a₂

Tactic:
ext v n
-- 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₁ a₂ : HVertexOperator Γ R V W
h :
  Eq (α := Γ → V →ₗ[R] W) ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₁ : Γ → V →ₗ[R] W)
    ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₂ : Γ → V →ₗ[R] W)
v : V
n : Γ
⊢ Eq.{u_4 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₁ : (a : V) → HahnModule Γ R W) v)) n)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₂ : (a : V) → HahnModule Γ R W) v)) n)

Tactic:
congrFun (congrArg DFunLike.coe (congrFun h n)) v

Premises used: congrArg, congrFun, DFunLike.coe
-- 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₁ a₂ : HVertexOperator Γ R V W
h :
  Eq (α := Γ → V →ₗ[R] W) ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₁ : Γ → V →ₗ[R] W)
    ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) a₂ : Γ → V →ₗ[R] W)
v : V
n : Γ
⊢ Eq.{u_4 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₁ : (a : V) → HahnModule Γ R W) v)) n)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ R W) → HahnSeries Γ W) ((a₂ : (a : V) → HahnModule Γ R W) v)) n)

Tactic:
exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

Premises used: congrArg, congrFun, DFunLike.coe