-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_conj (s : ℂ) : Gamma (conj s) = conj (Gamma s)

Proof state:
s : ℂ
this : ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
⊢ Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Gamma s)

Tactic:
simp [Gamma, this]

Result:
no goals

Proof state:
case succ
s : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
⊢ ∀ (s : ℂ), GammaAux (n + 1) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux (n + 1) s)

Tactic:
intro s

Result:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux (n + 1) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux (n + 1) s)

Proof state:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (starRingEnd ℂ) s + 1 = (starRingEnd ℂ) (s + 1)

Tactic:
rw [RingHom.map_add, RingHom.map_one]

Result:
no goals

Proof state:
s : ℂ
n : ℕ
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Tactic:
induction n with
| zero => rw [GammaAux]; exact GammaIntegral_conj
| succ n IH =>
  intro s
  rw [GammaAux]
  dsimp only
  rw [div_eq_mul_inv _ s, RingHom.map_mul, conj_inv, ← div_eq_mul_inv]
  suffices conj s + 1 = conj (s + 1) by rw [this, IH]
  rw [RingHom.map_add, RingHom.map_one]

Result:
no goals

Proof state:
case zero
s : ℂ
⊢ ∀ (s : ℂ), GammaAux 0 ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux 0 s)

Tactic:
rw [GammaAux]

Result:
case zero
s : ℂ
⊢ ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Proof state:
case zero
s : ℂ
⊢ ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Tactic:
exact GammaIntegral_conj

Result:
no goals

Proof state:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1) / s)

Tactic:
rw [div_eq_mul_inv _ s, RingHom.map_mul, conj_inv, ← div_eq_mul_inv]

Result:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1)) / (starRingEnd ℂ) s

Proof state:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux (n + 1) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux (n + 1) s)

Tactic:
rw [GammaAux]

Result:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (fun s => GammaAux n (s + 1) / s) ((starRingEnd ℂ) s) = (starRingEnd ℂ) ((fun s => GammaAux n (s + 1) / s) s)

Proof state:
s : ℂ
⊢ ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Tactic:
intro n

Result:
s : ℂ
n : ℕ
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Proof state:
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
this : (starRingEnd ℂ) s + 1 = (starRingEnd ℂ) (s + 1)
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1)) / (starRingEnd ℂ) s

Tactic:
rw [this, IH]

Result:
no goals

Proof state:
s : ℂ
⊢ Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Gamma s)

Tactic:
suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
  simp [Gamma, this]

Result:
s : ℂ
⊢ ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Proof state:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (fun s => GammaAux n (s + 1) / s) ((starRingEnd ℂ) s) = (starRingEnd ℂ) ((fun s => GammaAux n (s + 1) / s) s)

Tactic:
dsimp only

Result:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1) / s)

Proof state:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1)) / (starRingEnd ℂ) s

Tactic:
suffices conj s + 1 = conj (s + 1) by rw [this, IH]

Result:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (starRingEnd ℂ) s + 1 = (starRingEnd ℂ) (s + 1)