awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitEpi f
⊢ IsRegularEpi f

Tactic:
isRegularEpi_of_regularEpi <| RegularEpi.ofSplitEpi f

Premises used: CategoryTheory.isRegularEpi_of_regularEpi, CategoryTheory.RegularEpi.ofSplitEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
rw : gr.left ≫ g ≫ k = gr.right ≫ g ≫ k
⊢ (gr.left ≫ f) ≫ h = (gr.right ≫ f) ≫ h

Tactic:
rw [Category.assoc, Category.assoc, comm]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ gr.left ≫ g ≫ k = gr.right ≫ g ≫ k

Tactic:
simp only [← Category.assoc, eq_whisker gr.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.RegularEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
apply :
  (s : Cofork (gr.left ≫ f) (gr.right ≫ f)) →
    { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
      (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
⊢ IsColimit (Cofork.ofπ h ⋯)

Tactic:
apply Cofork.IsColimit.mk' _ _

Premises used: CategoryTheory.Limits.Cofork.IsColimit.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
rw : (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π
rw₁ : (gr.left ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
rw₂ rw₃ : (gr.right ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π

Tactic:
rw [← Category.assoc, ← Category.assoc, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π

Tactic:
have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by
      rw [← Category.assoc, ← Category.assoc, s.condition]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
obtain :
  (l : (Cofork.ofπ g ⋯).pt ⟶ s.pt) →
    (hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π) →
      { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
        (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) l₁

Premises used: CategoryTheory.RegularEpi.isColimit, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cofork.IsColimit.desc', CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
obtain :
  (p : (PushoutCocone.mk h k comm).pt ⟶ s.pt) →
    (hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π) →
      (PushoutCocone.mk h k comm).inr ≫ p = l →
        { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
          (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.desc', Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
refine : ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = p
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
refine ⟨p, hp₁, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
⊢ (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p

Tactic:
have z := w.trans hp₁.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
apply : ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p
⊢ m = p

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
⊢ Epi g

Tactic:
have := gr.epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
h₀ : (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
h₁ : (PushoutCocone.mk h k comm).inr ≫ m = (PushoutCocone.mk h k comm).inr ≫ p
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p

Tactic:
apply (PushoutCocone.mk _ _ comm).coequalizer_ext

Premises used: CategoryTheory.Limits.PushoutCocone.coequalizer_ext, CategoryTheory.Limits.PushoutCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p

Tactic:
z

Premises used: CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p

Tactic:
exact z
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
h₁ : (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p
⊢ (PushoutCocone.mk h k comm).inr ≫ m = (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
erw [← cancel_epi g, ← Category.assoc, ← eq_whisker comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
h₁ : (f ≫ h) ≫ m = (f ≫ h) ≫ p
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
erw [← Category.assoc, ← eq_whisker comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : h ≫ m = h ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p

Tactic:
simp only [Category.assoc, z]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularEpi f
⊢ StrongEpi f

Tactic:
have := isRegularEpi_of_regularEpi h
  inferInstance

Premises used: CategoryTheory.isRegularEpi_of_regularEpi, inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularEpi f
inst_1 : Mono f
⊢ IsIso f

Tactic:
have := isRegularEpi_of_regularEpi h
  isIso_of_mono_of_strongEpi _

Premises used: CategoryTheory.isRegularEpi_of_regularEpi, CategoryTheory.isIso_of_mono_of_strongEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y : C
f : X ⟶ Y
hf : RegularMono f
⊢ Eq.{v₁ + 1} (α := Opposite.op hf.Z ⟶ Opposite.op X) (hf.left.op ≫ f.op) (hf.right.op ≫ f.op)

Tactic:
simp [← op_comp, hf.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.RegularMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ⟶ Y
hf : RegularMono.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ hf.left.unop ≫ f.unop = hf.right.unop ≫ f.unop

Tactic:
simp [← unop_comp, hf.w]

Premises used: CategoryTheory.unop_comp, CategoryTheory.RegularMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y : C
f : X ⟶ Y
hf : RegularEpi f
⊢ Eq.{v₁ + 1} (α := Opposite.op Y ⟶ Opposite.op hf.W) (f.op ≫ hf.left.op) (f.op ≫ hf.right.op)

Tactic:
simp [← op_comp, hf.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.RegularEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ⟶ Y
hf : RegularEpi.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ f.unop ≫ hf.left.unop = f.unop ≫ hf.right.unop

Tactic:
simp [← unop_comp, hf.w]

Premises used: CategoryTheory.unop_comp, CategoryTheory.RegularEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsRegularMono.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ IsRegularEpi f

Tactic:
⟨fun hf ↦ ⟨⟨hf.regularMono.some.unop⟩⟩, fun hf ↦ ⟨⟨hf.regularEpi.some.op⟩⟩⟩

Premises used: CategoryTheory.IsRegularEpi.regularEpi, CategoryTheory.RegularEpi.op, CategoryTheory.RegularMono.unop, Nonempty.some, CategoryTheory.IsRegularMono.regularMono, Nonempty.intro, CategoryTheory.IsRegularEpi.mk, Iff.intro, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y : C
f : X ⟶ Y
inst_1 : IsRegularEpi f
⊢ IsRegularMono.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsRegularMono f.unop ↔ IsRegularEpi.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
⟨fun hf ↦ ⟨⟨hf.regularMono.some.op⟩⟩, fun hf ↦ ⟨⟨hf.regularEpi.some.unop⟩⟩⟩

Premises used: CategoryTheory.IsRegularEpi.regularEpi, Nonempty.some, CategoryTheory.IsRegularMono.regularMono, Nonempty.intro, CategoryTheory.RegularEpi.unop, CategoryTheory.IsRegularEpi.mk, Iff.intro, CategoryTheory.RegularMono.op, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsRegularEpi.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ IsRegularMono f.unop

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsRegularEpi.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ IsRegularMono f

Tactic:
⟨fun hf ↦ ⟨⟨hf.regularEpi.some.unop⟩⟩, fun hf ↦ ⟨⟨hf.regularMono.some.op⟩⟩⟩

Premises used: CategoryTheory.IsRegularEpi.regularEpi, Nonempty.some, CategoryTheory.IsRegularMono.regularMono, Nonempty.intro, CategoryTheory.RegularEpi.unop, CategoryTheory.IsRegularEpi.mk, Iff.intro, CategoryTheory.RegularMono.op, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y : C
f : X ⟶ Y
inst_1 : IsRegularMono f
⊢ IsRegularEpi.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsRegularEpi f.unop ↔ IsRegularMono.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
⟨fun hf ↦ ⟨⟨hf.regularEpi.some.op⟩⟩, fun hf ↦ ⟨⟨hf.regularMono.some.unop⟩⟩⟩

Premises used: CategoryTheory.IsRegularEpi.regularEpi, CategoryTheory.RegularEpi.op, CategoryTheory.RegularMono.unop, Nonempty.some, CategoryTheory.IsRegularMono.regularMono, Nonempty.intro, CategoryTheory.IsRegularEpi.mk, Iff.intro, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsRegularMono.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ IsRegularEpi f.unop

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : SplitEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
⊢ IsSplitEpi f

Tactic:
haveI := isSplitEpi_of_epi f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : SplitEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
this : IsSplitEpi f
⊢ IsRegularEpi f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : IsRegularEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
⊢ IsRegularEpi f

Tactic:
haveI := isRegularEpi_of_regularEpi <| regularEpiOfEpi f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : IsRegularEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
this : IsRegularEpi f
⊢ StrongEpi f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
n m : ℕ
h : m < n
⊢ (fun (i : ℕ) ↦ (if x : i < n then M i else N i : C)) m = M m

Tactic:
dif_pos h

Premises used: dif_pos
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
n m : ℕ
h : ¬m < n
⊢ (fun (i : ℕ) ↦ (if x : i < n then M i else N i : C)) m = N m

Tactic:
dif_neg h

Premises used: dif_neg
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
⊢ m < n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
⊢ ¬m < n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
refine_1 :
  ∀ (m : ℕ) (h : m < n), Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
refine_2 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), (if x : m < n + 1 then M m else N m) = M m
refine_3 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), N m = if x : m < n then M m else N m
refine_4 :
  ∀ (m : ℕ) (h : ¬m < n) (h' : ¬m < n + 1),
    Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
⊢ functorObj.{v_1, u_1} M N (n + 1) ⟶ functorObj.{v_1, u_1} M N n

Tactic:
refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_

Premises used: CategoryTheory.eqToHom, dite, HAdd.hAdd, LT.lt, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Limits.Pi.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
pos : m < n + 1 → M m = M m
neg : ¬m < n + 1 → N m = M m
⊢ Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
h_1 : m < n + 1
⊢ M m = M m

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
h_1 : ¬m < n + 1
⊢ N m = M m

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
h_1 : ¬m < n + 1
⊢ N m = M m

Tactic:
try lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
h_1 : m < n + 1
⊢ M m = M m

Tactic:
try rfl; try lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
refine_2 : M m = M m
⊢ (if x : m < n + 1 then M m else N m) = M m

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m

Tactic:
try rfl; try lia
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
refine_3 : N m = N m
⊢ N m = if x : m < n then M m else N m

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m

Tactic:
try rfl; try lia