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

Goal state before:
pp: α : 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₂
⊢ Valid' o₁ (insertWith f x (node sz l y r)) o₂ ∧ Raised (node sz l y r).size (insertWith f x (node sz l y r)).size

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Ordnode.insert x (node size✝ l y r) = insertWith (fun x_1 ↦ x) x (node size✝ l y r)

Tactic:
by

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
⊢ ∀ (a b : (P F).M α),
    Mcongr a b →
      (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) a) =
        (TypeVec.id ::: Quot.mk Mcongr) <$$> abs (M.dest (P F) b)

Tactic:
by

Goal state after:
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
⊢ supp (g <$$> x) i = g i '' supp x i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
by

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 α
⊢ recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ insert' x (node size✝ l y r) = insertWith id x (node size✝ l y r)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insert' x t).Valid

Tactic:
by

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 : (P F).W α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' x))

Tactic:
by

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 : β
⊢ (corec g x).dest = (TypeVec.id ::: corec g) <$$> g x

Tactic:
by

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
by

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
h : SuppPreservation
⊢ LiftPPreservation

Tactic:
rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_isUniform] at h'
    dsimp only [SuppPreservation, supp] at h
    simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
      image_univ, mem_range, exists_imp]
    constructor <;> intros <;> subst_vars <;> solve_by_elim

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation

Tactic:
by

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation ↔ IsUniform

Tactic:
by

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

Goal state before:
pp: n : ℕ
F✝ : TypeVec.{u} n → Type u_1
q✝ : MvQPF F✝
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst✝ : MvFunctor F
eqv : (α : TypeVec.{u} n) → F α ≃ F' α
map_eq : ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α), f <$$> a = (eqv β).symm (f <$$> (eqv α) a)
⊢ ∀ {α : TypeVec.{u} n} (x : F α), (eqv α).symm (abs (repr ((eqv α) x))) = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
F✝ : TypeVec.{u} n → Type u_1
q✝ : MvQPF F✝
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst✝ : MvFunctor F
eqv : (α : TypeVec.{u} n) → F α ≃ F' α
map_eq : ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α), f <$$> a = (eqv β).symm (f <$$> (eqv α) a)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F') α), (eqv β).symm (abs (f <$$> p)) = f <$$> (eqv α).symm (abs p)

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
⊢ Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size

Tactic:
by

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
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
⊢ (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)

Tactic:
by

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

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
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)
⊢ ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ∀ {α β : TypeVec.{?u.11} n} (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p

Tactic:
by

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
u : F (α ::: β) → β
x y : (P F).W α
⊢ WEquiv x y → recF u x = recF u y

Tactic:
by

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec.{u} n
x : G α✝
⊢ FG_abs (abs (repr (FG_repr x))) = x

Tactic:
by

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
x y : (P F).W α
h : abs ((P F).wDest' x) = abs ((P F).wDest' y)
⊢ WEquiv x y

Tactic:
by

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
x y : (P F).W α
⊢ WEquiv x y → WEquiv y x

Tactic:
by

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec.{u} n
f : α✝ ⟹ β✝
p : ↑(P F) α✝
⊢ FG_abs (abs (f <$$> p)) = f <$$> FG_abs (abs p)

Tactic:
by

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 α
⊢ wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
by

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} (x : Sigma F α), Sigma.abs F (Sigma.repr F x) = x

Tactic:
by

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 : α ⟹ β) (p : ↑(Sigma.P F) α), Sigma.abs F (f <$$> p) = f <$$> Sigma.abs F p

Tactic:
by

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} (x : Pi F α), Pi.abs F (Pi.repr F x) = x

Tactic:
by

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 : α ⟹ β) (p : ↑(Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p

Tactic:
by

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
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
⊢ ∀ (a b : Cofix F α), r a b → Quot.lift (Quot.mk r') h₁ a = Quot.lift (Quot.mk r') h₁ b

Tactic:
by

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 α
⊢ id <$> x = x

Tactic:
by

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 α
⊢ (g ∘ f) <$> x = g <$> f <$> x

Tactic:
by

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
x : (P F).W α
⊢ WEquiv (wrepr x) x

Tactic:
by

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

Goal state before:
pp: α : 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_balanceable : ?m.149
⊢ Valid' a₁
      (match Ordering.lt 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₂ ∧
    Raised
      (match Ordering.lt 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
      (t_l.size + t_r.size + 1)

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ u, abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)

Tactic:
by

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
g : α ⟹ β
x y : (P F).W α
⊢ WEquiv x y → WEquiv (g <$$> x) (g <$$> y)

Tactic:
by

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 α)
⊢ recF g ∘ fixToW = rec g

Tactic:
by

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
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)
⊢ IsPrecongr r'

Tactic:
by

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

Goal state before:
pp: α : 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_balanceable : ?m.286
⊢ Valid' a₁
      (match Ordering.gt 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₂ ∧
    Raised
      (match Ordering.gt 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
      (t_l.size + t_r.size + 1)

Tactic:
by

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
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 : Cofix F α), r x y → x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
⊢ Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size

Tactic:
by

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 α)
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
g : F α → α
x : (P F).W
⊢ recF g x = g (abs ((P F).map (recF g) x.dest))

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
⊢ Wequiv x y → recF u x = recF u y

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv x x

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
⊢ Wequiv x y → Wequiv y x

Tactic:
by

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 α
⊢ mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧

Tactic:
by

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 α
⊢ mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

Tactic:
by

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x

Tactic:
by

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ recF g ∘ fixToW = rec g

Tactic:
by

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
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
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
by

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
by

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
by
  have : recF g ∘ fixToW = Fix.rec g := by
    ext ⟨x⟩
    apply recF_eq_of_Wequiv
    rw [fixToW]
    apply Wrepr_equiv
  conv =>
    lhs
    rw [Fix.rec, Fix.mk]
    dsimp
  rcases h : repr x with ⟨a, f⟩
  rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]

Goal state after:
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
⊢ mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧

Tactic:
by

Goal state after:
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
⊢ mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
by

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
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)
⊢ (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]

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)
⊢ MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₀⟩ = MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ 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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ (g₁ ∘ fun x ↦ ⟦f x⟧) = g₂ ∘ fun x ↦ ⟦f x⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
h_mem : x ∈ t
⊢ (erase x t).size = t.size - 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
by

Goal state after:
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₁ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩ = g₂ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩

Tactic:
rw [← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]

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))
⊢ abs ⟨a, g₁ ∘ fun x ↦ ⟦f x⟧⟩ = abs ⟨a, g₂ ∘ fun x ↦ ⟦f x⟧⟩
Module: Mathlib.Data.Rat.Cast.OfScientific

Goal state before:
pp: K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e

Tactic:
by

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

Goal state before:
pp: 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), g₁ x = g₂ x

Tactic:
by

Goal state after: