awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
pos : m = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg : ¬m = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases m = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have pos : n = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases n = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
pos : n = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg : ¬n = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases n = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have pos : ∀ (hb : b = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
pos : ∀ (hb : b = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg : ∀ (hb : ¬b = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have pos : ∀ (ha : a = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
pos : ∀ (ha : a = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg : ∀ (ha : ¬a = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
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
⊢ a = HPow.hPow (α := α) 0 n ∧ b = HPow.hPow (α := α) 0 m
have this : b ^ n = a ^ m
Tactic: have := h.symm
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg : a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
Tactic: refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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 : a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have neg₁ : b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
Tactic: refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
have neg : HPow.hPow (β := ℕ) a 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
Tactic: refine (pow_one _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
| HPow.hPow (β := ℕ) a 1
have rw : a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n)
Tactic: rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℕ) a 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
have neg : a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
Tactic: conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
have neg : a ^ ((↑m : ℤ) * m.gcdA n) * a ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑n : ℤ) * m.gcdB n) * b ^ ((↑n : ℤ) * m.gcdA n)
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)]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ ((↑m : ℤ) * m.gcdA n) * a ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑n : ℤ) * m.gcdB n) * b ^ ((↑n : ℤ) * m.gcdA n)
have neg : (b ^ n) ^ m.gcdA n * (a ^ n) ^ m.gcdB n = (a ^ n) ^ m.gcdB n * (b ^ n) ^ m.gcdA n
Tactic: simp only [zpow_mul, zpow_natCast, h]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
have neg : HPow.hPow (β := ℕ) b 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
Tactic: refine (pow_one _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
| HPow.hPow (β := ℕ) b 1
have rw : b ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n)
Tactic: rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℕ) b 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
have neg : b ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
Tactic: conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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 + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
have neg : b ^ ((↑m : ℤ) * m.gcdA n) * b ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑m : ℤ) * m.gcdB n) * b ^ ((↑m : ℤ) * m.gcdA n)
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)]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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) = a ^ ((↑m : ℤ) * m.gcdB n) * b ^ ((↑m : ℤ) * m.gcdA n)
have neg : (b ^ m) ^ m.gcdA n * (b ^ n) ^ m.gcdB n = (b ^ n) ^ m.gcdB n * (b ^ m) ^ m.gcdA n
Tactic: simp only [zpow_mul, zpow_natCast, h]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
α : Type u_1
inst : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ x ^ n) (a ^ m) ↔
    Membership.mem (γ := Set α) (Set.range fun (x : α) ↦ x ^ n) a
have simp : (∃ (c : α), a = c ^ n) ↔ ∃ (y : α), y ^ n = a
Tactic: simp [pow_eq_pow_iff_of_coprime hmn.symm]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
⊢ (-a.succ).succ = -a
have rw : (-a).pred.succ = -a
Tactic: rw [neg_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
rw : (-a).pred.succ = -a
⊢ (-a.succ).succ = -a
have rw₁ : -a = -a
Tactic: rw [neg_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
⊢ -a.pred = (-a).succ
have rw : -a.pred = -(- -a).pred
Tactic: rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
rw : -a.pred = -(- -a).pred
⊢ -a.pred = (-a).succ
have rw₁ : -a.pred = -a.pred
Tactic: rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
⊢ (-a.pred).pred = -a
have rw : (-a).succ.pred = -a
Tactic: rw [neg_pred, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
Goal:
a : ℤ
rw : (-a).succ.pred = -a
⊢ (-a.pred).pred = -a
have rw₁ : -a = -a
Tactic: rw [neg_pred, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 (ofNat i)
have ofNat : motive (ofNat 0)
Tactic: induction i with
    | zero => exact zero
    | succ i ih => exact succ _ ih
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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)
⊢ motive (Int.ofNat i)
have ofNat₁ : ∀ (i : ℕ) (ih : motive (Int.ofNat i)), motive (Int.ofNat (i + 1))
Tactic: induction i with
    | zero => exact zero
    | succ i ih => exact succ _ ih
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 -[i+1]
have negSucc : ∀ (n : ℕ), motive (-(↑n : ℤ))
Tactic: suffices ∀ n : ℕ, motive (-n) from this (i + 1)
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 : ℕ
⊢ motive (-(↑n : ℤ))
have negSucc : motive (-(↑0 : ℤ))
Tactic: induction n with
    | zero => simp [zero]
    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 : ℤ))
⊢ motive (-(↑n : ℤ))
have negSucc₁ : ∀ (n : ℕ) (ih : motive (-(↑n : ℤ))), motive (-(↑(n + 1) : ℤ))
Tactic: induction n with
    | zero => simp [zero]
    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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)
⊢ motive i
have ofNat : ∀ (i : ℕ), motive (ofNat 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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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)
⊢ motive i
have negSucc : ∀ (i : ℕ), motive -[i+1]
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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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)
⊢ 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)
have rw : cast sorry 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
Tactic: rw [b.sub_self, ← cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ 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)
have rw₁ : motive b = (fun (x : ℤ) ↦ motive x) (b + 0)
Tactic: rw [b.sub_self, ← cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ 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)
have unfold : cast sorry
    (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 sorry
      (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: unfold Int.inductionOn'
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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 ⋯
      (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))
have rw! : cast (α := (fun (x : ℤ) ↦ motive x) (b + (↑((z - b).toNat + 1) : ℤ))) sorry
    (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 : ℤ))) sorry
      (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: rw! [show z - b = (z - b).toNat by lia, show z + 1 - b = ((z - b).toNat + 1 : ℕ) by lia]
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ 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)
have unfold : cast sorry
    (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 sorry
      (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: unfold Int.inductionOn'
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
| 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))
have lhs : cast sorry
  (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: lhs
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
| 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)
have unfold : cast sorry
  (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 sorry zero
    | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)))
Tactic: unfold inductionOn'.neg
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
| 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))
have unfold : cast sorry
  (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 sorry zero
    | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n)))
Tactic: lhs; unfold inductionOn'.neg
-- Lean 4 proof step from Mathlib.Data.Int.Init (goal)
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
⊢ 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))
have conv : cast sorry
    (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 sorry zero
      | n.succ => cast sorry (pred (b + -[n+1]) sorry (inductionOn'.neg (motive := fun (x : ℤ) ↦ motive x) b zero pred n))) =
  pred z hz
    (cast sorry
      (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