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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ 0 < (dropWhile p tl).length

Tactic:
simp_all only [dropWhile_cons_of_pos]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ↑↑1 - 1 < ↑(b % r - v % r) / ↑r ∧ ↑(b % r - v % r) / ↑r ≤ ↑↑1

Tactic:
div_le_iff₀ hr',

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ↑↑1 - 1 < ↑(b % r - v % r) / ↑r ∧ ↑(b % r - v % r) ≤ ↑↑1 * ↑r
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 < (↑(b % r) - ↑(v % r)) / ↑r ∧ (↑(b % r) - ↑(v % r)) / ↑r ≤ 0

Tactic:
div_le_iff₀ hr',

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 < (↑(b % r) - ↑(v % r)) / ↑r ∧ ↑(b % r) - ↑(v % r) ≤ 0 * ↑r
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.cons.len_eq
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ (head :: tail ++ t₁).length = (head :: tail ++ t₂).length

pp: case inr.cons.h_lex
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
· simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1

Goal state after:
case inr.cons.h_lex
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
rw [splitByLoop_eq_append, mem_append]
      simpa using IH

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ w[i % p]? = w[i]?

Tactic:
have len' : i - p < w.length := by lia
        have IH : w[(i - p) % p]? = w[i - p]? := per.getElem?_mod p (i - p) w len'
        rw [hasPeriod_iff_getElem?] at per
        have minus : i - p < w.length - p := by lia
        have per' := per (i - p) minus
        simp only [large, Nat.sub_add_cancel] at per'
        have mod : i % p = (i - p) % p := mod_eq_sub_mod large
        aesop

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors =
    Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.image Subtype.val (Finset.Iic n.factorization).attach)

Tactic:
Finset.attach_image_val

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iic n.factorization)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ { k // ∀ i ∈ t, k ≡ a i [MOD s i] }

Tactic:
by
  simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.image Subtype.val (Finset.Iio n.factorization).attach)

Tactic:
Finset.attach_image_val

Goal state after:
n : ℕ
⊢ n.properDivisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iio n.factorization)
Module: Mathlib.Data.Ordmap.Ordnode

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

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

Tactic:
· exact node 2 nil x r

Goal state after:
case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
rlx : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

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

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 2 nil x r

Goal state after:
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 α
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ count p (nth p (k + 1)) = k + 1

Tactic:
| succ k ihk =>

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i | p i ∧ n ≤ i}

Tactic:
refine (nth_eq_sInf _ _).trans (congr_arg sInf ?_)
  refine Set.ext fun a => and_congr_right fun hpa => ?_
  refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
  have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
  rwa [nth_count hpa, lt_self_iff_false] at hn

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ nth p n = 0

Tactic:
have : Set.ofPred p ⊆ Finset.range n := by
    intro n' hn'
    contrapose! hp
    exact ⟨n', by simpa using hp, Set.mem_ofPred.mp hn'⟩
  rw [nth_of_card_le ((finite_toSet _).subset this)]
  · refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
    exact Set.Finite.toFinset_subset.mpr this

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

Goal state before:
pp: α : Type u_1
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c

Tactic:
apply le_trans

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h

Tactic:
by
  ext i x; cases x <;> rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i ↦ h ⊚ g i

Tactic:
by
  ext i x; cases x <;> rfl

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

Goal state before:
pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ b₂✝

Tactic:
apply le_trans

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?right.right.b

case right.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ ?right.right.b ≤ b₂✝

case right.right.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ α a₁
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)

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
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

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⟩
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)

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

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⟩
Module: Mathlib.Data.PSigma.Order

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

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)

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

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⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
⊢ a.gcdD b = a.gcd b

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Goal state after:
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b = a.gcd b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
y : α
yx : y < x
⊢ All (fun z ↦ y < z) t₂

Tactic:
exact h₂.mem_gt.imp fun z xz => lt_trans yx xz

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

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b

Tactic:
← hi

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u (f' u i)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Tactic:
· rw [sign_of_pos hp] at h
    exact (one_ne_zero h).elim

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

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left✝ : i ∈ univ
hi : f i = u
⊢ p u

Tactic:
← hi

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left✝ : i ∈ univ
hi : f i = u
⊢ p (f i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u

Tactic:
← hi

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)
Module: Mathlib.Data.Set.Enumerate

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

Tactic:
have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂

Goal state after:
case zero.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ 0 = 0 + (m + 1)
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 α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
· intro s IH l S m
    have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := by
      induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        -- Porting note: `revert e'` is required.
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e : 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 with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
        · contradiction
        have := IH' m _ e
        grind
    rcases h : parallel.aux2 l with a | l'
    · exact lem1 _ _ ⟨a, h⟩
    · have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by
        simp only [parallel.aux1, rmap, corec_eq]
        rw [h])
      rw [H2]
      refine @Computation.think_terminates _ _ ?_
      have := H1 _ h
      rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]

Goal state after:
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
x : α
⊢ x ∈ s → Nat.card ↑(s ∩ ⋯.choose) ≠ 0 ∧ x ∈ s ∧ x ∈ ⋯.choose

Tactic:
intro hx

Goal state after:
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
x : α
hx : x ∈ s
⊢ Nat.card ↑(s ∩ ⋯.choose) ≠ 0 ∧ x ∈ s ∧ x ∈ ⋯.choose
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: 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 α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) c.destruct)

Tactic:
· rcases h : destruct c with a | c' <;> simp only [rmap]
        · refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem
        · intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩

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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

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

Goal state before:
pp: a b c : String
⊢ a.toList ≤ b.toList → b.toList ≤ c.toList → a.toList ≤ c.toList

Tactic:
apply le_trans

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (s.append S.join).destruct s2.destruct

Tactic:
h2

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (s.append S.join).destruct (t.append T.join).destruct
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
      (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ?_⟩
  any_goals rintro a b rfl rfl; exact map_eq_empty.1 h
  · rintro a b rfl rfl; exact disjSum_eq_empty.1 h
  cases a <;> cases b
  · exact map_eq_empty.2 (h.1 _ _ rfl rfl)
  · simp [h.2.1 _ _ rfl rfl]
  · rfl
  · exact map_eq_empty.2 (h.2.2 _ _ rfl rfl)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Icc a₁ a₂)

Tactic:
rw [← Finset.map_map]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ico a₁ a₂)

Tactic:
rw [← Finset.map_map]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioc a₁ a₂)

Tactic:
rw [← Finset.map_map]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))