awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
change : (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s
⊢ (fun (x : G) ↦ g' • x) y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s

Tactic:
change (zpowGroupHom n)^[j] (g' * y) ∈ s

Premises used: HMul.hMul, Nat.iterate, zpowGroupHom, DFunLike.coe
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1

Tactic:
simpa [zpowGroupHom]

Premises used: zpowGroupHom
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1

Tactic:
replace hg' : (zpowGroupHom n)^[j] g' = 1 := by simpa [zpowGroupHom]
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' = 1
rwa : (⇑(zpowGroupHom n) : (a : G) → G)^[j] g' * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
rwa₁ : 1 * (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : (⇑(zpowGroupHom n) : (a : G) → G)^[j] y ∈ s
⊢ (⇑(zpowGroupHom n) : (a : G) → G)^[j] (g' * y) ∈ s

Tactic:
rwa [iterate_map_mul, hg', one_mul]

Premises used: iterate_map_mul, one_mul
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y

Tactic:
tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, Function.IsFixedPt, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
refine : Tendsto (fun (n : ℕ) ↦ f^[n + 1] x) atTop (𝓝 (f y))
⊢ IsFixedPt f y

Tactic:
refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
simp : Tendsto (fun (n : ℕ) ↦ (f ∘ f^[n]) x) atTop (𝓝 (f y))
⊢ Tendsto (fun (n : ℕ) ↦ f^[n + 1] x) atTop (𝓝 (f y))

Tactic:
simp only [iterate_succ' f]

Premises used: Function.iterate_succ'
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun (n : ℕ) ↦ (f ∘ f^[n]) x) atTop (𝓝 (f y))

Tactic:
hf.tendsto.comp hy

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
x y : α
hy : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun (n : ℕ) ↦ (f ∘ f^[n]) x) atTop (𝓝 (f y))

Tactic:
exact hf.tendsto.comp hy

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Dynamics.FixedPoints.Topology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
f : α → α
hf : Continuous[inst, inst] f
⊢ IsClosed[inst] (fixedPoints f)

Tactic:
isClosed_eq hf continuous_id

Premises used: setOf, Function.fixedPoints, continuous_id, isClosed_eq, Function.IsFixedPt
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
α : Type u_2
inst : Preorder τ
inst_1 : Zero τ
ϕ : τ → α → α
s : Set α
h : IsInvariant ϕ s
⊢ IsForwardInvariant ϕ s

Tactic:
fun t _ht => h t

Premises used: IsForwardInvariant
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
α : Type u_2
inst : AddMonoid τ
inst_1 : PartialOrder τ
inst_2 : CanonicallyOrderedAdd τ
ϕ : τ → α → α
s : Set α
h : IsForwardInvariant ϕ s
⊢ IsInvariant ϕ s

Tactic:
fun _ => h zero_le

Premises used: zero_le, IsInvariant
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
α : Type u_2
inst : AddMonoid τ
inst_1 : PartialOrder τ
inst_2 : CanonicallyOrderedAdd τ
ϕ : τ → α → α
s : Set α
⊢ IsForwardInvariant ϕ s ↔ IsInvariant ϕ s

Tactic:
⟨IsForwardInvariant.isInvariant, IsInvariant.isForwardInvariant⟩

Premises used: IsInvariant.isForwardInvariant, Iff.intro, IsForwardInvariant.isInvariant
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
t : τ
⊢ toFun (Flow.id τ α) t = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
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'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
e_toFun : f₁ = f₂
⊢ Eq (α := Flow τ α) { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' }
    { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 }

Tactic:
congr
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
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'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
e_toFun : ∀ (x : τ) (x_1 : α), f₁ x x_1 = f₂ x x_1
⊢ f₁ = f₂

Tactic:
funext
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
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'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
x : τ
x_1 : α
⊢ f₁ x x_1 = f₂ x x_1

Tactic:
h _ _
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
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'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
x : τ
x_1 : α
⊢ f₁ x x_1 = f₂ x x_1

Tactic:
exact h _ _
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
β : Type u_3
inst_4 : TopologicalSpace β
t : β → τ
ht : Continuous t
f : β → α
hf : Continuous f
⊢ Continuous.{u_3, u_2} (Y := α) fun (x : β) ↦ ϕ.toFun (t x) (f x)

Tactic:
ϕ.cont'.comp (ht.prodMk hf)

Premises used: Flow.cont', Continuous.comp, Continuous.prodMk
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t₁ t₂ : τ
x : α
⊢ ϕ.toFun (t₁ + t₂) x = ϕ.toFun t₁ (ϕ.toFun t₂ x)

Tactic:
ϕ.map_add' _ _ _

Premises used: Flow.map_add'
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
⊢ ϕ.toFun 0 = id

Tactic:
funext ϕ.map_zero'

Premises used: Flow.map_zero', funext
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ ϕ.toFun 0 x = x

Tactic:
ϕ.map_zero' x

Premises used: Flow.map_zero'
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : IsInvariant ϕ.toFun s
⊢ Continuous (Y := α) fun (x : Prod.{u_1, u_2} τ (↑s : Type u_2)) ↦ ϕ.toFun x.1 (↑x.2 : α)

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : IsInvariant ϕ.toFun s
t : τ
x : (↑s : Type u_2)
⊢ (↑((ϕ.restrict (s := s) h).toFun t x) : α) = ϕ.toFun t (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
S : AddSubmonoid τ
t : ↥S
x : α
⊢ (ϕ.restrictAddSubmonoid S).toFun t x = ϕ.toFun (↑t : τ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ ϕ.orbit x = range fun (t : τ) ↦ ϕ.toFun t x

Tactic:
rfl

Premises used: AddAction.orbit, Flow.orbit, rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x₁ x₂ : α
⊢ x₂ ∈ ϕ.orbit x₁ ↔ ∃ (t : τ), ϕ.toFun t x₁ = x₂

Tactic:
Iff.rfl

Premises used: AddAction.orbit, Set.Mem, Iff.rfl, setOf, Flow.orbit, Set.range
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
t : τ
⊢ ϕ.toFun t x ∈ ϕ.orbit x

Tactic:
@AddAction.mem_orbit _ _ ϕ.toAddAction.toVAdd x t

Premises used: Set.Mem, Flow.orbit, AddAction.mem_orbit
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ x ∈ ϕ.orbit x

Tactic:
ϕ.toAddAction.mem_orbit_self x

Premises used: Set.Mem, AddAction.mem_orbit_self, Flow.orbit
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ (ϕ.orbit x).Nonempty

Tactic:
ϕ.toAddAction.nonempty_orbit x

Premises used: AddAction.nonempty_orbit, Flow.orbit
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x₁ x₂ : α
t : τ
h : x₂ ∈ ϕ.orbit x₁
⊢ ϕ.toFun t x₂ ∈ ϕ.orbit x₁

Tactic:
ϕ.toAddAction.mem_orbit_of_mem_orbit t h

Premises used: Set.Mem, Flow.orbit, AddAction.mem_orbit_of_mem_orbit
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ IsInvariant ϕ.toFun (ϕ.orbit x)

Tactic:
fun t _ => ϕ.toAddAction.mem_orbit_of_mem_orbit t

Premises used: Set.Mem, Flow.orbit, Set.MapsTo, AddAction.mem_orbit_of_mem_orbit, IsInvariant
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
hs : IsInvariant ϕ.toFun s
x_1 x : (↑s : Type u_2)
⊢ x ∈ (ϕ.restrict (s := s) hs).orbit x_1 ↔
    Membership.mem (γ := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' ϕ.orbit (↑x_1 : α)) x

Tactic:
simp [orbit_eq_range, Subtype.ext_iff]

Premises used: Flow.orbit_eq_range, Subtype.ext_iff
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
inst_4 : Preorder τ
inst_5 : AddLeftMono τ
x : α
⊢ ϕ.forwardOrbit x = range fun (t : { t : τ // 0 ≤ t }) ↦ ϕ.toFun (↑t : τ) x

Tactic:
rfl

Premises used: AddAction.orbit, Set.Ici, Set.Mem, setOf, Flow.orbit, Flow.forwardOrbit, rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
inst_4 : Preorder τ
inst_5 : AddLeftMono τ
x : α
⊢ IsForwardInvariant ϕ.toFun (ϕ.forwardOrbit x)

Tactic:
fun t h => IsInvariant.isForwardInvariant (isInvariant_orbit ϕ.restrictNonneg x) (t := ⟨t, h⟩) h

Premises used: IsInvariant.isForwardInvariant, Flow.isInvariant_orbit, Flow.restrictNonneg, Flow.forwardOrbit, IsForwardInvariant
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
inst_4 : Preorder τ
inst_5 : AddLeftMono τ
x : α
⊢ ϕ.forwardOrbit x ⊆ ϕ.orbit x

Tactic:
ϕ.toAddAction.orbit_addSubmonoid_subset (AddSubmonoid.nonneg τ) x

Premises used: Flow.orbit, AddAction.orbit_addSubmonoid_subset, Flow.forwardOrbit, AddSubmonoid.nonneg
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
inst_4 : Preorder τ
inst_5 : AddLeftMono τ
x₁ x₂ : α
h : x₁ ∈ ϕ.forwardOrbit x₂
⊢ x₁ ∈ ϕ.orbit x₂

Tactic:
ϕ.forwardOrbit_subset_orbit x₂ h

Premises used: Flow.forwardOrbit_subset_orbit
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
β : Type u_3
γ : Type u_4
inst_4 : TopologicalSpace β
inst_5 : TopologicalSpace γ
ψ : Flow τ β
χ : Flow τ γ
π : α → β
ρ : β → γ
h₁ : IsSemiconjugacy π ϕ ψ
h₂ : IsSemiconjugacy ρ ψ χ
⊢ IsSemiconjugacy (ρ ∘ π) ϕ χ

Tactic:
⟨h₂.cont.comp h₁.cont, h₂.surj.comp h₁.surj, fun t => (h₂.semiconj t).comp_left (h₁.semiconj t)⟩

Premises used: Flow.IsSemiconjugacy.semiconj, Continuous.comp, Flow.IsSemiconjugacy.cont, Flow.IsSemiconjugacy.mk, Function.Semiconj.comp_left, Flow.IsSemiconjugacy.surj, Function.Surjective.comp
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ ψ : Flow τ α
⊢ IsSemiconjugacy id ϕ ψ ↔ ϕ = ψ

Tactic:
⟨fun h => ext h.semiconj, fun h => h.recOn ⟨continuous_id, surjective_id, fun _ => .id_left⟩⟩

Premises used: Flow.IsSemiconjugacy.semiconj, Eq.recOn, Iff.intro, Flow.ext
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
β : Type u_3
inst_4 : TopologicalSpace β
ψ : Flow τ β
π : α → β
h : IsSemiconjugacy π ϕ ψ
⊢ ψ.IsFactorOf ϕ

Tactic:
⟨π, h⟩

Premises used: Flow.IsFactorOf, Exists.intro
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
β : Type u_3
γ : Type u_4
inst_4 : TopologicalSpace β
inst_5 : TopologicalSpace γ
ψ : Flow τ β
χ : Flow τ γ
h₁ : ϕ.IsFactorOf ψ
h₂ : ψ.IsFactorOf χ
⊢ ϕ.IsFactorOf χ

Tactic:
h₁.elim fun π hπ => h₂.elim fun ρ hρ => ⟨π ∘ ρ, hρ.comp χ ψ ϕ hπ⟩

Premises used: Function.comp, Flow.IsSemiconjugacy.comp, Exists.intro, Exists.elim
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
⊢ ϕ = ϕ

Tactic:
rfl
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s ⊆ s
t : τ
x : α
hx : x ∈ s
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x

Tactic:
simp [← map_add]

Premises used: Flow.map_add
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s = s
t : τ
rw rw₁ : s ⊆ s
⊢ ϕ.toFun t '' s ⊆ s

Tactic:
rw [h t]
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x x_1 : τ
x_2 : α
rw : ϕ.toFun (-x + -x_1) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
rw₁ rw₂ : ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2) = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
⊢ ϕ.toFun (-(x + x_1)) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)

Tactic:
rw [neg_add, map_add]

Premises used: neg_add, Flow.map_add
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
rw : ϕ.toFun 0 x = x
rw₁ rw₂ : x = x
⊢ ϕ.toFun (-0) x = x

Tactic:
rw [neg_zero, map_zero_apply]

Premises used: neg_zero, Flow.map_zero_apply
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (ϕ.toFun t)

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (-t + t) x = x
rw₁ : ϕ.toFun 0 x = x
rw₂ rw₃ : x = x
⊢ ϕ.toFun (-t) (ϕ.toFun t x) = x

Tactic:
rw [← map_add, neg_add_cancel, map_zero_apply]

Premises used: Flow.map_add, neg_add_cancel, Flow.map_zero_apply
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (t + -t) x = x
rw₁ : ϕ.toFun 0 x = x
rw₂ rw₃ : x = x
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x

Tactic:
rw [← map_add, add_neg_cancel, map_zero_apply]

Premises used: add_neg_cancel, Flow.map_add, Flow.map_zero_apply
-- Module: Mathlib.Dynamics.Flow
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
s : Set α
⊢ ϕ.toFun t '' s = ϕ.toFun (-t) ⁻¹' s

Tactic:
(ϕ.toHomeomorph t).toEquiv.image_eq_preimage_symm s

Premises used: Homeomorph.toEquiv, Flow.toHomeomorph, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
x : α
⊢ Dense (orbit M x)

Tactic:
MulAction.IsMinimal.dense_orbit x

Premises used: MulAction.IsMinimal.dense_orbit
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
x : α
⊢ DenseRange.{u_3, u_1} (X := α) fun (c : M) ↦ c • x

Tactic:
MulAction.dense_orbit M x

Premises used: MulAction.dense_orbit, MulAction.orbit, DenseRange
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
G : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : Group G
inst_2 : TopologicalSpace α
inst_3 : MulAction M α
inst_4 : MulAction G α
inst_5 : IsPretransitive M α
⊢ IsMinimal M α

Tactic:
⟨fun x ↦ (surjective_smul M x).denseRange⟩

Premises used: Function.Surjective.denseRange, MulAction.surjective_smul, MulAction.IsMinimal.mk
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
x : α
U : Set α
hUo : IsOpen U
hne : U.Nonempty
⊢ ∃ (c : M), c • x ∈ U

Tactic:
(denseRange_smul M x).exists_mem_open hUo hne

Premises used: denseRange_smul, DenseRange.exists_mem_open
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
U : Set α
hUo : IsOpen U
hne : U.Nonempty
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ (c : M), (fun (x : α) ↦ c • x) ⁻¹' U) univ

Tactic:
iUnion_eq_univ_iff.2 fun x ↦ hUo.exists_smul_mem M x hne

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, IsOpen.exists_smul_mem
-- Module: Mathlib.Dynamics.Minimal
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : TopologicalSpace α
inst_2 : MulAction G α
inst_3 : IsMinimal G α
U : Set α
hUo : IsOpen U
hne : U.Nonempty
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ (g : G), g • U) univ

Tactic:
iUnion_eq_univ_iff.2 fun x ↦
    let ⟨g, hg⟩ := hUo.exists_smul_mem G x hne
    ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩

Premises used: Iff.mpr, _private.0.IsOpen.iUnion_smul.match_1, Set.iUnion_eq_univ_iff, Membership.mem, Exists, inv_smul_smul, Inv.inv, And.intro, Exists.intro, HSMul.hSMul, IsOpen.exists_smul_mem
-- Module: Mathlib.Dynamics.Minimal
Goal:
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : TopologicalSpace α
inst_2 : MulAction G α
inst_3 : IsMinimal G α
inst_4 : ContinuousConstSMul G α
K U : Set α
hK : IsCompact K
hUo : IsOpen U
hne : U.Nonempty
⊢ ∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g • U

Tactic:
(hK.elim_finite_subcover (fun g ↦ g • U) fun _ ↦ hUo.smul _) <| calc
    K ⊆ univ := subset_univ K
    _ = ⋃ g : G, g • U := (hUo.iUnion_smul G hne).symm

Premises used: Trans.trans, Set.subset_univ, IsOpen.iUnion_smul, IsOpen.smul, IsCompact.elim_finite_subcover, HSMul.hSMul, Eq.symm
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
s : Set α
hne : s.Nonempty
hsmul : ∀ (c : M), c • s ⊆ s
⊢ Dense s

Tactic:
let ⟨x, hx⟩ := hne
  (MulAction.dense_orbit M x).mono (range_subset_iff.2 fun c ↦ hsmul c ⟨x, hx, rfl⟩)

Premises used: Iff.mpr, Dense, Dense.mono, MulAction.dense_orbit, And.intro, Exists.intro, Set.range_subset_iff, _private.0.dense_of_nonempty_smul_invariant.match_1, rfl
-- Module: Mathlib.Dynamics.Minimal
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : IsMinimal M α
s : Set α
hs : IsClosed s
hsmul : ∀ (c : M), c • s ⊆ s
⊢ s = ∅ ∨ s = univ

Tactic:
s.eq_empty_or_nonempty.imp_right fun hne ↦
    hs.closure_eq ▸ (dense_of_nonempty_smul_invariant M hne hsmul).closure_eq

Premises used: IsClosed.closure_eq, Eq.rec, Dense.closure_eq, Set.eq_empty_or_nonempty, dense_of_nonempty_smul_invariant, Or.imp_right