awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ (b ^ n) ^ m.gcdA n * (a ^ n) ^ m.gcdB n = (a ^ n) ^ m.gcdB n * (b ^ n) ^ m.gcdA n

Tactic:
exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

Premises used: Commute.pow_pow, Commute.symm, Commute.zpow_zpow₀
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
(pow_one _).symm.trans ?_

Premises used: pow_one, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : HPow.hPow (β := ℕ) b 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
refine (pow_one _).symm.trans ?_

Premises used: pow_one, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
rw : b ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n)
| HPow.hPow (β := ℕ) b 1

Tactic:
rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Premises used: zpow_natCast, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : b ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
⊢ HPow.hPow (β := ℕ) b 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Premises used: zpow_natCast, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : b ^ ((↑m : ℤ) * m.gcdA n) * b ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑m : ℤ) * m.gcdB n) * b ^ ((↑m : ℤ) * m.gcdA n)
⊢ b ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]

Premises used: zpow_natCast, zpow_mul, Commute.mul_zpow, zpow_add₀, Nat.gcdB, mul_comm, Nat.gcdA, Commute.zpow_zpow₀
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : (b ^ m) ^ m.gcdA n * (b ^ n) ^ m.gcdB n = (b ^ n) ^ m.gcdB n * (b ^ m) ^ m.gcdA n
⊢ b ^ ((↑m : ℤ) * m.gcdA n) * b ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑m : ℤ) * m.gcdB n) * b ^ ((↑m : ℤ) * m.gcdA n)

Tactic:
simp only [zpow_mul, zpow_natCast, h]

Premises used: zpow_natCast, zpow_mul
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute b b

Tactic:
aesop
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ (b ^ m) ^ m.gcdA n * (b ^ n) ^ m.gcdB n = (b ^ n) ^ m.gcdB n * (b ^ m) ^ m.gcdA n

Tactic:
exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm

Premises used: Commute.pow_pow, Commute.symm, Commute.zpow_zpow₀
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : CommGroupWithZero α
a b : α
m n : ℕ
hmn : m.Coprime n
⊢ a ^ m = b ^ n ↔ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
(Commute.all _ _).pow_eq_pow_iff_of_coprime hmn

Premises used: Commute.pow_eq_pow_iff_of_coprime
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
simp : (∃ (c : α), a = c ^ n) ↔ ∃ (y : α), y ^ n = a
⊢ Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ x ^ n) (a ^ m) ↔
    Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ x ^ n) a

Tactic:
simp [pow_eq_pow_iff_of_coprime hmn.symm]

Premises used: Nat.Coprime.symm, pow_eq_pow_iff_of_coprime
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ (c : α), a = c ^ n) ↔ ∃ (y : α), y ^ n = a

Tactic:
aesop
-- Module: Mathlib.Data.Int.Init
Goal:
a b : ℤ
h : -a = -b
⊢ a = b

Tactic:
Int.neg_inj.1 h

Premises used: Iff.mp, Int.neg_inj
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ a.succ.pred = a

Tactic:
Int.add_sub_cancel _ _

Premises used: Int.pred, Int.add_sub_cancel, Int.succ
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ a.pred.succ = a

Tactic:
Int.sub_add_cancel _ _

Premises used: Int.pred, Int.sub_add_cancel, Int.succ
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ -a.succ = (-a).pred

Tactic:
Int.neg_add

Premises used: Int.pred, Int.neg_add, Int.sub, Int.succ
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
rw : (-a).pred.succ = -a
rw₁ rw₂ : -a = -a
⊢ (-a.succ).succ = -a

Tactic:
rw [neg_succ, succ_pred]

Premises used: Int.succ_pred, Int.neg_succ
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
rw : -a.pred = -(- -a).pred
rw₁ rw₂ : -a.pred = -a.pred
⊢ -a.pred = (-a).succ

Tactic:
rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]

Premises used: Int.neg_eq_comm, Iff.mp, Int.neg_neg, Int.neg_succ, Neg.neg
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
rw : (-a).succ.pred = -a
rw₁ rw₂ : -a = -a
⊢ (-a.pred).pred = -a

Tactic:
rw [neg_pred, pred_succ]

Premises used: Int.pred_succ, Int.neg_pred
-- Module: Mathlib.Data.Int.Init
Goal:
n : ℕ
⊢ pred (↑n.succ : ℤ) = (↑n : ℤ)

Tactic:
pred_succ n

Premises used: Int.pred_succ, Nat.cast, Int.succ, Int.add
-- Module: Mathlib.Data.Int.Init
Goal:
n : ℕ
⊢ -(↑n.succ : ℤ) = pred (-(↑n : ℤ))

Tactic:
neg_succ n

Premises used: Nat.cast, Int.succ, Int.add, Int.neg_succ
-- Module: Mathlib.Data.Int.Init
Goal:
n : ℕ
⊢ succ (-(↑n.succ : ℤ)) = -(↑n : ℤ)

Tactic:
succ_neg_succ n

Premises used: Nat.cast, Int.succ, Int.succ_neg_succ, Int.add
-- Module: Mathlib.Data.Int.Init
Goal:
n : ℕ
h : 0 < n
⊢ (↑(n - 1) : ℤ) = HSub.hSub (α := ℤ) (↑n : ℤ) 1

Tactic:
grind
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ a < a + 1

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a : ℤ
⊢ a - 1 < a

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
⊢ motive (ofNat 0)

Tactic:
zero
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
⊢ motive (ofNat 0)

Tactic:
exact zero
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i : ℕ
ih : motive (ofNat i)
⊢ motive (ofNat (i + 1))

Tactic:
succ _ ih

Premises used: Int.add
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i : ℕ
ih : motive (ofNat i)
⊢ motive (ofNat (i + 1))

Tactic:
exact succ _ ih
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i : ℕ
ofNat : motive (Int.ofNat 0)
ofNat₁ : ∀ (i : ℕ) (ih : motive (Int.ofNat i)), motive (Int.ofNat (i + 1))
⊢ motive (Int.ofNat i)

Tactic:
induction i with
    | zero => exact zero
    | succ i ih => exact succ _ ih
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i : ℕ
negSucc : ∀ (n : ℕ), motive (-(↑n : ℤ))
⊢ motive -[i+1]

Tactic:
suffices ∀ n : ℕ, motive (-n) from this (i + 1)
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i : ℕ
⊢ motive (-(↑0 : ℤ))

Tactic:
simp [zero]
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i n : ℕ
ih : motive (-(↑n : ℤ))
⊢ motive (-(↑(n + 1) : ℤ))

Tactic:
simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih

Premises used: Int.sub_eq_add_neg, Int.natCast_succ, Int.neg_add
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
i n : ℕ
negSucc : motive (-(↑0 : ℤ))
negSucc₁ : ∀ (n : ℕ) (ih : motive (-(↑n : ℤ))), motive (-(↑(n + 1) : ℤ))
⊢ motive (-(↑n : ℤ))

Tactic:
induction n with
    | zero => simp [zero]
    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih

Premises used: Int.sub_eq_add_neg, Int.natCast_succ, Int.neg_add
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Prop
i : ℤ
zero : motive 0
succ : ∀ (i : ℕ), motive (↑i : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred : ∀ (i : ℕ), motive (-(↑i : ℤ)) → motive (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
ofNat : ∀ (i : ℕ), motive (Int.ofNat i)
negSucc : ∀ (i : ℕ), motive -[i+1]
⊢ motive i

Tactic:
cases i with
  | ofNat i =>
    induction i with
    | zero => exact zero
    | succ i ih => exact succ _ ih
  | negSucc i =>
    suffices ∀ n : ℕ, motive (-n) from this (i + 1)
    intro n; induction n with
    | zero => simp [zero]
    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih

Premises used: Int.ofNat, Int.sub_eq_add_neg, Int.natCast_succ, Int.neg_add, Int.negSucc
-- Module: Mathlib.Data.Int.Init
Goal:
a b_1 c d m n : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = motive (b + (↑0 : ℤ))

Tactic:
simp
-- Module: Mathlib.Data.Int.Init
Goal:
a b_1 c d m n_1 : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + (↑n : ℤ) + 1) = motive (b + (↑(n + 1) : ℤ))

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b_1 c d m n_1 : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ motive (b + -[n+1] - 1) = motive (b + -[n + 1+1])

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b_1 c d m n_1 : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
n : ℕ
⊢ b + -[n+1] ≤ b

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
a b_1 c d m n : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ b + (z - b) = z

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
rw :
  cast ⋯ zero =
    match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) 0 with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n
rw₁ : motive b = (fun (x : ℤ) ↦ motive x) (b + 0)
⊢ HEq zero (β := (fun (x : ℤ) ↦ motive x) (b + (b - b)))
    (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) b - b with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)

Tactic:
rw [b.sub_self, ← cast_eq_iff_heq]

Premises used: cast_eq_iff_heq, Int.sub_self
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
unfold :
  cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z + 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    succ z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ Int.inductionOn' (motive := fun (x : ℤ) ↦ motive x) (z + 1) b zero succ pred =
    succ z hz (Int.inductionOn' (motive := fun (x : ℤ) ↦ motive x) z b zero succ pred)

Tactic:
unfold Int.inductionOn'
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ z - b = (↑(z - b).toNat : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ z + 1 - b = (↑((z - b).toNat + 1) : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
rw! :
  cast (α := (fun (x : ℤ) ↦ motive x) (b + (↑((z - b).toNat + 1) : ℤ))) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) (↑((z - b).toNat + 1) : ℤ) with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    succ z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + (↑(z - b).toNat : ℤ))) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) (↑(z - b).toNat : ℤ) with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z + 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    succ z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
rw! [show z - b = (z - b).toNat by lia, show z + 1 - b = ((z - b).toNat + 1 : ℕ) by lia]
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ b + (↑(z - b).toNat : ℤ) = z

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ cast (α := (fun (x : ℤ) ↦ motive x) (b + (↑((z - b).toNat + 1) : ℤ))) ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) (↑((z - b).toNat + 1) : ℤ) with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    succ z hz
      (cast (α := (fun (x : ℤ) ↦ motive x) (b + (↑(z - b).toNat : ℤ))) ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) (↑(z - b).toNat : ℤ) with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
grind [inductionOn'.pos, show b + (z - b).toNat = z by lia]

Premises used: Int.inductionOn'.pos
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
unfold :
  cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ Int.inductionOn' (motive := fun (x : ℤ) ↦ motive x) (z - 1) b zero succ pred =
    pred z hz (Int.inductionOn' (motive := fun (x : ℤ) ↦ motive x) z b zero succ pred)

Tactic:
unfold Int.inductionOn'
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
lhs :
  cast ⋯
    (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)
| cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
lhs
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
unfold :
  cast ⋯
    (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] =>
      match (motive := (x : ℕ) → motive (b + -[x+1])) n with
      | 0 => pred b ⋯ zero
      | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)))
| cast ⋯
    (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)

Tactic:
unfold inductionOn'.neg

Premises used: Int.inductionOn'.neg
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
unfold :
  cast ⋯
    (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
    | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
    | -[n+1] =>
      match (motive := (x : ℕ) → motive (b + -[x+1])) n with
      | 0 => pred b ⋯ zero
      | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)))
| cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
lhs; unfold inductionOn'.neg

Premises used: Int.inductionOn'.neg
-- Module: Mathlib.Data.Int.Init
Goal:
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
conv :
  cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] =>
        match (motive := (x : ℕ) → motive (b + -[x+1])) n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))
⊢ cast ⋯
      (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - 1 - b with
      | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
      | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n) =
    pred z hz
      (cast ⋯
        (match (motive := (x : ℤ) → (fun (x : ℤ) ↦ motive x) (b + x)) z - b with
        | ofNat n => inductionOn'.pos (motive := fun (x : ℤ) ↦ motive x) b zero succ n
        | -[n+1] => inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))

Tactic:
conv => lhs; unfold inductionOn'.neg

Premises used: Int.inductionOn'.neg