mathlib-initiative/mathlib-tactics huggingface dataset:
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 := ⋯
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
c d : (P F).M α
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ r' c d

Tactic:
;

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 := ⋯
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
c d : (P F).M α
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ r' c d
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ ∀ (x : (P F).last.B a), WEquiv (lastFun (splitFun f' (wrepr ∘ f)) x) (f x)

Tactic:
;

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ ∀ (x : (P F).last.B a), WEquiv (lastFun (splitFun f' (wrepr ∘ f)) x) (f x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : 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
⊢ ∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size

Tactic:
;

Goal state after:
case node.lt
α : 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
⊢ ∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : 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
⊢ Raised (erase x t_l).size t_l.size ∧ BalancedSz t_l.size t_r.size

Tactic:
;

Goal state after:
case node.lt
α : 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
⊢ Raised (erase x t_l).size t_l.size ∧ BalancedSz t_l.size t_r.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₀ i) ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₁ i)

Tactic:
;

Goal state after:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₀ i) ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₁ i)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)

Tactic:
;

Goal state after:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩

Tactic:
;

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.eq.right
α : 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
⊢ t_l.size + t_r.size + 1 =
    (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)).size +
      1

Tactic:
;

Goal state after:
case node.eq.right
α : 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
⊢ t_l.size + t_r.size + 1 =
    (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)).size +
      1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₀ (g ⊚ f'₀) fun i ↦ g <$$> f₀ i) ((P F).wMk a₁ (g ⊚ f'₁) fun i ↦ g <$$> f₁ i)

Tactic:
;

Goal state after:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₀ (g ⊚ f'₀) fun i ↦ g <$$> f₀ i) ((P F).wMk a₁ (g ⊚ f'₁) fun i ↦ g <$$> f₁ i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B ⟨a, f⟩.fst), p (⟨a, f⟩.snd i)
⊢ Liftp p x

Tactic:
;

Goal state after:
case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B ⟨a, f⟩.fst), p (⟨a, f⟩.snd i)
⊢ Liftp p x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩

Tactic:
;

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨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₁ (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
⊢ ∃ r', Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'

Tactic:
;

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₁ (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
⊢ ∃ r', Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'
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₁ (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
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size

Tactic:
;

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₁ (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
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : 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₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (match cmpLE x t_x with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    (match cmpLE x t_x 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)).size =
      (node size✝ t_l t_x t_r).size - 1

Tactic:
;

Goal state after:
case node
α : 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₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (match cmpLE x t_x with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    (match cmpLE x t_x 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)).size =
      (node size✝ t_l t_x t_r).size - 1
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 α
⊢ (wSetoid α) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))
    (wrepr ((P F).wMk a f' f))

Tactic:
;

Goal state after:
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 α
⊢ (wSetoid α) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))
    (wrepr ((P F).wMk a f' f))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → 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 : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ((P F).map (fun t ↦ (↑t).2) ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
;

Goal state after:
case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → 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 : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ((P F).map (fun t ↦ (↑t).2) ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f

Tactic:
;

Goal state after:
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 α
⊢ ((TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : 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_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ 0 < t_l.size → t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
;

Goal state after:
case node.lt
α : 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_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ 0 < t_l.size → t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)

Tactic:
;

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.eq
α : 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₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ t_l.size + t_r.size = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
;

Goal state after:
case node.eq
α : 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₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ t_l.size + t_r.size = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ r x y

Tactic:
;

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ r x y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ Wsetoid (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x ↦ ⟦f x⟧⟩)))) (Wrepr (WType.mk a f))

Tactic:
;

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ Wsetoid (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x ↦ ⟦f x⟧⟩)))) (Wrepr (WType.mk 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_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < t_r.size → t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
;

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_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < t_r.size → t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))

Tactic:
;

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refl
α : Type u_1
inst✝ : Preorder α
⊢ (↑∅).empty = true

Tactic:
;

Goal state after:
case refl
α : Type u_1
inst✝ : Preorder α
⊢ (↑∅).empty = true
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x

Tactic:
;

Goal state after:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = 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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
i : Fin2 (n + 1)
j : (P F).B a i
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) i j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) i j

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
i : Fin2 (n + 1)
j : (P F).B a i
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) i j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) i j
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

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

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → (mk ∘ dest) (mk x) = mk 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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (α.RelLast r) x✝.dest y✝.dest

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (α.RelLast r) x✝.dest y✝.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest