-- Mathlib/CategoryTheory/Sites/Over.lean
lemma overEquiv_pullback {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : Sieve Y₂) :
    overEquiv _ (S.pullback f) = (overEquiv _ S).pullback f.left

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Tactic:
let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Tactic:
let d : T ⟶ W := Over.homMk b

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Tactic:
let T := Over.mk (b ≫ W.hom)

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Proof state:
case h.mp.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ ∃ Z_1 g h, S.arrows g ∧ (b ≫ a.left) ≫ f.left = h ≫ g.left

Tactic:
exact ⟨W, a ≫ f, b, h, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ c ≫ f = d ≫ a

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ (c ≫ f).left = (d ≫ a).left

Proof state:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left) → ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left

Tactic:
rintro ⟨W, a, b, h, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ ∃ Z_1 g h, S.arrows g ∧ (b ≫ a.left) ≫ f.left = h ≫ g.left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ (b ≫ a.left) ≫ f.left = b ≫ (a ≫ f).left

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
⊢ (overEquiv Y₁) (pullback f S) = pullback f.left ((overEquiv Y₂) S)

Tactic:
ext Z g

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ ((overEquiv Y₁) (pullback f S)).arrows g ↔ (pullback f.left ((overEquiv Y₂) S)).arrows g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom

Tactic:
dsimp [T]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = b ≫ W.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ g = 𝟙 Z ≫ c.left

Tactic:
simp [T, c]

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ (c ≫ f).left = (d ≫ a).left

Tactic:
exact w

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)

Tactic:
exact S.downward_closed h _

Result:
no goals

Proof state:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left) → ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Tactic:
rintro ⟨W, a, b, h, w⟩

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Tactic:
refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (c ≫ f)