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

Goal state before:
pp: case fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (j : (P F).B a Fin2.fz), α.RelLast R ((P F).appendContents f' f₀ Fin2.fz j) ((P F).appendContents f' f₁ Fin2.fz j)

pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 n
⊢ ∀ (j : (P F).B a a✝.fs), α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)

Tactic:
· apply h'

Goal state after:
case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 n
⊢ ∀ (j : (P F).B a a✝.fs), α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ r' x x

Tactic:
left

Goal state after:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ x = 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 : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (mk x).dest = x

Tactic:
Cofix.mk,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (corec (fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) x).dest = x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
rw [h _ _ r'xy]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ r.sign⁻¹ = r.sign

Tactic:
obtain hn | hz | hp := sign_apply_eq r
  · rw [hn]
    simp
  · rw [hz]
    exact inv_zero
  · rw [hp]
    exact inv_one

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).destruct.destruct = Sum.inl (some (a, s))

Tactic:
by simp [destruct, cons, Computation.rmap]

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

Goal state before:
pp: case cons.inr.inl
α : 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
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'

pp: case cons.inr.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
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls
⊢ s ∈ l'

Tactic:
· contradiction

Goal state after:
case cons.inr.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
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls
⊢ s ∈ l'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
h' : o.1 = a
⊢ ∃ a', some a' ∈ s.head

Tactic:
clear h'

Goal state after:
case some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none.inl
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h✝ : some a = none
⊢ C s'

pp: case none.inr
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h✝ : C s'
⊢ C s'

Tactic:
· contradiction

Goal state after:
case none.inr
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h✝ : C s'
⊢ C s'
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten s'.think ~ʷ s

Tactic:
apply Equiv.trans

Goal state after:
case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s'.think ~ʷ flatten s'
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
c : Computation α
l : List (Computation α)
⊢ F l
      (List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) l) →
    F (c :: l)
      (match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
cases List.foldr (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c)) (Sum.inr List.nil) l

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✝ : α
⊢ F l (Sum.inl val✝) →
    F (c :: l)
      (match Sum.inl val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

case inr
α : 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 val✝ : List (Computation α)
⊢ F l (Sum.inr val✝) →
    F (c :: l)
      (match Sum.inr val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.MapsTo (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩) ↑hs.toFinset ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset)

pp: case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.LeftInvOn (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩)
    (fun x ↦
      match x with
      | ⟨t, x⟩ => x)
    ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset)

pp: case right_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.RightInvOn (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩)
    (fun x ↦
      match x with
      | ⟨t, x⟩ => x)
    ↑hs.toFinset

Tactic:
· intro x
      simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
      intro hx
      refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
      simp only [nonempty_subtype, Set.mem_inter_iff]
      use x, hx, (hP.2 x).exists.choose_spec.2

Goal state after:
case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.LeftInvOn (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩)
    (fun x ↦
      match x with
      | ⟨t, x⟩ => x)
    ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset)

case right_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.RightInvOn (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩)
    (fun x ↦
      match x with
      | ⟨t, x⟩ => x)
    ↑hs.toFinset
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x : α
⊢ ∀ x_1 ∈ s, x_1 ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
intro y hy hyt _ hxs hxt

Goal state after:
case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ⟨⋯.choose, ⋯⟩ = t
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : 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 α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ 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 (some b))

Tactic:
obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩

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

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

Tactic:
intro ss IH s S ej m

Goal state after:
case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (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 α)
ej : s.append S.join = ss.think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.Seq.Parallel

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

Tactic:
rw [h'] at this
    rcases this with ⟨c, cl, ac⟩
    exact ⟨c, Or.inl cl, ac⟩

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

Goal state before:
pp: case neg.cons
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
h : ¬c₁ = c₁
h' : List.Lex (fun x1 x2 ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
· contradiction

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

Goal state before:
pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
· rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
    simp only [Legacy.Iterator.hasNext, Pos.Raw.byteIdx_zero, rawEndPos_ofList, utf8Len_cons,
      add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Legacy.Iterator.curr,
      Pos.Raw.get, String.toList_ofList, Pos.Raw.utf8GetAux, Legacy.Iterator.next, Pos.Raw.next,
      Bool.ite_eq_true_distrib, decide_eq_true_eq]
    split_ifs with h
    · subst c₂
      suffices ltb ⟨ofList (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩
          ⟨ofList (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
            ltb ⟨ofList cs₁, 0⟩ ⟨ofList cs₂, 0⟩ by
        rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
      apply ltb_cons_addChar
    · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
      cases e <;> rename_i h'
      · assumption
      · contradiction

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

Goal state before:
pp: α : Type u
s t : WSeq α
⊢ (s.append t).destruct = s.destruct.bind (destruct_append.aux t)

Tactic:
apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t))
      _ ⟨s, t, rfl, rfl⟩

Goal state after:
α : Type u
s t : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 ↦
    ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map (map fun c ↦ c.1) T

Tactic:
← WSeq.map_comp

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map ((map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c) S
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
c : Computation α
⊢ c = map (fun c ↦ c.1) (map (fun a ↦ (a, c)) c)

Tactic:
← map_comp

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
c : Computation α
⊢ c = map ((fun c ↦ c.1) ∘ fun a ↦ (a, c)) c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = parallel (WSeq.map (map fun c ↦ c.1) T)
⊢ C a

Tactic:
rw [← map_parallel] at pe

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
⊢ C a
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
⊢ ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s

Tactic:
exact ae_of_all _ fun b ↦ (hs b).mem_iff

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

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + (g 0 - 1) < f 0 + ↑⌊g 0⌋

Tactic:
gcongr; exact sub_one_lt_floor _

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

Goal state before:
pp: f g₁ g₂ : CircleDeg1Lift
h : Semiconj ⇑f ⇑g₁ ⇑g₂
⊢ dist (g₁ 0) (f (g₁ 0) - f 0) + dist (f (g₁ 0) - f 0) (g₂ 0) =
    dist (f 0 + g₁ 0) (f (g₁ 0)) + dist (g₂ 0 + f 0) (g₂ (f 0))

Tactic:
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub,
        abs_sub_comm (g₂ (f 0))]

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
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₂ g)) + 1 ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1

Tactic:
by grw [map_lt_add_translationNumber_add_one]

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

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ Dense ↑s → ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

pp: case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s

Tactic:
· rintro hd a ha rfl
    rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd
    exact ha hd

Goal state after:
case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
rw [Nat.frequently_atTop_iff_infinite] at hx

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s