mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

Tactic:
· simp only [if_pos hi, eq_one_of_ne_zero j hj,
          if_neg (Ne.symm Fin.zero_ne_one)] at hij
          apply (h hij).elim

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a ⟦s.toAList⟧ = dlookup a s

Tactic:
lookup_toFinmap,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ AList.lookup a s.toAList = dlookup a s
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a ⟦AList.singleton a b⟧ = some b

Tactic:
lookup_toFinmap,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ AList.lookup a (AList.singleton a b) = some b
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
lookupAll_cons_ne,

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a l).head? = dlookup a (⟨a', b⟩ :: l)

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a l).head? = dlookup a l

pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Tactic:
head?_lookupAll a l

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ dlookup a l = dlookup a l

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ lookup a f.toAList = some (f a)

Tactic:
apply mem_lookup_iff.2

Goal state after:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ ⟨a, f a⟩ ∈ f.toAList.entries
Module: Mathlib.Data.Int.Fib.Lemmas

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

Tactic:
if hn : n = 0 then simp [hn] else
    obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind

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

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ b = a ↔ b = 0

Tactic:
rw [xor_eq_iff_right_eq, xor_self a]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
⊢ ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Tactic:
by
  induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ foldl (flip cons) [] l = l.reverse

Tactic:
induction l <;> simp [flip, foldl_eq_foldr_reverse, -foldr_reverse]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
by rw [rtakeWhile_concat, if_pos h]

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

Goal state before:
pp: case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
· rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i]? = w[i + p]?

Tactic:
mod (i + p) (by lia),

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i]? = w[(i + p) % p]?
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
x✝ : Matrix n o A
i✝ : l
j✝ : o
⊢ (mulLeftLinearMap o R (a * b)) x✝ i✝ j✝ = (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b) x✝ i✝ j✝

Tactic:
simp only [mulLeftLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R a = 0

Tactic:
· rw [h]
    exact mulRightLinearMap_zero_eq_zero _ _

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

Goal state before:
pp: n k m : ℕ
⊢ n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k

Tactic:
tsub_mul m

Goal state after:
n k m : ℕ
⊢ n * k - m * k + (m * k - n * k) = n * k - m * k + (m * k - n * k)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∃ y, f y = x

Tactic:
apply @h fun x => ∃ y : P.B a, f y = x

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ Liftp (fun x ↦ ∃ y, f y = x) ⟨a, f⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
r : F.M → Sort w
f : (x : ↑F F.M) → r (M.mk x)
x : F.M
this : r (M.mk x.dest)
⊢ r x

Tactic:
← mk_dest x

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
r : F.M → Sort w
f : (x : ↑F F.M) → r (M.mk x)
x : F.M
this : r (M.mk x.dest)
⊢ r (M.mk x.dest)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)

Tactic:
← PosNum.to_nat_to_int,

Goal state after:
n d : PosNum
⊢ -↑↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)

Tactic:
← PosNum.to_nat_to_int,

Goal state after:
n d : PosNum
⊢ ↑↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % ↑d.abs) = ↑n % ↑d

Tactic:
← PosNum.to_nat_to_int,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % ↑d.abs) = ↑↑n % ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.succ.f.f.intro
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
constructor <;> try rfl

Goal state after:
case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos.h
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)

Tactic:
constructor <;> try rfl

Goal state after:
case pos.h.a
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (x_f i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
h : t.Sized
⊢ t.toList.length = t.size

Tactic:
rw [length_toList', size_eq_realSize h]

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

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m

Tactic:
rw [PrimeMultiset.prod_dvd_iff']

Goal state after:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hn
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n

Tactic:
rw [PrimeMultiset.prod_dvd_iff']

Goal state after:
case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case e'_3
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p

Tactic:
apply Multiset.eq_replicate.mpr

Goal state after:
case e'_3
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs

Tactic:
rw [splitMin_eq]
    · obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr
      suffices H : _ by
        refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
        · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
          exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
        · exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)
        · rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
      refine Or.inr ⟨_, Or.inr e, ?_⟩
      rwa [hr.2.eq_node'] at bal

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ TypeVec.id <$$> x = x

Tactic:
rw [← abs_repr x, ← abs_map]
  rfl

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
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

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

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ ↑(f i j)⟩
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 y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
⊢ (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) x) =
    (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)

Tactic:
conv =>
        lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

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

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

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

Goal state after:
case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)
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 : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl

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 : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((P F).map Subtype.val ⟨a, f⟩) = abs ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ u, abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)

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

Goal state after:
case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ u, abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = x

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = abs ((P F).map Subtype.val ⟨a, f⟩)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_r_h := Valid'.erase_aux x h.right

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_h : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
⊢ abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)

Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos (by simp) hn.le

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl a

Tactic:
simp only [rmap]

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl a

Tactic:
simp only [rmap]

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∃ n, some a ∈ s.get? n

Tactic:
apply mem_rec_on h
  · intro a' s' h
    rcases h with h | h
    · exists 0
      simp only [get?, drop, head_cons]
      rw [h]
      apply ret_mem
    · obtain ⟨n, h⟩ := h
      exists n + 1
      simpa [get?]
  · intro s' h
    obtain ⟨n, h⟩ := h
    exists n
    simp only [get?, dropn_think, head_think]
    apply think_mem h

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

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

Tactic:
by
      apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)
      intro a b; apply LiftRelO.imp_right
      intro s t; apply Or.inl

Goal state after: