mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Sign

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

pp: case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Tactic:
·

Goal state after:
case inr.inl
h : sign 0 = 0
⊢ 0 = 0
Module: Mathlib.Data.Real.Sign

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

Tactic:
·

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

Goal state before:
pp: case inl
z : ℤ
hn : z < 0
⊢ (↑z).sign = ↑z.sign

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

pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
·

Goal state after:
case inl
z : ℤ
hn : z < 0
⊢ (↑z).sign = ↑z.sign
Module: Mathlib.Data.Real.Sign

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

pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
·

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

Goal state before:
pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
·

Goal state after:
case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign
Module: Mathlib.Data.Real.Sign

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

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

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

Tactic:
·

Goal state after:
case inl
r : ℝ
hn : r < 0
⊢ (-r).sign = -r.sign
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 } := ⋯
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := ⋯
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ⋯
⊢ dropFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) =
    dropFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)

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 } := ⋯
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := ⋯
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ⋯
⊢ lastFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) =
    lastFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)

Tactic:
·

Goal state after:
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 } := ⋯
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := ⋯
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ⋯
⊢ dropFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) =
    dropFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)
Module: Mathlib.Data.Real.Sign

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r

pp: case inr.inl
⊢ 0 ≤ sign 0 * 0

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
·

Goal state after:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 ≤ sign 0 * 0

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
·

Goal state after:
case inr.inl
⊢ 0 ≤ sign 0 * 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
·

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

pp: case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
·

Goal state after:
case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign
Module: Mathlib.Data.Real.Sign

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

pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
·

Goal state after:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
·

Goal state after:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign

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

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Tactic:
·

Goal state after:
case inl
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign

Tactic:
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]

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

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

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Tactic:
·

Goal state after:
case inr.inl
⊢ 0⁻¹.sign = sign 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Tactic:
·

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n

pp: case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))

Tactic:
·

Goal state after:
case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))

Tactic:
·

Goal state after:
case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))
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⟩ →
    α
⊢ f <$> abs ⟨b, fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩ = ?m.190

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⟩ →
    α
⊢ ?m.190 =
    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.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 ⟨⟨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⟩⟩⟩

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⟩ →
    α
⊢ F₂ (F₁ β)

Tactic:
·

Goal state after:
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⟩ →
    α
⊢ f <$> abs ⟨b, fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩ = ?m.190
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⟩ →
    α
⊢ ⟨b, (fun x ↦ f <$> x) ∘ fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, 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⟩).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 ⟨⟨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:
dsimp [Function.comp_def]

Goal state after:
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⟩ →
    α
⊢ ⟨b, fun x ↦ f <$> abs ⟨h x, fun y ↦ g ⟨x, 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⟩).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 ⟨⟨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⟩⟩⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) → ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ) → ∀ ⦃p : α → Prop⦄, Liftp p x → p u

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) → ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → ∀ u ∈ supp x, p u

pp: case mpr.mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∀ u ∈ supp x, p u) → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
·

Goal state after:
case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → ∀ u ∈ supp x, p u
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 ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl i) =
    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 ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inr i) =
    corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) 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 ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl i) =
    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 α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        corec
          (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
            Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)) <$$>
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
          Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
        (Sum.inl x))
    x.dest

Tactic:
dsimp [Function.comp_def]

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 α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        corec fun x ↦
          (TypeVec.id ::: fun x ↦ x) <$$>
            Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) <$$>
      (TypeVec.id ::: fun x ↦ x) <$$> (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) → u ∈ f '' univ

pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ u ∈ f '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 → α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) → u ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u

pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u
Module: Mathlib.Data.QPF.Univariate.Basic

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

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

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → IsUniform
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
⊢ IsUniform → SuppPreservation

Tactic:
·

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
⊢ IsUniform → SuppPreservation
Module: Mathlib.Data.QPF.Univariate.Basic

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

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

Tactic:
·

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
·

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

Goal state before:
pp: α : 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 : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

pp: α : 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 α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
α : 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 : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates
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 α
R : Cofix F α → Cofix F α → Prop := ⋯
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    R
      ((((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl)
        x)
      x

Tactic:
dsimp [Function.comp_def]

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 α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    R
      (corec
        (fun x ↦
          (TypeVec.id ::: fun x ↦ x) <$$>
            Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x)
        (Sum.inl x))
      x
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
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 ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inr i) =
    corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i)

Tactic:
·

Goal state after:
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 ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inr i) =
    corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i)