have : ∃ (n m : ℕ), a ≃ n - m := this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this : motive a
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this✝ : motive a
this : ∃ n m, a ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m