awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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)))
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))
have rw₁ : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf ((fun (i : S) ↦ untrop (f i)) '' Set.univ))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))
have rw₂ : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf ((fun (i : S) ↦ untrop (f i)) '' (↑univ : Set S)))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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)))
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))
have rw₃ : sInf (untrop ∘ f '' (↑univ : Set S)) = sInf ((fun (i : S) ↦ untrop (f i)) '' (↑univ : Set S))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))
have 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)))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
⊢ sSup s = sSup ∅
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ sSup s = sSup ∅
have simp : sSup (untrop '' s) = sSup ∅
Tactic: simp only [sSup, Set.image_empty, trop_inj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ sSup (untrop '' s) = sSup ∅
have hs₁ : ¬BddAbove (untrop '' s)
Tactic: apply csSup_of_not_bddAbove
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ ¬BddAbove (untrop '' s)
have hs₁ : ∀ (hs : BddAbove (untrop '' s)), BddAbove s
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (hypothesis)
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 s
have hs₁ : BddAbove (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
Tactic: change BddAbove (tropOrderIso.symm '' s) at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
⊢ sInf s = sInf ∅
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ sInf s = sInf ∅
have simp : sInf (untrop '' s) = sInf ∅
Tactic: simp only [sInf, Set.image_empty, trop_inj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ sInf (untrop '' s) = sInf ∅
have hs₁ : ¬BddBelow (untrop '' s)
Tactic: apply csInf_of_not_bddBelow
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (goal)
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
⊢ ¬BddBelow (untrop '' s)
have hs₁ : ∀ (hs : BddBelow (untrop '' s)), BddBelow s
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Lattice (hypothesis)
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 s
have hs₁ : BddBelow (α := R) ((⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) '' s)
Tactic: change BddBelow (tropOrderIso.symm '' s) at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ (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 }
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : V →ₗ[R] W })
            x_2 :
          (a : V) → W)
        x_3 :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ (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 }
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : V →ₗ[R] W })
            x_2 :
          (a : V) → W)
        x_3 :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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)
⊢ a₁ = a₂
have 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)
Tactic: ext v n
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ (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)
have 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' := sorry }))
      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' := sorry } :
            HahnModule Γ R W)
          ((of R : (a : HahnSeries Γ W) → HahnModule Γ R W)
              { coeff := fun (g : Γ) ↦ (f g : (a : V) → W) x_1, isPWO_support' := sorry } :
            HahnModule Γ R W)))
      x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ (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)
have 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' := sorry }))
      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' := sorry } :
            HahnModule Γ R W)))
      x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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))
have 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))))
Tactic: refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ 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))))
have 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
Tactic: simp only [coeff_apply_apply, Function.support_subset_iff, ne_eq, Function.mem_support]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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 : Γ
⊢ ((A.compHahnSeries B (u + v)).coeff x).coeff x_1 = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x).coeff x_1
have 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)
Tactic: simp only [compHahnSeries_coeff, map_add, coeff_apply_apply, HahnSeries.coeff_add', Pi.add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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 : Γ
⊢ (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)
have 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
Tactic: rw [← HahnSeries.coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u
have coeff : ∀ (x : Γ') (x_1 : Γ), ((A.compHahnSeries B (r • u)).coeff x).coeff x_1 = ((r • A.compHahnSeries B u).coeff x).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
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 : Γ
⊢ ((A.compHahnSeries B (r • u)).coeff x).coeff x_1 = ((r • A.compHahnSeries B u).coeff x).coeff x_1
have 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)
Tactic: simp only [compHahnSeries_coeff, map_smul, coeff_apply_apply, HahnSeries.coeff_smul]