[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x
[PROOFSTEP]
simp [Equiv.map, id_map]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)
[PROOFSTEP]
simp [Equiv.map]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ (h ∘ g) <$> ↑(eqv α).symm x = h <$> g <$> ↑(eqv α).symm x
[PROOFSTEP]
apply comp_map
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'
[PROOFSTEP]
have : F = Equiv.functor eqv := by
  cases F
  dsimp [Equiv.functor]
  congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]] <;> rfl
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ F = Equiv.functor eqv
[PROOFSTEP]
cases F
[GOAL]
case mk
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := map✝, mapConst := mapConst✝ } = Equiv.functor eqv
[PROOFSTEP]
dsimp [Equiv.functor]
[GOAL]
case mk
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := map✝, mapConst := mapConst✝ } =
    { map := fun {α β} => Equiv.map eqv, mapConst := fun {α β} => Equiv.map eqv ∘ Function.const β }
[PROOFSTEP]
congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]]
[GOAL]
case mk
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := map✝, mapConst := mapConst✝ } =
    { map := fun {α β} => Equiv.map eqv, mapConst := fun {α β} => Equiv.map eqv ∘ Function.const β }
[PROOFSTEP]
congr
[GOAL]
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ map✝ = fun {α β} => Equiv.map eqv
[PROOFSTEP]
ext
[GOAL]
case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ mapConst✝ = fun {α β} => Equiv.map eqv ∘ Function.const β
[PROOFSTEP]
ext
[GOAL]
case mk.e_map.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = Equiv.map eqv x✝¹ x✝
[PROOFSTEP]
dsimp only
[GOAL]
case mk.e_mapConst.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = (fun {α β} => Equiv.map eqv ∘ Function.const β) x✝¹ x✝
[PROOFSTEP]
dsimp only
[GOAL]
case mk.e_map.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = Equiv.map eqv x✝¹ x✝
[PROOFSTEP]
rw [← h₀]
[GOAL]
case mk.e_mapConst.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = (Equiv.map eqv ∘ Function.const x✝²) x✝¹ x✝
[PROOFSTEP]
rw [← h₁]
[GOAL]
case mk.e_map.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
case mk.e_mapConst.h.h.h.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = mapConst x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
this : F = Equiv.functor eqv
⊢ LawfulFunctor t'
[PROOFSTEP]
subst this
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'
[PROOFSTEP]
exact Equiv.lawfulFunctor eqv
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
x : t' α
⊢ Equiv.traverse eqv pure x = x
[PROOFSTEP]
simp [Equiv.traverse]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : α → β
x : t' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)
[PROOFSTEP]
simp [Equiv.traverse, traverse_eq_map_id, functor_norm]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : α → β
x : t' α
⊢ ↑(eqv β) (id.mk (f <$> ↑(eqv α).symm x)) = Equiv.map eqv f x
[PROOFSTEP]
rfl
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
[PROOFSTEP]
simp [Equiv.traverse, comp_traverse, functor_norm]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk (((fun x => ↑(eqv γ) <$> x) ∘ traverse f) <$> traverse g (↑(eqv α).symm x)) =
    Comp.mk (((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) <$> traverse g (↑(eqv α).symm x))
[PROOFSTEP]
congr
[GOAL]
case e_x.e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ (fun x => ↑(eqv γ) <$> x) ∘ traverse f = (fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)
[PROOFSTEP]
ext
[GOAL]
case e_x.e_a.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
x✝ : t β
⊢ ((fun x => ↑(eqv γ) <$> x) ∘ traverse f) x✝ = ((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) x✝
[PROOFSTEP]
simp
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : α → F β
x : t' α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Equiv.traverse eqv f x) =
    Equiv.traverse eqv ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
simp only [Equiv.traverse, functor_norm]
[GOAL]
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
⊢ LawfulTraversable t'
[PROOFSTEP]
refine' { toLawfulFunctor := Equiv.lawfulFunctor' eqv @h₀ @h₁ .. }
[GOAL]
case refine'_1
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
⊢ ∀ {α : Type u} (x : t' α), traverse pure x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t' α),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_3
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
⊢ ∀ {α β : Type u} (f : α → β) (x : t' α), traverse (pure ∘ f) x = id.mk (f <$> x)
[PROOFSTEP]
intros
[GOAL]
case refine'_4
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t' α),
    (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =
      traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ : Type u
x✝ : t' α✝
⊢ traverse pure x✝ = x✝
[PROOFSTEP]
rw [h₂, Equiv.id_traverse]
[GOAL]
case refine'_2
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹⁰ : Traversable t
inst✝⁹ : LawfulTraversable t
F G : Type u → Type u
inst✝⁸ : Applicative F
inst✝⁷ : Applicative G
inst✝⁶ : LawfulApplicative F
inst✝⁵ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)
[PROOFSTEP]
rw [h₂, Equiv.comp_traverse, h₂]
[GOAL]
case refine'_2
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹⁰ : Traversable t
inst✝⁹ : LawfulTraversable t
F G : Type u → Type u
inst✝⁸ : Applicative F
inst✝⁷ : Applicative G
inst✝⁶ : LawfulApplicative F
inst✝⁵ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv f✝ <$> Equiv.traverse eqv g✝ x✝) = Comp.mk (Equiv.traverse eqv f✝ <$> traverse g✝ x✝)
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_x.e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹⁰ : Traversable t
inst✝⁹ : LawfulTraversable t
F G : Type u → Type u
inst✝⁸ : Applicative F
inst✝⁷ : Applicative G
inst✝⁶ : LawfulApplicative F
inst✝⁵ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv g✝ x✝ = traverse g✝ x✝
[PROOFSTEP]
rw [h₂]
[GOAL]
case refine'_3
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t' α✝
⊢ traverse (pure ∘ f✝) x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
rw [h₂, Equiv.traverse_eq_map_id, h₀]
[GOAL]
case refine'_3
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulApplicative F
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t' α✝
⊢ pure (Equiv.map eqv f✝ x✝) = id.mk (Equiv.map eqv f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹⁰ : Traversable t
inst✝⁹ : LawfulTraversable t
F G : Type u → Type u
inst✝⁸ : Applicative F
inst✝⁷ : Applicative G
inst✝⁶ : LawfulApplicative F
inst✝⁵ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t' α✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (traverse f✝ x✝) =
    traverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝) x✝
[PROOFSTEP]
rw [h₂, Equiv.naturality, h₂]


[GOAL]
τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s
[PROOFSTEP]
simp_rw [IsInvariant, mapsTo']
[GOAL]
τ : Type u_1
inst✝³ : AddMonoid τ
inst✝² : TopologicalSpace τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ } t x =
      toFun { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ } t x
⊢ { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ } =
    { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }
[PROOFSTEP]
congr
[GOAL]
case e_toFun
τ : Type u_1
inst✝³ : AddMonoid τ
inst✝² : TopologicalSpace τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ } t x =
      toFun { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ } t x
⊢ f₁ = f₂
[PROOFSTEP]
funext
[GOAL]
case e_toFun.h.h
τ : Type u_1
inst✝³ : AddMonoid τ
inst✝² : TopologicalSpace τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ } t x =
      toFun { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ } t x
x✝¹ : τ
x✝ : α
⊢ f₁ x✝¹ x✝ = f₂ x✝¹ x✝
[PROOFSTEP]
exact h _ _
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), toFun ϕ t '' s ⊆ s
t : τ
x✝ : α
hx : x✝ ∈ s
⊢ toFun ϕ t (toFun ϕ (-t) x✝) = x✝
[PROOFSTEP]
simp [← map_add]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), toFun ϕ t '' s = s
t : τ
⊢ toFun ϕ t '' s ⊆ s
[PROOFSTEP]
rw [h t]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
x✝² x✝¹ : τ
x✝ : α
⊢ (fun t => toFun ϕ (-t)) (x✝² + x✝¹) x✝ = (fun t => toFun ϕ (-t)) x✝² ((fun t => toFun ϕ (-t)) x✝¹ x✝)
[PROOFSTEP]
dsimp
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
x✝² x✝¹ : τ
x✝ : α
⊢ toFun ϕ (-(x✝² + x✝¹)) x✝ = toFun ϕ (-x✝²) (toFun ϕ (-x✝¹) x✝)
[PROOFSTEP]
rw [neg_add, map_add]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
x✝ : α
⊢ (fun t => toFun ϕ (-t)) 0 x✝ = x✝
[PROOFSTEP]
dsimp
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
x✝ : α
⊢ toFun ϕ (-0) x✝ = x✝
[PROOFSTEP]
rw [neg_zero, map_zero_apply]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (toFun ϕ t)
[PROOFSTEP]
rw [← curry_uncurry ϕ.toFun]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (curry (uncurry ϕ.toFun) t)
[PROOFSTEP]
apply continuous_curry
[GOAL]
case h
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (uncurry ϕ.toFun)
[PROOFSTEP]
exact ϕ.cont'
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
⊢ toFun ϕ (-t) (toFun ϕ t x) = x
[PROOFSTEP]
rw [← map_add, neg_add_self, map_zero_apply]
[GOAL]
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
⊢ toFun ϕ t (toFun ϕ (-t) x) = x
[PROOFSTEP]
rw [← map_add, add_neg_self, map_zero_apply]


[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ sinh (dist z w / 2) = dist ↑z ↑w / (2 * sqrt (im z * im w))
[PROOFSTEP]
rw [dist_eq, mul_div_cancel_left (arsinh _) two_ne_zero, sinh_arsinh]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ cosh (dist z w / 2) = dist (↑z) (↑(starRingEnd ℂ) ↑w) / (2 * sqrt (im z * im w))
[PROOFSTEP]
have H₁ : (2 ^ 2 : ℝ) = 4 := by norm_num1
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ 2 ^ 2 = 4
[PROOFSTEP]
norm_num1
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
⊢ cosh (dist z w / 2) = dist (↑z) (↑(starRingEnd ℂ) ↑w) / (2 * sqrt (im z * im w))
[PROOFSTEP]
have H₂ : 0 < z.im * w.im := mul_pos z.im_pos w.im_pos
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
H₂ : 0 < im z * im w
⊢ cosh (dist z w / 2) = dist (↑z) (↑(starRingEnd ℂ) ↑w) / (2 * sqrt (im z * im w))
[PROOFSTEP]
have H₃ : 0 < 2 * sqrt (z.im * w.im) := mul_pos two_pos (sqrt_pos.2 H₂)
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
H₂ : 0 < im z * im w
H₃ : 0 < 2 * sqrt (im z * im w)
⊢ cosh (dist z w / 2) = dist (↑z) (↑(starRingEnd ℂ) ↑w) / (2 * sqrt (im z * im w))
[PROOFSTEP]
rw [← sq_eq_sq (cosh_pos _).le (div_nonneg dist_nonneg H₃.le), cosh_sq', sinh_half_dist, div_pow, div_pow,
  one_add_div (pow_ne_zero 2 H₃.ne'), mul_pow, sq_sqrt H₂.le, H₁]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
H₂ : 0 < im z * im w
H₃ : 0 < 2 * sqrt (im z * im w)
⊢ (4 * (im z * im w) + dist ↑z ↑w ^ 2) / (4 * (im z * im w)) = dist (↑z) (↑(starRingEnd ℂ) ↑w) ^ 2 / (4 * (im z * im w))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
H₂ : 0 < im z * im w
H₃ : 0 < 2 * sqrt (im z * im w)
⊢ 4 * (im z * im w) + dist ↑z ↑w ^ 2 = dist (↑z) (↑(starRingEnd ℂ) ↑w) ^ 2
[PROOFSTEP]
simp only [Complex.dist_eq, Complex.sq_abs, Complex.normSq_sub, Complex.normSq_conj, Complex.conj_conj, Complex.mul_re,
  Complex.conj_re, Complex.conj_im, coe_im]
[GOAL]
case e_a
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H₁ : 2 ^ 2 = 4
H₂ : 0 < im z * im w
H₃ : 0 < 2 * sqrt (im z * im w)
⊢ 4 * (im z * im w) + (↑Complex.normSq ↑z + ↑Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - im z * -im w)) =
    ↑Complex.normSq ↑z + ↑Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - im z * im w)
[PROOFSTEP]
ring
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) (↑(starRingEnd ℂ) ↑w)
[PROOFSTEP]
rw [tanh_eq_sinh_div_cosh, sinh_half_dist, cosh_half_dist, div_div_div_comm, div_self, div_one]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ 2 * sqrt (im z * im w) ≠ 0
[PROOFSTEP]
exact (mul_pos (zero_lt_two' ℝ) (sqrt_pos.2 <| mul_pos z.im_pos w.im_pos)).ne'
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ exp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) (↑(starRingEnd ℂ) ↑w)) / (2 * sqrt (im z * im w))
[PROOFSTEP]
rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * im z * im w)
[PROOFSTEP]
rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
  sq_sqrt (mul_pos z.im_pos w.im_pos).le, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc,
  mul_div_mul_left _ _ (two_ne_zero' ℝ)]
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) (↑(starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) (↑(starRingEnd ℂ) ↑b)) /
      (2 * sqrt (im a * im c) * dist (↑b) (↑(starRingEnd ℂ) ↑b))
[PROOFSTEP]
simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ dist ↑a ↑b * dist (↑b) (↑(starRingEnd ℂ) ↑c) / (2 * sqrt (im a * im b) * (2 * sqrt (im b * im c))) +
      dist (↑a) (↑(starRingEnd ℂ) ↑b) * dist ↑b ↑c / (2 * sqrt (im a * im b) * (2 * sqrt (im b * im c))) =
    (dist ↑a ↑b * dist (↑c) (↑(starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) (↑(starRingEnd ℂ) ↑b)) /
      (2 * sqrt (im a * im c) * dist (↑b) (↑(starRingEnd ℂ) ↑b))
[PROOFSTEP]
rw [← add_div, Complex.dist_self_conj, coe_im, abs_of_pos b.im_pos, mul_comm (dist (b : ℂ) _), dist_comm (b : ℂ),
  Complex.dist_conj_comm, mul_mul_mul_comm, mul_mul_mul_comm _ _ _ b.im]
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑c) (↑(starRingEnd ℂ) ↑b) + dist (↑a) (↑(starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (sqrt (im a * im b) * sqrt (im b * im c))) =
    (dist ↑a ↑b * dist (↑c) (↑(starRingEnd ℂ) ↑b) + dist (↑a) (↑(starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (sqrt (im a * im c) * im b))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ sqrt (im a * im b) * sqrt (im b * im c) = sqrt (im a * im c) * im b
[PROOFSTEP]
rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (sqrt a.im), mul_mul_mul_comm, mul_self_sqrt, mul_comm]
[GOAL]
case e_a.e_a
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ 0 ≤ im b
[PROOFSTEP]
exact (im_pos _).le
[GOAL]
case e_a.e_a.hx
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ 0 ≤ im a
[PROOFSTEP]
exact (im_pos _).le
[GOAL]
case e_a.e_a.hx
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ 0 ≤ im b
[PROOFSTEP]
exact (im_pos _).le
[GOAL]
case e_a.e_a.hx
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ 0 ≤ im a
[PROOFSTEP]
exact (im_pos _).le
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ dist z w = dist w z
[PROOFSTEP]
simp only [dist_eq, dist_comm (z : ℂ), mul_comm]
[GOAL]
z w : ℍ
r R : ℝ
⊢ dist z w ≤ r ↔ dist ↑z ↑w / (2 * sqrt (im z * im w)) ≤ sinh (r / 2)
[PROOFSTEP]
rw [← div_le_div_right (zero_lt_two' ℝ), ← sinh_le_sinh, sinh_half_dist]
[GOAL]
z w : ℍ
r R : ℝ
⊢ dist z w = r ↔ dist ↑z ↑w / (2 * sqrt (im z * im w)) = sinh (r / 2)
[PROOFSTEP]
rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]
[GOAL]
z w : ℍ
r R : ℝ
hr : 0 ≤ r
⊢ dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * im z * im w) = sinh (r / 2) ^ 2
[PROOFSTEP]
rw [dist_eq_iff_eq_sinh, ← sq_eq_sq, div_pow, mul_pow, sq_sqrt, mul_assoc]
[GOAL]
z w : ℍ
r R : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (im z * im w)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (im z * im w)) = sinh (r / 2) ^ 2
[PROOFSTEP]
norm_num
[GOAL]
z w : ℍ
r R : ℝ
hr : 0 ≤ r
⊢ 0 ≤ im z * im w
[PROOFSTEP]
exact (mul_pos z.im_pos w.im_pos).le
[GOAL]
case ha
z w : ℍ
r R : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * sqrt (im z * im w))
[PROOFSTEP]
exact div_nonneg dist_nonneg (mul_nonneg zero_le_two <| sqrt_nonneg _)
[GOAL]
case hb
z w : ℍ
r R : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)
[PROOFSTEP]
exact sinh_nonneg_iff.2 (div_nonneg hr zero_le_two)
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c
[PROOFSTEP]
rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff, div_mul_eq_mul_div]
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) (↑(starRingEnd ℂ) ↑b) / (2 * sqrt (im a * im c)) ≤
    (dist ↑a ↑b * dist (↑c) (↑(starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) (↑(starRingEnd ℂ) ↑b)) /
      (2 * sqrt (im a * im c))
[PROOFSTEP]
exact
  div_le_div_of_le (mul_nonneg zero_le_two (sqrt_nonneg _))
    (EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ)))
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ 0 < dist (↑b) (↑(starRingEnd ℂ) ↑b)
[PROOFSTEP]
rw [dist_comm, dist_pos, Ne.def, Complex.conj_eq_iff_im]
[GOAL]
z w : ℍ
r R : ℝ
a b c : ℍ
⊢ ¬(↑b).im = 0
[PROOFSTEP]
exact b.im_ne_zero
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / sqrt (im z * im w)
[PROOFSTEP]
rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * sqrt (im z * im w))
[PROOFSTEP]
exact div_nonneg dist_nonneg (mul_nonneg zero_le_two (sqrt_nonneg _))
[GOAL]
z✝ w : ℍ
r R : ℝ
z : ℍ
⊢ dist z z = 0
[PROOFSTEP]
rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]
[GOAL]
z w : ℍ
r R : ℝ
x✝¹ x✝ : ℍ
⊢ (fun x y =>
        ↑{
            val :=
              2 *
                arsinh
                  (↑(let src := Complex.abs;
                          {
                            toAddGroupSeminorm :=
                              { toFun := src.toFun, map_zero' := Complex.instNormedAddCommGroupComplex.proof_1,
                                add_le' :=
                                  (_ :
                                    ∀ (x y : ℂ),
                                      MulHom.toFun src.toMulHom (x + y) ≤
                                        MulHom.toFun src.toMulHom x + MulHom.toFun src.toMulHom y),
                                neg' := Complex.instNormedAddCommGroupComplex.proof_2 },
                            eq_zero_of_map_eq_zero' :=
                              Complex.instNormedAddCommGroupComplex.proof_3 }).toAddGroupSeminorm
                      (↑x - ↑y) /
                    (2 * sqrt (im x * im y))),
            property :=
              (_ :
                0 ≤
                  2 *
                    arsinh
                      (↑(let src := Complex.abs;
                              {
                                toAddGroupSeminorm :=
                                  { toFun := src.toFun, map_zero' := Complex.instNormedAddCommGroupComplex.proof_1,
                                    add_le' :=
                                      (_ :
                                        ∀ (x y : ℂ),
                                          MulHom.toFun src.toMulHom (x + y) ≤
                                            MulHom.toFun src.toMulHom x + MulHom.toFun src.toMulHom y),
                                    neg' := Complex.instNormedAddCommGroupComplex.proof_2 },
                                eq_zero_of_map_eq_zero' :=
                                  Complex.instNormedAddCommGroupComplex.proof_3 }).toAddGroupSeminorm
                          (↑x - ↑y) /
                        (2 * sqrt (im x * im y)))) })
      x✝¹ x✝ =
    ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
h : dist z w = 0
⊢ z = w
[PROOFSTEP]
simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_le, ext_iff] using h
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ Real.cosh (dist z w) = ((re z - re w) ^ 2 + im z ^ 2 + im w ^ 2) / (2 * im z * im w)
[PROOFSTEP]
have H : 0 < 2 * z.im * w.im := mul_pos (mul_pos two_pos z.im_pos) w.im_pos
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H : 0 < 2 * im z * im w
⊢ Real.cosh (dist z w) = ((re z - re w) ^ 2 + im z ^ 2 + im w ^ 2) / (2 * im z * im w)
[PROOFSTEP]
field_simp [cosh_dist, Complex.dist_eq, Complex.sq_abs, normSq_apply, H, H.ne']
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
H : 0 < 2 * im z * im w
⊢ 2 * im z * im w + ((re z - re w) * (re z - re w) + (im z - im w) * (im z - im w)) =
    (re z - re w) ^ 2 + im z ^ 2 + im w ^ 2
[PROOFSTEP]
ring
[GOAL]
z✝ w : ℍ
r R : ℝ
z : ℍ
⊢ im (center z 0) = im z
[PROOFSTEP]
rw [center_im, Real.cosh_zero, mul_one]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
⊢ dist ↑z ↑(center w r) ^ 2 = 2 * im z * im w * (Real.cosh (dist z w) - Real.cosh r) + (im w * Real.sinh r) ^ 2
[PROOFSTEP]
have H : 2 * z.im * w.im ≠ 0 := by apply_rules [mul_ne_zero, two_ne_zero, im_ne_zero]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
⊢ 2 * im z * im w ≠ 0
[PROOFSTEP]
apply_rules [mul_ne_zero, two_ne_zero, im_ne_zero]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
H : 2 * im z * im w ≠ 0
⊢ dist ↑z ↑(center w r) ^ 2 = 2 * im z * im w * (Real.cosh (dist z w) - Real.cosh r) + (im w * Real.sinh r) ^ 2
[PROOFSTEP]
simp only [Complex.dist_eq, Complex.sq_abs, normSq_apply, coe_re, coe_im, center_re, center_im, cosh_dist',
  mul_div_cancel' _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ← sq]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
H : 2 * im z * im w ≠ 0
⊢ (re z - re w) ^ 2 + (im z ^ 2 - 2 * im z * (im w * Real.cosh r) + im w ^ 2 * (Real.sinh r ^ 2 + 1)) =
    (re z - re w) ^ 2 + im z ^ 2 + im w ^ 2 - 2 * im z * im w * Real.cosh r + im w ^ 2 * Real.sinh r ^ 2
[PROOFSTEP]
ring
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
⊢ dist ↑z ↑(center w r) = sqrt (2 * im z * im w * (Real.cosh (dist z w) - Real.cosh r) + (im w * Real.sinh r) ^ 2)
[PROOFSTEP]
rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
letI := metricSpaceAux
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
cases' lt_or_le r 0 with hr₀ hr₀
[GOAL]
case inl
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
trans Ordering.gt
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ cmp (dist z w) r = Ordering.gt
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : r < 0
⊢ Ordering.gt = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
exacts [(hr₀.trans_le dist_nonneg).cmp_eq_gt,
  ((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm]
[GOAL]
case inr
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
have hr₀' : 0 ≤ w.im * Real.sinh r := mul_nonneg w.im_pos.le (sinh_nonneg_iff.2 hr₀)
[GOAL]
case inr
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ im w * Real.sinh r
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
have hzw₀ : 0 < 2 * z.im * w.im := mul_pos (mul_pos two_pos z.im_pos) w.im_pos
[GOAL]
case inr
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ im w * Real.sinh r
hzw₀ : 0 < 2 * im z * im w
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(center w r)) (im w * Real.sinh r)
[PROOFSTEP]
simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀, ←
  (@strictMonoOn_pow ℝ _ _ two_pos).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq]
[GOAL]
case inr
z✝ w✝ : ℍ
r✝ R : ℝ
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ im w * Real.sinh r
hzw₀ : 0 < 2 * im z * im w
⊢ cmp (Real.cosh (dist z w)) (Real.cosh r) =
    cmp (2 * im z * im w * (Real.cosh (dist z w) - Real.cosh r) + (im w * Real.sinh r) ^ 2) ((im w * Real.sinh r) ^ 2)
[PROOFSTEP]
rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ dist ↑z ↑(center z r) = im z * (Real.cosh r - 1)
[PROOFSTEP]
rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ |(↑(center z r)).im - (↑z).im| = im z * Real.cosh r - im z
[PROOFSTEP]
exact abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
⊢ dist z w = dist (log (im z)) (log (im w))
[PROOFSTEP]
have h₀ : 0 < z.im / w.im := div_pos z.im_pos w.im_pos
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ dist z w = dist (log (im z)) (log (im w))
[PROOFSTEP]
rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero, sinh_log h₀,
    dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div] <;>
  [skip; exact h]
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ dist z w = dist (log (im z)) (log (im w))
[PROOFSTEP]
rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero, sinh_log h₀,
  dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div]
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ dist (im z) (im w * ((im z / im w + im w / im z) / 2)) = im w * |(im z / im w - im w / im z) / 2|
[PROOFSTEP]
skip
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ (↑z).re = (↑(center w |log (im z / im w)|)).re
[PROOFSTEP]
exact h
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ dist (im z) (im w * ((im z / im w + im w / im z) / 2)) = im w * |(im z / im w - im w / im z) / 2|
[PROOFSTEP]
nth_rw 4 [← abs_of_pos w.im_pos]
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ dist (im z) (im w * ((im z / im w + im w / im z) / 2)) = |im w| * |(im z / im w - im w / im z) / 2|
[PROOFSTEP]
simp only [← _root_.abs_mul, coe_im, Real.dist_eq]
[GOAL]
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ |im z - im w * ((im z / im w + im w / im z) / 2)| = |im w * ((im z / im w - im w / im z) / 2)|
[PROOFSTEP]
congr 1
[GOAL]
case e_a
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ im z - im w * ((im z / im w + im w / im z) / 2) = im w * ((im z / im w - im w / im z) / 2)
[PROOFSTEP]
field_simp [z.im_pos, w.im_pos, z.im_ne_zero, w.im_ne_zero]
[GOAL]
case e_a
z w : ℍ
r R : ℝ
h : re z = re w
h₀ : 0 < im z / im w
⊢ im z * (im w * im z * 2) - im w * (im z * im z + im w * im w) = im w * (im z * im z - im w * im w)
[PROOFSTEP]
ring
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ dist ↑(mk { re := 0, im := im z } (_ : 0 < im z)) ↑(mk { re := 0, im := im w } (_ : 0 < im w)) ≤ dist ↑z ↑w
[PROOFSTEP]
simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_abs (z - w)
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ im z ≤ im w * Real.exp (dist z w)
[PROOFSTEP]
rw [← div_le_iff' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ log (im z) - log (im w) ≤ dist z w
[PROOFSTEP]
exact (le_abs_self _).trans (dist_log_im_le z w)
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ dist ↑z ↑(center w (dist z w)) + dist ↑w ↑(center w (dist z w)) = im w * (Real.exp (dist z w) - 1)
[PROOFSTEP]
rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ im w * (1 - Real.exp (-dist z w)) = dist ↑z ↑(center w (dist z w)) - dist ↑w ↑(center w (dist z w))
[PROOFSTEP]
rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]
[GOAL]
z✝ w✝ : ℍ
r R : ℝ
z w : ℍ
⊢ im w * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    im w * Real.sinh (dist z w) - im w * (Real.cosh (dist z w) - 1)
[PROOFSTEP]
ring
[GOAL]
z w : ℍ
r R : ℝ
⊢ instTopologicalSpaceUpperHalfPlane = UniformSpace.toTopologicalSpace
[PROOFSTEP]
refine' le_antisymm (continuous_id_iff_le.1 _) _
[GOAL]
case refine'_1
z w : ℍ
r R : ℝ
⊢ Continuous id
[PROOFSTEP]
refine' (@continuous_iff_continuous_dist ℍ ℍ metricSpaceAux.toPseudoMetricSpace _ _).2 _
[GOAL]
case refine'_1
z w : ℍ
r R : ℝ
⊢ Continuous fun x => dist (id x.fst) (id x.snd)
[PROOFSTEP]
have : ∀ x : ℍ × ℍ, 2 * Real.sqrt (x.1.im * x.2.im) ≠ 0 := fun x =>
  mul_ne_zero two_ne_zero (Real.sqrt_pos.2 <| mul_pos x.1.im_pos x.2.im_pos).ne'
[GOAL]
case refine'_1
z w : ℍ
r R : ℝ
this : ∀ (x : ℍ × ℍ), 2 * sqrt (im x.fst * im x.snd) ≠ 0
⊢ Continuous fun x => dist (id x.fst) (id x.snd)
[PROOFSTEP]
apply_rules [Continuous.div, Continuous.mul, continuous_const, Continuous.arsinh, Continuous.dist, continuous_coe.comp,
  continuous_fst, continuous_snd, Real.continuous_sqrt.comp, continuous_im.comp]
[GOAL]
case refine'_2
z w : ℍ
r R : ℝ
⊢ UniformSpace.toTopologicalSpace ≤ instTopologicalSpaceUpperHalfPlane
[PROOFSTEP]
letI : MetricSpace ℍ := metricSpaceAux
[GOAL]
case refine'_2
z w : ℍ
r R : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ UniformSpace.toTopologicalSpace ≤ instTopologicalSpaceUpperHalfPlane
[PROOFSTEP]
refine' le_of_nhds_le_nhds fun z => _
[GOAL]
case refine'_2
z✝ w : ℍ
r R : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ 𝓝 z
[PROOFSTEP]
rw [nhds_induced]
[GOAL]
case refine'_2
z✝ w : ℍ
r R : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap Subtype.val (𝓝 ↑z)
[PROOFSTEP]
refine' (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => _
[GOAL]
case refine'_2
z✝ w : ℍ
r R✝ : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
⊢ ∃ i, 0 < i ∧ ball z i ⊆ Subtype.val ⁻¹' ball (↑z) R
[PROOFSTEP]
have h₁ : 1 < R / im z + 1 := lt_add_of_pos_left _ (div_pos hR z.im_pos)
[GOAL]
case refine'_2
z✝ w : ℍ
r R✝ : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / im z + 1
⊢ ∃ i, 0 < i ∧ ball z i ⊆ Subtype.val ⁻¹' ball (↑z) R
[PROOFSTEP]
have h₀ : 0 < R / im z + 1 := one_pos.trans h₁
[GOAL]
case refine'_2
z✝ w : ℍ
r R✝ : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / im z + 1
h₀ : 0 < R / im z + 1
⊢ ∃ i, 0 < i ∧ ball z i ⊆ Subtype.val ⁻¹' ball (↑z) R
[PROOFSTEP]
refine' ⟨log (R / im z + 1), Real.log_pos h₁, _⟩
[GOAL]
case refine'_2
z✝ w : ℍ
r R✝ : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / im z + 1
h₀ : 0 < R / im z + 1
⊢ ball z (log (R / im z + 1)) ⊆ Subtype.val ⁻¹' ball (↑z) R
[PROOFSTEP]
refine' fun w hw => (dist_coe_le w z).trans_lt _
[GOAL]
case refine'_2
z✝ w✝ : ℍ
r R✝ : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / im z + 1
h₀ : 0 < R / im z + 1
w : ℍ
hw : w ∈ ball z (log (R / im z + 1))
⊢ im z * (Real.exp (dist w z) - 1) < R
[PROOFSTEP]
rwa [← lt_div_iff' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀]
[GOAL]
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
h : dist w ↑(center z r) ≤ im z * Real.sinh r
⊢ dist (↑(center z r)) w ≤ im z * Real.sinh r
[PROOFSTEP]
rwa [dist_comm]
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
ext w
[GOAL]
case h
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r → w ∈ closedBall (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mp.intro.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ closedBall z r
⊢ ↑w ∈ closedBall (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
exact dist_le_iff_dist_coe_center_le.1 hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ closedBall (↑(center z r)) (im z * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r
[PROOFSTEP]
intro hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ closedBall (↑(center z r)) (im z * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r
[PROOFSTEP]
lift w to ℍ using im_pos_of_dist_center_le hw
[GOAL]
case h.mpr.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ closedBall (↑(center z r)) (im z * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' closedBall z r
[PROOFSTEP]
exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' ball z r = ball (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
ext w
[GOAL]
case h
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r → w ∈ ball (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mp.intro.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ ↑w ∈ ball (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
exact dist_lt_iff_dist_coe_center_lt.1 hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ ball (↑(center z r)) (im z * Real.sinh r) → w ∈ UpperHalfPlane.coe '' ball z r
[PROOFSTEP]
intro hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ ball (↑(center z r)) (im z * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' ball z r
[PROOFSTEP]
lift w to ℍ using im_pos_of_dist_center_le (ball_subset_closedBall hw)
[GOAL]
case h.mpr.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ ball (↑(center z r)) (im z * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' ball z r
[PROOFSTEP]
exact mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
ext w
[GOAL]
case h
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r → w ∈ sphere (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mp.intro.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ sphere z r
⊢ ↑w ∈ sphere (↑(center z r)) (im z * Real.sinh r)
[PROOFSTEP]
exact dist_eq_iff_dist_coe_center_eq.1 hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(center z r)) (im z * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r
[PROOFSTEP]
intro hw
[GOAL]
case h.mpr
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ sphere (↑(center z r)) (im z * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' sphere z r
[PROOFSTEP]
lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)
[GOAL]
case h.mpr.intro
z✝ w✝ : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ sphere (↑(center z r)) (im z * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' sphere z r
[PROOFSTEP]
exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)
[GOAL]
z w : ℍ
r R : ℝ
⊢ ProperSpace ℍ
[PROOFSTEP]
refine' ⟨fun z r => _⟩
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ IsCompact (closedBall z r)
[PROOFSTEP]
rw [← inducing_subtype_val.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
[GOAL]
z✝ w : ℍ
r✝ R : ℝ
z : ℍ
r : ℝ
⊢ IsCompact (closedBall (↑(center z r)) (im z * Real.sinh r))
[PROOFSTEP]
apply isCompact_closedBall
[GOAL]
z w : ℍ
r R a : ℝ
⊢ Isometry fun y => mk { re := a, im := Real.exp y } (_ : 0 < Real.exp y)
[PROOFSTEP]
refine' Isometry.of_dist_eq fun y₁ y₂ => _
[GOAL]
z w : ℍ
r R a y₁ y₂ : ℝ
⊢ dist (mk { re := a, im := Real.exp y₁ } (_ : 0 < Real.exp y₁))
      (mk { re := a, im := Real.exp y₂ } (_ : 0 < Real.exp y₂)) =
    dist y₁ y₂
[PROOFSTEP]
rw [dist_of_re_eq]
[GOAL]
z w : ℍ
r R a y₁ y₂ : ℝ
⊢ dist (log (im (mk { re := a, im := Real.exp y₁ } (_ : 0 < Real.exp y₁))))
      (log (im (mk { re := a, im := Real.exp y₂ } (_ : 0 < Real.exp y₂)))) =
    dist y₁ y₂
z w : ℍ
r R a y₁ y₂ : ℝ
⊢ re (mk { re := a, im := Real.exp y₁ } (_ : 0 < Real.exp y₁)) =
    re (mk { re := a, im := Real.exp y₂ } (_ : 0 < Real.exp y₂))
[PROOFSTEP]
exacts [congr_arg₂ _ (log_exp _) (log_exp _), rfl]
[GOAL]
z w : ℍ
r R a : ℝ
y₁ y₂ : ℍ
⊢ dist ((fun x x_1 => x +ᵥ x_1) a y₁) ((fun x x_1 => x +ᵥ x_1) a y₂) = dist y₁ y₂
[PROOFSTEP]
simp only [dist_eq, coe_vadd, vadd_im, dist_add_left]
[GOAL]
z w : ℍ
r R : ℝ
a : { x // 0 < x }
⊢ Isometry ((fun x x_1 => x • x_1) a)
[PROOFSTEP]
refine' Isometry.of_dist_eq fun y₁ y₂ => _
[GOAL]
z w : ℍ
r R : ℝ
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist ((fun x x_1 => x • x_1) a y₁) ((fun x x_1 => x • x_1) a y₂) = dist y₁ y₂
[PROOFSTEP]
simp only [dist_eq, coe_pos_real_smul, pos_real_im]
[GOAL]
z w : ℍ
r R : ℝ
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ 2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * sqrt (↑a * im y₁ * (↑a * im y₂)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * sqrt (im y₁ * im y₂)))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_x
z w : ℍ
r R : ℝ
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * sqrt (↑a * im y₁ * (↑a * im y₂))) = dist ↑y₁ ↑y₂ / (2 * sqrt (im y₁ * im y₂))
[PROOFSTEP]
rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs, Real.norm_eq_abs,
  mul_left_comm]
[GOAL]
case e_a.e_x
z w : ℍ
r R : ℝ
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * sqrt (im y₁ * im y₂))) = dist ↑y₁ ↑y₂ / (2 * sqrt (im y₁ * im y₂))
[PROOFSTEP]
exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
⊢ Isometry fun x => g • x
[PROOFSTEP]
have h₀ : Isometry (fun z => ModularGroup.S • z : ℍ → ℍ) :=
  Isometry.of_dist_eq fun y₁ y₂ =>
    by
    have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le
    have h₂ : Complex.abs (y₁ * y₂) ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
    simp only [dist_eq, modular_S_smul, inv_neg, neg_div, div_mul_div_comm, coe_mk, mk_im, div_one, Complex.inv_im,
      Complex.neg_im, coe_im, neg_neg, Complex.normSq_neg, mul_eq_mul_left_iff, Real.arsinh_inj, bit0_eq_zero,
      one_ne_zero, or_false_iff, dist_neg_neg, mul_neg, neg_mul, dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, ←
      AbsoluteValue.map_mul, ← Complex.normSq_mul, Real.sqrt_div h₁, ← Complex.abs_apply, mul_div (2 : ℝ),
      div_div_div_comm, div_self h₂, Complex.norm_eq_abs]
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂
[PROOFSTEP]
have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ im y₁ * im y₂
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂
[PROOFSTEP]
have h₂ : Complex.abs (y₁ * y₂) ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ im y₁ * im y₂
⊢ ↑Complex.abs (↑y₁ * ↑y₂) ≠ 0
[PROOFSTEP]
simp [y₁.ne_zero, y₂.ne_zero]
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ im y₁ * im y₂
h₂ : ↑Complex.abs (↑y₁ * ↑y₂) ≠ 0
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂
[PROOFSTEP]
simp only [dist_eq, modular_S_smul, inv_neg, neg_div, div_mul_div_comm, coe_mk, mk_im, div_one, Complex.inv_im,
  Complex.neg_im, coe_im, neg_neg, Complex.normSq_neg, mul_eq_mul_left_iff, Real.arsinh_inj, bit0_eq_zero, one_ne_zero,
  or_false_iff, dist_neg_neg, mul_neg, neg_mul, dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, ← AbsoluteValue.map_mul, ←
  Complex.normSq_mul, Real.sqrt_div h₁, ← Complex.abs_apply, mul_div (2 : ℝ), div_div_div_comm, div_self h₂,
  Complex.norm_eq_abs]
[GOAL]
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
⊢ Isometry fun x => g • x
[PROOFSTEP]
by_cases hc : g 1 0 = 0
[GOAL]
case pos
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ↑g 1 0 = 0
⊢ Isometry fun x => g • x
[PROOFSTEP]
obtain ⟨u, v, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_eq_zero g hc
[GOAL]
case pos.intro.intro
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ↑g 1 0 = 0
u : { x // 0 < x }
v : ℝ
h : (fun x x_1 => x • x_1) g = (fun z => v +ᵥ z) ∘ fun z => u • z
⊢ Isometry fun x => g • x
[PROOFSTEP]
dsimp only at h
[GOAL]
case pos.intro.intro
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ↑g 1 0 = 0
u : { x // 0 < x }
v : ℝ
h : (fun x => g • x) = (fun z => v +ᵥ z) ∘ fun z => u • z
⊢ Isometry fun x => g • x
[PROOFSTEP]
rw [h]
[GOAL]
case pos.intro.intro
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ↑g 1 0 = 0
u : { x // 0 < x }
v : ℝ
h : (fun x => g • x) = (fun z => v +ᵥ z) ∘ fun z => u • z
⊢ Isometry ((fun z => v +ᵥ z) ∘ fun z => u • z)
[PROOFSTEP]
exact (isometry_real_vadd v).comp (isometry_pos_mul u)
[GOAL]
case neg
z w : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ¬↑g 1 0 = 0
⊢ Isometry fun x => g • x
[PROOFSTEP]
obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc
[GOAL]
case neg.intro.intro.intro
z w✝ : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h :
  (fun x x_1 => x • x_1) g =
    (fun x x_1 => x +ᵥ x_1) w ∘
      (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
⊢ Isometry fun x => g • x
[PROOFSTEP]
dsimp only at h
[GOAL]
case neg.intro.intro.intro
z w✝ : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h : (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
⊢ Isometry fun x => g • x
[PROOFSTEP]
rw [h]
[GOAL]
case neg.intro.intro.intro
z w✝ : ℍ
r R : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z => ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h : (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
⊢ Isometry ((fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x)
[PROOFSTEP]
exact (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)