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

Goal state before:
pp: case nil.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
hr : nil.Balanced
sr : nil.Sized
⊢ nil.balance x nil = nil.balance' x nil

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ =
    ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
      splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
        ((fun x ↦ g <$$> x) ∘ fun x ↦ ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩

Tactic:
rfl

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

Goal state before:
pp: case nil.node.nil.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
hr : (nil.node' rx nil).Balanced
sr : (node rs nil rx nil).Sized
⊢ node 2 nil x (nil.node' rx nil) = nil.node' x (nil.node' rx nil)

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
i : P.last.B a
fst✝ : P.wp.A
snd✝ : P.wp.B fst✝ ⟹ α
⊢ g <$$> ⟨fst✝, snd✝⟩ = ⟨⟨fst✝, snd✝⟩.fst, g ⊚ ⟨fst✝, snd✝⟩.snd⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
x : P.last.B a
fst✝ : P.wp.A
snd✝ : P.wp.B fst✝ ⟹ α
⊢ ⟨fst✝, snd✝⟩ = ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩

Tactic:
rfl

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

Goal state before:
pp: case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = nil.node3L x nil rx (node 1 nil rrx nil)

Tactic:
rfl

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

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ l.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1

Tactic:
rfl

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

Goal state before:
pp: v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Nat.Primes.toPNat) v = Multiset.map Subtype.val v

Tactic:
rfl

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

Goal state before:
pp: v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → p.Prime
p : ℕ+
h : p.Prime
⊢ ↑↑⟨↑p, h⟩ = ↑(id p)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ ⟨a, splitFun (g ⊚ f') (P.wMap g ∘ f)⟩ = ⟨a, splitFun (g ⊚ f') fun x ↦ P.wMap g (f x)⟩

Tactic:
rfl

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

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
have n := Nat.findX this

Goal state after:
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = nil.node4L x (node 1 nil rlx nil) rx nil

Tactic:
rfl

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

Goal state before:
pp: case refine_3
α : 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
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ll.size + lr.size + 1 + rs

Tactic:
rfl

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

Goal state before:
pp: case node.nil.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx nil).Balanced
sl : (node ls nil lx nil).Sized
⊢ node 2 (nil.node' lx nil) x nil = (nil.node' lx nil).node' x nil

Tactic:
rfl

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

Goal state before:
pp: case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = nil.node4R lx (node 1 nil lrx nil) x nil

Tactic:
rfl

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

Goal state before:
pp: case refine_2
α : 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
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ All (fun x ↦ x < (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1)
    (Ordnode.node ls ll lx lr)

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

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

Goal state before:
pp: case refine_3
α : 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
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).size = ls + (rl.size + rr.size + 1)

Tactic:
rfl

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

Goal state before:
pp: case refine_3
α : 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
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
    ls + rs

Tactic:
rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl

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 α
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
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H : ?m.298
⊢ Valid' o₁
      ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2)
      o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
          (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2).size =
      ls + rs

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

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

Goal state before:
pp: case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = (node 1 nil llx nil).node3R lx nil x nil

Tactic:
rfl

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

Goal state before:
pp: u : XgcdType
⊢ u.finish.ap = u.finish.bp

Tactic:
rfl

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 α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)

Tactic:
rfl

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
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)

Tactic:
rfl

Goal state after:
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⟩
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
sr : nil.Sized
H1 : l.size = 0 → nil.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ nil.size → nil.size ≤ delta * l.size
⊢ l.balanceL x nil = l.balance x nil

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (nil.node' rx nil) = nil.balance x (nil.node' rx nil)

Tactic:
rfl

Goal state after:
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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
rfl

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

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
rfl

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

Goal state before:
pp: case right.right.right.right.right
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
grind

Goal state after:
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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
x : (P F).M α
⊢ (Quot.mk r' ∘ fun x ↦ g <$$> x) x = (u ∘ Quot.mk r) x

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
· rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_ge h_1 h_2) with ⟨vl, e⟩
      suffices H : _ by
        refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _
      exact Or.inl ⟨_, e, h.3.1⟩

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
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
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ (g ⊚ f) i '' univ = g i ∘ f i '' univ

Tactic:
rfl

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
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i ↦ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
rfl

Goal state after:
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
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ⊚ TypeVec.id ::: Quot.mk Mcongr ∘ corecF g) <$$> g x = (TypeVec.id ::: corec g) <$$> g x

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{?u.5} n
α✝ : TypeVec.{?u.5} n
x✝ : ↑P α✝
⊢ id (id x✝) = x✝

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{?u.5} n
α✝ β✝ : TypeVec.{?u.5} n
f✝ : α✝ ⟹ β✝
p✝ : ↑P α✝
⊢ id (f✝ <$$> p✝) = f✝ <$$> id p✝

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
i : Fin2 n
α✝ : TypeVec.{?u.11} n
x✝ : Prj i α✝
⊢ abs i (repr i x✝) = x✝

Tactic:
rfl

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

Goal state before:
pp: case mk
n : ℕ
i : Fin2 n
α β : TypeVec.{?u.11} n
f : α ⟹ β
fst✝ : (P i).A
snd✝ : (P i).B fst✝ ⟹ α
⊢ abs i (f <$$> ⟨fst✝, snd✝⟩) = f <$$> abs i ⟨fst✝, snd✝⟩

Tactic:
rfl

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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, splitFun f' f⟩)) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Pi.P F).A
g : (Pi.P F).B x ⟹ α
⊢ (match (Pi.P F).map f ⟨x, g⟩ with
    | ⟨a, f⟩ => fun x ↦ abs ⟨a x, fun i y ↦ f i ⟨x, y⟩⟩) =
    fun a ↦ abs ((P (F a)).map f ⟨x a, fun i y ↦ g i ⟨a, y⟩⟩)

Tactic:
rfl

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map id ⟨a, f⟩) = abs ⟨a, f⟩

Tactic:
rfl

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ abs ((P F).map (g ∘ f) (repr x)) = abs ((P F).map g ((P F).map f (repr x)))

Tactic:
rfl

Goal state after:
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 ((P F).map Subtype.val ⟨a, f⟩) = abs ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
rfl

Goal state after: