mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lll.size + llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lll.size = 0 ∧ llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.flip.v = u.v.swap

Tactic:
by
  dsimp [v]
  ext
  · simp only
    ring
  · simp only
    ring

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, b < a

Tactic:
rintro ⟨i, a⟩
    obtain ⟨b, h⟩ := exists_lt a
    exact ⟨⟨i, b⟩, right _ h⟩

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
· rw [← xeq, ← abs_repr u, h, ← abs_map]; rfl

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size + rr.size = 0
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size = 0 ∧ rr.size = 0
⊢ rl.size = 0 ∧ rr.size = 0
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : y ≤ x
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size

Tactic:
rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
      rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
      refine
        ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
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 : (P F).M α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y

Tactic:
intro y

Goal state after:
case mk
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 : (P F).M α
y : Cofix F α
⊢ r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]
      rfl

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = x

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]
      rfl

Goal state after:
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
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> ⟨a, f⟩)))) =
    g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
MvPFunctor.wDest'_wMk'

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (TypeVec.id ::: fixToW) <$$> ⟨a, f⟩)) = g ((TypeVec.id ::: rec g) <$$> x)
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 α
⊢ mk x.dest = x

Tactic:
by
  change (Fix.mk ∘ Fix.dest) x = x
  apply Fix.ind_rec
  intro x; dsimp
  rw [Fix.dest, Fix.rec_eq, ← comp_map, ← appendFun_comp, id_comp]
  intro h; rw [h]
  change Fix.mk (appendFun id id <$$> x) = Fix.mk x
  rw [appendFun_id_id, MvFunctor.id_map]

Goal state after:
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₂ (F₁ α) → ↑((P F₂).comp (P F₁)) α

Tactic:
intro y

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
y : F₂ (F₁ α)
⊢ ↑((P F₂).comp (P F₁)) α
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
have lem1 :
    ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := by
    intro l S e
    obtain ⟨a, e⟩ := e
    have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
    rw [this]
    exact ret_terminates a

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none

Tactic:
have hm : n ≤ m' := Nat.le_of_succ_le_succ hm

Goal state after:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm✝ : n + 1 ≤ m' + 1
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
hm : n ≤ m'
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case pure
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct

Tactic:
| pure a =>

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

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

Tactic:
obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md

Goal state after:
case some
α : Type u
s : WSeq α
a✝ : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
a : α × WSeq α
am : some a ∈ s.destruct
⊢ ∃ a', some a' ∈ s.head
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'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.247

Tactic:
by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h]

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

Goal state before:
pp: α : Type u
l : List α
s : WSeq α
⊢ (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s.think)).destruct =
    Sum.inr
      (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s))

Tactic:
simp [think]

Goal state after:
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

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 : α
⊢ y ∈ s → y ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
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 t
      simp only [implies_true]

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
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 t
      simp only [implies_true]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba
      · rintro ⟨⟨a, b, hij⟩ | ⟨a, b, hab⟩, hba⟩
        · exact Sigma.Lex.left _ _ hij
        · exact Sigma.Lex.right _ _ (hab.lt_of_not_ge fun h => hba <| Sigma.Lex.right _ _ h)

Goal state after:
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
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

Goal state after:
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
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

Goal state after:
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
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
exact
        let ⟨k1, rs3, ek⟩ := of_results_think rs2
        let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
        let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
        match o', p', rop', rs4, rs5, mt with
        | none, none, _, _, rs5', mt => by
          have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb
        | some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt => by
          simp only [destruct_append.aux] at rs5
          refine ⟨some (b, append t' (join T')), ?_, ?_⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem
          rw [eq_of_pure_mem rs5.mem]
          exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩

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

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

Tactic:
Vector.head_cons,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)

Tactic:
intro y

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | (f ∘ ⇑e) x ≤ y} ((⇑e.symm ∘ g) y)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s)

Tactic:
add_apply,

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) (f ⁻¹' s)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s = (μ.singularPart ν) s

Tactic:
add_apply,

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (ν.withDensity (μ.rnDeriv ν)) s + (μ.singularPart ν) s = (μ.singularPart ν) s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ (c • μ[|s]) univ = c

Tactic:
rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
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:
· refine ⟨hf, ⟨?_⟩⟩
    have : IsFiniteMeasure μ := by
      constructor
      rwa [h.1.2, lt_top_iff_ne_top]
    set S := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
    have {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s) (hμs : μ s ≠ 0) :
        c • μ[|s] ∈ S := by
      refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
      · convert! hf.restrict_preimage hsm
        exact hfs.symm
      · rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
    intro s hsm hfs
    by_contra H
    obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by
      simpa [eventuallyConst_set, ae_iff, and_comm] using! H
    have hcond : c • μ[|s] = μ := by
      apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
      refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
      · rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
      · simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel,
          ENNReal.mul_inv_cancel, *]
    rw [← hcond] at hs'
    simp [ProbabilityTheory.cond_apply, hsm] at hs'

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst✝¹, inst✝] gb
⊢ ∀ ⦃x : β⦄, (∀ i ∈ f, x ∈ closure[inst✝¹] (image2 ϕ i s)) → ∀ i ∈ f, gb x ∈ closure[inst✝] (image2 ϕ' i s')

Tactic:
intro y

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst✝¹, inst✝] gb
y : β
⊢ (∀ i ∈ f, y ∈ closure[inst✝¹] (image2 ϕ i s)) → ∀ i ∈ f, gb y ∈ closure[inst✝] (image2 ϕ' i s')
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ∀ (i : ↑(Ico 0 n)), ball x ((map T T)^[↑i] ⁻¹' U) ∈ 𝓝 x

Tactic:
Subtype.forall

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ∀ (a : ℕ) (b : a ∈ Ico 0 n), ball x ((map T T)^[↑⟨a, b⟩] ⁻¹' U) ∈ 𝓝 x
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : { config := cfg, support := dom, condition := cond }.support = U
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, hU⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, hU⟩

Tactic:
simp only at hU

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : dom = U
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, hU⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, hU⟩
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 0 = univ

Tactic:
by simp [dynEntourage]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 1 = U

Tactic:
by simp [dynEntourage]

Goal state after: