Theorem: ExtrDisc.everything_proj (ExtrDisc/ExplicitSheaves.lean)

State before:
⊢ EverythingIsProjective ExtrDisc
Tactic:
refine' fun P => ⟨(@fun X Y f e he => _)⟩
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
⊢ ∃ f', f' ≫ e = f

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
⊢ ∃ f', f' ≫ e = f
Tactic:
have proj : Projective (toCompHaus.obj P) := inferInstanceAs (Projective P.compHaus)
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ ∃ f', f' ≫ e = f

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ ∃ f', f' ≫ e = f
Tactic:
have : Epi (toCompHaus.map e) := by rw [CompHaus.epi_iff_surjective]
  change Function.Surjective e
  rwa [← ExtrDisc.epi_iff_surjective]
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
⊢ ∃ f', f' ≫ e = f

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
⊢ ∃ f', f' ≫ e = f
Tactic:
set g := toCompHaus.preimage <| Projective.factorThru (toCompHaus.map f) (toCompHaus.map e) with hg
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ ∃ f', f' ≫ e = f

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ ∃ f', f' ≫ e = f
Tactic:
refine' ⟨g, toCompHaus.map_injective _⟩
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ toCompHaus.map (g ≫ e) = toCompHaus.map f

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ toCompHaus.map (g ≫ e) = toCompHaus.map f
Tactic:
rw [map_comp, hg, image_preimage, Projective.factorThru_comp]
State after:
no goals

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Epi (toCompHaus.map e)
Tactic:
rw [CompHaus.epi_iff_surjective]
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑(toCompHaus.map e)

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑(toCompHaus.map e)
Tactic:
change Function.Surjective e
State after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑e

State before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑e
Tactic:
rwa [← ExtrDisc.epi_iff_surjective]
State after:
no goals