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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
| =>

Goal state after:
α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil.nil
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ [].head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r [] a g [] = (g.reverse ++ [a]) :: splitBy r []

Tactic:
simp [splitBy.loop]

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

Goal state before:
pp: case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
⊢ w.HasPeriod (p.gcd q)

Tactic:
have gcd_stable : (p - q).gcd q = p.gcd q := gcd_sub_self_left (le_of_lt q_lt_p)

Goal state after:
case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    snd ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

Tactic:
snd_mul,

Goal state after:
case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    (fst (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) •
          snd (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j)) +
        MulOpposite.op (fst (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) •
          snd (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)))
      i✝ j✝
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N

Tactic:
by
  classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  refine .tail (b := X + Y' + Z) (ih (X + Y') (Y - Y') hZ ?_ rfl fun y hy ↦ ?_) <|
    ⟨X + Z, Y', z, add_right_comm .., by simp [hN, add_comm (_ + _)], by simp [Y']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iio a = Ico 0 ↑a

Tactic:
rw [← Ico_bot, image_cast_int_Ico]; rfl

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
h : n < p
⊢ IsUnit ↑n !

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
    refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
    rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact Nat.not_dvd_of_pos_of_lt (by lia) h

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p) * (n / p).choose (k / p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ n.choose k ≡ ∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (p * a).choose (p * b) ≡ a.choose b [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Goal state after:
a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p * a).choose (p * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Goal state after:
k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ a
⊢ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b

Tactic:
exact ha.imp fun hf hle => hle.trans hab

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

Goal state before:
pp: case inl
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)
⊢ nth p n ≤ nth p k

Tactic:
rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk

Goal state after:
case inl.inl
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 : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

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
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n k : PosNum
h : (↑n).sqrt < ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
Nat.sqrt_lt

Goal state after:
n k : PosNum
h : ↑n < ↑k.bit1 * ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n + ↑n + 1).sqrt < ↑n + (1 + 1 + 1)

Tactic:
Nat.sqrt_lt

Goal state after:
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n + 1 ≤ m

Tactic:
Nat.succ_le_iff

Goal state after:
case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n < m
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
simp [not_lt_of_gt h]

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

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ (node s l x r).size = (node s l x r).realSize

Tactic:
by
    rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]; rfl

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

Goal state before:
pp: case neg.inr.refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ ml.size + mr.size + 1 ≤ delta * ml.size + delta * ml.size

Tactic:
Nat.succ_le_iff

Goal state after:
case neg.inr.refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ ml.size + mr.size < delta * ml.size + delta * ml.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
split_ifs with h <;> repeat simp [add_comm]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ f₂ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₁, f₂⟩

Tactic:
congr with (i p)

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ f₂ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩
i : Fin2 n
p : P.mp.B a₁ i
⊢ f₁ i p = f₂ i p
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)

Tactic:
splitMin',

Goal state after:
α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (match ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
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) ⟹ α
i✝ : Fin2 n
x : P.WPath (WType.mk a f) i✝
i : Fin2 n
c : P.drop.B a i
⊢ α i

Tactic:
| =>

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
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) ⟹ α
i✝ : Fin2 n
x : P.WPath (WType.mk a f) i✝
i : Fin2 n
c : P.drop.B a i
⊢ α i
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
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) ⟹ α
i✝ : Fin2 n
x : P.WPath (WType.mk a f) i✝
i : Fin2 n
j : P.last.B a
c : P.WPath (f j) i
⊢ α i

Tactic:
| =>

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
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) ⟹ α
i✝ : Fin2 n
x : P.WPath (WType.mk a f) i✝
i : Fin2 n
j : P.last.B a
c : P.WPath (f j) i
⊢ α i
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.step.IsSpecial

Tactic:
dsimp [IsSpecial, step] at hs ⊢
  rw [mul_add, mul_comm u.y u.x, ← hs]
  ring

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d

Tactic:
exact eq hb''

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x

Tactic:
induction h with
  | ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
  | abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
  | trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

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
⊢ ∀ (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p

Tactic:
g

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
⊢ ∀ (p : ↑(P F).wp α), Quot.mk WEquiv (g <$$> p) = g <$$> Quot.mk WEquiv p
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
⊢ closure (range fun x ↦ x ^ n) = ⊤

Tactic:
refine (eq_top_iff' _).2 fun x ↦ ?_

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x ∈ closure (range fun x ↦ x ^ n)
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
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
apply lem1

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
c : Computation α
T : c.Terminates
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 l = Sum.inl a
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t1 : LiftRelO R (LiftRel R) a b
t2 : LiftRelO R (LiftRel R) b c
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) a c

Tactic:
obtain - | a := a

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none c

case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) c
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) b)

Tactic:
intro a b h

Goal state after:
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) b)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.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✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d✝ : Computation α
dm✝ : d✝ ∈ c' :: val✝
ad : a' ∈ d✝
dl : d✝ ∈ val✝
d : Computation α
dm : d ∈ l ∧ a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
obtain ⟨dm, ad⟩ := dm

Goal state after:
case inr.inr.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✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d✝ : Computation α
dm✝ : d✝ ∈ c' :: val✝
ad✝ : a' ∈ d✝
dl : d✝ ∈ val✝
d : Computation α
dm : d ∈ l
ad : a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
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:
by
      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 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⟩

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⟩ := exists_gt a
      exact ⟨⟨i, c⟩, right _ _ ha, left _ _ h⟩

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

Goal state before:
pp: case neg.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h✝ : c₁ < c₂
⊢ c₁ < c₂

Tactic:
rename_i h'

Goal state after:
case neg.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂
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:
rename_i h'

Goal state after:
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₁
Module: Mathlib.Data.String.Basic

Goal state before:
pp: l : List Char
h : ofList [] ≠ ""
⊢ (ofList []).toList = Legacy.front (ofList []) :: (Legacy.drop (ofList []) 1).toList

Tactic:
| =>

Goal state after:
l : List Char
h : ofList [] ≠ ""
⊢ (ofList []).toList = Legacy.front (ofList []) :: (Legacy.drop (ofList []) 1).toList
Module: Mathlib.Data.String.Basic

Goal state before:
pp: l : List Char
c : Char
cs : List Char
h : ofList (c :: cs) ≠ ""
⊢ (ofList (c :: cs)).toList = Legacy.front (ofList (c :: cs)) :: (Legacy.drop (ofList (c :: cs)) 1).toList

Tactic:
| =>

Goal state after:
l : List Char
c : Char
cs : List Char
h : ofList (c :: cs) ≠ ""
⊢ (ofList (c :: cs)).toList = Legacy.front (ofList (c :: cs)) :: (Legacy.drop (ofList (c :: cs)) 1).toList
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 γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
· simp only [inl.injEq, exists_and_left, exists_eq_left']

Goal state after:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Data.Vector.Mem

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

Tactic:
by
  rw [Vector.toList_cons, List.mem_cons]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).1 (mapAccumr f₂ nil s₂).1 ∧ (mapAccumr f₁ nil s₁).2 = (mapAccumr f₂ nil s₂).2

Tactic:
exact ⟨h₀, rfl⟩

Goal state after: