awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
x : (↑(G.obj (unop (op B))) : Type w)
y : (↑(G.obj Z) : Type w)
hy :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
          (G.map π) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
      y =
    x
⊢ Eq.{w' + 1} (α := X)
    ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)

Tactic:
exact congr_fun h y

Premises used: congr_fun
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : PreservesFiniteCoproducts G
⊢ PreservesFiniteProducts (yonedaPresheaf G X)

Tactic:
have := preservesFiniteProducts_op G
  ⟨fun _ ↦ comp_preservesLimitsOfShape G.op (yonedaPresheaf' X)⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.comp_preservesLimitsOfShape, CategoryTheory.Limits.preservesFiniteProducts_op, CategoryTheory.Limits.PreservesFiniteProducts.mk, ContinuousMap.yonedaPresheaf'
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
⊢ Preregular.{u, u + 1} (CompHausLike P)

Tactic:
have := CompHausLike.preregular hs
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
rw :
  PreservesFiniteProducts (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w))) ∧
    EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))

Tactic:
rw [Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ PreservesFiniteProducts (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w))) ∧
    EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))

Tactic:
⟨inferInstance, ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
refine : EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
⊢ PreservesFiniteProducts (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w))) ∧
    EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))

Tactic:
refine ⟨inferInstance, ?_⟩
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
apply :
  ∀ (Z B : CompHausLike P) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑((CompHausLike.compHausLikeToTop P).obj Z) : Type u)) (Y :=
      (↑((CompHausLike.compHausLikeToTop P).obj B) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            ((CompHausLike.compHausLikeToTop P).map π)) :
        (a : (↑((CompHausLike.compHausLikeToTop P).obj Z) : Type u)) →
          (↑((CompHausLike.compHausLikeToTop P).obj B) : Type u))
⊢ EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))

Tactic:
apply +allowSynthFailures equalizerCondition_yonedaPresheaf
      (CompHausLike.compHausLikeToTop.{u} P) X
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
this : Preregular.{u, u + 1} (CompHausLike P)
Z B : CompHausLike P
π : Z ⟶ B
he : EffectiveEpi π
⊢ IsQuotientMap (X := (↑((CompHausLike.compHausLikeToTop P).obj Z) : Type u)) (Y :=
    (↑((CompHausLike.compHausLikeToTop P).obj B) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((CompHausLike.compHausLikeToTop P).map π)) :
      (a : (↑((CompHausLike.compHausLikeToTop P).obj Z) : Type u)) →
        (↑((CompHausLike.compHausLikeToTop P).obj B) : Type u))

Tactic:
apply IsQuotientMap.of_surjective_continuous (hs _ he) π.hom.hom.continuous

Premises used: ContinuousMap.continuous, IsQuotientMap.of_surjective_continuous, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ f <$> x <*> g <$> y = ((fun (x : β → γ) ↦ x ∘ g) ∘ f) <$> x <*> y

Tactic:
simp [functor_norm, Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
α β : Type u
f : α → β
⊢ Eq.{v + 1} (α := F α → F β) (fun (x : F α) ↦ pure f <*> x) fun (x : F α) ↦ f <$> x

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
h : ∀ (α : Type u) (x : α), p1 x = p2 x
⊢ @p1 = @p2

Tactic:
funext α x
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α : Type u
x : α
⊢ p1 x = p2 x

Tactic:
apply H1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
obtain :
  ∀ (L2 : LawfulApplicative F) (H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x))
    (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x),
    Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
      { toFunctor := F2, pure := p1, seq := s2, seqLeft := sl2, seqRight := sr2 }
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p2, seq := s2, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain rfl : @p1 = @p2 := by
      funext α x
      apply H1

Premises used: rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
h : ∀ (α β : Type u) (f : F (α → β)) (x : Unit → F α), s1 f x = s2 f x
⊢ @s1 = @s2

Tactic:
funext α β f x
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x

Tactic:
H2 f (x Unit.unit)

Premises used: Unit.unit
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x

Tactic:
exact H2 f (x Unit.unit)

Premises used: Unit.unit
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
obtain :
  ∀ (L2 : LawfulApplicative F) (H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x))
    (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x),
    Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
      { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s2, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain rfl : @s1 = @s2 := by
      funext α β f x
      exact H2 f (x Unit.unit)

Premises used: rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ LawfulFunctor F

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
⊢ ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
⊢ ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
⊢ ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
⊢ ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
⊢ ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x

Tactic:
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ LawfulFunctor F

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2