-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem sSup_le {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, g ≤ f) :
    sSup s ≤ f

Proof state:
case f.refine_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j => ((equivShrink (Subobject A)).symm ↑j).arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ sSup s ≤ f

Tactic:
fapply le_of_comm

Result:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f

case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ?f ≫ f.arrow = (sSup s).arrow

Proof state:
case f.refine_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject A)
m : g ∈ ⇑(equivShrink (Subobject A)) '' s
⊢ (equivShrink (Subobject A)).symm ↑⟨g, m⟩ ∈ s

Tactic:
simpa using m

Result:
no goals

Proof state:
case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (Sigma.desc fun b => Subtype.casesOn b fun g m => underlying.map (homOfLE ⋯)) ≫ f.arrow = smallCoproductDesc s

Tactic:
ext

Result:
case f.refine_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => Subtype.casesOn b fun g m => underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s

Proof state:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (b : ↑(⇑(equivShrink (Subobject A)) '' s)) → underlying.obj ((equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f

Tactic:
rintro ⟨g, m⟩

Result:
case f.refine_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject A)
m : g ∈ ⇑(equivShrink (Subobject A)) '' s
⊢ underlying.obj ((equivShrink (Subobject A)).symm ↑⟨g, m⟩) ⟶ underlying.obj f

Proof state:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (∐ fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

Tactic:
refine Sigma.desc ?_

Result:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (b : ↑(⇑(equivShrink (Subobject A)) '' s)) → underlying.obj ((equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f

Proof state:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f

Tactic:
refine(underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩

Result:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (∐ fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ?f.refine_1 ≫ f.arrow = smallCoproductDesc s

Proof state:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) f.arrow
            (Sigma.desc fun b => Subtype.casesOn b fun g m => underlying.map (homOfLE ⋯)) ⋯)) ≫
      f.arrow =
    (sSup s).arrow

Tactic:
dsimp [sSup]

Result:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) f.arrow (Sigma.desc fun b => underlying.map (homOfLE ⋯)) ⋯)) ≫
      f.arrow =
    (mk (image.ι (smallCoproductDesc s))).arrow

Proof state:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) f.arrow (Sigma.desc fun b => underlying.map (homOfLE ⋯)) ⋯)) ≫
      f.arrow =
    (mk (image.ι (smallCoproductDesc s))).arrow

Tactic:
rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

Result:
no goals

Proof state:
case f.refine_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject A)
m : g ∈ ⇑(equivShrink (Subobject A)) '' s
⊢ underlying.obj ((equivShrink (Subobject A)).symm ↑⟨g, m⟩) ⟶ underlying.obj f

Tactic:
refine underlying.map (homOfLE (k _ ?_))

Result:
case f.refine_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject A)
m : g ∈ ⇑(equivShrink (Subobject A)) '' s
⊢ (equivShrink (Subobject A)).symm ↑⟨g, m⟩ ∈ s