awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompl t F G α α'
⊢ Eq (α := Id (bicompl t F G β β')) (bitraverse (t := t) (traverse (pure ∘ f)) (traverse (pure ∘ f')) x)
    (pure (bimap (F := t) (Functor.map f) (Functor.map f') x))

Tactic:
simp [traverse_eq_map_id', bitraverse_eq_bimap_id]

Premises used: LawfulBitraversable.bitraverse_eq_bimap_id, Traversable.traverse_eq_map_id'
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
F_1 G_1 : Type u → Type u
inst_6 : Applicative F_1
inst_7 : Applicative G_1
inst_8 : LawfulApplicative F_1
inst_9 : LawfulApplicative G_1
η : ApplicativeTransformation F_1 G_1
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompl t F G α α'
binaturality :
  η.app (t (F β) (G β')) (bitraverse (t := t) (traverse f) (traverse f') x) =
    bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x
⊢ η.app (bicompl t F G β β') (bitraverse (t := t) (traverse f) (traverse f') x) =
    bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x

Tactic:
dsimp only [bicompl]

Premises used: Function.bicompl
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
F_1 G_1 : Type u → Type u
inst_6 : Applicative F_1
inst_7 : Applicative G_1
inst_8 : LawfulApplicative F_1
inst_9 : LawfulApplicative G_1
η : ApplicativeTransformation F_1 G_1
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompl t F G α α'
⊢ η.app (t (F β) (G β')) (bitraverse (t := t) (traverse f) (traverse f') x) =
    bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x

Tactic:
simp [binaturality, naturality_pf]

Premises used: LawfulBitraversable.binaturality, Traversable.naturality_pf
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
id_bitraverse :
  ∀ {α β : Type u} (x : bicompr F t α β),
    Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β) (g' : α' → G β')
    (x : bicompr F t α α'),
    bitraverse (t := bicompr F t) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := bicompr F t) f f' <$> bitraverse (t := bicompr F t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompr F t α α'),
    Eq (α := Id (bicompr F t β β')) (bitraverse (t := bicompr F t) (pure ∘ f) (pure ∘ f') x)
      (pure (bimap (F := bicompr F t) f f' x))
binaturality :
  ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] (η : ApplicativeTransformation F_1 G) {α α' β β' : Type u} (f : α → F_1 β) (f' : α' → F_1 β')
    (x : bicompr F t α α'),
    Eq (α := G (bicompr F t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompr F t) f f' x))
      (bitraverse (t := bicompr F t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ LawfulBitraversable.{u} (bicompr F t)

Tactic:
constructor
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α β : Type u
x : bicompr F t α β
⊢ Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)

Tactic:
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]

Premises used: LawfulBitraversable.bitraverse_id_id, Bicompr.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : bicompr F t α α'
⊢ bitraverse (t := bicompr F t) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse (t := bicompr F t) f f' <$> bitraverse (t := bicompr F t) g g' x)

Tactic:
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]

Premises used: LawfulBitraversable.bitraverse_id_id, Bicompr.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompr F t α α'
bitraverse_eq_bimap_id :
  Eq (α := Id (bicompr F t β β')) (traverse (bitraverse (t := t) (pure ∘ f) (pure ∘ f')) x)
    (pure (bimap (F := bicompr F t) f f' x))
⊢ Eq (α := Id (bicompr F t β β')) (bitraverse (t := bicompr F t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := bicompr F t) f f' x))

Tactic:
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]

Premises used: LawfulBitraversable.bitraverse_id_id, Bicompr.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompr F t α α'
binaturality :
  η.app (bicompr F t β β') (traverse (bitraverse (t := t) f f') x) =
    traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x
⊢ Eq (α := G (bicompr F t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompr F t) f f' x))
    (bitraverse (t := bicompr F t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)

Tactic:
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]

Premises used: LawfulBitraversable.bitraverse_id_id, Bicompr.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompr F t α α'
bitraverse_eq_bimap_id :
  Eq (α := Id (bicompr F t β β')) (pure (bimap (F := t) f f' <$> x)) (pure (bimap (F := bicompr F t) f f' x))
⊢ Eq (α := Id (bicompr F t β β')) (traverse (bitraverse (t := t) (pure ∘ f) (pure ∘ f')) x)
    (pure (bimap (F := bicompr F t) f f' x))

Tactic:
simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]

Premises used: Traversable.traverse_eq_map_id', Function.comp_apply, LawfulBitraversable.bitraverse_eq_bimap_id'
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompr F t α α'
⊢ Eq (α := Id (bicompr F t β β')) (pure (bimap (F := t) f f' <$> x)) (pure (bimap (F := bicompr F t) f f' x))

Tactic:
rfl
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompr F t α α'
binaturality :
  η.app (F (t β β')) (traverse (bitraverse (t := t) f f') x) =
    traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x
⊢ η.app (bicompr F t β β') (traverse (bitraverse (t := t) f f') x) =
    traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x

Tactic:
dsimp only [bicompr]

Premises used: Function.bicompr
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompr F t α α'
⊢ η.app (F (t β β')) (traverse (bitraverse (t := t) f f') x) =
    traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x

Tactic:
simp [naturality, binaturality']

Premises used: LawfulTraversable.naturality, LawfulBitraversable.binaturality'
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
inst_1 : LawfulBitraversable t
α β : Type u
⊢ ∀ (x : t α β), Eq (α := Id (t α β)) (tfst (t := t) pure x) (pure x)

Tactic:
id_bitraverse

Premises used: LawfulBitraversable.id_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
inst_1 : LawfulBitraversable t
α β : Type u
⊢ ∀ (x : t α β), Eq (α := Id (t α β)) (tsnd (t := t) pure x) (pure x)

Tactic:
id_bitraverse

Premises used: LawfulBitraversable.id_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
rw : bitraverse (t := t) (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (t := t) (Comp.mk ∘ map f' ∘ f) x
⊢ Comp.mk (tfst (t := t) f' <$> tfst (t := t) f x) = tfst (t := t) (Comp.mk ∘ map f' ∘ f) x

Tactic:
rw [← comp_bitraverse]

Premises used: LawfulBitraversable.comp_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (t := t) (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (t := t) (Comp.mk ∘ map f' ∘ f) x

Tactic:
simp only [Function.comp_def, tfst, map_pure, Pure.pure]

Premises used: Pure.pure, Function.comp_def, LawfulApplicative.map_pure, Bitraversable.tfst
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
rw :
  bitraverse (t := t) (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (t := t) (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
⊢ Comp.mk (tfst (t := t) f <$> tsnd (t := t) f' x) =
    bitraverse (t := t) (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Tactic:
rw [← comp_bitraverse]

Premises used: LawfulBitraversable.comp_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (t := t) (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (t := t) (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x

Tactic:
simp only [Function.comp_def, map_pure]

Premises used: Function.comp_def, LawfulApplicative.map_pure
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
rw :
  bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
⊢ Comp.mk (tsnd (t := t) f' <$> tfst (t := t) f x) =
    bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x

Tactic:
rw [← comp_bitraverse]

Premises used: LawfulBitraversable.comp_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x

Tactic:
simp only [Function.comp_def, map_pure]

Premises used: Function.comp_def, LawfulApplicative.map_pure
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
rw : bitraverse (t := t) (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x
⊢ Comp.mk (tsnd (t := t) g' <$> tsnd (t := t) g x) = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x

Tactic:
rw [← comp_bitraverse]

Premises used: LawfulBitraversable.comp_bitraverse
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
simp :
  Eq (α := Comp F G (t α β₂))
    (bitraverse (t := t) (fun (x : α) ↦ Comp.mk (pure (pure x))) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)
    (tsnd (t := t) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)
⊢ bitraverse (t := t) (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x

Tactic:
simp only [Function.comp_def, map_pure]

Premises used: Function.comp_def, LawfulApplicative.map_pure
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Eq (α := Comp F G (t α β₂))
    (bitraverse (t := t) (fun (x : α) ↦ Comp.mk (pure (pure x))) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)
    (tsnd (t := t) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)

Tactic:
rfl
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
inst_1 : LawfulBitraversable t
α α' β : Type u
f : α → α'
x : t α β
⊢ Eq (α := Id (t α' β)) (tfst (t := t) (pure ∘ f) x) (pure (fst (F := t) f x))

Tactic:
apply bitraverse_eq_bimap_id

Premises used: LawfulBitraversable.bitraverse_eq_bimap_id
-- Module: Mathlib.Control.Bitraversable.Lemmas
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
inst_1 : LawfulBitraversable t
α β β' : Type u
f : β → β'
x : t α β
⊢ Eq (α := Id (t α β')) (tsnd (t := t) (pure ∘ f) x) (pure (snd (F := t) f x))

Tactic:
apply bitraverse_eq_bimap_id

Premises used: LawfulBitraversable.bitraverse_eq_bimap_id
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
⊢ Eq (α := Unique α → Unique α) (⇑(Equiv.refl α).uniqueCongr : (a : Unique α) → Unique α) id

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
⊢ ∀ {α β γ : Type u_1} (k : α ≃ β) (h : β ≃ γ),
    Eq (α := Unique α → Unique γ) (⇑(k.trans h).uniqueCongr : (a : Unique α) → Unique γ)
      (Function.comp (β := Unique β) (⇑h.uniqueCongr : (a : Unique β) → Unique γ)
        (⇑k.uniqueCongr : (a : Unique α) → Unique β))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
h :
  ∀ (x : Perm α) (x_1 : α),
    Eq (α := α) ((((Equiv.refl α).symm.trans x).trans (Equiv.refl α) : (a : α) → α) x_1 : α)
      ((id x : (a : α) → α) x_1 : α)
⊢ Eq.{u_1 + 1} (α := Perm α → Perm α) (fun (p : Perm α) ↦ ((Equiv.refl α).symm.trans p).trans (Equiv.refl α)) id

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
x : Perm α
x_1 : α
⊢ Eq (α := α) ((((Equiv.refl α).symm.trans x).trans (Equiv.refl α) : (a : α) → α) x_1 : α)
    ((id x : (a : α) → α) x_1 : α)

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
x : α ≃ β
x_1 : β ≃ γ
h :
  ∀ (x_2 : Perm α) (x_3 : γ),
    Eq (α := γ) ((((x.trans x_1).symm.trans x_2).trans (x.trans x_1) : (a : γ) → γ) x_3 : γ)
      ((((fun (p : Perm β) ↦ (x_1.symm.trans p).trans x_1) ∘ fun (p : Perm α) ↦ (x.symm.trans p).trans x) x_2 :
            (a : γ) → γ)
          x_3 :
        γ)
⊢ Eq.{u_1 + 1} (α := Perm α → Perm γ) (fun (p : Perm α) ↦ ((x.trans x_1).symm.trans p).trans (x.trans x_1))
    ((fun (p : Perm β) ↦ (x_1.symm.trans p).trans x_1) ∘ fun (p : Perm α) ↦ (x.symm.trans p).trans x)

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
x : α ≃ β
x_1 : β ≃ γ
x_2 : Perm α
x_3 : γ
⊢ Eq (α := γ) ((((x.trans x_1).symm.trans x_2).trans (x.trans x_1) : (a : γ) → γ) x_3 : γ)
    ((((fun (p : Perm β) ↦ (x_1.symm.trans p).trans x_1) ∘ fun (p : Perm α) ↦ (x.symm.trans p).trans x) x_2 :
          (a : γ) → γ)
        x_3 :
      γ)

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
h : ∀ (x : Finset α) (a : α), a ∈ Finset.map (Equiv.refl α).toEmbedding x ↔ a ∈ id x
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α) (fun (s : Finset α) ↦ Finset.map (Equiv.refl α).toEmbedding s) id

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
x : Finset α
a : α
⊢ a ∈ Finset.map (Equiv.refl α).toEmbedding x ↔ a ∈ id x

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
h₁ :
  ∀ (x : Finset α) (a : γ),
    a ∈ Finset.map (k.trans h).toEmbedding x ↔
      Membership.mem (γ := Finset γ)
        (((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s) x) a
⊢ Eq.{u_1 + 1} (α := Finset α → Finset γ) (fun (s : Finset α) ↦ Finset.map (k.trans h).toEmbedding s)
    ((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s)

Tactic:
ext _ a
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h₁ :
  (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) ↔
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
⊢ a ∈ Finset.map (k.trans h).toEmbedding x ↔
    Membership.mem (γ := Finset γ)
      (((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s) x) a

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h₁ :
  (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) →
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
h₂ :
  Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) →
    ∃ a_2 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_2 : β) = a
⊢ (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) ↔
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)

Tactic:
constructor
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h' : ∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a
h₁ :
  ∀ (a_1 : α) (ha₁ : a_1 ∈ x) (ha₂ : (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a),
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
⊢ Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)

Tactic:
let ⟨a, ha₁, ha₂⟩ := h'
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a_1 : γ
h' : ∃ a ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
a : α
ha₁ : a ∈ x
ha₂ : (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
h₁ :
  Membership.mem (α := α) x
    ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) ((h : (a : β) → γ) ((k : (a : α) → β) a : β) : γ) : β) : α)
⊢ Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a_1 : β) : α)

Tactic:
rw [← ha₂]
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a_1 : γ
h' : ∃ a ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
a : α
ha₁ : a ∈ x
ha₂ : (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
⊢ Membership.mem (α := α) x
    ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) ((h : (a : β) → γ) ((k : (a : α) → β) a : β) : γ) : β) : α)

Tactic:
simpa
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h' : Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
h₁ :
  Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) ∧
    (h : (a : β) → γ) ((k : (a : α) → β) ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) : β) = a
⊢ ∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a

Tactic:
exists (Equiv.symm k) ((Equiv.symm h) a)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h' : Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
⊢ Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) ∧
    (h : (a : β) → γ) ((k : (a : α) → β) ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) : β) = a

Tactic:
simp [h']
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
h : ∀ (x : Fintype α), Fintype.ofBijective (⇑(Equiv.refl α) : (a : α) → α) ⋯ = id x
⊢ Eq.{u_1 + 1} (α := Fintype α → Fintype α)
    (fun (x : Fintype α) ↦ Fintype.ofBijective (⇑(Equiv.refl α) : (a : α) → α) ⋯) id

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
α : Type u_1
x : Fintype α
⊢ Fintype.ofBijective (⇑(Equiv.refl α) : (a : α) → α) ⋯ = id x

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Control.EquivFunctor.Instances
Goal:
⊢ ∀ {α β γ : Type u_1} (k : α ≃ β) (h : β ≃ γ),
    Eq.{u_1 + 1} (α := Fintype α → Fintype γ) (fun (x : Fintype α) ↦ Fintype.ofBijective (⇑(k.trans h) : (a : α) → γ) ⋯)
      ((fun (x : Fintype β) ↦ Fintype.ofBijective (⇑h : (a : β) → γ) ⋯) ∘ fun (x : Fintype α) ↦
        Fintype.ofBijective (⇑k : (a : α) → β) ⋯)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton