Theorem: toCircle_neg (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T : ℝ
x : AddCircle T
⊢ (-x).toCircle = x.toCircle⁻¹
Tactic:
induction x using QuotientAddGroup.induction_on'
State after:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z✝ : ℝ
⊢ (-↑z✝).toCircle = (AddCircle.toCircle ↑z✝)⁻¹

State before:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z✝ : ℝ
⊢ (-↑z✝).toCircle = (AddCircle.toCircle ↑z✝)⁻¹
Tactic:
rw [←AddCircle.coe_neg]
State after:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z✝ : ℝ
⊢ AddCircle.toCircle ↑(-z✝) = (AddCircle.toCircle ↑z✝)⁻¹

State before:
case H
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T✝ : Type
inst✝¹³ : RCLike T✝
inst✝¹² : SMulCommClass ℝ T✝ T✝
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r T z✝ : ℝ
⊢ AddCircle.toCircle ↑(-z✝) = (AddCircle.toCircle ↑z✝)⁻¹
Tactic:
simp only [← AddCircle.coe_neg, AddCircle.toCircle, Function.Periodic.lift_coe, mul_neg,
  expMapCircle_neg]
State after:
no goals