mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
⊢ (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π =
    lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
        (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
      y' ▷ ℕ∪{∞}

Tactic:
apply CartesianMonoidalCategory.hom_ext<;> ext x; exacts [x.prop n ∞, (x.val n).prop]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup

Tactic:
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]

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

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = acc.toListAppend (lookmap f l)

Tactic:
by
  cases l with
  | nil => simp [go, lookmap]
  | cons hd tl =>
    rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => simp

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

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

Tactic:
simp [*, mem_lookupAll]

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

Goal state before:
pp: case neg
α : 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:
simp [*, mem_lookupAll]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).Nodup

Tactic:
lookupAll_eq_dlookup a h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
⊢ (if t = ∅ then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f t

Tactic:
ext a
        rw [if_neg ht.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := hf
        obtain ⟨_, _, rfl⟩ := ha
        exact hb

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

Goal state before:
pp: case neg
α : 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
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
by_cases h' : a = x.1

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

case neg
α : 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))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ l.dedupKeys.NodupKeys

Tactic:
dsimp [dedupKeys]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) [] l).NodupKeys
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ f x ≠ 0

Tactic:
AList.mem_keys,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList.keys ↔ f x ≠ 0
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝)).sup ↔
    ∃ f ∈ Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝, x ∈ f.support

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
    using! List.mem_foldr_sup_support_iff

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t

Tactic:
by
    rw [assocLeft]
    unfold mul
    rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]
    · rfl
    rw [append_assoc]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑(i + 1) + 1) * fib (-↑(i + 1) - 1) - fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Tactic:
rw [zero_add, add_comm]
      rfl

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

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ (↑a - ↑b).natAbs ≤ n

Tactic:
rw [← Nat.cast_le (α := ℤ), natCast_natAbs]
  exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n)
    (natCast_nonneg b) (ofNat_le.mpr b_le_n)

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

Goal state before:
pp: case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
intro ⟨rfl, rfl⟩

Goal state after:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < |b|
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k

Tactic:
← rdrop_add,

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ ((l₁ ++ l₂).rdrop l₂.length).rdrop k = l₁.rdrop k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = [n]

Tactic:
← filter_lt_of_succ_bot hnm

Goal state after:
n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = filter (fun x ↦ decide (x < n + 1)) (Ico n m)
Module: Mathlib.Data.List.Shortlex

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

Tactic:
List.length_cons

Goal state after:
case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (tail.length + 1)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this✝ : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
this : n = p ^ multiplicity p n
dvd_pow : n.minFac ∣ p ^ multiplicity p n
⊢ p = n.minFac

Tactic:
exact (Nat.prime_dvd_prime_iff_eq isPrime hp₁).mp (isPrime.dvd_of_dvd_pow dvd_pow)|>.symm

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

Goal state before:
pp: m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m <;> constructor <;> intro h

Goal state after:
case zero.mp
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

case zero.mpr
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

case pos.mp
p a✝ : PosNum
h : pos p = pos a✝
⊢ ZNum.pos p = (pos a✝).toZNum

case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: d n : PosNum
⊢ ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2

Tactic:
rw [Nat.div_mod_unique (PosNum.cast_pos _)]
  induction n with
  | one =>
    exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
  | bit1 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
    · lia
  | bit0 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux
    · simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
    · simpa using IH.2

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d

Tactic:
by
      rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
          abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
      rfl

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

Goal state before:
pp: case mpr.succ.step.f.f.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (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)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
h_a_2 : ⟨y_a, y_f⟩ = ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j ↦ (x' j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))

Tactic:
cases h_a_2

Goal state after:
case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (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✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j ↦ (x' j).approx n✝) (CofixA.intro a fun j ↦ (y' j).approx (n✝ + 1))
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₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h : ⟨ax, (TypeVec.id ::: Quot.mk R) ⊚ fx⟩ = ⟨ay, (TypeVec.id ::: Quot.mk R) ⊚ fy⟩
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
injection h with h₀ h₁

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀✝ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h₀ : ax = ay
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx ≍ (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ x ∈ t.toList

Tactic:
unfold Emem

Goal state after:
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂

Tactic:
by
  inhabit M F
  classical
  introv Hr; apply ext
  introv
  by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
  · have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left
  · rw [not_or] at h
    obtain ⟨h₀, h₁⟩ := h
    simp only [iselect_eq_default, *, not_false_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
delta

Goal state after:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr.mpr
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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
⊢ f j y ∈ supp x j

Tactic:
rw [mem_supp]

Goal state after:
case mpr.mpr
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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
⊢ ∀ (a : (P F).A) (f_1 : (P F).B a ⟹ α), abs ⟨a, f_1⟩ = x → f j y ∈ f_1 j '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
rw [mem_supp]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) ↔ u ∈ f i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ recF g ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr x)) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
rcases h : repr x with ⟨a, f⟩

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ recF g ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> ⟨a, f⟩)) = g ((TypeVec.id ::: rec g) <$$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)

Tactic:
rcases h : repr x with ⟨a, f⟩

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ recF g (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)) = g (rec g <$> x)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r < 0
⊢ (if r < 0 then -1 else if 0 < r then 1 else 0) = -1

Tactic:
if_pos hr

Goal state after:
r : ℝ
hr : r < 0
⊢ -1 = -1
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 f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → ∀ u ∈ supp x, p u

pp: case mpr.mpr
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
⊢ (∀ u ∈ supp x, p u) → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
· rintro ⟨a', f', xeq', h'⟩ u usuppx
    rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩
    rw [← f'ieq]
    apply h'

Goal state after:
case mpr.mpr
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
⊢ (∀ u ∈ supp x, p u) → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mpr
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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
⊢ f i ∈ supp x

Tactic:
rw [mem_supp]

Goal state after:
case mpr.mpr
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
h' : ∀ u ∈ supp x, p u
i : (P F).B a
⊢ ∀ (a : (P F).A) (f_1 : (P F).B a → α), abs ⟨a, f_1⟩ = x → f i ∈ f_1 '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ u ∈ supp (abs ⟨a, f⟩) ↔ u ∈ f '' univ

Tactic:
rw [mem_supp]

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) ↔ u ∈ f '' univ
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
val : Seq1 (Option α)
⊢ match
    match
      match some val with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some val with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
obtain ⟨o, s'⟩ := val

Goal state after:
case some
α : Type u
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (do
        let a ← s.destruct
        Pure.pure (Option.rec nil Prod.snd a)) >>=
      destruct =
    s.destruct >>= tail.aux

Tactic:
LawfulMonad.bind_assoc

Goal state after:
α : Type u
s : WSeq α
⊢ (s.destruct >>= fun x ↦ Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ s.destruct >>= tail.aux >>= drop.aux n = s.destruct >>= drop.aux (n + 1)

Tactic:
LawfulMonad.bind_assoc

Goal state after:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 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 α
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)).destruct = Sum.inr ?m.407

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

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

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ t.head

Tactic:
exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
      (some (b, t')) (destruct t) dtm

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

Goal state before:
pp: α : 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
⊢ Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard

Tactic:
let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩

Goal state after:
α : 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
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s :=
  fun x ↦
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
⊢ Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).tail = ↑s.tail

Tactic:
simp only [tail, destruct_ofSeq, map_pure', flatten_pure]

Goal state after:
α : Type u
s : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑s.tail)) s.head) = ↑s.tail