-- Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean
lemma isSmall_iff_eq_ofHoms :
    IsSmall.{w} W ↔ ∃ (ι : Type w) (A B : ι → C) (f : ∀ i, A i ⟶ B i),
      W = ofHoms f

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W → ∃ ι A B f, W = ofHoms f

Tactic:
intro

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ ∃ ι A B f, W = ofHoms f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm ((equivShrink ↑W.toSet) ⟨Arrow.mk f, hf⟩))).hom

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
w✝³ : Type w
w✝² w✝¹ : w✝³ → C
w✝ : (i : w✝³) → w✝² i ⟶ w✝¹ i
⊢ IsSmall.{w, v, u} (ofHoms w✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp.h.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
exact ⟨equivShrink _ ⟨f, hf⟩, by simp⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (∃ ι A B f, W = ofHoms f) → IsSmall.{w, v, u} W

Tactic:
rintro ⟨_, _, _, _, rfl⟩

Result:
case mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
w✝³ : Type w
w✝² w✝¹ : w✝³ → C
w✝ : (i : w✝³) → w✝² i ⟶ w✝¹ i
⊢ IsSmall.{w, v, u} (ofHoms w✝)

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ W = ofHoms fun i => (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
ext A B f

Result:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ofHoms (fun i => (↑((equivShrink ↑W.toSet).symm i)).hom) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W ↔ ∃ ι A B f, W = ofHoms f

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W → ∃ ι A B f, W = ofHoms f

case mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (∃ ι A B f, W = ofHoms f) → IsSmall.{w, v, u} W

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ ∃ ι A B f, W = ofHoms f

Tactic:
refine ⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ W = ofHoms fun i => (↑((equivShrink ↑W.toSet).symm i)).hom

Proof state:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ofHoms (fun i => (↑((equivShrink ↑W.toSet).symm i)).hom) f

Tactic:
rw [ofHoms_iff]

Result:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

Proof state:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
constructor

Result:
case mp.h.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f → ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

case mp.h.mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ (∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom) → W f

Proof state:
case mp.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
i : Shrink.{w, max u v} ↑W.toSet
hi : Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom
⊢ W f

Tactic:
simp only [← W.arrow_mk_mem_toSet_iff, hi, Arrow.mk_eq, Subtype.coe_prop]

Result:
no goals

Proof state:
case mp.h.mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ (∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom) → W f

Tactic:
rintro ⟨i, hi⟩

Result:
case mp.h.mpr.intro
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
i : Shrink.{w, max u v} ↑W.toSet
hi : Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom
⊢ W f

Proof state:
case mp.h.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f → ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
intro hf

Result:
case mp.h.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom