-- Mathlib/Topology/Homeomorph.lean
theorem _root_.Fin.appendEquiv_eq_Homeomorph (m n : ℕ) : Fin.appendEquiv m n =
    ((sumArrowHomeomorphProdArrow).symm.trans
    (piCongrLeft (Y := fun _ ↦ X) finSumFinEquiv)).toEquiv

Proof state:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
h : ¬↑l < m
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
h : ↑l < m
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l

Tactic:
simp [h]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Fin.appendEquiv m n = (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Tactic:
ext ⟨x1, x2⟩ l

Result:
case H.mk.h
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
⊢ (Fin.appendEquiv m n) (x1, x2) l =
    (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv (x1, x2) l

Proof state:
case H.mk.h
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
⊢ (Fin.appendEquiv m n) (x1, x2) l =
    (sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv (x1, x2) l

Tactic:
simp only [sumArrowHomeomorphProdArrow, Equiv.sumArrowEquivProdArrow,
  finSumFinEquiv, Fin.addCases, Fin.appendEquiv, Fin.append, Equiv.coe_fn_mk]

Result:
case H.mk.h
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l

Proof state:
case H.mk.h
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l

Tactic:
by_cases h : l < m

Result:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
h : ↑l < m
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l

case neg
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x1 : Fin m → X
x2 : Fin n → X
l : Fin (m + n)
h : ¬↑l < m
⊢ (if h : ↑l < m then x1 (l.castLT ⋯) else ⋯ ▸ x2 (Fin.subNat m (Fin.cast ⋯ l) ⋯)) =
    ({ toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯,
                continuous_toFun := ⋯, continuous_invFun := ⋯ }.symm.trans
          (piCongrLeft
            { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m),
              invFun := fun i =>
                if h : ↑i < m then Sum.inl (i.castLT ⋯) else ⋯ ▸ Sum.inr (Fin.subNat m (Fin.cast ⋯ i) ⋯),
              left_inv := ⋯, right_inv := ⋯ })).toEquiv
      (x1, x2) l