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

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

Tactic:
cases cmpLE x y

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 => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

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

case gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.gt with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.gt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y 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 cmpLE x y 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:
cases cmpLE x y

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.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)

Tactic:
← abs_map,

Goal state after:
F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ abs ((P F).map (g ∘ f) (repr x)) = g <$> f <$> abs (repr x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ abs ((P F).map (g ∘ f) (repr x)) = g <$> f <$> abs (repr x)

Tactic:
← abs_map,

Goal state after:
F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ abs ((P F).map (g ∘ f) (repr x)) = g <$> abs ((P F).map f (repr x))
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)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x

Tactic:
← abs_map,

Goal state after:
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, ⋯⟩⟩) = x
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)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x

Tactic:
← abs_map,

Goal state after:
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, ⋯⟩⟩) = 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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ (TypeVec.id ::: fixToW) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
← abs_map,

Goal state after:
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 α
⊢ abs ((TypeVec.id ::: fixToW) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ (TypeVec.id ::: g₁) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    (TypeVec.id ::: g₂) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩

Tactic:
← abs_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ abs ((TypeVec.id ::: g₁) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) =
    (TypeVec.id ::: g₂) <$$> 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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ abs ((TypeVec.id ::: g₁) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) =
    (TypeVec.id ::: g₂) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩

Tactic:
← abs_map,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ abs ((TypeVec.id ::: g₁) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) =
    abs ((TypeVec.id ::: g₂) <$$> ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)
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
⊢ fixToW <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest

Tactic:
← abs_map,

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ((P F).map fixToW ⟨a, fun x ↦ ⟦f x⟧⟩) = abs (Wrepr (WType.mk a f)).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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₀⟩ = (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₁⟩

Tactic:
← abs_map,

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 ((TypeVec.id ::: Quot.mk r) <$$> ⟨a, f₀⟩) = (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₁⟩
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 ((TypeVec.id ::: Quot.mk r) <$$> ⟨a, f₀⟩) = (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₁⟩

Tactic:
← abs_map,

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 ((TypeVec.id ::: Quot.mk r) <$$> ⟨a, f₀⟩) = MvQPF.abs ((TypeVec.id ::: Quot.mk r) <$$> ⟨a, f₁⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩ = g₂ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩

Tactic:
← abs_map,

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ((P F).map g₁ ⟨a, fun x ↦ ⟦f x⟧⟩) = g₂ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ((P F).map g₁ ⟨a, fun x ↦ ⟦f x⟧⟩) = g₂ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩

Tactic:
← abs_map,

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ((P F).map g₁ ⟨a, fun x ↦ ⟦f x⟧⟩) = abs ((P F).map g₂ ⟨a, fun x ↦ ⟦f x⟧⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| Quot.factor r Mcongr this <$> Quot.mk r <$> abs x.dest

Tactic:
← abs_map,

Goal state after:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| Quot.factor r Mcongr this <$> abs ((P F).map (Quot.mk r) x.dest)
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)
⊢ Quot.mk r <$> abs ⟨a, f₀⟩ = Quot.mk r <$> abs ⟨a, f₁⟩

Tactic:
← abs_map,

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 ((P F).map (Quot.mk r) ⟨a, f₀⟩) = Quot.mk r <$> abs ⟨a, f₁⟩
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 ((P F).map (Quot.mk r) ⟨a, f₀⟩) = Quot.mk r <$> abs ⟨a, f₁⟩

Tactic:
← abs_map,

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 ((P F).map (Quot.mk r) ⟨a, f₀⟩) = abs ((P F).map (Quot.mk r) ⟨a, f₁⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (g <$> abs ⟨a, f⟩) = g '' supp (abs ⟨a, f⟩)

Tactic:
← abs_map,

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ((P F).map g ⟨a, f⟩)) = g '' supp (abs ⟨a, f⟩)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
⊢ IsTrans (WSeq α) (LiftRel R)

Tactic:
refine ⟨fun s t u h1 h2 ↦ ?_⟩

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
⊢ LiftRel R s u
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some.some
α : 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✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u✝.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
obtain ⟨ab, st⟩ := t1

Goal state after:
case some.some.some
α : 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✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u✝.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
obtain ⟨a, s'⟩ := a

Goal state after:
case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
b : α × WSeq α
dtm : some b ∈ t.destruct
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ t.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s

Tactic:
injection h2 with h'

Goal state after:
case some
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h' : o.1 = a
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
obtain ⟨a, s'⟩ := a

Goal state after:
case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)

Tactic:
obtain ⟨a, s'⟩ := a

Goal state after:
case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : α × WSeq α
mb : some b ∈ t.destruct
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some b)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
⊢ map f (ret a) = ret (f a)

Tactic:
by simp [ret]

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

Goal state before:
pp: case h2.inr.some
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
o : Option (Computation α)
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some (o, S') with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some (o, S')
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
obtain - | c := o

Goal state after:
case h2.inr.some.none
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some (none, S') with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some (none, S')
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2.inr.some.some
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some (some c, S') with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some (some c, S')
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inr
α : Type u_1
k : ℕ
h✝ : Infinite α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
cases k

Goal state after:
case inr.zero
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym α 0) = (Nat.card α).multichoose 0

case inr.succ
α : Type u_1
h✝ : Infinite α
n✝ : ℕ
⊢ Nat.card (Sym α (n✝ + 1)) = (Nat.card α).multichoose (n✝ + 1)