mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a

Tactic:
simp only [parallel.aux1, rmap, corec_eq]

Goal state after:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inl a
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
this

Goal state after:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ (Pure.pure a).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
⊢ nil.tail = nil

Tactic:
simp [tail]

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).tail = s

Tactic:
simp [tail]

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think.tail = s.tail.think

Tactic:
simp [tail]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.407

Tactic:
simp only [parallel.aux1, rmap, corec_eq]

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?m.407
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : (cons x✝ s✝).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
simp only [destruct_cons, destruct_pure, Sum.inl.injEq, Option.some.injEq,
      Prod.mk.injEq] at this
    obtain ⟨i1, i2⟩ := this
    rw [i1, i2]
    dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]
    have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
    rw [h_a_eq_a']
    refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
    rcases o with e | m
    · rw [e]
      apply Stream'.mem_cons
    · exact Stream'.mem_cons_of_mem _ m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
m : a ∈ nil.tail
e : some (some a) = (↑nil.tail).get 0
⊢ a ∈ nil

Tactic:
simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
m : a ∈ nil.tail
e : some (some a) = (↑nil.tail).get (n✝ + 1)
⊢ a ∈ nil

Tactic:
simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ s✝

Tactic:
simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ s✝

Tactic:
simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
h1 : none ∈ (s.drop 0).destruct
h2 : Prod.fst <$> none = some a
⊢ a ∈ s

Tactic:
injection h2

Goal state after:
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Icc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Icc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ico) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ico) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
b : α
⊢ ∀ (s' : WSeq α),
    (a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
ss

Goal state after:
case h1
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
⊢ (a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioo) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioo) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₁ :: cs₂), i := 0 + c₁ } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₁ :: cs₂), i := 0 + c₁ } = true ↔ c₁ :: cs₁ < c₁ :: cs₂

Tactic:
this

Goal state after:
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₁ :: cs₂), i := 0 + c₁ } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 } = true ↔ c₁ :: cs₁ < c₁ :: cs₂
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
⊢ match
    match
      match
        match
          match parallel.aux2 l with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match
      match parallel.aux2 (List.map (map f) l) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ l S, s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False

Tactic:
this

Goal state after:
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
⊢ match
    match
      match
        match
          match parallel.aux2 l with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match
      match lmap f (rmap (List.map (map f)) (parallel.aux2 l)) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ l S, s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
[

Goal state after:
case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
[

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
[

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
obtain ⟨a', v', h⟩ := exists_eq_cons v

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
[

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + ↑⌈g 0⌉ < f 0 + (g 0 + 1)

Tactic:
gcongr; exact ceil_lt_add_one _

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) =
    dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|

Tactic:
[

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) =
    dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ ↑n) = ↑↑n * τ ↑f

Tactic:
by simp [translationNumber_pow f n]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
⊢ Disjoint s (a • V)

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
⊢ Disjoint s (a • V)
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ ↦ volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))

Tactic:
[

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ ↦ volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
[

Goal state after:
case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop

Tactic:
[

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) volume

Tactic:
this

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (fun y ↦ n • y) volume
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y

Tactic:
rintro x - y - h

Goal state after:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
⊢ x = y
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
hf : HasCompactFixedSupport f
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
exact ⟨closure (fixedPoints f)ᶜ, isClosed_closure, hf, subset_closure⟩

Goal state after:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s

Tactic:
[

Goal state after:
τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty

Tactic:
[

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty

Tactic:
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) ↔
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty

Tactic:
[

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t ↦ ϕ t x

Tactic:
[

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t ↦ ϕ t x
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ MapClusterPt y f fun t ↦ ϕ t x

Tactic:
mapClusterPt_iff_frequently,

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n

Tactic:
[

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n