[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]
