-- Module: Mathlib.Data.DFinsupp.Defs
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
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 : ι)))
                      ⋯ :
                    { 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 ⋯))) :
            Π₀ (i : ι), β i) :
          (a : ι) → β a)
        i =
      ((↑(Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f ⋯) :
            Π₀ (i : ι), β i) :
          (a : ι) → β a)
        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 ⋯)

Tactic:
ext i