Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_eval (Lean4Axiomatic/Integer/Impl/Difference/Induction.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
have sed : (n:Difference ℕ) - m ≃ n——m := sub_eqv_diff
State after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m

State before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
have des : n——m ≃ n - m := Rel.symm sed
State after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
des : n——m ≃ n——0 - m——0
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m

State before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
des : n——m ≃ n——0 - m——0
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
calc
  _ = ctx.ind_diff (n - m)                         := rfl
  _ ≃ fsubst des (ctx.ind_diff (n——m))             := Rel.symm ind_diff_subst
  _ = fsubst des (fsubst sed (ctx.on_diff n m))    := rfl
  _ ≃ fsubst (Rel.trans sed des) (ctx.on_diff n m) := fsubst_trans
  _ = fsubst Rel.refl (ctx.on_diff n m)            := rfl
  _ ≃ ctx.on_diff n m                              := fsubst_refl
State after:
no goals