mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rfl

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

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = abs ((P F).map Subtype.val ⟨a, f⟩)

Tactic:
rfl

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

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x)

Tactic:
rw [Fix.rec, Fix.mk]

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
| Quot.lift (recF g) ⋯ (Quot.mk (⇑(wSetoid α)) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr x)))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((P F).map (fun t ↦ (↑t).1) ⟨a, f⟩) = abs ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
rfl

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

Goal state before:
pp: case h.right.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((P F).map (fun t ↦ (↑t).2) ⟨a, f⟩) = abs ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
rfl

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

Goal state before:
pp: case h'
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
x : Cofix F α
⊢ x = x

Tactic:
rfl

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

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
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).1) ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
rfl

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

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

Goal state before:
pp: case mk
F : Type u → Type v
q : QPF F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk a✝ f✝))))

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
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)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs ((P F).map Wrepr ⟨a, f⟩) = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
rfl

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)
this : recF g ∘ fixToW = rec g
| rec g (mk x)

Tactic:
rw [Fix.rec, Fix.mk]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
| Quot.lift (recF g) ⋯ (Quot.mk (⇑Wsetoid) (PFunctor.W.mk ((P F).map fixToW (repr 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:
rfl

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
⊢ abs ⟨a, fixToW ∘ fun x ↦ ⟦f x⟧⟩ = abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk a f)))

Tactic:
rfl

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

Goal state before:
pp: case mk.nil
α : Type u_1
inst✝ : Preorder α
property✝ : Ordnode.nil.Valid
h : (↑⟨Ordnode.nil, property✝⟩).empty = true
⊢ ⟨Ordnode.nil, property✝⟩ = ∅

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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, splitFun (TypeVec.id ⊚ dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ splitFun (dropFun f₁) (lastFun f₁)⟩

Tactic:
appendFun_comp_splitFun

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, splitFun (TypeVec.id ⊚ dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ =
    MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩
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:
rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
x : ↑(P F).wp α
⊢ Quot.mk WEquiv (g <$$> x) = Fix.map g (Quot.mk WEquiv x)

Tactic:
rfl

Goal state after:
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
x✝ x y : Cofix F α
h : x = mk y.dest
| TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest

pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
| (mk y.dest).dest

Tactic:
rfl

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

Goal state before:
pp: case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ mk ((fun i ↦ i.dest) x) = mk x.dest

Tactic:
rfl

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

Tactic:
rfl

Goal state after:
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), r x y → x = y

Tactic:
by
  apply Cofix.bisim_rel
  intro x y rxy
  rcases (liftr_iff r _ _).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
  rw [dxeq, dyeq, ← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
  congr 2 with i
  apply Quot.sound
  apply h'

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

Goal state before:
pp: case left
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 <$$> x = f <$$> x

Tactic:
rfl

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

Goal state before:
pp: case right
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
⊢ g <$$> x = g <$$> x

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
inv_zero,

Goal state after:
case inr.inl
⊢ sign 0 = 0
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h₀.fz
n : ℕ
ι ι' : Type u
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : (α ::: ι).drop Fin2.fz
⊢ subtypeVal α.repeatEq Fin2.fz (diagSub Fin2.fz x) = prod.diag Fin2.fz x

Tactic:
rfl

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

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
x✝ : (α ::: ι).last
⊢ (Subtype.val ∘ lastFun c ∘ h) x✝ = (Prod.map f g ∘ lastFun prod.diag) x✝

Tactic:
rfl

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

Goal state before:
pp: case R
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 α
| α.RelLast' R

pp: case a
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 α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝)

pp: case a
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 α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)

Tactic:
rfl

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 := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝)

case a
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 α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
x : (P F₂).B b
⊢ abs ((P F₁).map f ⟨h x, fun y ↦ g ⟨x, y⟩⟩) =
    abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f ⟨⟨b, h⟩, g⟩).fst.snd
          x,
        fun y ↦
        ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).snd
          ⟨x, y⟩⟩

Tactic:
rfl

Goal state after:
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✝ x✝ : (P F).M α
⊢ R
    (((Quot.mk Mcongr ∘
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
        Quot.mk Mcongr)
      x✝)
    (Quot.mk Mcongr x✝)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a✝ b : Cofix F α
x : X
Ha : a✝ = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a : X
⊢ R (Cofix.corec (g ∘ f) a) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) a)

Tactic:
refine ⟨a, rfl, rfl⟩

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ β✝ : TypeVec.{u} n
f✝ : α✝ ⟹ β✝
p✝ : ↑(P F).mp α✝
⊢ Quot.mk Mcongr (f✝ <$$> p✝) = f✝ <$$> Quot.mk Mcongr p✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) none none = LiftRelO (Function.swap R) (Function.swap C) none none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) none (some (hy, jy)) = LiftRelO (Function.swap R) (Function.swap C) none (some (hy, jy))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) none = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) (some (hy, jy)) =
    LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) (some (hy, jy))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case zero.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
h₂ : enumerate sel s (0 + 0) = some a
⊢ 0 = 0 + 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s t u : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ LiftRel R s u

Tactic:
refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t u✝ : WSeq α
h1 : LiftRel R s✝ t
h2 : LiftRel R t u✝
s u : WSeq α
h : (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s u
⊢ Computation.LiftRel (LiftRelO R fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (flatten c).destruct.destruct
    (c.bind destruct).destruct

Tactic:
induction c using Computation.recOn with

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr.inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case pos.refine_2
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty ↑s
f : ℕ → ↑s
hf : Function.Surjective f
⊢ ∀ (n : ℕ), Subtype.val ∘ f '' {i | i ≤ n} ⊆ Subtype.val ∘ f '' {i | i ≤ n + 1}

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
n : ℕ
⊢ (K.prod K') n = K n ×ˢ K' n

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ op a ∈ s.op ↔ a ∈ s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ unop a ∈ s.unop ↔ a ∈ s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
have lem1 :
    ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := by
    intro l S e
    obtain ⟨a, e⟩ := e
    have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
    rw [this]
    exact ret_terminates a
  intro l S c m T
  revert l S
  apply @terminatesRecOn _ _ c T _ _
  · intro a l S m
    apply lem1
    induction l with | nil => simp at m | cons c l IH => ?_
    simp only [List.mem_cons] at m
    rcases m with e | m
    · rw [← e]
      simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
      split <;> simp
    · obtain ⟨a', e⟩ := IH m
      simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
      rw [e]
      exact ⟨a', rfl⟩
  · intro s IH l S m
    have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := by
      induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        -- Porting note: `revert e'` is required.
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e : List.foldr (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
          (Sum.inr List.nil) l with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
        · contradiction
        have := IH' m _ e
        grind
    rcases h : parallel.aux2 l with a | l'
    · exact lem1 _ _ ⟨a, h⟩
    · have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by
        simp only [parallel.aux1, rmap, corec_eq]
        rw [h])
      rw [H2]
      refine @Computation.think_terminates _ _ ?_
      have := H1 _ h
      rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case mk
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail.think).get (n + 1)
val✝ : Stream' (Option (Option α))
property✝ : val✝.IsSeq
⊢ (↑(think ⟨val✝, property✝⟩)).get (n + 1) = (↑⟨val✝, property✝⟩).get n

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
by
    let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h
    rcases o with - | a
    · injection oe
    injection oe with h'
    exact ⟨a, om, h'⟩

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
⊢ Option.map (fun a' ↦ (a', S.tail)) (some o) = some (o, S.tail)

Tactic:
rfl

Goal state after: