-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ Eq (α := { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) })
    ((fun (f_1 : (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }) ↦
        (Subtype.mk (p := fun (f_2 : Π₀ (i : ι), β i) ↦ f_2.support (β := β) = f.support (β := β))
            (mk (β := β) (f.support (β := β)) fun (i : (↑(↑(f.support (β := β)) : Set ι) : Type u)) ↦
              (↑(f_1 i) : β (↑i : ι)))
            ⋯ :
          { f_2 : Π₀ (i : ι), β i // f_2.support (β := β) = f.support (β := β) }))
      ((fun (x : { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) }) ↦
          (match (motive :=
              { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) } →
                (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 })
              x with
            | ⟨f_1, hf⟩ => fun (x : ↥(f.support (β := β))) ↦
              match (motive := (x : ↥(f.support (β := β))) → { x_1 : β (↑x : ι) // x_1 ≠ 0 }) x with
              | ⟨i, hi⟩ =>
                Subtype.mk (p := fun (x : β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ f.support (β := β)) i hi) : ι)) ↦
                  x ≠ 0) ((f_1 : (a : ι) → β a) i) ⋯ :
            (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }))
        (Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f ⋯)))
    (Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f ⋯)
have a : ∀ (i : ι),
  ((↑((fun (f_1 : (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }) ↦
                (Subtype.mk (p := fun (f_2 : Π₀ (i : ι), β i) ↦ f_2.support (β := β) = f.support (β := β))
                    (mk (β := β) (f.support (β := β)) fun (i : (↑(↑(f.support (β := β)) : Set ι) : Type u)) ↦
                      (↑(f_1 i) : β (↑i : ι)))
                    sorry :
                  { f_2 : Π₀ (i : ι), β i // f_2.support (β := β) = f.support (β := β) }))
              ((fun (x : { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) }) ↦
                  (match (motive :=
                      { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) } →
                        (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 })
                      x with
                    | ⟨f_1, hf⟩ => fun (x : ↥(f.support (β := β))) ↦
                      match (motive := (x : ↥(f.support (β := β))) → { x_1 : β (↑x : ι) // x_1 ≠ 0 }) x with
                      | ⟨i, hi⟩ =>
                        Subtype.mk (p :=
                          fun (x : β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ f.support (β := β)) i hi) : ι)) ↦ x ≠ 0)
                          ((f_1 : (a : ι) → β a) i) sorry :
                    (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }))
                (Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f sorry))) :
          Π₀ (i : ι), β i) :
        (a : ι) → β a)
      i =
    ((↑(Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f sorry) :
          Π₀ (i : ι), β i) :
        (a : ι) → β a)
      i
Tactic: ext i