-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_isoClosure : W P.isoClosure = W P

Proof state:
case h.mpr.intro.intro.intro.right.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
a : Y ⟶ Z'
h : (fun g => f ≫ g) a = g ≫ e.hom
⊢ ∃ a, (fun g => f ≫ g) a = g

Tactic:
exact ⟨a ≫ e.inv, by simp only [reassoc_of% h, e.hom_inv_id, comp_id]⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Bijective fun g => f ≫ g

Tactic:
constructor

Result:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Injective fun g => f ≫ g

case h.mpr.intro.intro.intro.right
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Surjective fun g => f ≫ g

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
⊢ W P.isoClosure = W P

Tactic:
ext X Y f

Result:
case h
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P.isoClosure f ↔ W P f

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P.isoClosure f ↔ W P f

Tactic:
constructor

Result:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P.isoClosure f → W P f

case h.mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P f → W P.isoClosure f

Proof state:
case h.mpr.intro.intro.intro.right
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
⊢ ∃ a, (fun g => f ≫ g) a = g

Tactic:
obtain ⟨a, h⟩ := (hf _ hZ').2 (g ≫ e.hom)

Result:
case h.mpr.intro.intro.intro.right.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
a : Y ⟶ Z'
h : (fun g => f ≫ g) a = g ≫ e.hom
⊢ ∃ a, (fun g => f ≫ g) a = g

Proof state:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P.isoClosure f
Z : C
hZ : P Z
⊢ Function.Bijective fun g => f ≫ g

Tactic:
exact hf _ (P.le_isoClosure _ hZ)

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.left.a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ (fun g => f ≫ g) (g₁ ≫ e.hom) = (fun g => f ≫ g) (g₂ ≫ e.hom)

Tactic:
simp only [reassoc_of% eq]

Result:
no goals

Proof state:
case h.mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P f → W P.isoClosure f

Tactic:
rintro hf Z ⟨Z', hZ', ⟨e⟩⟩

Result:
case h.mpr.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Bijective fun g => f ≫ g

Proof state:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ ≫ e.hom = g₂ ≫ e.hom

Tactic:
apply (hf _ hZ').1

Result:
case h.mpr.intro.intro.intro.left.a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ (fun g => f ≫ g) (g₁ ≫ e.hom) = (fun g => f ≫ g) (g₂ ≫ e.hom)

Proof state:
case h.mpr.intro.intro.intro.right
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Surjective fun g => f ≫ g

Tactic:
intro g

Result:
case h.mpr.intro.intro.intro.right
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
⊢ ∃ a, (fun g => f ≫ g) a = g

Proof state:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ W P.isoClosure f → W P f

Tactic:
intro hf Z hZ

Result:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P.isoClosure f
Z : C
hZ : P Z
⊢ Function.Bijective fun g => f ≫ g

Proof state:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Function.Injective fun g => f ≫ g

Tactic:
intro g₁ g₂ eq

Result:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ = g₂

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g : X ⟶ Z
a : Y ⟶ Z'
h : (fun g => f ≫ g) a = g ≫ e.hom
⊢ (fun g => f ≫ g) (a ≫ e.inv) = g

Tactic:
simp only [reassoc_of% h, e.hom_inv_id, comp_id]

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ = g₂

Tactic:
rw [← cancel_mono e.hom]

Result:
case h.mpr.intro.intro.intro.left
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : W P f
Z Z' : C
hZ' : P Z'
e : Z ≅ Z'
g₁ g₂ : Y ⟶ Z
eq : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ ≫ e.hom = g₂ ≫ e.hom