mathlib-initiative/mathlib-tactics huggingface dataset:
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 α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: fun x ↦ x) <$$> 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 α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: fun x ↦ x) <$$> x) = mk x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g 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
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk x = mk x

Tactic:
]

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 : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = 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
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> 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
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ TypeVec.id <$$> x = TypeVec.id <$$> x

Tactic:
]

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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (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), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ p (mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩))

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (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), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ p (mk (abs ⟨a, (P F).appendContents f' fun 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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (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), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ∃ a_1 f_1,
    abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧
      ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (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), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ∃ a_1 f_1,
    abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧
      ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
u v : (P F).M
cuv : Mcongr u v
⊢ r (Quot.mk Mcongr v) (Quot.mk Mcongr v)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (Quot.lift (Quot.mk r') h₁) ⋯
this : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r'
⊢ f <$> Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest = abs ((P F).map (f ∘ Quot.mk r ∘ Quot.mk Mcongr) b.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
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> (mk y.dest).dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ ⟨mk
          ((TypeVec.id ::: Sigma.fst) <$$>
            (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x'),
        g ((TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x')⟩.fst =
    _root_.id (mk x')

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ ⟨mk
          ((TypeVec.id ::: Sigma.fst) <$$>
            (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x'),
        g ((TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x')⟩.fst =
    _root_.id (mk x')
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
]

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
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.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
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x : Cofix F), r' x x

pp: case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

pp: case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ r' x y

Tactic:
· intro x
    left
    rfl

Goal state after:
case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = 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.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ x = x

Tactic:
]

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
x y : Cofix F α
h : x.dest = y.dest
⊢ y = y

Tactic:
]

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
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: case h.inl
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : x = y
⊢ Quot.mk r' <$> y.dest = Quot.mk r' <$> y.dest

Tactic:
]

Goal state after:
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
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x

Tactic:
]

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
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> 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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ (TypeVec.id ::: Sigma.fst ∘ rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ (TypeVec.id ::: Sigma.fst ∘ rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x' =
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest

Tactic:
]

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
this : x = y.fst
⊢ β y.fst = β y.fst

Tactic:
]

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

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
]

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
]

Goal state after:
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 ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
]

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 ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ⟨a, Quot.mk r ∘ f₀⟩ = abs ⟨a, Quot.mk r ∘ f₁⟩

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ⟨a, Quot.mk r ∘ f₀⟩ = abs ⟨a, Quot.mk r ∘ f₁⟩
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 ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x

Tactic:
]

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 ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r < 0
⊢ -1 = -1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : 0 < r
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: ⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
h : -1 = 0
hn : r < 0
⊢ r = 0

Tactic:
neg_eq_zero

Goal state after:
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0

Tactic:
]

Goal state after:
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0

Tactic:
]

Goal state after:
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
z : ℤ
hn : z < 0
⊢ -1 = -1

Tactic:
]

Goal state after:
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'
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'
⊢ ∃ a f₀ f₁, x.dest = abs ⟨a, f₀⟩ ∧ y.dest = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)

Tactic:
]

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'
⊢ ∃ a f₀ f₁, x.dest = abs ⟨a, f₀⟩ ∧ y.dest = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ sign 0 = ↑(Int.sign 0)

Tactic:
sign_zero,

Goal state after:
case inr.inl
⊢ 0 = ↑(Int.sign 0)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ (-0).sign = -sign 0

Tactic:
sign_zero,

Goal state after:
case inr.inl
⊢ (-0).sign = -0
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:
]

Goal state after:
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)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ -1 = -1

Tactic:
]

Goal state after: