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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x

Tactic:
rw [h]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: fun x ↦ x) <$$> x) = mk x
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
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> x.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
rw [h]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 ≤ sign 0 * 0

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
· rw [mul_zero]

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
TypeVec.id_comp

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ (fun i x ↦ subtypeVal α.repeatEq i (diagSub i x)) = prod.diag
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ Liftp (fun x_1 ↦ x_1 ∈ supp x) x

Tactic:
rw [h]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ ∀ u ∈ supp x, u ∈ supp x
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr
α : 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

Tactic:
obtain ⟨a', e⟩ := IH m
      simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
      rw [e]
      exact ⟨a', rfl⟩

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
n₁ : ℕ
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
⊢ n₁ = n₁ + m

Tactic:
induction n₁ generalizing s with
  | zero =>
    cases m with
    | zero => rfl
    | succ m =>
      have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
      have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
      simp_all
  | succ k ih =>
    rw [show k + 1 + m = (k + m) + 1 by lia] at h₂
    cases h : sel s <;> simp_all [enumerate]; tauto

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
n : ℕ
⊢ (cons a s).drop (n + 1) = s.drop n

Tactic:
induction n with
  | zero => simp [drop]
  | succ n n_ih =>
    simp [drop, ← n_ih]

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'
⊢ (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

Tactic:
rw [h]

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

Goal state before:
pp: case zero
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? 0 → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro l S c o T

Goal state after:
case zero
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case succ
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n✝ : ℕ
a✝ :
  ∀ (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 α),
    c ∈ l ∨ some (some c) = S.get? (n✝ + 1) → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro l S c o T

Goal state after:
case succ
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n✝ : ℕ
a✝ :
  ∀ (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 α
o : c ∈ l ∨ some (some c) = S.get? (n✝ + 1)
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
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)
      (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

Tactic:
rw [h]

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'))
        (Sum.inl a)) =
    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)
      (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

Tactic:
rw [h]

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'))
        (Sum.inl a)) =
    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)
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 S.destruct 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.247

Tactic:
rw [h]

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

Goal state before:
pp: case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')

Tactic:
rw [h]

Goal state after:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case 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
c : Computation α
l : List (Computation α)
val✝ : α
IH : F l (Sum.inl val✝)
⊢ F (c :: l) (Sum.inl val✝)

Tactic:
rcases IH with ⟨c', cl, ac⟩

Goal state after:
case 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
c : Computation α
l : List (Computation α)
val✝ : α
c' : Computation α
cl : c' ∈ l
ac : val✝ ∈ c'
⊢ F (c :: l) (Sum.inl val✝)
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
⊢ (∃ (h : i = k) (h_1 : j = k), c ∈ Ioc (⋯ ▸ a) (⋯ ▸ b)) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
mem_Ioc,

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
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a < c ∧ c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1
α : 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
have := lem1 l

Goal state after:
case h1
α : 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2
α : 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
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
have := lem1 l

Goal state after:
case h2
α : 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
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'

Goal state after:
case h1
α : 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
this : F l (parallel.aux2 l)
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2
α : 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
this : F l (parallel.aux2 l)
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inr C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if
        { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
      ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
    else
      decide
        ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)) =
    ltb s₁.next s₂.next

Tactic:
if_pos,

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next =
    ltb s₁.next s₂.next

case case1.hc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
i₀ : ι
f : (j : { i // i ≠ i₀ }) → M ↑j
x : M i₀
i : ι
h : i = i₀
⊢ M i

Tactic:
rw [h]

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
i₀ : ι
f : (j : { i // i ≠ i₀ }) → M ↑j
x : M i₀
i : ι
h : i = i₀
⊢ M i₀
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel Eq (f1 a) (f2 b)

Tactic:
rw [h]

Goal state after:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel Eq (f1 b) (f2 b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ (map ((fun y ↦ (map g y).join) ∘ f) s).join

Tactic:
rw [← map_comp f (map g), ← Function.comp_def, comp_assoc, map_comp (map g ∘ f) join s]

Goal state after:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join
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₂ : σ₂
h :
  ∃ R, R s₁ s₂ ∧ ∀ {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:
rcases h with ⟨R, h₀, hR⟩
  exact (mapAccumr₂_bisim R h₀ hR).2

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
⊢ τ ↑(f₂.toHomUnits g⁻¹) = -τ (f₂ g)

Tactic:
map_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
⊢ τ ↑(f₂.toHomUnits g)⁻¹ = -τ (f₂ g)
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ ⨆ g', (f₂ g'⁻¹) ((f₁ g') (x + 1)) = (⨆ g', (f₂ g'⁻¹) ((f₁ g') x)) + 1

pp: case refine_3
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))

Tactic:
· simp only [map_add_one]
    exact (Monotone.map_ciSup_of_continuousAt (by fun_prop)
      (monotone_id.add_const (1 : ℝ)) (this x)).symm

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
this : ∀ᶠ (j : ι) in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
hd : μ s / ENNReal.ofReal T = 1
⊢ μ s = ENNReal.ofReal T

Tactic:
ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
this : ∀ᶠ (j : ι) in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
hd : μ s = ENNReal.ofReal T
⊢ μ s = ENNReal.ofReal T