Theorem: Lean4Axiomatic.Integer.as_diff (Lean4Axiomatic/Integer/Induction.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let motive (z : ℤ) : Prop := ∃ (n m : ℕ), z ≃ n - m
State after:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m

State before:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let msubst {x₁ x₂ : ℤ} : x₁ ≃ x₂ → motive x₁ → motive x₂ := by
  intro (_ : x₁ ≃ x₂) (_ : motive x₁)
  show motive x₂
  have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : x₁ ≃ n - m)) :=
    ‹motive x₁›
  have : x₂ ≃ n - m := calc
    _ = x₂    := rfl
    _ ≃ x₁    := Rel.symm ‹x₁ ≃ x₂›
    _ ≃ n - m := ‹x₁ ≃ n - m›
  have : ∃ (n m : ℕ), x₂ ≃ n - m := Exists.intro n (Exists.intro m this)
  have : motive x₂ := this
  exact this
State after:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m

State before:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let idx_fam := Function.idx_fam_prop msubst
State after:
ℕ : 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 ⋯
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m

State before:
ℕ : 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 ⋯
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let on_diff (k j : ℕ) : motive ((k:ℤ) - j) :=
  Exists.intro k (Exists.intro j Rel.refl)
State after:
ℕ : 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)
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m

State before:
ℕ : 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)
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let ctx := ind_ctx_prop on_diff
State after:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m

State before:
ℕ : 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
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
have : motive a := ctx.ind_diff a
State after:
ℕ : 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

State before:
ℕ : 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
Tactic:
have : ∃ (n m : ℕ), a ≃ n - m := this
State after:
ℕ : 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

State before:
ℕ : 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
Tactic:
exact this
State after:
no goals

State before:
ℕ : 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
x₁ x₂ : ℤ
⊢ x₁ ≃ x₂ → motive x₁ → motive x₂
Tactic:
intro (_ : x₁ ≃ x₂) (_ : motive x₁)
State after:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
⊢ motive x₂

State before:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
⊢ motive x₂
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : x₁ ≃ n - m)) :=
  ‹motive x₁›
State after:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂

State before:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : x₂ ≃ n - m := calc
  _ = x₂    := rfl
  _ ≃ x₁    := Rel.symm ‹x₁ ≃ x₂›
  _ ≃ n - m := ‹x₁ ≃ n - m›
State after:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this : x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂

State before:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this : x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : ∃ (n m : ℕ), x₂ ≃ n - m := Exists.intro n (Exists.intro m this)
State after:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝ : x₂ ≃ Coe.coe n - Coe.coe m
this : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂

State before:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝ : x₂ ≃ Coe.coe n - Coe.coe m
this : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : motive x₂ := this
State after:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝¹ : x₂ ≃ Coe.coe n - Coe.coe m
this✝ : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
this : motive x₂
⊢ motive x₂

State before:
ℕ : 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
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝¹ : x₂ ≃ Coe.coe n - Coe.coe m
this✝ : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
this : motive x₂
⊢ motive x₂
Tactic:
exact this
State after:
no goals