mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
x : (P F₂).B b
⊢ f <$> abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩ =
    abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f ⟨⟨b, h⟩, g⟩).fst.snd
          x,
        fun y ↦
        ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).snd
          ⟨x, y⟩⟩

Tactic:
rw [← abs_map]

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
x : (P F₂).B b
⊢ abs ((P F₁).map f ⟨h x, fun y ↦ g ⟨x, y⟩⟩) =
    abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f ⟨⟨b, h⟩, g⟩).fst.snd
          x,
        fun y ↦
        ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).snd
          ⟨x, y⟩⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : SuppPreservation
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Tactic:
suppPreservation_iff_uniform

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
suppPreservation_iff_uniform

Goal state after:
F : Type u → Type u
q : QPF F
⊢ IsUniform ↔ IsUniform
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
T : s.tail.head.Terminates
⊢ s.destruct.Terminates

Tactic:
by
    rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
    simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h
    rcases exists_of_mem_bind h with ⟨s', h1, _⟩
    exact terminates_of_mem h1

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1) (parallel.aux1 (l, S)) = Sum.inl a

Tactic:
parallel.aux1

Goal state after:
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl a
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1) (parallel.aux1 (l, S)) = Sum.inl a

Tactic:
parallel.aux1

Goal state after:
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl a
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
⊢ a ∈ s

Tactic:
have ⟨n, e⟩ := h
  revert s
  induction n <;> intro s m e <;> induction s using WSeq.recOn
  case zero.nil | succ.nil => simpa using m
  case zero.cons | succ.cons => exact WSeq.mem_cons_iff .. |>.mpr <| Or.inr (by simpa using m)
  case zero.think => injections
  case succ.think n IH s =>
    simp only [tail_think, mem_think] at m e ⊢
    apply IH m
    rw [e]
    cases tail s
    rfl

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
l'✝ : List (Computation α)
⊢ (corec parallel.aux1 (l'✝, S.tail)).Terminates

Tactic:
apply IH _ _ _ (Or.inr _) T

Goal state after:
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
l'✝ : List (Computation α)
⊢ some (some c) = S.tail.get? n
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ (parallel S).Terminates

Tactic:
by
  suffices
    ∀ (n) (l : List (Computation α)) (S c),
      c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
    from
    let ⟨n, h⟩ := h
    this n [] S c (Or.inr h) T
  intro n; induction n <;> intro l S c o T
  case zero =>
    rcases o with a | a
    · exact terminates_parallel.aux a T
    have H : Seq.destruct S = some (some c, Seq.tail S) := by simp [Seq.destruct, (· <$> ·), ← a]
    rcases h : parallel.aux2 l with a | l'
    · have C : corec parallel.aux1 (l, S) = pure a := by
        apply destruct_eq_pure
        rw [corec_eq, parallel.aux1]
        rw [h]
        simp only [rmap]
      rw [C]
      infer_instance
    · have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h, H])
      rw [C]
      refine @Computation.think_terminates _ _ ?_
      apply terminates_parallel.aux _ T
      simp
  case succ n IH =>
    rcases o with a | a
    · exact terminates_parallel.aux a T
    rcases h : parallel.aux2 l with a | l'
    · have C : corec parallel.aux1 (l, S) = pure a := by
        apply destruct_eq_pure
        rw [corec_eq, parallel.aux1]
        rw [h]
        simp only [rmap]
      rw [C]
      infer_instance
    · have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h])
      rw [C]
      refine @Computation.think_terminates _ _ ?_
      have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
        intro
        apply IH _ _ _ (Or.inr _) T
        rw [a, Seq.get?_tail]
      rcases e : Seq.get? S 0 with - | o
      · grind [Seq.get?_zero_eq_none, Seq.get?_nil]
      · have D : Seq.destruct S = some (o, S.tail) := by
          dsimp [Seq.destruct]
          rw [e]
          rfl
        rw [D]
        cases o <;> simp [TT]

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd

Tactic:
exact ⟨rfl, h⟩

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd

Tactic:
exact ⟨rfl, h⟩

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ → x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝

Tactic:
· rintro ⟨i, a, b, hab⟩
        rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

Tactic:
constructor
      · rintro ⟨i, a, b, hab⟩
        rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]
      · rintro ⟨⟨i, a, b, hab⟩, h⟩
        rw [mk_le_mk_iff] at h
        exact mk_lt_mk_iff.2 (hab.lt_of_not_ge h)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr.some.some.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dl : d ∈ c :: l'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
simp only [List.mem_cons] at dl
        rcases dl with dc | dl
        · rw [dc] at ad
          refine ⟨c, Or.inr ?_, ad⟩
          rw [Seq.destruct_eq_cons e]
          apply Seq.mem_cons
        · exact
            let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
            ⟨c, Or.inl cl, ac⟩

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

Goal state before:
pp: α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
t : BinaryTree α
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) t = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g t)

Tactic:
by
  induction t with
  | nil => rw [traverse, traverse, map_pure, traverse]; rfl
  | node v l r hl hr =>
    rw [traverse, hl, hr, traverse]
    simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]
    rfl

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

Goal state before:
pp: case nil
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (nil.append (S.append T).join).destruct.destruct (nil.append (S.join.append T.join)).destruct.destruct

Tactic:
induction S using WSeq.recOn with
    | nil =>
      simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
    | cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
    | think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp

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

Goal state before:
pp: case mpr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b

Tactic:
· rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩) <;> exact mem_map_of_mem _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
exact (mapAccumr₂_bisim R h₀ hR).2

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ↑(↑s).toSeq n = ↑s n

Tactic:
dsimp [toSeq]

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).get = s.get? n
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:
by
      simp_rw [transnumAuxSeq, Real.dist_eq]
      rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) ≤ ε / 3

pp: case h₂
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤ ε / 3

Tactic:
· rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]

Goal state after:
case h₂
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤ ε / 3
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n ↦ ((f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))

Tactic:
← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n ↦ ((f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x)))))
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
⊢ Ergodic f volume

Tactic:
suffices e ∘ f ∘ e.symm = fun y => n • y by
    rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h

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
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
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 : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
intro h _ hn _ hu

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
⊢ ∃ x ∈ U✝, (s ∩ ϕ x ⁻¹' n✝).Nonempty
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ IsClosed[Pi.topologicalSpace] {x | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}

Tactic:
have h_eq : {x | ∀ p ∈ F, ∀ v : G, ¬ p.mulOccursInAt x v}
    = ⋂ (p : Pattern A G) (hp : p ∈ F) (v : G), {x | ¬ p.mulOccursInAt x v} := by ext; simp

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
⊢ IsClosed[Pi.topologicalSpace] {x | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
⊢ ∃ i, ∃ (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U

Tactic:
by use k, lt_of_lt_of_le k_m m_n

Goal state after: