mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
h₂ : M.mk ⟨a✝¹, f✝¹⟩ = M.mk ⟨a, f₂⟩
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✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
⊢ (CofixA.intro a✝¹ fun j ↦ (f✝¹ j).approx (n + 1)) = CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)

Tactic:
have := mk_inj h₁

Goal state after:
case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
h₂ : M.mk ⟨a✝¹, f✝¹⟩ = M.mk ⟨a, f₂⟩
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✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
this : ⟨a✝, f✝⟩ = ⟨a, f₁⟩
⊢ (CofixA.intro a✝¹ fun j ↦ (f✝¹ j).approx (n + 1)) = CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)
Module: Mathlib.Data.PFunctor.Multivariate.M

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

Tactic:
obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁

Goal state after:
case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
f₂' : (P.B a').last → (α ::: P.M α).last
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) f₂'⟩
h'' : ∀ (i : (P.B a').last), R ((fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) (f₂' i)
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩⟩
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Module: Mathlib.Data.PFunctor.Multivariate.M

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

Tactic:
obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁

Goal state after:
case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
f₂' : (P.B a').last → (α ::: P.M α).last
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) f₂'⟩
h'' : ∀ (i : (P.B a').last), R ((fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) (f₂' i)
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩⟩
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
have := balancedSz_zero.1 hr.1.symm

Goal state after:
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
⊢ rrl.size = 0 ∧ rrr.size = 0
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) =
    if nil.size < ratio * (node 1 nil rrx nil).size then nil.node3L x nil rx (node 1 nil rrx nil)
    else nil.node4L x nil rx (node 1 nil rrx nil)

pp: case nil.node.nil.node.refl.refl.hnc
α : 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
⊢ ¬0 + (0 + 1 + 1) ≤ 1

Tactic:
if_pos

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

case nil.node.nil.node.refl.refl.hc
α : 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
⊢ nil.size < ratio * (node 1 nil rrx nil).size

case nil.node.nil.node.refl.refl.hnc
α : 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
⊢ ¬0 + (0 + 1 + 1) ≤ 1
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g

Tactic:
ext x
  apply bisim' (fun _ => True) _ _ _ _ trivial
  clear x
  intro x _
  rcases gxeq : g x with ⟨a, f'⟩
  have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
  have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
  refine ⟨_, _, _, h₀, h₁, ?_⟩
  intro i
  exact ⟨f' i, trivial, rfl, rfl⟩

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

Goal state before:
pp: u : PrimeMultiset
n : ℕ+
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
let h := @prod_dvd_iff u n.factorMultiset
  rw [n.prod_factorMultiset] at h
  exact h

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) =
    if nil.size < ratio * (node 1 nil llx nil).size then (node 1 nil llx nil).node3R lx nil x nil
    else (node 1 nil llx nil).node4R lx nil x nil

pp: case node.nil.node.nil.refl.refl.hnc
α : 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
⊢ ¬1 + 1 ≤ 1

Tactic:
if_pos

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

case node.nil.node.nil.refl.refl.hc
α : 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
⊢ nil.size < ratio * (node 1 nil llx nil).size

case node.nil.node.nil.refl.refl.hnc
α : 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
⊢ ¬1 + 1 ≤ 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : 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
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3

pp: case refine_2
α : 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
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs

Tactic:
· rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)

Goal state after:
case refine_2
α : 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
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hab : a ≤ b
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
exact Or.inl (Lex.right _ hab)

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ x✝.reduce.v = x✝.v

Tactic:
rw [reduce_a h, finish_v u h]

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

Goal state before:
pp: a b : ℕ+
⊢ ↑(a.gcdA' b) = ↑(a.gcdW b) + a.gcdX b

Tactic:
by
  dsimp [gcdA', gcdX, gcdW, XgcdType.w]
  rw [add_right_comm]

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

Goal state before:
pp: n m : ℕ
H : Raised n m
⊢ m.dist n ≤ 1

Tactic:
Nat.dist_comm

Goal state after:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1
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 : β
⊢ M.dest (P F) (M.corec (P F) (fun x ↦ repr (g x)) x) =
    (TypeVec.id ::: M.corec (P F) fun x ↦ repr (g x)) <$$> repr (g x)

Tactic:
M.dest_corec

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: M.corec (P F) fun x ↦ repr (g x)) <$$> repr (g x) =
    (TypeVec.id ::: M.corec (P F) fun x ↦ repr (g x)) <$$> repr (g x)
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
supp_eq_of_isUniform h,

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ f u '' univ, p u u_1
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 ⟹ α
⊢ supp (abs ⟨a, g ⊚ f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Tactic:
supp_eq_of_isUniform h,

Goal state after:
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 '' supp (abs ⟨a, f⟩) i
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 '' supp (abs ⟨a, f⟩) i

Tactic:
supp_eq_of_isUniform h,

Goal state after:
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
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case sz.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f l✝).Sized ∧ (map f r✝).Sized

Tactic:
· constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz

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

Goal state before:
pp: case node.eq.left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
h_glue_sized : (t_l.glue t_r).size = t_l.size + t_r.size
⊢ Valid' a₁
    (match Ordering.eq with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂

Tactic:
exact h_glue_valid

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 (α ::: β) → β
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⟩
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk' ⟨a, (TypeVec.id ::: fixToW) ⊚ f⟩))) =
    g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
← MvPFunctor.map_eq,

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⟩
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> ⟨a, f⟩)))) =
    g ((TypeVec.id ::: rec g) <$$> 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 y : Cofix F α
h : x.dest = y.dest
⊢ x = y

Tactic:
← Cofix.mk_dest x,

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

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (prod.fst ⊚ (f ⊗' g) ⊚ prod.diag) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
← comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ((prod.fst ⊚ (f ⊗' g)) ⊚ prod.diag) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ (f ⊗' g) ⊚ prod.diag) <$$> x = g <$$> x

Tactic:
← comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ ((prod.snd ⊚ (f ⊗' g)) ⊚ prod.diag) <$$> x = g <$$> x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ Liftr R x.dest y.dest

Tactic:
rcases h x' Qx' with ⟨a, f, f', ux'eq, vx'eq, h'⟩

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs ⟨a, f⟩
vx'eq : (v x').dest = abs ⟨a, f'⟩
h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ Liftr R x.dest y.dest
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
⊢ (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n ∈ closure (range fun x ↦ x ^ n)

Tactic:
exact nsmul_mem (subset_closure <| mem_range_self _) _

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * (1 * (↑x.den)⁻¹)

pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

pp: case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

pp: case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
one_mul,

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * (↑x.den)⁻¹

n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
conv => congr; rfl; rw [Cofix.dest]

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
        Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ supp (abs ⟨a, f⟩) → p u

Tactic:
supp_eq_of_isUniform h,

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ f '' univ → p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)

Tactic:
supp_eq_of_isUniform h,

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ g ∘ f '' univ = g '' supp (abs ⟨a, f⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
supp_eq_of_isUniform h,

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ g ∘ f '' univ = g '' f '' univ