awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
have rw : PreservesFiniteProducts (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w))) ∧
  EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
Tactic: rw [Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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)))
have refine : EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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)
⊢ EqualizerCondition (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
have 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))
Tactic: apply +allowSynthFailures equalizerCondition_yonedaPresheaf
      (CompHausLike.compHausLikeToTop.{u} P) X
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ @p1 = @p2
have h : ∀ (α : Type u) (x : α), p1 x = p2 x
Tactic: funext α x
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p2, seq := s2, seqLeft := sl2, seqRight := sr2 }
have 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 }
Tactic: obtain rfl : @p1 = @p2 := by
      funext α x
      apply H1
Cleared hypotheses: p2, L2, H1, H2
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ @s1 = @s2
have h : ∀ (α β : Type u) (f : F (α → β)) (x : Unit → F α), s1 f x = s2 f x
Tactic: funext α β f x
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s2, seqLeft := sl2, seqRight := sr2 }
have 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 }
Tactic: obtain rfl : @s1 = @s2 := by
      funext α β f x
      exact H2 f (x Unit.unit)
Cleared hypotheses: s2, L2, H1, H2
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have toLawfulFunctor : LawfulFunctor F
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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)
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
Tactic: obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have toLawfulFunctor : LawfulFunctor F
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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_1 : 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
toLawfulFunctor : LawfulFunctor F
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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_1 : 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
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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_1 : 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
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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_1 : 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
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2