awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
h₁ :
  Ne (α := ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v :
      ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v' :
      ℂ)
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
use (a / (L (v - v') w)) • w

Premises used: HSub.hSub, HDiv.hDiv, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
h₁ :
  ¬Eq (α := ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
              ((a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                w))) :
        ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
              ((a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                w))) :
        ℂ)
⊢ Ne (α := ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v :
      ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v' :
      ℂ)

Tactic:
simp only [map_sub, LinearMap.sub_apply, char_apply, ne_eq]

Premises used: map_sub, ne_eq, LinearMap.sub_apply, BoundedContinuousFunction.char_apply
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
h₁ :
  ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HAdd.hAdd (α := ℝ) (β := ℝ)
            (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                  ((a /
                      HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                        ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                    w) :
              ℝ)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                ((a /
                    HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                  w) :
              ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
⊢ ¬Eq (α := ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
              ((a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                w))) :
        ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
              ((a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                w))) :
        ℂ)

Tactic:
rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv,
    ← e.map_neg_eq_inv, ← Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]

Premises used: div_eq_one_iff_eq, AddChar.map_neg_eq_inv, AddChar.map_add_eq_mul, OneMemClass.coe_eq_one, Metric.unitSphere.coe_inv, Circle.coe_ne_zero, div_eq_inv_mul, Submonoid.coe_mul
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
h₁ :
  ∀
    (hw :
      HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
          ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
        0),
    ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
        ((e : (a : ℝ) → Circle)
            (-HMul.hMul (β := ℝ)
                  (a /
                    HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) +
              HMul.hMul (β := ℝ)
                (a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) :
          Circle)
        (1 : ↥(Submonoid.unitSphere ℂ))
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HAdd.hAdd (α := ℝ) (β := ℝ)
            (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                  ((a /
                      HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                        ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                    w) :
              ℝ)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                ((a /
                    HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                  w) :
              ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))

Tactic:
simp only [map_sub, LinearMap.sub_apply, LinearMap.zero_apply, AddChar.one_apply,
    map_smul, smul_eq_mul] at ha hw ⊢

Premises used: LinearMap.zero_apply, map_sub, AddChar.one_apply, LinearMap.sub_apply, smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) (1 : Circle)
hw :
  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
    0
h₁ :
  ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹ -
            HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (-HMul.hMul (β := ℝ)
                (a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) +
            HMul.hMul (β := ℝ)
              (a /
                HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
              ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) (1 : Circle)
hw :
  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
    0
h₁ : ¬Eq (α := ↥(Submonoid.unitSphere ℂ)) ((e : (a : ℝ) → Circle) a : Circle) (1 : ↥(Submonoid.unitSphere ℂ))
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹ -
            HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))

Tactic:
field_simp
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) (1 : Circle)
hw :
  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
    0
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ)) ((e : (a : ℝ) → Circle) a : Circle) (1 : ↥(Submonoid.unitSphere ℂ))

Tactic:
assumption
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : Multiplicative W
v : V
⊢ Eq (α := ℂ) ((((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ) w : V →ᵇ ℂ) : (a : V) → ℂ) v : ℂ)
    ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)

Tactic:
simp [charMonoidHom]

Premises used: BoundedContinuousFunction.charMonoidHom
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : AddMonoidAlgebra ℂ W
v : V
simp :
  Eq (α := ℂ)
    ((Finsupp.sum w fun (a : W) (b : ℂ) ↦
            HSMul.hSMul (β := V →ᵇ ℂ) b
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) a) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
⊢ Eq (α := ℂ) ((((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) w : V →ᵇ ℂ) : (a : V) → ℂ) v : ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)

Tactic:
simp only [charAlgHom, AddMonoidAlgebra.lift_apply]

Premises used: BoundedContinuousFunction.charAlgHom, AddMonoidAlgebra.lift_apply
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : AddMonoidAlgebra ℂ W
v : V
rw :
  Eq (α := ℂ)
    ((∑ x ∈ w.support,
            HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) ((w : (a : W) → ℂ) x : ℂ)
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) x) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
h :
  ∀ i ∈ w.support,
    HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) 0
        ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
            ((Multiplicative.ofAdd : (a : W) → Multiplicative W) i) :
          V →ᵇ ℂ) =
      0
⊢ Eq (α := ℂ)
    ((Finsupp.sum w fun (a : W) (b : ℂ) ↦
            HSMul.hSMul (β := V →ᵇ ℂ) b
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) a) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)

Tactic:
rw [Finsupp.sum_of_support_subset w subset_rfl]

Premises used: subset_rfl, Finsupp.sum_of_support_subset
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : AddMonoidAlgebra ℂ W
v : V
simp :
  Eq (α := ℂ)
    (∑ c ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) c : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) c : Multiplicative W))) :
            ℂ) :
          ℂ))
    (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ))
⊢ Eq (α := ℂ)
    ((∑ x ∈ w.support,
            HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) ((w : (a : W) → ℂ) x : ℂ)
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) x) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)

Tactic:
simp only [coe_sum, coe_smul, charMonoidHom_apply, smul_eq_mul, Finset.sum_apply]

Premises used: BoundedContinuousFunction.coe_smul, Finset.sum_apply, BoundedContinuousFunction.coe_sum, smul_eq_mul, BoundedContinuousFunction.charMonoidHom_apply
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : AddMonoidAlgebra ℂ W
v : V
⊢ Eq (α := ℂ)
    (∑ c ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) c : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) c : Multiplicative W))) :
            ℂ) :
          ℂ))
    (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ))

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : AddMonoidAlgebra ℂ W
v : V
⊢ ∀ i ∈ w.support,
    HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) 0
        ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
            ((Multiplicative.ofAdd : (a : W) → Multiplicative W) i) :
          V →ᵇ ℂ) =
      0

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
x : V →ᵇ ℂ
hx : x ∈ (charAlgHom he hL).range
⊢ ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = x

Tactic:
simp only [AlgHom.mem_range] at hx ⊢

Premises used: AlgHom.mem_range
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
x : V →ᵇ ℂ
hx : ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = x
obtain :
  ∀ (y : AddMonoidAlgebra ℂ W),
    ∃ (x : AddMonoidAlgebra ℂ W),
      Eq.{u_1 + 1} (α := V →ᵇ ℂ) ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x : V →ᵇ ℂ)
        (star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ)
⊢ ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = star x

Tactic:
obtain ⟨y, rfl⟩ := hx

Premises used: rfl