mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom
        (Y.map
          ((sigmaIncl f
                (Fiber.mk (⇑f)
                  ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a)))).op ≫
            (componentHom f g.unop a).op)))
      ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f)

Tactic:
Functor.map_comp_apply,

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom (Y.map (componentHom f g.unop a).op))
      ((ConcreteCategory.hom
          (Y.map
            (sigmaIncl f
                (Fiber.mk (⇑f)
                  ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a)))).op))
        ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
⊢ ∃ h, f ≫ h = g

Tactic:
have h_down (n : ℕ) : f ≫ (k_seq n).val = g ≫ lightToProfinite.map (S.proj n) :=
      (k_seq n).prop

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod

Tactic:
constructor <;> intros

Goal state after:
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✝ : α✝ × β✝
⊢ bitraverse pure pure x✝ = pure x✝

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✝ : α✝ × α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

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✝ : α✝ × α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

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✝ : α✝ × α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Sum

Tactic:
constructor <;> intros

Goal state after:
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✝ : α✝ ⊕ β✝
⊢ bitraverse pure pure x✝ = pure x✝

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✝ : α✝ ⊕ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

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✝ : α✝ ⊕ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

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✝ : α✝ ⊕ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h✝ : lightToProfinite.map f ≫ h = lightToProfinite.map g
⊢ ∃ h, f ≫ h = g

Tactic:
refine ⟨lightToProfiniteFullyFaithful.preimage h, ?_⟩

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h✝ : lightToProfinite.map f ≫ h = lightToProfinite.map g
⊢ f ≫ lightToProfiniteFullyFaithful.preimage h = g
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Const

Tactic:
constructor <;> intros

Goal state after:
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 α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

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 α✝ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

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 α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

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 α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (_root_.flip t)

Tactic:
constructor <;> intros

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : _root_.flip t α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

case binaturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ LawfulTraversable (t α)

Tactic:
constructor <;> intros

Goal state after:
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ : Type u
x✝ : t α α✝
⊢ traverse pure x✝ = pure x✝

case comp_traverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t α α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)

case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ traverse (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)

case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ (fun {α} ↦ η✝.app α) (traverse f✝ x✝) = traverse ((fun {α} ↦ η✝.app α) ∘ f✝) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompl t F G)

Tactic:
constructor <;> intros

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : bicompl t F G α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
constructor <;> intros

Goal state after:
case id_bitraverse
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
x✝ : bicompr F t α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

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 α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Data.Fin.Fin2

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

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x

Tactic:
by
      simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f),
        foldlm.ofFreeMonoid_comp_of, foldlM.get, FreeMonoid.ofList_toList]

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

Goal state before:
pp: case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)

Tactic:
apply (h₁ u).mp h₂

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.snd Fin2.fz (prod.mk Fin2.fz a b) = b

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x y : α Fin2.fz
⊢ ofRepeat (α.repeatEq Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : α Fin2.fz
⊢ (subtypeVal α.repeatEq ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a

Tactic:
| fz =>

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
h : 2 ^ (w + 1) = ↑(2 ^ (w + 1))
⊢ (z % ↑(2 ^ (w + 1))).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

Tactic:
Int.emod_bmod

Goal state after:
z : ℤ
w : ℕ
h : 2 ^ (w + 1) = ↑(2 ^ (w + 1))
⊢ z.bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ a ∈ s >>= fun x ↦ f x >>= g

Tactic:
by
    simp only [bind_def, mem_bind]
    exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,
      fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

Tactic:
by
  induction xs generalizing s with
  | nil => simp [enum, eq_empty_iff_forall_notMem]
  | cons x xs ih =>
      simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]
      refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
      simp only [or_iff_not_imp_left] at hs
      simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Fintype.card (Perm α) = (Nat.card α)!
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Fintype.card (Perm α) = (Nat.card α)!

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Fintype.card (Perm α) = (Fintype.card α)!
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ ¬∃ a b c, a ∈ _root_.Set.univ ∧ b ∈ _root_.Set.univ ∧ c ∈ _root_.Set.univ ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩

Goal state after:
α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left✝² : a ∈ _root_.Set.univ
left✝¹ : b ∈ _root_.Set.univ
left✝ : c ∈ _root_.Set.univ
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))

Tactic:
| cons hd tl =>

Goal state after: