mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? p l = (dropWhile (fun x ↦ !p x) l).head?

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x ↦ !p x) []).head?

case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x ↦ !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x ↦ !p x) (head✝ :: tail✝)).head?
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (range' n (m - n)).length = m - n

Tactic:
simp [length_range']

Goal state after:
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ foldr (fun y x ↦ f x y) a '' Set.univ ⊆ foldr (fun y x ↦ g x y) a '' Set.univ

Tactic:
Set.image_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ Set.range (foldr (fun y x ↦ f x y) a) ⊆ Set.range (foldr (fun y x ↦ g x y) a)
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∑ a ∈ s, f a).toNNRat = ↑(∑ a ∈ s, (f a).toNNRat)

Tactic:
cast_sum,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, ↑(f a).toNNRat
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ ∅ ∪ s.toFinset, (count x s + 1 - count x 0) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
empty_union,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ s.toFinset, (count x s + 1 - count x 0) = ∏ i ∈ s.toFinset, (count i s + 1)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
ofDigits_neg_one

Goal state after:
n : ℕ
t : ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD ↑11]
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum

Tactic:
ofDigits_neg_one

Goal state after:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n.dist m = m.dist n

Tactic:
simp [dist, add_comm]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
h : n.greatestFib = 0
⊢ n = 0

Tactic:
by simpa using findGreatest_eq_zero_iff.1 h zero_lt_one le_add_self

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ nth p '' Set.Iio #hf.toFinset = Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
by
      ext x
      simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
        Set.mem_Iio, exists_prop]

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
rw [nth_of_card_le _ hk] at h

Goal state after:
case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < 0
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rx rr

Goal state after:
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rx rr

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
hl : nil.Sized
⊢ C nil

Tactic:
exact H0

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
h₂ : ↑r₂ + ↑d < ↑d + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d

Tactic:
add_lt_add_iff_right

Goal state after:
case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
h₂ : ↑r₂ < ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * ↑b < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n

Tactic:
← Nat.mod_add_div b (pos a)

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ F.B (M.mk ⟨a, x⟩).head = F.B a

Tactic:
by rw [head_mk]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
· exact hl.rotateR_size

Goal state after:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1
Module: Mathlib.Data.PSigma.Order

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

Tactic:
obtain ⟨c⟩ : Nonempty (α k) := inferInstance

Goal state after:
case left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ f i '' univ = f' i '' univ

Tactic:
rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]

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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rw [wrepr, recF_eq', q.P.wDest'_wMk]; rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
dxeq,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₀⟩ = (TypeVec.id ::: Quot.mk r) <$$> y.dest
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 ::: _root_.id) <$$> x) = mk x

Tactic:
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
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest

Tactic:
dxeq,

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Quot.mk r <$> abs ⟨a, f₀⟩ = Quot.mk r <$> y.dest
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
s' : Option (α × WSeq α)
h1 : s' ∈ s.destruct
right✝ : a ∈ (Option.rec nil Prod.snd s').destruct
⊢ s.destruct.Terminates

Tactic:
exact terminates_of_mem h1

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
i1,

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons a' s✝ ↔ a = a' ∨ a ∈ 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
l : List (Computation α)
⊢ F l (parallel.aux2 l)

Tactic:
induction l

Goal state after:
case nil
α : 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
⊢ F [] (parallel.aux2 [])

case cons
α : 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
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝) (parallel.aux2 (head✝ :: tail✝))
Module: Mathlib.Data.Sigma.Order

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

Tactic:
obtain ⟨c⟩ : Nonempty (α k) := inferInstance

Goal state after:
case left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩
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) (_ : ⋯ ▸ a ≤ c) (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : i = k) (_ : ⋯ ▸ a ≤ c) (h : k = j), ⋯ ▸ c ≤ b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

Goal state after:
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) (_ : ⋯ ▸ a ≤ c) (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : i = k) (_ : ⋯ ▸ a ≤ c) (h : k = j), ⋯ ▸ c < b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

Goal state after:
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) (_ : ⋯ ▸ a < c) (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : i = k) (_ : ⋯ ▸ a < c) (h : k = j), ⋯ ▸ c ≤ b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

Goal state after:
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) (_ : ⋯ ▸ a < c) (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : i = k) (_ : ⋯ ▸ a < c) (h : k = j), ⋯ ▸ c < b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

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

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1.destruct
    c2.destruct

Tactic:
exact
    match c1, c2, h with
    | c, _, Or.inl <| rfl => by cases c.destruct <;> simp
    | _, _, Or.inr ⟨S, rfl, rfl⟩ => by
      induction S using WSeq.recOn
      case nil | cons => simp
      case think S => exact Or.inr ⟨S, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
U : WSeq α → WSeq β → Prop
ST : LiftRel (LiftRel R) S T
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
a : Option (α × WSeq α)
ma : a ∈ S.join.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
obtain ⟨n, h⟩ := exists_results_of_mem ma; clear ma; revert S T ST a
  induction n using Nat.strongRecOn with | _ n IH
  intro S T ST a ra; simp only [destruct_join] at ra
  exact
    let ⟨o, m, k, rs1, rs2, en⟩ := of_results_bind ra
    let ⟨p, mT, rop⟩ := Computation.exists_of_liftRel_left (liftRel_destruct ST) rs1.mem
    match o, p, rop, rs1, rs2, mT with
    | none, none, _, _, rs2, mT => by
      simp only [destruct_join]
      exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
    | some (s, S'), some (t, T'), ⟨st, ST'⟩, _, rs2, mT => by
      simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
      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.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 = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
d : α × Computation α
dT : d ∈ parallel T
cd : d.1 = a
⊢ a ∈ c ∧ c ∈ S

Tactic:
rw [get_eq_of_mem _ dT] at e

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)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
a' : α
c : Computation α
d : α × Computation α
e : d = (a', c)
dT : d ∈ parallel T
cd : d.1 = a
⊢ a ∈ c ∧ c ∈ S
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case refl.refl.left
α : 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 α)) := ⋯
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c

Tactic:
i1,

Goal state after:
case refl.refl.left
α : 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)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)

Tactic:
refine Fin2.cases' ?_ ?_ (insertPerm i j)

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).Terminates

Tactic:
rw [get?_ofSeq]

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ (Computation.pure (s.get? n)).Terminates
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ (↑s).get? n

Tactic:
rw [get?_ofSeq]

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ Computation.pure (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:
simp_rw [transnumAuxSeq, Real.dist_eq]

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| =
    |(f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0 - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ f x - x ≤ τ f

Tactic:
apply le_translationNumber_of_add_le

Goal state after:
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (f x - x) ≤ f x_1
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
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝[>] 0)

Tactic:
refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩

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
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝 0)