mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁)
        (by
          intro c
          apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
          clear c
          intro c d
          apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
          clear d
          intro d rcd; apply Quot.sound; apply rcd)

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
⊢ id <$> x = x

Tactic:
by
  rw [← abs_repr x]
  obtain ⟨a, f⟩ := repr x
  rw [← abs_map]
  rfl

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

Goal state before:
pp: case none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
val✝ : α × WSeq α
hb : some val✝ ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
· cases t1

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

Goal state before:
pp: case some.none.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

pp: case some.none.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

Tactic:
· cases t1

Goal state after:
case some.none.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

pp: case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
· cases t1

Goal state after:
case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
intro a b ma mb
      rcases a with - | a <;> rcases b with - | b
      · trivial
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · obtain ⟨a, s'⟩ := a
        obtain ⟨b, t'⟩ := b
        injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab
        refine ⟨ab, fun n => ?_⟩
        refine
          (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
            ((?_ : get? (tail s) n ~ get? (tail t) n).trans
              (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
        rw [get?_tail, get?_tail]
        apply h

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

Goal state before:
pp: case some.none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) none)

Tactic:
cases a; cases h

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

Goal state before:
pp: case some.none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 none)

Tactic:
cases a; cases h

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

Goal state before:
pp: s₁ s₂ : String
⊢ s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList

Tactic:
String.le_iff_not_lt,

Goal state after:
s₁ s₂ : String
⊢ ¬s₂ < s₁ ↔ s₁.toList ≤ s₂.toList
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (destruct_append.aux S.join none) (destruct_append.aux T.join none)

Tactic:
dsimp only [destruct_append.aux, Computation.LiftRel]; constructor
        · intro
          apply liftRel_join.lem _ ST fun _ _ => id
        · intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : BinaryTree α
⊢ traverse (pure ∘ f) t = pure (map f t)

Tactic:
by
  induction t with
  | nil => rw [traverse, map]
  | node v l r hl hr =>
    rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S

Tactic:
by
  have := terminates_of_mem ac
  have := terminates_parallel cs
  exact mem_of_promises _ (parallel_promises H)

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)

Tactic:
by
  induction xs <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ xs) = map (fun x ↦ f₁ (f₂ x)) xs

Tactic:
by
  induction xs <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ xs.toList → p x
⊢ map f₁ (pmap f₂ xs H) = pmap (fun x hx ↦ f₁ (f₂ x hx)) xs H

Tactic:
by
  induction xs <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x
⊢ pmap f₁ (map f₂ xs) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) xs ⋯

Tactic:
by
  induction xs <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

Tactic:
by
  refine v.recOn ?_ ?_
  · exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
  · simp only [vectorAllP_cons]
    refine fun {n} a v IH =>
      (and_congr_right fun _ => IH).trans
        ⟨fun ⟨pa, h⟩ i => by
          refine i.cases' ?_ ?_
          exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩
    · simpa using h fz
    · simpa using h (fs i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Icc a₁ a₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ico a₁ a₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioc a₁ a₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioo a₁ a₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Icc b₁ b₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ico b₁ b₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioc b₁ b₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioo b₁ b₂)

Tactic:
← Finset.map_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s ≤ᵐ[μ] s
h_fin : μ s ≠ ∞
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_
  refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin
  exact hs.preimage hf.quasiMeasurePreserving

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s

Tactic:
by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs b).mem_iff
    · exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mp
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ ↑(AddSubgroup.closure {a, b}) ⊆ range fun x ↦ x • (b / ↑r.den)

Tactic:
rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]

Goal state after:
case inr.mp
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (a ∈ range fun x ↦ x • (b / ↑r.den)) ∧ b ∈ range fun x ↦ x • (b / ↑r.den)
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : 0 ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 0}
⊢ Ergodic f μ

pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ

Tactic:
· convert! zero_measure hf.measurable
    rw [← measure_univ_eq_zero, h.1.2]

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

Tactic:
exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
⊢ ∃ x ∈ U✝, (s ∩ ϕ x ⁻¹' n✝).Nonempty

Tactic:
rcases h _ hu _ hn with ⟨_, _, _, ht, _, hx, rfl⟩

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝¹ : τ
ht : w✝¹ ∈ U✝
w✝ : α
hx : w✝ ∈ s
left✝ : ϕ w✝¹ w✝ ∈ n✝
⊢ ∃ x ∈ U✝, (s ∩ ϕ x ⁻¹' n✝).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
x y : X
⊢ y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U

Tactic:
by
  simp only [ball, mem_preimage, mem_dynEntourage]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ map φ φ ⁻¹' dynEntourage T U n = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
dynEntourage,

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ map φ φ ⁻¹' ⋂ k, ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = sSup (WithTop.some ∘ Finset.card '' {s | IsDynNetIn T F U n ↑s})

Tactic:
sSup_image

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = ⨆ a ∈ {s | IsDynNetIn T F U n ↑s}, (WithTop.some ∘ Finset.card) a