awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
⊢ ContinuousAt sinc x
have rw : ContinuousAt (dslope sin 0) x
Tactic: rw [sinc_eq_dslope]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
⊢ ContinuousAt (dslope sin 0) x
have pos : ∀ (hx : x = 0), ContinuousAt (dslope sin 0) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
pos : ∀ (hx : x = 0), ContinuousAt (dslope sin 0) x
⊢ ContinuousAt (dslope sin 0) x
have neg : ∀ (hx : ¬x = 0), ContinuousAt (dslope sin 0) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt (dslope sin 0) x
have neg : ContinuousAt sin x
Tactic: rw [continuousAt_dslope_of_ne hx]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H ↔ PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
have this : F.IsLeftAdjoint
Tactic: have := adj.isLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H ↔ PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
have refine : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H) → ∀ {K : Functor.{v, v₂, u, u₂} J D}, PreservesColimit K H
Tactic: refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {K} ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
K : Functor.{v, v₂, u, u₂} J D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ PreservesColimit K H
have refine : IsColimit (H.mapCocone ((Cocone.precompose iso.inv).obj (F.mapCocone (colimit.cocone (K ⋙ G)))))
Tactic: refine preservesColimit_of_preserves_colimit_cocone
    ((IsColimit.precomposeInvEquiv iso _).symm
      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
have this : F.IsLeftAdjoint
Tactic: have := adj.isLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
have refine : PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H) →
  ∀ {J : Type u} {x : Category.{v, u} J}, PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H
Tactic: refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {J _} ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
J : Type u
x : Category.{v, u} J
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H
have rw : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
Tactic: rw [adj.preservesColimitsOfShape_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Balanced (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
fmono : Mono f
fepi : Epi f
⊢ IsIso f
have rw : IsIso.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f.unop.op
Tactic: rw [← Quiver.Hom.op_unop f]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ Eq (α := Z ⟶ W) (g₁ ≫ (fun (a : α) ↦ i a ≫ e a) a₁) (g₂ ≫ (fun (a : α) ↦ i a ≫ e a) a₂)
have simp : (g₁ ≫ i a₁) ≫ e a₁ = (g₂ ≫ i a₂) ≫ e a₂
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ (g₁ ≫ i a₁) ≫ e a₁ = (g₂ ≫ i a₂) ≫ e a₂
have apply : (g₁ ≫ i a₁) ≫ g a₁ ≫ f a₁ = (g₂ ≫ i a₂) ≫ g a₂ ≫ f a₂
Tactic: apply w _ _ (g₁ ≫ i a₁) (g₂ ≫ i a₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ (g₁ ≫ i a₁) ≫ g a₁ ≫ f a₁ = (g₂ ≫ i a₂) ≫ g a₂ ≫ f a₂
have simp : g₁ ≫ i a₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ i a₂ ≫ g a₂ ≫ f a₂
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ g₁ ≫ i a₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ i a₂ ≫ g a₂ ≫ f a₂
have simp : (g₁ ≫ 𝟙 (X a₁)) ≫ f a₁ = (g₂ ≫ 𝟙 (X a₂)) ≫ f a₂
Tactic: simp only [← Category.assoc, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ (g a ≫ f a) ≫ EffectiveEpiFamily.desc X f (fun (a : α) ↦ i a ≫ e a) ⋯ = e a
have simp : g a ≫ i a ≫ e a = e a
Tactic: simp only [Category.assoc, EffectiveEpiFamily.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ g a ≫ i a ≫ e a = e a
have rw : ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ e a = 𝟙 (Y a) ≫ e a
Tactic: rw [← Category.id_comp (e a), ← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ e a = 𝟙 (Y a) ≫ e a
have a₁ : ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ g a ≫ f a = 𝟙 (Y a) ≫ g a ≫ f a
Tactic: apply w
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
e : (a : α) → Y a ⟶ W
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ g a ≫ f a = 𝟙 (Y a) ≫ g a ≫ f a
have a₁ : ((g a ≫ i a) ≫ g a) ≫ f a = g a ≫ f a
Tactic: simp only [Category.comp_id, Category.id_comp, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
⊢ x_1 = EffectiveEpiFamily.desc X f (fun (a : α) ↦ i a ≫ x a) ⋯
have hm₁ : ∀ (a : α), f a ≫ x_1 = i a ≫ x a
Tactic: apply EffectiveEpiFamily.uniq _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
a : α
⊢ f a ≫ x_1 = i a ≫ x a
have hm₁ : f a ≫ x_1 = i a ≫ (g a ≫ f a) ≫ x_1
Tactic: rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
a : α
hm₁ : f a ≫ x_1 = i a ≫ (g a ≫ f a) ≫ x_1
⊢ f a ≫ x_1 = i a ≫ x a
have hm₂ : f a ≫ x_1 = (i a ≫ g a ≫ f a) ≫ x_1
Tactic: rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
a : α
hm₁ : f a ≫ x_1 = i a ≫ (g a ≫ f a) ≫ x_1
hm₂ : f a ≫ x_1 = (i a ≫ g a ≫ f a) ≫ x_1
⊢ f a ≫ x_1 = i a ≫ x a
have hm₃ : f a ≫ x_1 = ((i a ≫ g a) ≫ f a) ≫ x_1
Tactic: rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
a : α
hm₁ : f a ≫ x_1 = i a ≫ (g a ≫ f a) ≫ x_1
hm₂ : f a ≫ x_1 = (i a ≫ g a ≫ f a) ≫ x_1
hm₃ : f a ≫ x_1 = ((i a ≫ g a) ≫ f a) ≫ x_1
⊢ f a ≫ x_1 = i a ≫ x a
have hm₄ : f a ≫ x_1 = (𝟙 (X a) ≫ f a) ≫ x_1
Tactic: rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst_1 : EffectiveEpiFamily X f
W : C
x : (a : α) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), (g a ≫ f a) ≫ x_1 = x a
a : α
hm₁ : f a ≫ x_1 = i a ≫ (g a ≫ f a) ≫ x_1
hm₂ : f a ≫ x_1 = (i a ≫ g a ≫ f a) ≫ x_1
hm₃ : f a ≫ x_1 = ((i a ≫ g a) ≫ f a) ≫ x_1
hm₄ : f a ≫ x_1 = (𝟙 (X a) ≫ f a) ≫ x_1
⊢ f a ≫ x_1 = i a ≫ x a
have hm₅ : f a ≫ x_1 = f a ≫ x_1
Tactic: rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : IsSplitEpi f
⊢ CategoryTheory.EffectiveEpi f
have rw : CategoryTheory.EffectiveEpi (f ≫ 𝟙 B)
Tactic: rw [← Category.comp_id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_2
inst_1 : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst_2 : EffectiveEpiFamily.{v_2, u_2, u_3} (B := X) Z fun (i : I) ↦ g i ≫ f i
inst_3 : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = φ i
have rw : g i ≫ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) sorry = g i ≫ φ i
Tactic: rw [← cancel_epi (g i), ← assoc, EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_2
inst_1 : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst_2 : EffectiveEpiFamily.{v_2, u_2, u_3} (B := X) Z fun (i : I) ↦ g i ≫ f i
inst_3 : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
rw : g i ≫ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = g i ≫ φ i
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = φ i
have rw₁ : (g i ≫ f i) ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) sorry = g i ≫ φ i
Tactic: rw [← cancel_epi (g i), ← assoc, EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_2
inst_1 : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst_2 : EffectiveEpiFamily.{v_2, u_2, u_3} (B := X) Z fun (i : I) ↦ g i ≫ f i
inst_3 : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
rw : g i ≫ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = g i ≫ φ i
rw₁ : (g i ≫ f i) ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = g i ≫ φ i
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun (i : I) ↦ g i ≫ f i) (fun (i : I) ↦ g i ≫ φ i) ⋯ = φ i
have rw₂ : g i ≫ φ i = g i ≫ φ i
Tactic: rw [← cancel_epi (g i), ← assoc, EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_2
inst_1 : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst_2 : EffectiveEpiFamily.{v_2, u_2, u_3} (B := X) Z fun (i : I) ↦ g i ≫ f i
inst_3 : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
m : X ⟶ W
hm : ∀ (a : I), f a ≫ m = φ a
i : I
⊢ (fun (i : I) ↦ g i ≫ f i) i ≫ m = g i ≫ φ i
have rw : g i ≫ f i ≫ m = g i ≫ φ i
Tactic: rw [assoc, hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_2
inst_1 : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst_2 : EffectiveEpiFamily.{v_2, u_2, u_3} (B := X) Z fun (i : I) ↦ g i ≫ f i
inst_3 : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
m : X ⟶ W
hm : ∀ (a : I), f a ≫ m = φ a
i : I
rw : g i ≫ f i ≫ m = g i ≫ φ i
⊢ (fun (i : I) ↦ g i ≫ f i) i ≫ m = g i ≫ φ i
have rw₁ : g i ≫ φ i = g i ≫ φ i
Tactic: rw [assoc, hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Comp (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
inst_1 : EffectiveEpiFamily X π
inst_2 : IsIso i
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B' ⟶ W
hm : ∀ (a : α), (π a ≫ i) ≫ m = e a
⊢ m = inv i ≫ EffectiveEpiFamily.desc X π e ⋯
have hm₁ : ∀ (a : α), π a ≫ i ≫ m = e a
Tactic: simp only [Category.assoc] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit (goal)
Goal:
K : Type v
inst : SmallCategory K
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty.{v + 1} (limit (colimit F.flip) ⟶ colimit (limit F))
⊢ IsFiltered K
have refine : ∀ {J : Type v} (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ K),
  ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
Tactic: refine IsFiltered.iff_nonempty_limit.2 (fun {J} _ _ F => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit (goal)
Goal:
K : Type v
inst : SmallCategory K
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty.{v + 1} (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ K
this : Nonempty.{v + 1} (limit (colimit (F.op ⋙ coyoneda).flip))
⊢ ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have obtain : ∀ (X : K) (y : (limit (F.op ⋙ coyoneda)).obj X), ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
Tactic: obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit (goal)
Goal:
K : Type v
inst : SmallCategory K
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty.{v + 1} (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ K
⊢ ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have suffices : Nonempty.{v + 1} (limit (colimit (F.op ⋙ coyoneda).flip))
Tactic: suffices Nonempty (limit (colimit (F.op ⋙ coyoneda).flip)) by
    obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some
    exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Equivalence (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
⊢ (functorToContAction F).essImage X
have this : ContinuousSMul.{u₁, u₁} (Aut F)
  X.obj (P :=
        Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
          fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj
Tactic: have : ContinuousSMul (Aut F) X.obj.V := X.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Equivalence (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
this :
  ContinuousSMul.{u₁, u₁} (Aut F)
    X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj
⊢ (functorToContAction F).essImage X
have obtain : ∀ (A : C)
  (i :
    (functorToAction F).obj A ≅
      X.obj (P :=
        Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
          fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))),
  (functorToContAction F).essImage X
Tactic: obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Equivalence (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
⊢ (functorToContAction F).EssSurj
have this₁ : (functorToContAction F').EssSurj
Tactic: have : (functorToContAction F').EssSurj := inferInstance