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

Goal state before:
pp: case lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.lt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

pp: case eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.eq with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.eq with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

pp: case gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.gt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.gt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.lt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

case eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.eq with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.eq with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

case gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.gt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.gt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)
Module: Mathlib.Data.QPF.Multivariate.Basic

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

pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation → SuppPreservation

Tactic:
<;>

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation → LiftPPreservation

case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation → SuppPreservation
Module: Mathlib.Data.QPF.Multivariate.Basic

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

pp: case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)) → ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u

Tactic:
<;>

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) → ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)) → ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
Module: Mathlib.Data.QPF.Multivariate.Basic

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

pp: case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝¹ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
u✝ : α i✝
x✝ : (P F).B a i✝
a✝ : f i✝ x✝ = u✝
⊢ p u✝

Tactic:
<;>

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)

case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝¹ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
u✝ : α i✝
x✝ : (P F).B a i✝
a✝ : f i✝ x✝ = u✝
⊢ p u✝
Module: Mathlib.Data.QPF.Multivariate.Basic

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

pp: case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)

Tactic:
<;>

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)

case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt.zero
α : 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 < 0 → 0 - 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1

pp: case node.lt.succ
α : 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
t_l_size : ℕ
⊢ 0 < t_l_size + 1 → t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
<;>

Goal state after:
case node.lt.zero
α : 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 < 0 → 0 - 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1

case node.lt.succ
α : 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
t_l_size : ℕ
⊢ 0 < t_l_size + 1 → t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt.zero
α : 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 < 0 → t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

pp: case node.gt.succ
α : 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
t_r_size : ℕ
⊢ 0 < t_r_size + 1 → t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Tactic:
<;>

Goal state after:
case node.gt.zero
α : 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 < 0 → t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

case node.gt.succ
α : 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
t_r_size : ℕ
⊢ 0 < t_r_size + 1 → t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1
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

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

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

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
Module: Mathlib.Data.Real.Sign

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

Tactic:
· rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

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

Goal state before:
pp: r : ℝ
⊢ r⁻¹.sign = r.sign

Tactic:
by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
  · rw [sign_zero, inv_zero, sign_zero]
  · rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]

Goal state after:
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 : α → β
p :
  ↑{ 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) }
    α
⊢ 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 p).fst.fst,
        fun x ↦
        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 p).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 p).snd
              ⟨x, y⟩⟩⟩ =
    f <$> abs ⟨p.fst.fst, fun x ↦ abs ⟨p.fst.snd x, fun y ↦ p.snd ⟨x, y⟩⟩⟩

Tactic:
obtain ⟨a, g⟩ := p

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
a :
  { 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) }.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
      a →
    α
⊢ 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 ⟨a, g⟩).fst.fst,
        fun x ↦
        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 ⟨a, 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 ⟨a, g⟩).snd
              ⟨x, y⟩⟩⟩ =
    f <$> abs ⟨⟨a, g⟩.fst.fst, fun x ↦ abs ⟨⟨a, g⟩.fst.snd x, fun y ↦ ⟨a, g⟩.snd ⟨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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ (corec' g x).dest = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
Cofix.corec',

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ (corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr x)).dest =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

pp: case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)

Tactic:
<;>

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

pp: case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)

Tactic:
<;>

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → LiftpPreservation

pp: case mpr
F : Type u → Type u
q : QPF F
⊢ LiftpPreservation → SuppPreservation

Tactic:
<;>

Goal state after:
case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → LiftpPreservation

case mpr
F : Type u → Type u
q : QPF F
⊢ LiftpPreservation → SuppPreservation
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h_1
α : 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
a✝ : α
heq✝ :
  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.inl a✝
⊢ ∃ a, Sum.inl a✝ = Sum.inl a

pp: case h_2
α : 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  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✝
⊢ ∃ a_1, Sum.inl a = Sum.inl a_1

Tactic:
<;>

Goal state after:
case h_1
α : 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
a✝ : α
heq✝ :
  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.inl a✝
⊢ ∃ a, Sum.inl a✝ = Sum.inl a

case h_2
α : 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  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✝
⊢ ∃ a_1, Sum.inl a = Sum.inl a_1
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inl
α : 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 α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
e : s.think = c
⊢ s ∈ l'

pp: case cons.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 α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think ∈ l
⊢ s ∈ l'

Tactic:
<;>

Goal state after:
case cons.inl
α : 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 α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
e : s.think = c
⊢ s ∈ l'

case cons.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 α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think ∈ l
⊢ s ∈ l'