-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp] lemma card_eq [Fintype α] : card (AddChar α ℂ) = card α

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ n i ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : 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 ((AddChar.mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : 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 ((AddChar.mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
hf : Injective f
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
⊢ NeZero (n i)

Tactic:
have := hn i

Result:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ NeZero (n i)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : 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 ((AddChar.mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

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)

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : 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 ((AddChar.mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
hf : Injective f
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ Fintype.card (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)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ NeZero (n i)

Tactic:
exact ⟨by positivity⟩

Result:
no goals