-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
n : ℕ+
k l : ℕ
h_1 : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
a :
  Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
      ((fun (x : ℕ+ × ℕ+) ↦
          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
              (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
              (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                x_1 ∈ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) : ℕ).divisorsAntidiagonal)
                ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
            (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
        ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
            divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
              (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) =
    Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
      (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
        (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))
a₁ :
  Eq (α := ℕ)
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
              ((fun (x : ℕ+ × ℕ+) ↦
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                      (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                        x_1 ∈
                          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                              ℕ).divisorsAntidiagonal)
                        ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                    (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                    divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                      (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                    (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) :
            ↥(↑(Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
                      ((fun (x : ℕ+ × ℕ+) ↦
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                              (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                              (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                                x_1 ∈
                                  (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                                      ℕ).divisorsAntidiagonal)
                                ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                            (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                        ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                            divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                              (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))))) :
                  ℕ).divisorsAntidiagonal) :
        ℕ × ℕ).1
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
            (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
              (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))) :
        ℕ × ℕ).1
⊢ Eq (α := (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal)
    ((fun (x : ℕ+ × ℕ+) ↦
        (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
            (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
            (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
              x_1 ∈ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) : ℕ).divisorsAntidiagonal)
              ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
          (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
      ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
          divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
            (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
        (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
          (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))))
    (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
      (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))
have a₂ : Eq (α := ℕ)
  (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
            ((fun (x : ℕ+ × ℕ+) ↦
                (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                    (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) sorry)
                    (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                      x_1 ∈
                        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) sorry) : ℕ).divisorsAntidiagonal)
                      ((↑x.1 : ℕ), (↑x.2 : ℕ)) sorry) :
                  (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
              ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                  divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                    (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                  (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) :
          ↥(↑(Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
                    ((fun (x : ℕ+ × ℕ+) ↦
                        (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                            (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) sorry)
                            (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                              x_1 ∈
                                (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) sorry) :
                                    ℕ).divisorsAntidiagonal)
                              ((↑x.1 : ℕ), (↑x.2 : ℕ)) sorry) :
                          (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                      ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                          divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                            (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                        (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                          (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))))) :
                ℕ).divisorsAntidiagonal) :
      ℕ × ℕ).2
  (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))) :
      ℕ × ℕ).2
Tactic: ext