mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → (mk ∘ dest) (mk x) = mk x

Tactic:
dsimp

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)) = corec g <$> g x

Tactic:
dsimp

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
abs_map,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> corecF g <$> abs (repr (g x)) = corec g <$> g x
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
abs_map,

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

Tactic:
abs_map,

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

Tactic:
abs_map,

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

Tactic:
abs_map,

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

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

Tactic:
dsimp

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

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

Tactic:
abs_map,

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

Tactic:
dsimp

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 } := 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
⊢ subtypeVal α.repeatEq ⊚ (toSubtype fun i ↦ α.RelLast' R i.fs) ⊚ dropFun c ⊚ diagSub =
    (TypeVec.id ⊗' TypeVec.id) ⊚ prod.diag
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
x : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
⊢ abs ⟨⟨a, f⟩.fst, fun x ↦ abs ⟨(repr (⟨a, f⟩.snd x)).fst, fun y ↦ (repr (⟨a, f⟩.snd x)).snd y⟩⟩ = abs ⟨a, f⟩

Tactic:
dsimp

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
⊢ abs ⟨a, fun x ↦ abs ⟨(repr (f x)).fst, fun y ↦ (repr (f x)).snd y⟩⟩ = abs ⟨a, f⟩
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
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
b : (P F₁).A
g : (P F₁).B b → α
h' : repr (f x) = ⟨b, g⟩
⊢ abs ⟨⟨b, g⟩.fst, fun y ↦ ⟨b, g⟩.snd y⟩ = f x

Tactic:
dsimp

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
b : (P F₁).A
g : (P F₁).B b → α
h' : repr (f x) = ⟨b, g⟩
⊢ abs ⟨b, fun y ↦ g y⟩ = f x
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 : α → β
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⟩⟩⟩

Tactic:
dsimp

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.fst, fun x ↦ abs ⟨a.snd x, fun y ↦ g ⟨x, y⟩⟩⟩
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⟩ →
    α
⊢ 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⟩⟩⟩ =
    f <$> abs ⟨⟨b, h⟩.fst, fun x ↦ abs ⟨⟨b, h⟩.snd x, fun y ↦ g ⟨x, y⟩⟩⟩

Tactic:
dsimp

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : ↑(P F) α
⊢ FG_abs (abs ((P F).map f x)) = f <$> FG_abs (abs x)

Tactic:
abs_map,

Goal state after:
F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : ↑(P F) α
⊢ FG_abs (f <$> abs x) = f <$> FG_abs (abs x)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
dsimp

Goal state after:
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.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 : β
⊢ (TypeVec.id ::: corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g)) <$$>
      Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g (Sum.inr x) =
    (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
dsimp

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

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

Tactic:
constructor <;> intro h
  · rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_uniform] at h'
    dsimp only [SuppPreservation, supp] at h
    rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
    simp
  · rintro α ⟨a, f⟩
    simp only [LiftpPreservation] at h
    simp only [supp, h]

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
rcases t' with - | t'

Goal state after:
case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
⊢ ∃ a', some a' ∈ s.destruct

case some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩

Tactic:
exact LE.fiber _ _ _ h

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False

Tactic:
exact lt_irrefl _ hij

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (↑s).drop (n + 1) = ↑(s.drop (n + 1))

Tactic:
simp only [drop, Seq.drop]

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).tail = ↑(s.drop n).tail