-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem baseChange_map [HasPullbacks C]
    [IsStableUnderBaseChange P] {S S' : C} (f : S' ⟶ S) {X Y : Over S} (g : X ⟶ Y)
    (H : P g.left) : P ((Over.pullback f).map g).left

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
⊢ e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left

Tactic:
ext <;> dsimp [e] <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
⊢ P ((Over.pullback f).map g).left

Tactic:
have : e.inv ≫ (pullback.snd _ _) = ((Over.pullback f).map g).left := by
  ext <;> dsimp [e] <;> simp

Result:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left
⊢ P ((Over.pullback f).map g).left

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left
⊢ P ((Over.pullback f).map g).left

Tactic:
rw [← this, P.cancel_left_of_respectsIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left
⊢ P (pullback.snd g.left (pullback.fst Y.hom f))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
⊢ P ((Over.pullback f).map g).left

Tactic:
let e :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫
    pullback.congrHom (g.w.trans (Category.comp_id _)) rfl

Result:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
⊢ P ((Over.pullback f).map g).left

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
inst✝¹ : HasPullbacks C
inst✝ : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯
this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left
⊢ P (pullback.snd g.left (pullback.fst Y.hom f))

Tactic:
exact pullback_snd _ _ H

Result:
no goals