-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
have : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
have₁ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    σ ∈ (sumCongrHom m n).range
have₂ : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
have₃ have₄ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    σ ∈ (sumCongrHom m n).range
have₅ have₆ have₇ have₈ have₉ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x))
    (h3 :
      ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    σ ∈ (sumCongrHom m n).range
have₁₀ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x))
    (h3 :
      ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ
h₁ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x))
    (h3 :
      ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    let σ₁' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1;
    let σ₂' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3;
    let σ₁ : Perm m :=
      (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m)
        σ₁';
    let σ₂ : Perm n :=
      (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n)
        σ₂';
    (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (σ₁, σ₂) = σ
h₂ :
  ∀
    (h1 :
      ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x))
    (h3 :
      ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    let σ₁' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1;
    let σ₂' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3;
    let σ₁ : Perm m :=
      (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m)
        σ₁';
    let σ₂ : Perm n :=
      (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n)
        σ₂';
    (σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 = σ
⊢ σ ∈ (sumCongrHom m n).range
have h₃ : ∀
  (h1 :
    ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x))
  (h3 :
    ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
  let σ₁' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1;
  let σ₂' := σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3;
  let σ₁ : Perm m :=
    (permCongr (Equiv.symm (ofInjective Sum.inl sorry)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m)
      σ₁';
  let σ₂ : Perm n :=
    (permCongr (Equiv.symm (ofInjective Sum.inr sorry)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n)
      σ₂';
  ∀ (a : m),
    Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
      ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: classical
  have h1 : ∀ x : m ⊕ n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
    rintro _ ⟨a, rfl⟩; exact h ⟨a, rfl⟩
  have h3 : ∀ x : m ⊕ n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
    rintro _ ⟨b, rfl⟩; exact (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h ⟨b, rfl⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
    dsimp [Set.range]
    rw [subtypePerm_apply]
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    dsimp [Set.range]
    rw [subtypePerm_apply]