-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudo_pullback {P Q R : C} {f : P ⟶ R} {g : Q ⟶ R} {p : P} {q : Q} :
    f p = g q →
      ∃ s, pullback.fst f g s = p ∧ pullback.snd f g s = q :=
  Quotient.inductionOn₂ p q fun x y h => by
    obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h
    obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
      simp only [Category.assoc]
      exact comm)
    exact ⟨l, ⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
      Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩

Proof state:
case intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
exact ⟨l, ⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
  Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app (pullback.snd f g) g_1) (Over.mk l)).hom = b ≫ y.hom

Tactic:
rwa [Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app (pullback.fst f g) g_1) (Over.mk l)).hom = a ≫ x.hom

Tactic:
rwa [Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g

Tactic:
simp only [Category.assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
  simp only [Category.assoc]
  exact comm)

Result:
case intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Tactic:
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ ∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g

Tactic:
exact comm

Result:
no goals