-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem periodic_comp_ofComplex [SlashInvariantFormClass F Γ(n) k] :
    Periodic (f ∘ ofComplex) n

Proof state:
case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : ¬0 < w.im
this : (w + ↑n).im ≤ 0
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Tactic:
simp only [comp_apply, ofComplex_apply_of_im_nonpos this,
  ofComplex_apply_of_im_nonpos (not_lt.mp hw)]

Result:
no goals

Proof state:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Tactic:
have : 0 < im (w + n) := by simp only [add_im, natCast_im, add_zero, hw]

Result:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
⊢ Periodic (⇑f ∘ ↑ofComplex) ↑n

Tactic:
intro w

Result:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Proof state:
case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : ¬0 < w.im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Tactic:
have : im (w + n) ≤ 0 := by simpa only [add_im, natCast_im, add_zero, not_lt] using hw

Result:
case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : ¬0 < w.im
this : (w + ↑n).im ≤ 0
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Proof state:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ f ⟨w + ↑n, this⟩ = f ⟨w, hw⟩

Tactic:
convert SlashInvariantForm.vAdd_width_periodic n k 1 f ⟨w, hw⟩ using 2

Result:
case h.e'_2.h.e'_1
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ ⟨w + ↑n, this⟩ = ↑n * ↑1 +ᵥ ⟨w, hw⟩

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Tactic:
by_cases hw : 0 < im w

Result:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : ¬0 < w.im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
⊢ 0 < (w + ↑n).im

Tactic:
simp only [add_im, natCast_im, add_zero, hw]

Result:
no goals

Proof state:
case h.e'_2.h.e'_1
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ ⟨w + ↑n, this⟩ = ↑n * ↑1 +ᵥ ⟨w, hw⟩

Tactic:
simp only [Int.cast_one, mul_one, UpperHalfPlane.ext_iff, coe_mk_subtype, coe_vadd,
  ofReal_natCast, add_comm]

Result:
no goals

Proof state:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ (⇑f ∘ ↑ofComplex) (w + ↑n) = (⇑f ∘ ↑ofComplex) w

Tactic:
simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]

Result:
case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑n).im
⊢ f ⟨w + ↑n, this⟩ = f ⟨w, hw⟩

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝ : SlashInvariantFormClass F Γ(n) k
w : ℂ
hw : ¬0 < w.im
⊢ (w + ↑n).im ≤ 0

Tactic:
simpa only [add_im, natCast_im, add_zero, not_lt] using hw

Result:
no goals