mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `Z)
   []
   [(Term.typeSpec ":" (Term.arrow `S "→" (Term.app `Set [`Y])))]
   ":="
   (Term.fun
    "fun"
    (Term.basicFun
     [`i]
     []
     "↦"
     (Set.term_''_
      `f
      "''"
      (Set.«term_⁻¹'_»
       `g
       "⁻¹'"
       (choice
        («term{_}» "{" [`i] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields [(Term.structInstField (Term.structInstLVal `i []) [])])
         (Term.optEllipsis [])
         []
         "}")))))))))

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
y : Y
a✝ : y ∈ univ
s : S
hs : f' s = g' y
⊢ ∃ i, y ∈ D i

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ x ∈ C i ∩ C j

Tactic:
grind

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
x✝³ x✝² : CompHausᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (x✝¹ ≫ (CompHausLike.const (of PUnit.{u + 1}) s).op))) x✝,
      continuous_toFun := ⋯ } =
    (ConcreteCategory.hom (↾fun g ↦ g.comp (TopCat.Hom.hom x✝¹.unop.hom)))
      { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x✝,
        continuous_toFun := ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (fun x ↦ Comp.mk (pure (pure x))) (fun x ↦ Comp.mk (g' <$> g x)) x = tsnd (fun x ↦ Comp.mk (g' <$> g x)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
f✝ : β → γ
α✝ β✝ : Type u
f : Id (α✝ → β✝)
x : Id α✝
⊢ pure (f <*> x) = pure (f x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ Functor.Comp.mk ((fun a ↦ (fun x2 ↦ Prod.mk <$> f✝ a <*> x2) ∘ f'✝) <$> g✝ fst✝ <*> g'✝ snd✝) =
    Functor.Comp.mk ((fun a ↦ Prod.bitraverse f✝ f'✝ ∘ Prod.mk a) <$> g✝ fst✝ <*> g'✝ snd✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ pure (f✝ fst✝, f'✝ snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α✝
⊢ pure (Sum.inl (f✝ x✝)) = pure (bimap f✝ f'✝ (Sum.inl x✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α'✝
⊢ pure (Sum.inr (f'✝ x✝)) = pure (bimap f✝ f'✝ (Sum.inr x✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : Const α✝ β✝
⊢ pure x✝ = pure x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : Const α✝ α'✝
⊢ (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (f✝ <$> g✝ x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : Const α✝ α'✝
⊢ (pure ∘ f✝) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : Const α✝ α'✝
⊢ η✝.app (Const β✝ β'✝) (f✝ x✝) = (η✝.app β✝ ∘ f✝) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ pure (bimap f✝ f'✝ <$> x✝) = pure (bimap f✝ f'✝ x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ none = Fix.approx f 0 x

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
α : Type u_1
⊢ Option.traverse pure none = pure none

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case some
α : Type u_1
val✝ : α
⊢ Option.traverse pure (some val✝) = pure (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
α β : Type u_1
f : α → β
⊢ Option.traverse (pure ∘ f) none = pure (f <$> none)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case some
α β : Type u_1
f : α → β
val✝ : α
⊢ Option.traverse (pure ∘ f) (some val✝) = pure (f <$> some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk ((fun a ↦ (fun x2 ↦ cons <$> f a <*> x2) ∘ List.traverse f) <$> g head✝ <*> List.traverse g tail✝) =
    Comp.mk ((fun a ↦ List.traverse f ∘ cons a) <$> g head✝ <*> List.traverse g tail✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ (match g <$> inl val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    pure (inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ (match g <$> inr val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    inr <$> f (g val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α : Type u_1
val✝ : σ
⊢ Sum.traverse pure (inl val✝) = inl val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ α : Type u_1
val✝ : α
⊢ Sum.traverse pure (inr val✝) = inr val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ pure (inl val✝) = Comp.mk (pure (pure (inl val✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ pure (inl val✝) = pure (f <$> inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ pure (inr (f val✝)) = pure (f <$> inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ op (↾fun a ↦ List.foldl f (List.foldl f a (FreeMonoid.toList x✝)) (FreeMonoid.toList y✝)) =
    op (↾fun a ↦ List.foldl f a (FreeMonoid.toList x✝)) * op (↾fun a ↦ List.foldl f a (FreeMonoid.toList y✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n n✝ : ℕ
⊢ ofFin fz.toFin = fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (fun a ↦ f a x) = fun a ↦ f a x

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case nil
α : Type u
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) Fin2.fz ⟨x, property✝⟩) = ↑(TypeVec.id Fin2.fz ⟨x, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) a✝.fs ⟨x, property✝⟩) = ↑(TypeVec.id a✝.fs ⟨x, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (α.PredLast' P Fin2.fz x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α Fin2.fz ⟨x, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : ofRepeat (α.PredLast' P a✝.fs x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α a✝.fs ⟨x, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) Fin2.fz ⟨x, property✝⟩ = TypeVec.id Fin2.fz ⟨x, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) a✝.fs ⟨x, property✝⟩ = TypeVec.id a✝.fs ⟨x, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).1

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).1

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_b.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).2

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_b.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).2

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ (α.drop ::: α.last) Fin2.fz = α Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
a✝ : Fin2 n
⊢ (α.drop ::: α.last) a✝.fs = α a✝.fs

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ : Type u_1
x✝ : ContT r m α✝
⊢ id <$> x✝ = x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
f✝¹ : α✝ → ContT r m β✝
f✝ : β✝ → m r
⊢ (pure x✝ >>= f✝¹).run f✝ = (f✝¹ x✝).run f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ γ✝ : Type u_1
x✝ : ContT r m α✝
f✝¹ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
f✝ : γ✝ → m r
⊢ (x✝ >>= f✝¹ >>= g✝).run f✝ = (x✝ >>= fun x ↦ f✝¹ x >>= g✝).run f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ ω✝ γ✝ : Type u_1
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
f✝ : ω✝ → m r
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f).run f✝ =
    (do
          let x ← cmd✝
          callCC fun f ↦ next✝ f x).run
      f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
f✝ : α✝ → m r
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f).run f✝ = (pure x✝).run f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
dummy✝ : ContT r m α✝
f✝ : α✝ → m r
⊢ (callCC fun x ↦ dummy✝).run f✝ = dummy✝.run f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case refl.refl.refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 nilFun

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ (ExceptT.mk (pure (Except.ok x✝))).run = (pure x✝).run

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (ExceptT.mk dummy✝.run).run = dummy✝.run

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = mk fun s ↦ goto { apply := apply✝ } (i, s)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) Fin2.fz = (TypeVec.const x α ::: fun x_1 ↦ x) Fin2.fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a✝ : Fin2 n
⊢ TypeVec.const x (α ::: β) a✝.fs = (TypeVec.const x α ::: fun x_1 ↦ x) a✝.fs

Tactic:
rfl

Goal state after: