-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem iso_eq_iso_refl {x : SimplexCategory} (e : x ≅ x) : e = Iso.refl x

Proof state:
case w.a
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ Hom.toOrderHom e.hom = Hom.toOrderHom (Iso.refl x).hom

Tactic:
convert congr_arg (fun φ => (OrderEmbedding.toOrderHom φ)) (eq₁.trans eq₂.symm)

Result:
case h.e'_2
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ Hom.toOrderHom e.hom = OrderEmbedding.toOrderHom (RelIso.toRelEmbedding (orderIsoOfIso e))

Proof state:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
⊢ e = Iso.refl x

Tactic:
have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)

Result:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
⊢ e = Iso.refl x

Proof state:
case h.e'_2.h.h
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
i : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.hom) i = (OrderEmbedding.toOrderHom (RelIso.toRelEmbedding (orderIsoOfIso e))) i

Tactic:
rfl

Result:
no goals

Proof state:
x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x

Tactic:
have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)

Result:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
⊢ e = Iso.refl x

Proof state:
case h.e'_2
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ Hom.toOrderHom e.hom = OrderEmbedding.toOrderHom (RelIso.toRelEmbedding (orderIsoOfIso e))

Tactic:
ext i : 2

Result:
case h.e'_2.h.h
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
i : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.hom) i = (OrderEmbedding.toOrderHom (RelIso.toRelEmbedding (orderIsoOfIso e))) i

Proof state:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ e = Iso.refl x

Tactic:
ext : 2

Result:
case w.a
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ Hom.toOrderHom e.hom = Hom.toOrderHom (Iso.refl x).hom

Proof state:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
⊢ e = Iso.refl x

Tactic:
have eq₂ :=
  Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)

Result:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ e = Iso.refl x