awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
simp [HahnSeries.ofIterate]

Premises used: HahnSeries.ofIterate
-- 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
r : R
x : 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 (r • x)).ofIterate))
        g)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
          (HSMul.hSMul (α := R) (β := HahnModule (Lex (Γ' × Γ)) R W) ((RingHom.id R : (a : R) → R) r : R)
            ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
                (A.compHahnSeries B x).ofIterate :
              HahnModule (Lex (Γ' × Γ)) R W)))
        g)
⊢ (of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B (r • x)).ofIterate =
    HSMul.hSMul (α := R) (β := HahnModule (Lex (Γ' × Γ)) R W) ((RingHom.id R : (a : R) → R) r : R)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B x).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)

Tactic:
ext g
-- 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
r : R
x : U
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 (r • x)).ofIterate))
      g)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
        (HSMul.hSMul (α := R) (β := HahnModule (Lex (Γ' × Γ)) R W) ((RingHom.id R : (a : R) → R) r : R)
          ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B x).ofIterate :
            HahnModule (Lex (Γ' × Γ)) R W)))
      g)

Tactic:
simp [HahnSeries.ofIterate]

Premises used: HahnSeries.ofIterate
-- 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
g : Lex (Γ' × Γ)
⊢ Eq (α := U →ₗ[R] W)
    ((coeff : (a : HVertexOperator (Lex (Γ' × Γ)) R U W) → Lex (Γ' × Γ) → U →ₗ[R] W) (A.comp B) g : U →ₗ[R] W)
    ((coeff : (a : HVertexOperator Γ R V W) → Γ → V →ₗ[R] W) A ((ofLex : (a : Lex (Γ' × Γ)) → Γ' × Γ) g).2 ∘ₗ
        (coeff : (a : HVertexOperator Γ' R U V) → Γ' → U →ₗ[R] V) B ((ofLex : (a : Lex (Γ' × Γ)) → Γ' × Γ) g).1 :
      U →ₗ[R] W)

Tactic:
rfl
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A B : VertexOperator R V
h :
  ∀ (v : V),
    Eq (α := HahnModule ℤ R V) ((A : (a : V) → HahnModule ℤ R V) v : HahnModule ℤ R V)
      ((B : (a : V) → HahnModule ℤ R V) v : HahnModule ℤ R V)
⊢ A = B

Tactic:
LinearMap.ext h

Premises used: LinearMap.ext
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x x_1 : VertexOperator R V
h :
  ∀ (x_2 : ℤ) (x_3 : V),
    Eq (α := V)
      ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x + x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 :
        V)
      ((HAdd.hAdd (α := ℤ → Module.End R V) (β := ℤ → Module.End R V)
              (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x (-n - 1))
              (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
            (a : V) → V)
          x_3 :
        V)
⊢ (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x + x_1) (-n - 1)) =
    HAdd.hAdd (α := ℤ → Module.End R V)
      (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x (-n - 1)) fun (n : ℤ) ↦
      (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x x_1 : VertexOperator R V
x_2 : ℤ
x_3 : V
⊢ Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x + x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 : V)
    ((HAdd.hAdd (α := ℤ → Module.End R V) (β := ℤ → Module.End R V)
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x (-n - 1))
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
          (a : V) → V)
        x_3 :
      V)

Tactic:
simp
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x : R
x_1 : VertexOperator R V
h :
  ∀ (x_2 : ℤ) (x_3 : V),
    Eq (α := V)
      ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x • x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 :
        V)
      ((HSMul.hSMul (α := R) (β := ℤ → Module.End R V) ((RingHom.id R : (a : R) → R) x : R)
              (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
            (a : V) → V)
          x_3 :
        V)
⊢ (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x • x_1) (-n - 1)) =
    HSMul.hSMul (α := R) (β := ℤ → Module.End R V) ((RingHom.id R : (a : R) → R) x : R) fun (n : ℤ) ↦
      (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x : R
x_1 : VertexOperator R V
x_2 : ℤ
x_3 : V
⊢ Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x • x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 : V)
    ((HSMul.hSMul (α := R) (β := ℤ → Module.End R V) ((RingHom.id R : (a : R) → R) x : R)
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
          (a : V) → V)
        x_3 :
      V)

Tactic:
simp
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
⊢ Eq (α := Module.End R V) ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A n : Module.End R V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-n - 1) : V →ₗ[R] V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
rw :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-(-n - 1) - 1) : V →ₗ[R] V)
rw₁ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 - -n - 1) : V →ₗ[R] V)
rw₂ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 + n - 1) : V →ₗ[R] V)
rw₃ rw₄ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
⊢ Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A (-n - 1) : Module.End R V)

Tactic:
rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]

Premises used: neg_sub, add_sub_cancel_left, VertexOperator.ncoeff_apply, Int.sub_neg
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  -n - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
simp :
  Eq.{u_2 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
      (-n - 1))
    0
⊢ Eq (α := V) ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A n : Module.End R V) : (a : V) → V) x : V)
    (0 : V)

Tactic:
simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, VertexOperator.ncoeff, HVertexOperator.coeff, AddHom.coe_mk
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  -n - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ Eq.{u_2 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
      (-n - 1))
    0

Tactic:
HahnSeries.coeff_eq_zero_of_lt_order h

Premises used: HahnSeries.coeff_eq_zero_of_lt_order
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  -n - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ Eq.{u_2 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
      (-n - 1))
    0

Tactic:
exact HahnSeries.coeff_eq_zero_of_lt_order h

Premises used: HahnSeries.coeff_eq_zero_of_lt_order
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  n <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
rw :
  -(-n - 1) - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ Eq (α := V) ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V) : (a : V) → V) x : V) (0 : V)

Tactic:
rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]

Premises used: HSub.hSub, VertexOperator.ncoeff_eq_zero_of_lt_order, OfNat.ofNat, VertexOperator.coeff_eq_ncoeff, Neg.neg
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  n <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ -(-n - 1) - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))

Tactic:
lia
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
x : V
n : ℤ
⊢ Eq (α := V)
    (HahnSeries.coeff
        ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V)
          ((of_coeff f hf : (a : V) → HahnModule ℤ R V) x))
        n :
      V)
    ((f n : (a : V) → V) x : V)

Tactic:
rfl
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
h :
  ∀ (v : V),
    Eq (α := V)
      ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
        V)
      ((f (-n - 1) : (a : V) → V) v : V)
⊢ (ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n = f (-n - 1)

Tactic:
ext v
-- Module: Mathlib.Algebra.Vertex.VertexOperator
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
v : V
h :
  Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (of_coeff f hf) (-n - 1) : V →ₗ[R] V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
h₁ :
  Eq (α := V)
    (HahnSeries.coeff
        ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V)
          ((of_coeff f hf : (a : V) → HahnModule ℤ R V) v))
        (-n - 1) :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
h₂ h₃ : Eq (α := V) ((f (-n - 1) : (a : V) → V) v : V) ((f (-n - 1) : (a : V) → V) v : V)
⊢ Eq (α := V)
    ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)

Tactic:
rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]

Premises used: VertexOperator.of_coeff_apply_coeff, VertexOperator.ncoeff_apply, HVertexOperator.coeff_apply_apply
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
x : A
⊢ (toConv x).ofConv = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
x : WithConv A
⊢ toConv x.ofConv = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := WithConv A) ofConv

Tactic:
Function.RightInverse.surjective ofConv_toConv

Premises used: WithConv.ofConv_toConv, Function.RightInverse.surjective
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := A) toConv

Tactic:
Function.RightInverse.surjective toConv_ofConv

Premises used: WithConv.toConv_ofConv, Function.RightInverse.surjective
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := WithConv A) ofConv

Tactic:
Function.LeftInverse.injective toConv_ofConv

Premises used: Function.LeftInverse.injective, WithConv.toConv_ofConv
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := A) toConv

Tactic:
Function.LeftInverse.injective ofConv_toConv

Premises used: Function.LeftInverse.injective, WithConv.ofConv_toConv
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Bijective.{u_2 + 1, u_2 + 1} (α := WithConv A) ofConv

Tactic:
⟨ofConv_injective, ofConv_surjective⟩

Premises used: WithConv.ofConv_surjective, WithConv.ofConv_injective, And.intro, Function.Bijective
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
⊢ Function.Bijective.{u_2 + 1, u_2 + 1} (α := A) toConv

Tactic:
⟨toConv_injective, toConv_surjective⟩

Premises used: And.intro, Function.Bijective, WithConv.toConv_injective, WithConv.toConv_surjective
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
x y : WithConv A
h : x.ofConv = y.ofConv
⊢ x = y

Tactic:
ofConv_injective h

Premises used: WithConv.ofConv_injective
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
x : WithConv A
⊢ (WithConv.equiv A : (a : WithConv A) → A) x = x.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
x : A
⊢ ((WithConv.equiv A).symm : (a : A) → WithConv A) x = toConv x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Nontrivial A
⊢ Nontrivial.{u_2} (WithConv A)

Tactic:
(WithConv.equiv A).nontrivial

Premises used: Equiv.nontrivial, WithConv.equiv
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
B : Type u_3
f : A ≃ B
x : WithConv A
⊢ Eq.{u_3 + 1} (α := WithConv B) ((WithConv.congr f : (a : WithConv A) → WithConv B) x : WithConv B)
    (toConv ((f : (a : A) → B) x.ofConv) : WithConv B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
B : Type u_3
f : A ≃ B
⊢ (WithConv.congr f).symm = WithConv.congr f.symm

Tactic:
rfl

Premises used: Equiv.trans, WithConv.congr, Equiv.symm, rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
B : Type u_3
f : A ≃ B
x : WithConv B
⊢ Eq.{u_2 + 1} (α := WithConv A) (((WithConv.congr f).symm : (a : WithConv B) → WithConv A) x : WithConv A)
    (toConv ((f.symm : (a : B) → A) x.ofConv) : WithConv A)

Tactic:
simp
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddGroup A
x y : A
⊢ toConv (x - y) = toConv x - toConv y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddGroup A
x y : WithConv A
⊢ (x - y).ofConv = x.ofConv - y.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddGroup A
x : WithConv A
⊢ (-x).ofConv = -x.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddGroup A
x : A
⊢ toConv (-x) = -toConv x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : MulAction R A
c : R
x : WithConv A
⊢ (c • x).ofConv = c • x.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : MulAction R A
c : R
x : A
⊢ toConv (c • x) = c • toConv x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
⊢ Eq.{u_2 + 1} (α := A) (ofConv 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
⊢ Eq.{u_2 + 1} (α := WithConv A) (toConv 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
x y : WithConv A
⊢ (x + y).ofConv = x.ofConv + y.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
x y : A
⊢ toConv (x + y) = toConv x + toConv y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
x : WithConv A
⊢ x.ofConv = 0 ↔ x = 0

Tactic:
ofConv_injective.eq_iff

Premises used: WithConv.ofConv_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ toConv x = 0 ↔ x = 0

Tactic:
toConv_injective.eq_iff

Premises used: Function.Injective.eq_iff, WithConv.toConv_injective
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : AddMonoid A
⊢ ∀ (x y : WithConv A), (WithConv.equiv A).toFun (x + y) = (WithConv.equiv A).toFun x + (WithConv.equiv A).toFun y

Tactic:
simp
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddMonoid A
⊢ (↑(WithConv.addEquiv A) : WithConv A ≃ A) = WithConv.equiv A

Tactic:
rfl

Premises used: WithConv.equiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
⊢ ∀ (m : R) (x : WithConv A),
    (AddEquiv.toEquiv (WithConv.addEquiv A)).toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) ((AddEquiv.toEquiv (WithConv.addEquiv A)).toFun x)

Tactic:
simp
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
a : WithConv A
⊢ (WithConv.linearEquiv R A : (a : WithConv A) → A) a = a.ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
a : A
⊢ (LinearEquiv.symm (WithConv.linearEquiv R A) : (a : A) → WithConv A) a = toConv a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
⊢ Eq (α := WithConv A ≃+ A) (LinearEquiv.toAddEquiv (WithConv.linearEquiv R A)) (WithConv.addEquiv A)

Tactic:
rfl

Premises used: WithConv.addEquiv, WithConv.equiv, rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
ι : Type u_5
s : Finset ι
f : ι → WithConv A
⊢ Eq.{u_2 + 1} (α := A) (ofConv (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).ofConv)

Tactic:
map_sum (WithConv.addEquiv _) _ _

Premises used: WithConv.addEquiv, map_sum
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
ι : Type u_5
s : Finset ι
f : ι → A
⊢ Eq.{u_2 + 1} (α := WithConv A) (toConv (∑ i ∈ s, f i)) (∑ i ∈ s, toConv (f i))

Tactic:
map_sum (WithConv.addEquiv _).symm _ _

Premises used: WithConv.addEquiv, map_sum, AddEquiv.symm
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
l : List (WithConv A)
⊢ l.sum.ofConv = (List.map ofConv l).sum

Tactic:
map_list_sum (WithConv.addEquiv _) _

Premises used: WithConv.addEquiv, map_list_sum
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
l : List A
⊢ toConv l.sum = (List.map toConv l).sum

Tactic:
map_list_sum (WithConv.addEquiv _).symm _

Premises used: WithConv.addEquiv, map_list_sum, AddEquiv.symm