-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
/-- Formulation of reflection formula tailored to functional equations of L-functions of odd
Dirichlet characters. -/
lemma inv_Gammaℝ_two_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
    (Gammaℝ (2 - s))⁻¹ = Gammaℂ s * sin (π * s / 2) * (Gammaℝ (s + 1))⁻¹

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
n : ℕ
⊢ s - 1 ≠ -↑n

Tactic:
rcases n with - | m

Result:
case zero
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
⊢ s - 1 ≠ -↑0

case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ s - 1 ≠ -↑(m + 1)

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * (A * ((s - 1) / 2 / ↑π)⁻¹)

Tactic:
field_simp [pi_ne_zero]

Result:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * A * (2 * ↑π * (s - 1)) =
    (s - 1).Gammaℂ * (s - 1) * sin (↑π * s / 2) * (A * (2 * ↑π))

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
rw [(by ring : 2 - s = 1 - (s - 1)), inv_Gammaℝ_one_sub h',
  (by rw [sub_add_cancel] : Gammaℂ s = Gammaℂ (s - 1 + 1)), Gammaℂ_add_one h,
  (by ring : s + 1 = (s - 1) + 2), Gammaℝ_add_two h, mul_sub, sub_div, mul_one,
    Complex.cos_sub_pi_div_two]

Result:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Proof state:
case h.e'_1.h.e'_3
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m

Tactic:
ring

Result:
no goals

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * A * (2 * ↑π * (s - 1)) =
    (s - 1).Gammaℂ * (s - 1) * sin (↑π * s / 2) * (A * (2 * ↑π))

Tactic:
ring

Result:
no goals

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / ↑π)⁻¹)

Tactic:
generalize (Gammaℝ (s - 1))⁻¹ = A

Result:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * (A * ((s - 1) / 2 / ↑π)⁻¹)

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹

Tactic:
simp_rw [mul_div_assoc, mul_inv]

Result:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / ↑π)⁻¹)

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 2 - 1 = 1

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_1.h.e'_3
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -↑(m + 1) + 1 = -↑m

Tactic:
push_cast

Result:
case h.e'_1.h.e'_3
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (1 + 1) / 2 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ ¬s = -↑(m + 1) + 1

Tactic:
convert hs m using 2

Result:
case h.e'_1.h.e'_3
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -↑(m + 1) + 1 = -↑m

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s + 1 = s - 1 + 2

Tactic:
ring

Result:
no goals

Proof state:
case zero
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
⊢ s - 1 ≠ -↑0

Tactic:
rwa [Nat.cast_zero, neg_zero]

Result:
no goals

Proof state:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
neg_div, (by norm_num : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
by_cases h : s = 1

Result:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Proof state:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
rw [← Ne, ← sub_ne_zero] at h

Result:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ 2 - s = 1 - (s - 1)

Tactic:
ring

Result:
no goals

Proof state:
case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ s - 1 ≠ -↑(m + 1)

Tactic:
rw [Ne, sub_eq_iff_eq_add]

Result:
case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ ¬s = -↑(m + 1) + 1

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s.Gammaℂ = (s - 1 + 1).Gammaℂ

Tactic:
rw [sub_add_cancel]

Result:
no goals