-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
/-- If a constant function is modular of weight `k`, then either `k = 0`, or the constant is `0`. -/
lemma wt_eq_zero_of_eq_const {f : F} {c : ℂ} (hf : ⇑f = Function.const _ c) :
    k = 0 ∨ c = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
⊢ k = 0 ∨ c = 0

Tactic:
have hI := slash_action_eqn'' f (mem_Gamma_one S) I

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : f (S • UpperHalfPlane.I) = denom (↑S) UpperHalfPlane.I ^ k * f UpperHalfPlane.I
⊢ k = 0 ∨ c = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
h2I2 : c = (2 * Complex.I) ^ k * c
hI : (2 ^ k = 1 ∨ Complex.I ^ k = 0) ∨ c = 0
x✝ : 2 ^ k = 1 ∨ Complex.I ^ k = 0
H : 2 ^ k = 1
⊢ 2 ≠ 1

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : f (S • UpperHalfPlane.I) = denom (↑S) UpperHalfPlane.I ^ k * f UpperHalfPlane.I
⊢ k = 0 ∨ c = 0

Tactic:
have h2I2 := slash_action_eqn'' f (mem_Gamma_one S) ⟨2 * Complex.I, by norm_num⟩

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : f (S • UpperHalfPlane.I) = denom (↑S) UpperHalfPlane.I ^ k * f UpperHalfPlane.I
h2I2 : f (S • ⟨2 * Complex.I, ⋯⟩) = denom ↑S ⟨2 * Complex.I, ⋯⟩ ^ k * f ⟨2 * Complex.I, ⋯⟩
⊢ k = 0 ∨ c = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : f (S • UpperHalfPlane.I) = denom (↑S) UpperHalfPlane.I ^ k * f UpperHalfPlane.I
h2I2 : f (S • ⟨2 * Complex.I, ⋯⟩) = denom ↑S ⟨2 * Complex.I, ⋯⟩ ^ k * f ⟨2 * Complex.I, ⋯⟩
⊢ k = 0 ∨ c = 0

Tactic:
simp only [sl_moeb, hf, Function.const, denom_S, coe_mk_subtype] at hI h2I2

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = (2 * Complex.I) ^ k * c
⊢ k = 0 ∨ c = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = (2 * Complex.I) ^ k * c
⊢ k = 0 ∨ c = 0

Tactic:
nth_rw 1 [h2I2] at hI

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : (2 * Complex.I) ^ k * c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = (2 * Complex.I) ^ k * c
⊢ k = 0 ∨ c = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
h2I2 : c = (2 * Complex.I) ^ k * c
hI : (2 ^ k = 1 ∨ Complex.I ^ k = 0) ∨ c = 0
x✝ : 2 ^ k = 1 ∨ Complex.I ^ k = 0
H : 2 ^ k = 1
⊢ k = 0

Tactic:
rwa [← ofReal_ofNat, ← ofReal_zpow, ← ofReal_one, ofReal_inj,
  zpow_eq_one_iff_right₀ (by norm_num) (by norm_num)] at H

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : f (S • UpperHalfPlane.I) = denom (↑S) UpperHalfPlane.I ^ k * f UpperHalfPlane.I
⊢ 0 < (2 * Complex.I).im

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
h2I2 : c = (2 * Complex.I) ^ k * c
hI : (2 ^ k = 1 ∨ Complex.I ^ k = 0) ∨ c = 0
x✝ : 2 ^ k = 1 ∨ Complex.I ^ k = 0
H : 2 ^ k = 1
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
hI : (2 * Complex.I) ^ k * c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = (2 * Complex.I) ^ k * c
⊢ k = 0 ∨ c = 0

Tactic:
simp only [mul_zpow, coe_I, mul_eq_mul_right_iff, mul_left_eq_self₀] at hI

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
h2I2 : c = (2 * Complex.I) ^ k * c
hI : (2 ^ k = 1 ∨ Complex.I ^ k = 0) ∨ c = 0
⊢ k = 0 ∨ c = 0