awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace
    (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))) volume
have h : ∀ (x : E),
  𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x =
    (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x : F₂)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
x_1 : E
⊢ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x_1 =
    (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂)
have h : Eq.{u_7 + 1} (α := F₃)
  ((𝓕 (E := 𝓢(E, F₃))
          (((((convolution B : 𝓢(E, F₁) →ₗ[ℂ] 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) f :
                  𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) :
                (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
              g :
            𝓢(E, F₃)) :
        (a : E) → F₃)
      x_1 :
    F₃)
  ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
    F₃)
Tactic: rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
x_1 : E
h :
  Eq.{u_7 + 1} (α := F₃)
    ((𝓕 (E := 𝓢(E, F₃))
            (((((convolution B : 𝓢(E, F₁) →ₗ[ℂ] 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) f :
                    𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) :
                  (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
                g :
              𝓢(E, F₃)) :
          (a : E) → F₃)
        x_1 :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
⊢ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x_1 =
    (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂)
have h₁ : Eq.{u_7 + 1} (α := F₃)
  (((((((pairing B : 𝓢(E, F₁) →ₗ[ℂ] 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) (𝓕 f) :
                𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) :
              (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
            (𝓕 g) :
          𝓢(E, F₃)) :
        (a : E) → F₃)
      x_1 :
    F₃)
  ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
    F₃)
Tactic: rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
x_1 : E
h :
  Eq.{u_7 + 1} (α := F₃)
    ((𝓕 (E := 𝓢(E, F₃))
            (((((convolution B : 𝓢(E, F₁) →ₗ[ℂ] 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) f :
                    𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) :
                  (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
                g :
              𝓢(E, F₃)) :
          (a : E) → F₃)
        x_1 :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
h₁ :
  Eq.{u_7 + 1} (α := F₃)
    (((((((pairing B : 𝓢(E, F₁) →ₗ[ℂ] 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) (𝓕 f) :
                  𝓢(E, F₂) →L[ℂ] 𝓢(E, F₃)) :
                (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
              (𝓕 g) :
            𝓢(E, F₃)) :
          (a : E) → F₃)
        x_1 :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
⊢ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x_1 =
    (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂)
have h₂ : Eq.{u_7 + 1} (α := F₃)
  ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
    F₃)
  ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
    F₃)
Tactic: rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : Fintype G
inst_2 : Semifield R
inst_3 : IsDomain R
inst_4 : CharZero R
ψ : AddChar G R
⊢ Eq.{u_3 + 1} (α := R) (𝔼 x : G, (ψ : (a : G) → R) x) 0 ↔ ψ ≠ 0
have rw : Eq.{u_3 + 1} (α := R) (if ψ = 0 then 1 else 0) 0 ↔ ψ ≠ 0
Tactic: rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : Fintype G
inst_2 : Semifield R
inst_3 : IsDomain R
inst_4 : CharZero R
ψ : AddChar G R
rw : Eq.{u_3 + 1} (α := R) (if ψ = 0 then 1 else 0) 0 ↔ ψ ≠ 0
⊢ Eq.{u_3 + 1} (α := R) (𝔼 x : G, (ψ : (a : G) → R) x) 0 ↔ ψ ≠ 0
have rw₁ : ¬ψ = 0 ↔ ψ ≠ 0
Tactic: rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R))
    (if ψ₁ = ψ₂ then 1 else 0)
have pos : ∀ (h : ψ₁ = ψ₂), Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
pos :
  ∀ (h : ψ₁ = ψ₂),
    Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R))
    (if ψ₁ = ψ₂ then 1 else 0)
have neg : ∀ (h : ¬ψ₁ = ψ₂),
  Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
have pos : Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₂ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
Tactic: rw [h, wInner_cWeight_self]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
pos : Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₂ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1
have pos₁ : Eq.{u_3 + 1} (α := R) 1 1
Tactic: rw [h, wInner_cWeight_self]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ψ₂ * ψ₁⁻¹ ≠ 1
have rwa : ¬ψ₂ * ψ₁⁻¹ = 1
Tactic: rwa [Ne, mul_inv_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
rwa : ¬ψ₂ * ψ₁⁻¹ = 1
⊢ ψ₂ * ψ₁⁻¹ ≠ 1
have rwa₁ : ¬ψ₂ = ψ₁
Tactic: rwa [Ne, mul_inv_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (hypothesis)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0
have this : ψ₂ * ψ₁⁻¹ ≠ 1
Tactic: have : ψ₂ * ψ₁⁻¹ ≠ 1 := by rwa [Ne, mul_inv_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₂ * ψ₁⁻¹ ≠ 1
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0
have neg : Eq.{u_3 + 1} (α := R) (𝔼 i : G, HMul.hMul (α := R) (β := R) ((ψ₂ : (a : G) → R) i : R) (((ψ₁ : (a : G) → R) i)⁻¹ : R)) 0
Tactic: simp_rw [wInner_cWeight_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0 ↔ ψ₁ ≠ ψ₂
have rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 0 ↔ ψ₁ ≠ ψ₂
Tactic: rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 0 ↔ ψ₁ ≠ ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 0 ↔ ψ₁ ≠ ψ₂
have rw₁ : ¬ψ₁ = ψ₂ ↔ ψ₁ ≠ ψ₂
Tactic: rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1 ↔ ψ₁ = ψ₂
have rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 1 ↔ ψ₁ = ψ₂
Tactic: rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
ψ₁ ψ₂ : AddChar G R
inst_2 : Fintype G
rw : Eq.{u_3 + 1} (α := R) (if ψ₁ = ψ₂ then 1 else 0) 1 ↔ ψ₁ = ψ₂
⊢ Eq.{u_3 + 1} (α := R) (wInner (E := fun (a : G) ↦ R) cWeight (⇑ψ₁ : (a : G) → R) (⇑ψ₂ : (a : G) → R)) 1 ↔ ψ₁ = ψ₂
have rw₁ : ψ₁ = ψ₂ ↔ ψ₁ = ψ₂
Tactic: rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality (goal)
Goal:
G : Type u_1
R : Type u_3
inst : AddCommGroup G
inst_1 : RCLike R
inst_2 : Finite G
⊢ LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))
have intro : ∀ (val : Fintype G), LinearIndependent (ι := AddChar G R) R (M := (a : G) → R) (DFunLike.coe (β := fun (x : G) ↦ R))
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Injective (zmod n)
have simp_rw : ∀ (x x_1 : ℤ), zmod n (↑x : ZMod n) = zmod n (↑x_1 : ZMod n) → Eq (α := ZMod n) (↑x : ZMod n) (↑x_1 : ZMod n)
Tactic: simp_rw [Injective, ZMod.intCast_surjective.forall]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x y : ℤ
h : zmod n (↑x : ZMod n) = zmod n (↑y : ZMod n)
⊢ Eq (α := ZMod n) (↑x : ZMod n) (↑y : ZMod n)
have hn : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn : (n : ℝ) ≠ 0 := NeZero.ne _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a_1 b_1 : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
a b : α
⊢ Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
      ((ψ : (a : α) → ℂ) (a + b)) ⋯ =
    HMul.hMul (α := Circle) (β := Circle)
      (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) a) ⋯ :
        ↥(Submonoid.unitSphere ℂ))
      (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
          ((ψ : (a : α) → ℂ) b) ⋯ :
        ↥(Submonoid.unitSphere ℂ))
have a₁ : (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
        ((ψ : (a : α) → ℂ) (a + b)) sorry) :
    ℂ) =
  (↑(HMul.hMul (α := Circle) (β := Circle)
        (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
            ((ψ : (a : α) → ℂ) a) sorry :
          ↥(Submonoid.unitSphere ℂ))
        (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
            ((ψ : (a : α) → ℂ) b) sorry :
          ↥(Submonoid.unitSphere ℂ))) :
    ℂ)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α Circle
⊢ (fun (ψ : AddChar α ℂ) ↦
        ({
            toFun := fun (a : α) ↦
              Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                ((ψ : (a : α) → ℂ) a) ⋯,
            map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
          AddChar α Circle))
      ((fun (ψ : AddChar α Circle) ↦
          ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
            AddChar α ℂ))
        ψ) =
    ψ
have h : ∀ (x : α),
  Eq (α := Circle)
    ((((fun (ψ : AddChar α ℂ) ↦
                ({
                    toFun := fun (a : α) ↦
                      Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                        ((ψ : (a : α) → ℂ) a) sorry,
                    map_zero_eq_one' := sorry, map_add_eq_mul' := sorry } :
                  AddChar α Circle))
              ((fun (ψ : AddChar α Circle) ↦
                  ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ)
                      (coeHom.comp ψ.toMonoidHom) :
                    AddChar α ℂ))
                ψ) :
            AddChar α Circle) :
          (a : α) → Circle)
        x :
      Circle)
    ((ψ : (a : α) → Circle) x : Circle)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n_1 : ℕ
a b : α
n : ℕ
inst_1 : NeZero n
inst_2 : Finite α
ψ : AddChar α ℂ
⊢ (fun (ψ : AddChar α Circle) ↦
        ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
          AddChar α ℂ))
      ((fun (ψ : AddChar α ℂ) ↦
          ({
              toFun := fun (a : α) ↦
                Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                  ((ψ : (a : α) → ℂ) a) ⋯,
              map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
            AddChar α Circle))
        ψ) =
    ψ
have h : ∀ (x : α),
  Eq (α := ℂ)
    (((fun (ψ : AddChar α Circle) ↦
              ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative α →* ℂ) → AddChar α ℂ) (coeHom.comp ψ.toMonoidHom) :
                AddChar α ℂ))
            ((fun (ψ : AddChar α ℂ) ↦
                ({
                    toFun := fun (a : α) ↦
                      Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                        ((ψ : (a : α) → ℂ) a) sorry,
                    map_zero_eq_one' := sorry, map_add_eq_mul' := sorry } :
                  AddChar α Circle))
              ψ) :
          (a : α) → ℂ)
        x :
      ℂ)
    ((ψ : (a : α) → ℂ) x : ℂ)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have obtain : ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (hn : ∀ (i : ι), 1 < n i) (e : α ≃+ ⨁ (i : ι), ZMod (n i)),
  Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
Tactic: obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
⊢ NeZero (n i)
have this : 1 < n i
Tactic: have := hn i
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have hn' : ∀ (i : ι), NeZero (n i)
Tactic: have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ :=
  fun (a : α) ↦
    coeHom.compAddChar
      ((mkZModAux n
            (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
              (a : ι) → ZMod (n a))).compAddMonoidHom
        (↑e : α →+ ⨁ (i : ι), ZMod (n i)))
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have hf : Injective f
Tactic: have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have have : ∀ (i : ι), NeZero (n i)
Tactic: classical
  have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
  have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
have : ∀ (i : ι), NeZero (n i)
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have have₁ : ∀ (hn' : ∀ (i : ι), NeZero (n i)), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
Tactic: classical
  have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
  have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : Fintype α
ι : Type
w : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
have : ∀ (i : ι), NeZero (n i)
have₁ : ∀ (hn' : ∀ (i : ι), NeZero (n i)), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have₂ : ∀ (i : ι), NeZero (n i)
have₃ have₄ have₅ : ∀ (hn' : ∀ (i : ι), NeZero (n i)), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
⊢ Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
have have₆ : ∀ (hn' : ∀ (i : ι), NeZero (n i)),
  let f : α → AddChar α ℂ := fun (a : α) ↦
    coeHom.compAddChar
      ((mkZModAux n
            (⇑((e : (a : α) → ⨁ (i : ι), ZMod (n i)) a : ⨁ (i : ι), ZMod (n i)) :
              (a : ι) → ZMod (n a))).compAddMonoidHom
        (↑e : α →+ ⨁ (i : ι), ZMod (n i)));
  ∀ (hf : Injective f), Fintype.card.{u_1} (AddChar α ℂ) = Fintype.card α
Tactic: classical
  have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
  have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)