awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 2 = 𝟙 ((mk₃ f₁₂ f₃ f₄).obj 2)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 3 = 𝟙 ((mk₃ f₁₂ f₃ f₄).obj 3)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
simp : (g₁ ≫ i a₁) ≫ e a₁ = (g₂ ≫ i a₂) ≫ e a₂
⊢ Eq (α := Z ⟶ W) (g₁ ≫ (fun (a : α) ↦ i a ≫ e a) a₁) (g₂ ≫ (fun (a : α) ↦ i a ≫ e a) a₂)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
apply : (g₁ ≫ i a₁) ≫ g a₁ ≫ f a₁ = (g₂ ≫ i a₂) ≫ g a₂ ≫ f a₂
⊢ (g₁ ≫ i a₁) ≫ e a₁ = (g₂ ≫ i a₂) ≫ e a₂

Tactic:
apply w _ _ (g₁ ≫ i a₁) (g₂ ≫ i a₂)

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
simp : g₁ ≫ i a₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ i a₂ ≫ g a₂ ≫ f a₂
⊢ (g₁ ≫ i a₁) ≫ g a₁ ≫ f a₁ = (g₂ ≫ i a₂) ≫ g a₂ ≫ f a₂

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
simp : (g₁ ≫ 𝟙 (X a₁)) ≫ f a₁ = (g₂ ≫ 𝟙 (X a₂)) ≫ f a₂
⊢ g₁ ≫ i a₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ i a₂ ≫ g a₂ ≫ f a₂

Tactic:
simp only [← Category.assoc, hi]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₁ ≫ 𝟙 (X a₁)) ≫ f a₁ = (g₂ ≫ 𝟙 (X a₂)) ≫ f a₂

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 : α
simp : g a ≫ i a ≫ e a = e a
⊢ (g a ≫ f a) ≫ EffectiveEpiFamily.desc X f (fun (a : α) ↦ i a ≫ e a) ⋯ = e a

Tactic:
simp only [Category.assoc, EffectiveEpiFamily.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.EffectiveEpiFamily.fac
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 : α
rw : ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ e a = 𝟙 (Y a) ≫ e a
⊢ g a ≫ i a ≫ e a = e a

Tactic:
rw [← Category.id_comp (e a), ← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 : α
a₁ : ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ g a ≫ f a = 𝟙 (Y a) ≫ g a ≫ f a
⊢ ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ e a = 𝟙 (Y a) ≫ e a

Tactic:
apply w
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 : α
a₁ : ((g a ≫ i a) ≫ g a) ≫ f a = g a ≫ f a
⊢ ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ g a ≫ f a = 𝟙 (Y a) ≫ g a ≫ f a

Tactic:
simp only [Category.comp_id, Category.id_comp, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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) ≫ g a) ≫ f a = g a ≫ f a

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
hm₁ : ∀ (a : α), f a ≫ x_1 = i a ≫ x a
⊢ x_1 = EffectiveEpiFamily.desc X f (fun (a : α) ↦ i a ≫ x a) ⋯

Tactic:
apply EffectiveEpiFamily.uniq _ f

Premises used: CategoryTheory.EffectiveEpiFamily.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
hm₅ hm₆ : f a ≫ x_1 = f a ≫ x_1
⊢ f a ≫ x_1 = i a ≫ x a

Tactic:
rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
inst_1 : ∀ (a : α), IsSplitEpi (g a)
inst_2 : EffectiveEpiFamily X f
⊢ EffectiveEpiFamily.{v_1, u_1, u_2} (B := B) Y fun (a : α) ↦ g a ≫ f a

Tactic:
⟨⟨effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi f g⟩⟩

Premises used: Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk, CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X Y : C
f : X ⟶ B
g : Y ⟶ X
inst_1 : IsSplitEpi g
inst_2 : EffectiveEpi f
⊢ EffectiveEpi (g ≫ f)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : IsSplitEpi f
rw : CategoryTheory.EffectiveEpi (f ≫ 𝟙 B)
⊢ CategoryTheory.EffectiveEpi f

Tactic:
rw [← Category.comp_id f]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 ≫ 𝟙 B)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : Eq (α := T ⟶ X) (g₁ ≫ (fun (i : I) ↦ g i ≫ f i) i₁) (g₂ ≫ (fun (i : I) ↦ g i ≫ f i) i₂)
⊢ (g₁ ≫ g i₁) ≫ f i₁ = (g₂ ≫ g i₂) ≫ f i₂

Tactic:
simpa [assoc] using eq

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : Eq (α := T ⟶ X) (g₁ ≫ (fun (i : I) ↦ g i ≫ f i) i₁) (g₂ ≫ (fun (i : I) ↦ g i ≫ f i) i₂)
⊢ Eq (α := T ⟶ W) (g₁ ≫ (fun (i : I) ↦ g i ≫ φ i) i₁) (g₂ ≫ (fun (i : I) ↦ g i ≫ φ i) i₂)

Tactic:
simpa [assoc] using h i₁ i₂ (g₁ ≫ g i₁) (g₂ ≫ g i₂) (by simpa [assoc] using eq)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
rw₂ rw₃ : 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

Tactic:
rw [← cancel_epi (g i), ← assoc, EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.EffectiveEpiFamily.fac, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
rw₁ rw₂ : g i ≫ φ i = g i ≫ φ i
⊢ (fun (i : I) ↦ g i ≫ f i) i ≫ m = g i ≫ φ i

Tactic:
rw [assoc, hm]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
inst_1 : ∀ (a : α), Epi (g a)
inst_2 : EffectiveEpiFamily.{v_1, u_1, u_2} (B := B) Y fun (a : α) ↦ g a ≫ f a
⊢ EffectiveEpiFamily X f

Tactic:
⟨⟨effectiveEpiFamilyStructOfComp g f⟩⟩

Premises used: CategoryTheory.effectiveEpiFamilyStructOfComp, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X Y : C
f : X ⟶ B
g : Y ⟶ X
inst_1 : Epi g
inst_2 : EffectiveEpi (g ≫ f)
⊢ EffectiveEpi f

Tactic:
have := (effectiveEpi_iff_effectiveEpiFamily (g ≫ f)).mp inferInstance
  have := effectiveEpiFamily_of_effectiveEpi_epi_comp
    (X := fun () ↦ X) (Y := fun () ↦ Y) (fun () ↦ f) (fun () ↦ g)
  inferInstance

Premises used: CategoryTheory.effectiveEpiFamily_of_effectiveEpi_epi_comp, inferInstance, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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'
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₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂

Tactic:
grind
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : α
⊢ (π x_1 ≫ i) ≫ inv i ≫ EffectiveEpiFamily.desc X π x ⋯ = x x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
⊢ ∀ (a : α), π a ≫ i ≫ m = e a

Tactic:
simp only [Category.assoc] at hm

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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 ⋯

Tactic:
simp [← EffectiveEpiFamily.uniq X π e
      (effectiveEpiFamilyStructCompIso_aux X π i e h) (i ≫ m) hm]

Premises used: CategoryTheory.EffectiveEpiFamily.uniq, CategoryTheory.effectiveEpiFamilyStructCompIso_aux, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
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
⊢ EffectiveEpiFamily.{v_1, u_1, u_2} (B := B') X fun (a : α) ↦ π a ≫ i

Tactic:
⟨⟨effectiveEpiFamilyStructCompIso X π i⟩⟩

Premises used: CategoryTheory.effectiveEpiFamilyStructCompIso, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Comp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X Y : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
i : (a : α) → Y a ⟶ X a
inst_2 : ∀ (a : α), IsIso (i a)
⊢ EffectiveEpiFamily.{v_1, u_1, u_2} (B := B) Y fun (a : α) ↦ i a ≫ π a

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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

Tactic:
IsFiltered.iff_nonempty_limit.2 (fun {J} _ _ F => ?_)

Premises used: Iff.mpr, CategoryTheory.IsFiltered.iff_nonempty_limit
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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))
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))
⊢ IsFiltered K

Tactic:
refine IsFiltered.iff_nonempty_limit.2 (fun {J} _ _ F => ?_)

Premises used: Iff.mpr, CategoryTheory.IsFiltered.iff_nonempty_limit
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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))
obtain :
  ∀ (X : K) (y : (limit (F.op ⋙ coyoneda)).obj X), ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda 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

Premises used: CategoryTheory.Functor.op, CategoryTheory.coyoneda, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, Nonempty.some, Nonempty.map, CategoryTheory.Limits.Types.jointly_surjective', DFunLike.coe
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.coyoneda, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, Nonempty.intro, Exists.intro, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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
suffices : Nonempty.{v + 1} (limit (colimit (F.op ⋙ coyoneda).flip))
⊢ ∃ (X : K), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

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⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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_2 : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun (j : Jᵒᵖ) ↦
    Equiv.unique
      (Iso.toEquiv
        (Iso.trans (Y := colimit ((F.op ⋙ coyoneda).flip ⋙ Functor.obj (evaluation Jᵒᵖ (Type v)) j))
          (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j :
            (colimit (F.op ⋙ coyoneda).flip).obj j ≅
              colimit ((F.op ⋙ coyoneda).flip ⋙ Functor.obj (evaluation Jᵒᵖ (Type v)) j))
          (Coyoneda.colimitCoyonedaIso (F.op.obj j) : colimit (Functor.obj coyoneda (F.op.obj j)) ≅ PUnit.{v + 1})))
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) ((colimit (F.op ⋙ coyoneda).flip).obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((colimit (F.op ⋙ coyoneda).flip).map f) :
          (a : (fun (X : Type v) ↦ X) ((colimit (F.op ⋙ coyoneda).flip).obj j)) →
            (fun (X : Type v) ↦ X) ((colimit (F.op ⋙ coyoneda).flip).obj j'))
        ((fun (j : Jᵒᵖ) ↦ (default : (colimit (F.op ⋙ coyoneda).flip).obj j)) j))
      ((fun (j : Jᵒᵖ) ↦ (default : (colimit (F.op ⋙ coyoneda).flip).obj j)) j')

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit
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_2 : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun (j : Jᵒᵖ) ↦
    Equiv.unique
      (Iso.toEquiv
        (Iso.trans (Y := colimit ((F.op ⋙ coyoneda).flip ⋙ Functor.obj (evaluation Jᵒᵖ (Type v)) j))
          (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j :
            (colimit (F.op ⋙ coyoneda).flip).obj j ≅
              colimit ((F.op ⋙ coyoneda).flip ⋙ Functor.obj (evaluation Jᵒᵖ (Type v)) j))
          (Coyoneda.colimitCoyonedaIso (F.op.obj j) : colimit (Functor.obj coyoneda (F.op.obj j)) ≅ PUnit.{v + 1})))
⊢ Nonempty.{v + 1} (limit (colimit (F.op ⋙ coyoneda).flip))

Tactic:
exact ⟨Types.Limit.mk (colimit (F.op ⋙ coyoneda).flip) (fun j => default) (by subsingleton)⟩
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
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
⊢ (functorToContAction F).Faithful

Tactic:
inferInstanceAs <| (ObjectProperty.lift _ _ _).Faithful

Premises used: _private.0.CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction._proof_1