awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
hn : 0 ≤ b
rw : |a| ≤ sqrt b ↔ |a| * |a| ≤ b
rw₁ : |a| ≤ sqrt (↑b.toNat : ℤ) ↔ |a| * |a| ≤ (↑b.toNat : ℤ)
rw₂ : (↑|a|.toNat : ℤ) ≤ sqrt (↑b.toNat : ℤ) ↔ HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
rw₃ :
  LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔
    HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
rw₄ : LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
rw₅ : |a|.toNat ≤ b.toNat.sqrt ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
rw₆ : |a|.toNat ≤ b.toNat.sqrt ↔ |a|.toNat * |a|.toNat ≤ b.toNat
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₇ : |a|.toNat * |a|.toNat ≤ b.toNat ↔ |a|.toNat * |a|.toNat ≤ b.toNat
Tactic: rw [← abs_mul_abs_self, eq_natCast_toNat.mpr hn, eq_natCast_toNat.mpr (abs_nonneg a),
    Int.sqrt_natCast, ← Int.natCast_mul, Nat.cast_le, Nat.cast_le, Nat.le_sqrt]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
x : ℤ
⊢ IsUnit x ↔ |x| = 1
have rw : x.natAbs = 1 ↔ |x| = 1
Tactic: rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
x : ℤ
rw : x.natAbs = 1 ↔ |x| = 1
⊢ IsUnit x ↔ |x| = 1
have rw₁ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) 1
Tactic: rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
x : ℤ
rw : x.natAbs = 1 ↔ |x| = 1
rw₁ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) 1
⊢ IsUnit x ↔ |x| = 1
have rw₂ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) (↑1 : ℤ)
Tactic: rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
x : ℤ
rw : x.natAbs = 1 ↔ |x| = 1
rw₁ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) 1
rw₂ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) (↑1 : ℤ)
⊢ IsUnit x ↔ |x| = 1
have rw₃ : x.natAbs = 1 ↔ x.natAbs = 1
Tactic: rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
a : ℤ
ha : IsUnit a
⊢ HPow.hPow (β := ℕ) a 2 = 1
have rw : a * a = 1
Tactic: rw [sq, isUnit_mul_self ha]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
a : ℤ
ha : IsUnit a
rw : a * a = 1
⊢ HPow.hPow (β := ℕ) a 2 = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [sq, isUnit_mul_self ha]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
⊢ HPow.hPow (β := ℕ) u 2 = 1
have rw : (↑(HPow.hPow (β := ℕ) u 2) : ℤ) = (↑1 : ℤ)
Tactic: rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : (↑(HPow.hPow (β := ℕ) u 2) : ℤ) = (↑1 : ℤ)
⊢ HPow.hPow (β := ℕ) u 2 = 1
have rw₁ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = (↑1 : ℤ)
Tactic: rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : (↑(HPow.hPow (β := ℕ) u 2) : ℤ) = (↑1 : ℤ)
rw₁ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = (↑1 : ℤ)
⊢ HPow.hPow (β := ℕ) u 2 = 1
have rw₂ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = 1
Tactic: rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : (↑(HPow.hPow (β := ℕ) u 2) : ℤ) = (↑1 : ℤ)
rw₁ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = (↑1 : ℤ)
rw₂ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = 1
⊢ HPow.hPow (β := ℕ) u 2 = 1
have rw₃ : Eq (α := ℤ) 1 1
Tactic: rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
⊢ u * u = 1
have rw : HPow.hPow (β := ℕ) u 2 = 1
Tactic: rw [← sq, units_sq]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : HPow.hPow (β := ℕ) u 2 = 1
⊢ u * u = 1
have rw₁ : Eq (α := ℤˣ) 1 1
Tactic: rw [← sq, units_sq]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
⊢ u⁻¹ = u
have rw : u * u = 1
Tactic: rw [inv_eq_iff_mul_eq_one, units_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : u * u = 1
⊢ u⁻¹ = u
have rw₁ : Eq (α := ℤˣ) 1 1
Tactic: rw [inv_eq_iff_mul_eq_one, units_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u₁ u₂ : ℤˣ
⊢ u₁ / u₂ = u₁ * u₂
have rw : u₁ * u₂⁻¹ = u₁ * u₂
Tactic: rw [div_eq_mul_inv, units_inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u₁ u₂ : ℤˣ
rw : u₁ * u₂⁻¹ = u₁ * u₂
⊢ u₁ / u₂ = u₁ * u₂
have rw₁ : u₁ * u₂ = u₁ * u₂
Tactic: rw [div_eq_mul_inv, units_inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
⊢ (↑u : ℤ) * (↑u : ℤ) = 1
have rw : (↑(u * u) : ℤ) = 1
Tactic: rw [← Units.val_mul, units_mul_self, Units.val_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : (↑(u * u) : ℤ) = 1
⊢ (↑u : ℤ) * (↑u : ℤ) = 1
have rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
Tactic: rw [← Units.val_mul, units_mul_self, Units.val_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
rw : (↑(u * u) : ℤ) = 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ (↑u : ℤ) * (↑u : ℤ) = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [← Units.val_mul, units_mul_self, Units.val_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
have lhs : u ^ n
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
| u ^ n
have rw : u ^ (n % 2 + 2 * (n / 2))
Tactic: rw [← Nat.mod_add_div n 2]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))
have rw : u ^ (n % 2)
Tactic: rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
have rw : u ^ (n % 2)
Tactic: lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)
have conv : u ^ n = u ^ (n % 2)
Tactic: conv =>
    lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Units (goal)
Goal:
u : ℤˣ
n : ℕ
conv : u ^ n = u ^ (n % 2)
⊢ u ^ n = u ^ (n % 2)
have conv₁ : u ^ (n % 2) = u ^ (n % 2)
Tactic: conv =>
    lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Int.Range (goal)
Goal:
m n r : ℤ
⊢ r ∈ m.range n ↔ m ≤ r ∧ r < n
have simp : (∃ (a : ℕ), m + (↑a : ℤ) < n ∧ m + (↑a : ℤ) = r) ↔ m ≤ r ∧ r < n
Tactic: simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℤ
⊢ sqrt (n * n) = (↑n.natAbs : ℤ)
have rw : Eq (α := ℤ) (↑(n * n).toNat.sqrt : ℤ) (↑n.natAbs : ℤ)
Tactic: rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(n * n).toNat.sqrt : ℤ) (↑n.natAbs : ℤ)
⊢ sqrt (n * n) = (↑n.natAbs : ℤ)
have rw₁ : Eq (α := ℤ) (↑(toNat (↑(n.natAbs * n.natAbs) : ℤ)).sqrt : ℤ) (↑n.natAbs : ℤ)
Tactic: rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(n * n).toNat.sqrt : ℤ) (↑n.natAbs : ℤ)
rw₁ : Eq (α := ℤ) (↑(toNat (↑(n.natAbs * n.natAbs) : ℤ)).sqrt : ℤ) (↑n.natAbs : ℤ)
⊢ sqrt (n * n) = (↑n.natAbs : ℤ)
have rw₂ : Eq (α := ℤ) (↑(n.natAbs * n.natAbs).sqrt : ℤ) (↑n.natAbs : ℤ)
Tactic: rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(n * n).toNat.sqrt : ℤ) (↑n.natAbs : ℤ)
rw₁ : Eq (α := ℤ) (↑(toNat (↑(n.natAbs * n.natAbs) : ℤ)).sqrt : ℤ) (↑n.natAbs : ℤ)
rw₂ : Eq (α := ℤ) (↑(n.natAbs * n.natAbs).sqrt : ℤ) (↑n.natAbs : ℤ)
⊢ sqrt (n * n) = (↑n.natAbs : ℤ)
have rw₃ : Eq (α := ℤ) (↑n.natAbs : ℤ) (↑n.natAbs : ℤ)
Tactic: rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
x : ℤ
h : ∃ (n : ℤ), n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x
have rw : sqrt (n * n) * sqrt (n * n) = n * n
Tactic: rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
x : ℤ
h : ∃ (n : ℤ), n * n = x
n : ℤ
hn : n * n = x
rw : sqrt (n * n) * sqrt (n * n) = n * n
⊢ sqrt x * sqrt x = x
have rw₁ : HMul.hMul (α := ℤ) (↑n.natAbs : ℤ) (↑n.natAbs : ℤ) = n * n
Tactic: rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
x : ℤ
h : ∃ (n : ℤ), n * n = x
n : ℤ
hn : n * n = x
rw : sqrt (n * n) * sqrt (n * n) = n * n
rw₁ : HMul.hMul (α := ℤ) (↑n.natAbs : ℤ) (↑n.natAbs : ℤ) = n * n
⊢ sqrt x * sqrt x = x
have rw₂ : (↑(n.natAbs * n.natAbs) : ℤ) = n * n
Tactic: rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
x : ℤ
h : ∃ (n : ℤ), n * n = x
n : ℤ
hn : n * n = x
rw : sqrt (n * n) * sqrt (n * n) = n * n
rw₁ : HMul.hMul (α := ℤ) (↑n.natAbs : ℤ) (↑n.natAbs : ℤ) = n * n
rw₂ : (↑(n.natAbs * n.natAbs) : ℤ) = n * n
⊢ sqrt x * sqrt x = x
have rw₃ : n * n = n * n
Tactic: rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℕ
⊢ sqrt (↑n : ℤ) = (↑n.sqrt : ℤ)
have rw : Eq (α := ℤ) (↑(toNat (↑n : ℤ)).sqrt : ℤ) (↑n.sqrt : ℤ)
Tactic: rw [sqrt, toNat_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Sqrt (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) (↑(toNat (↑n : ℤ)).sqrt : ℤ) (↑n.sqrt : ℤ)
⊢ sqrt (↑n : ℤ) = (↑n.sqrt : ℤ)
have rw₁ : Eq (α := ℤ) (↑n.sqrt : ℤ) (↑n.sqrt : ℤ)
Tactic: rw [sqrt, toNat_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Star (goal)
Goal:
n : ℕ
hn : Even n
⊢ Eq (α := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) (nonneg ℤ)
have refine : ∀ (x : ℤ) (hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x),
  Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) x
Tactic: refine le_antisymm (closure_le.2 <| range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Int.Star (hypothesis)
Goal:
n : ℕ
hn : Even n
x : ℤ
hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x
⊢ Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) x
have this : x = x.natAbs • HPow.hPow (α := ℤ) 1 n
Tactic: have : x = x.natAbs • 1 ^ n := by simpa [eq_comm (a := x)] using hx
-- Lean 4 proof step from Mathlib.Data.Int.Star (goal)
Goal:
n : ℕ
hn : Even n
x : ℤ
hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x
this : x = x.natAbs • HPow.hPow (α := ℤ) 1 n
⊢ Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) x
have rw : Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) (x.natAbs • HPow.hPow (α := ℤ) 1 n)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
⊢ Order.succ^[(b - a).toNat] a = b
have rw : a + (↑(b - a).toNat : ℤ) = b
Tactic: rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : a + (↑(b - a).toNat : ℤ) = b
⊢ Order.succ^[(b - a).toNat] a = b
have rw₁ : a + (b - a) = b
Tactic: rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : a + (↑(b - a).toNat : ℤ) = b
rw₁ : a + (b - a) = b
⊢ Order.succ^[(b - a).toNat] a = b
have rw₂ : a + b - a = b
Tactic: rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : a + (↑(b - a).toNat : ℤ) = b
rw₁ : a + (b - a) = b
rw₂ : a + b - a = b
⊢ Order.succ^[(b - a).toNat] a = b
have rw₃ : b = b
Tactic: rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
⊢ Order.pred^[(b - a).toNat] b = a
have rw : b - (↑(b - a).toNat : ℤ) = a
Tactic: rw [pred_iterate, toNat_sub_of_le h, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : b - (↑(b - a).toNat : ℤ) = a
⊢ Order.pred^[(b - a).toNat] b = a
have rw₁ : b - (b - a) = a
Tactic: rw [pred_iterate, toNat_sub_of_le h, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : b - (↑(b - a).toNat : ℤ) = a
rw₁ : b - (b - a) = a
⊢ Order.pred^[(b - a).toNat] b = a
have rw₂ : a = a
Tactic: rw [pred_iterate, toNat_sub_of_le h, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.SuccPred (goal)
Goal:
a b : ℕ
⊢ CovBy (α := ℤ) (↑a : ℤ) (↑b : ℤ) ↔ a ⋖ b
have rw : HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 = (↑b : ℤ) ↔ a + 1 = b
Tactic: rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
⊢ Eq (α := ℝ≥0)
    (if hx : Eq (α := WithZero (Multiplicative ℤ)) 1 0 then 0
    else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    1
have rw : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero (x := 1) sorry) : ℤ) = 1
Tactic: rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
rw : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero (x := 1) ⋯) : ℤ) = 1
⊢ Eq (α := ℝ≥0)
    (if hx : Eq (α := WithZero (Multiplicative ℤ)) 1 0 then 0
    else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    1
have rw₁ : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) 1 : ℤ) = 1
Tactic: rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
rw : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero (x := 1) ⋯) : ℤ) = 1
rw₁ : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) 1 : ℤ) = 1
⊢ Eq (α := ℝ≥0)
    (if hx : Eq (α := WithZero (Multiplicative ℤ)) 1 0 then 0
    else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    1
have rw₂ : HPow.hPow (β := ℤ) e 0 = 1
Tactic: rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
rw : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero (x := 1) ⋯) : ℤ) = 1
rw₁ : HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) 1 : ℤ) = 1
rw₂ : HPow.hPow (β := ℤ) e 0 = 1
⊢ Eq (α := ℝ≥0)
    (if hx : Eq (α := WithZero (Multiplicative ℤ)) 1 0 then 0
    else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    1
have rw₃ : Eq (α := ℝ≥0) 1 1
Tactic: rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos : ∀ (hxy : x * y = 0),
  (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: by_cases hxy : x * y = 0
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
pos :
  ∀ (hxy : x * y = 0),
    (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
      HMul.hMul (α := ℝ≥0)
        (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
        (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have neg : ∀ (hxy : ¬x * y = 0),
  (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: by_cases hxy : x * y = 0
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos : ∀ (hx : x = 0),
  (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: rcases mul_eq_zero.mp hxy with hx | hy
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
pos :
  ∀ (hx : x = 0),
    (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
      HMul.hMul (α := ℝ≥0)
        (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
        (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos₁ : ∀ (hy : y = 0),
  (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: rcases mul_eq_zero.mp hxy with hx | hy
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hx : x = 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos : 0 =
  HMul.hMul (α := ℝ≥0)
    (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: rw [dif_pos hxy, dif_pos hx, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hx : x = 0
pos :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos₁ : 0 =
  HMul.hMul (α := ℝ≥0) 0
    (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: rw [dif_pos hxy, dif_pos hx, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hx : x = 0
pos :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
pos₁ :
  0 =
    HMul.hMul (α := ℝ≥0) 0
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [dif_pos hxy, dif_pos hx, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hy : y = 0
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos : 0 =
  HMul.hMul (α := ℝ≥0)
    (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
Tactic: rw [dif_pos hxy, dif_pos hy, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Int.WithZero (goal)
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hy : y = 0
pos :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
⊢ (if hx : x * y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
      (if hx : y = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
have pos₁ : 0 =
  HMul.hMul (α := ℝ≥0)
    (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) 0
Tactic: rw [dif_pos hxy, dif_pos hy, mul_zero]