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

Goal state before:
pp: α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y

Tactic:
simp [singleton, mem_def]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
subst h
      simp [*, mem_lookupAll]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
subst a

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (erase x s ∪ singleton x b) = lookup x s
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
subst a

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = pure s

Tactic:
rw [traverse, Multiset.id_traverse]

Goal state after:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> pure s.val = pure s
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
h : f = g
⊢ f.neLocus f = ∅

Tactic:
by simp only [neLocus, Ne, not_true, Finset.filter_false]

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

Goal state before:
pp: n : ℕ
⊢ (bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Tactic:
show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl

Goal state after:
n : ℕ
⊢ ↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: b : Bool
n : ℤ
⊢ ((bif b then 1 else 0) + 2 * n) / 2 = n

Tactic:
Int.add_mul_ediv_left,

Goal state after:
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 + n = n

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
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
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑1

Tactic:
← cast_sub h.le,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ⌈↑(b % r - v % r) / ↑r⌉ = ↑1
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case pos
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ (take n w ++ w)[j]? = w[j % p]?

pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
· -- indices within `take n w` can be reduced due to the period of `w`
      calc
        (take n w ++ w)[j]? = (take n w)[j]? := getElem?_append_left (by simp_all)
        _ = w[j]? := getElem?_take_of_lt j_lt_n
        _ = w[j % p]? := Eq.symm (mod_w j (by lia))

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (j - n) % p = (j - p * (n / p)) % p

Tactic:
by rw [Nat.mul_div_cancel' dvd]

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑⌈x⌉₊

Tactic:
NNRat.cast_le_natCast

Goal state after:
case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ x ≤ ↑⌈x⌉₊
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
rw [Int.cast_natCast, NNRat.cast_le_natCast]

Goal state after:
case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ x ≤ ↑⌈x⌉₊
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈r⌉₊ = ↑⌈↑n / ↑d⌉₊

Tactic:
h.to_eq rfl rfl,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈↑n / ↑d⌉₊ = ↑⌈↑n / ↑d⌉₊
Module: Mathlib.Data.Nat.Dist

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

Tactic:
by unfold Nat.dist at h; lia

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

Goal state before:
pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
rw [← h.left, ← h.right, mod_add_div]

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

Goal state before:
pp: case inr
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst a

Goal state after:
case inr
n : ℕ
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
⊢ False

Tactic:
obtain ⟨m, hm⟩ := pow_multiplicity_dvd p n

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ ¬n.minFac ^ 2 ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
obtain ⟨k, _, k_pos, hn₁⟩ := (isPrimePow_nat_iff_bounded_log_minFac _).mp h

Goal state after:
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ (Icc 1 (n - 1)).gcd n.choose
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case e'_2.e'_3
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ f (nth (fun i ↦ p (f i)) m') = nth p m'

Tactic:
exact ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(a.sub' 1) = ↑a - ↑1

Tactic:
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑p).toNat?

Tactic:
← PosNum.to_nat_to_int p

Goal state after:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑↑p).toNat?
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑p).toNat

Tactic:
← PosNum.to_nat_to_int p

Goal state after:
p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑↑p).toNat
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
dsimp [delta, ratio] at lr₁ mr₁
      have r1 : r.size = 1 := by lia
      have l1 : l.size = 1 := by lia
      rw [r1, add_assoc] at lr₁
      rw [l1, r1]
      revert mm; cases size ml <;> cases size mr <;> intro mm
      · decide
      · rw [zero_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
        decide
      · rcases mm with (_ | ⟨⟨⟩⟩); decide
      · rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)

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

Goal state before:
pp: case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)

Tactic:
iterate 3 (have := mk_inj ‹_›; cases this)

Goal state after:
case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
{ simp [h.1] }

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

Goal state before:
pp: case node.nil.node.nil
α : 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
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
    else ((node lls lll llx llr).node' lx nil).rotateR x nil

Tactic:
have : size lll = 0 ∧ size llr = 0 := by
          have := balancedSz_zero.1 hl.1
          rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
        cases sl.2.1.2.1.size_eq_zero.1 this.1
        cases sl.2.1.2.2.size_eq_zero.1 this.2
        obtain rfl : lls = 1 := sl.2.1.1
        rw [if_neg, rotateR_node, if_pos]; · rfl
        all_goals (try dsimp only [size]); decide

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

Goal state before:
pp: case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False

pp: case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False

Tactic:
· exact lt_irrefl _ hij

Goal state after:
case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
← f'ieq

Goal state after:
case mpr.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : (P F).B a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ (f' i✝ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.Bounded ⊥ o₂

Tactic:
cases o₂ <;> trivial

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

Goal state before:
pp: case a
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 α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv
    ((P F).wMk a (dropFun (splitFun (TypeVec.id ⊚ f') (wrepr ∘ f))) (lastFun (splitFun (TypeVec.id ⊚ f') (wrepr ∘ f))))
    ((P F).wMk a f' f)

Tactic:
id_comp

Goal state after:
case a
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 α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv ((P F).wMk a (dropFun (splitFun f' (wrepr ∘ f))) (lastFun (splitFun f' (wrepr ∘ f)))) ((P F).wMk a f' f)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inr
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 → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> x.dest =
    ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> y.dest

Tactic:
rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]

Goal state after:
case h.inr
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 → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> y.dest
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)
⊢ MvQPF.abs ⟨a, splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩

Tactic:
id_comp

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)
⊢ MvQPF.abs ⟨a, splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩
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 α)
⊢ (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x →
    mk ((TypeVec.id ⊚ TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x

Tactic:
id_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x →
    mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk 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 : F (α ::: Fix F α)
⊢ (TypeVec.id ⊚ TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
id_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ⊚ TypeVec.id :::
        (Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
id_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> 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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ (TypeVec.id ⊚ TypeVec.id ::: Sigma.fst ∘ rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'

Tactic:
id_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ (TypeVec.id ::: Sigma.fst ∘ rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : (P F).B a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p u

Tactic:
← f'ieq

Goal state after:
case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : (P F).B a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p (f' i)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
⊢ C s

Tactic:
apply Seq.mem_rec_on M
  intro o s' h; rcases o with - | b
  · apply h2
    cases h
    · contradiction
    · assumption
  · apply h1
    apply Or.imp_left _ h
    intro h
    injection h

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

Goal state before:
pp: case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
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: