awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
rw : (↑(u * u) : ℤ) = 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ (↑u : ℤ) * (↑u : ℤ) = 1

Tactic:
rw [← Units.val_mul, units_mul_self, Units.val_one]

Premises used: Units.val_one, Units.val_mul, Int.units_mul_self
-- Module: Mathlib.Data.Int.Order.Units
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ) (-1) n ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Int.Order.Units
Goal:
x : ℤ
h1 : HPow.hPow (β := ℕ) x 2 < 4
h2 : x ≠ 0
⊢ HPow.hPow (β := ℕ) x 2 = 1

Tactic:
sq_eq_one_iff.mpr
    ((abs_eq (zero_le_one' ℤ)).mp
      (le_antisymm (lt_add_one_iff.mp (abs_lt_of_sq_lt_sq h1 zero_le_two))
        (sub_one_lt_iff.mp (abs_pos.mpr h2))))

Premises used: Iff.mpr, abs_lt_of_sq_lt_sq, sq_eq_one_iff, abs_eq, zero_le_one', Int, abs_pos, le_antisymm, Iff.mp, zero_le_two, Int.lt_add_one_iff, Int.sub_one_lt_iff
-- Module: Mathlib.Data.Int.Order.Units
Goal:
x : ℤ
h1 : HPow.hPow (β := ℕ) x 2 ≤ 3
h2 : x ≠ 0
⊢ HPow.hPow (β := ℕ) x 2 = 1

Tactic:
sq_eq_one_of_sq_lt_four (lt_of_le_of_lt h1 (lt_add_one (3 : ℤ))) h2

Premises used: lt_of_le_of_lt, lt_add_one, Int.sq_eq_one_of_sq_lt_four, OfNat.ofNat
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
n : ℕ
lhs : u ^ n
| u ^ n = u ^ (n % 2)

Tactic:
lhs
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
n : ℕ
rw : u ^ (n % 2 + 2 * (n / 2))
| u ^ n

Tactic:
rw [← Nat.mod_add_div n 2]

Premises used: Nat.mod_add_div, OfNat.ofNat
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
n : ℕ
rw : u ^ (n % 2)
| u ^ (n % 2 + 2 * (n / 2))

Tactic:
rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

Premises used: one_pow, pow_add, pow_mul, Int.units_sq, mul_one
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
n : ℕ
rw : u ^ (n % 2)
| u ^ n = u ^ (n % 2)

Tactic:
lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

Premises used: one_pow, pow_add, pow_mul, Nat.mod_add_div, Int.units_sq, mul_one, OfNat.ofNat
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
n : ℕ
conv : u ^ n = u ^ (n % 2)
conv₁ : u ^ (n % 2) = u ^ (n % 2)
⊢ 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]

Premises used: one_pow, pow_add, pow_mul, Nat.mod_add_div, Int.units_sq, mul_one, OfNat.ofNat
-- Module: Mathlib.Data.Int.Range
Goal:
m n r : ℤ
simp : (∃ (a : ℕ), m + (↑a : ℤ) < n ∧ m + (↑a : ℤ) = r) ↔ m ≤ r ∧ r < n
⊢ r ∈ m.range n ↔ m ≤ r ∧ r < n

Tactic:
simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]

Premises used: List.mem_range, add_comm, Int.range, Int.lt_toNat, lt_sub_iff_add_lt, List.mem_map
-- Module: Mathlib.Data.Int.Range
Goal:
m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + (↑(r - m).toNat : ℤ) < n ∧ m + (↑(r - m).toNat : ℤ) = r

Tactic:
simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]

Premises used: Iff.mpr, Int.toNat_of_nonneg, And.right, And.left, sub_nonneg
-- Module: Mathlib.Data.Int.Range
Goal:
m n r : ℤ
⊢ (∃ (a : ℕ), m + (↑a : ℤ) < n ∧ m + (↑a : ℤ) = r) ↔ m ≤ r ∧ r < n

Tactic:
exact ⟨fun ⟨a, ha⟩ => ha.2 ▸ ⟨le_add_of_nonneg_right (Int.natCast_nonneg _), ha.1⟩,
    fun h => ⟨toNat (r - m), by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2] ⟩⟩
-- Module: Mathlib.Data.Int.Range
Goal:
P : ℤ → Prop
inst : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ m.range n → P r) ↔ ∀ (r : ℤ), m ≤ r → r < n → P r

Tactic:
simp only [mem_range_iff, and_imp]

Premises used: Int.mem_range_iff, and_imp
-- Module: Mathlib.Data.Int.Range
Goal:
P : ℤ → Prop
inst : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ m.range (n + 1) → P r) ↔ ∀ (r : ℤ), m ≤ r → r ≤ n → P r

Tactic:
simp only [mem_range_iff, and_imp, lt_add_one_iff]

Premises used: Int.mem_range_iff, and_imp, Int.lt_add_one_iff
-- Module: Mathlib.Data.Int.Sqrt
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 : ℤ)
rw₃ rw₄ : Eq (α := ℤ) (↑n.natAbs : ℤ) (↑n.natAbs : ℤ)
⊢ sqrt (n * n) = (↑n.natAbs : ℤ)

Tactic:
rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]

Premises used: Int.toNat_natCast, Int.natAbs_mul_self, Int.sqrt, Nat.sqrt_eq
-- Module: Mathlib.Data.Int.Sqrt
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
rw₃ rw₄ : n * n = n * n
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]

Premises used: Int.natAbs_mul_self, Int.sqrt_eq, Int.natCast_mul
-- Module: Mathlib.Data.Int.Sqrt
Goal:
n : ℤ
⊢ 0 ≤ sqrt n

Tactic:
natCast_nonneg _

Premises used: Int.sqrt, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Sqrt
Goal:
n : ℕ
rw : Eq (α := ℤ) (↑(toNat (↑n : ℤ)).sqrt : ℤ) (↑n.sqrt : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑n.sqrt : ℤ) (↑n.sqrt : ℤ)
⊢ sqrt (↑n : ℤ) = (↑n.sqrt : ℤ)

Tactic:
rw [sqrt, toNat_natCast]

Premises used: Int.toNat_natCast, Int.sqrt
-- Module: Mathlib.Data.Int.Sqrt
Goal:
n : ℕ
⊢ sqrt (OfNat.ofNat n) = (↑(Nat.sqrt (OfNat.ofNat n)) : ℤ)

Tactic:
sqrt_natCast _

Premises used: Int.sqrt_natCast
-- Module: Mathlib.Data.Int.Star
Goal:
n : ℕ
hn : Even n
⊢ Eq (α := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) (nonneg ℤ)

Tactic:
le_antisymm (closure_le.2 <| range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ ?_

Premises used: Iff.mpr, Even.pow_nonneg, le_antisymm, AddSubmonoid.closure_le, Set.range_subset_iff
-- Module: Mathlib.Data.Int.Star
Goal:
n : ℕ
hn : Even n
refine :
  ∀ (x : ℤ) (hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x),
    Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) x
⊢ Eq (α := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) (nonneg ℤ)

Tactic:
refine le_antisymm (closure_le.2 <| range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ ?_

Premises used: Iff.mpr, le_antisymm, AddSubmonoid.closure_le, Set.range_subset_iff
-- Module: Mathlib.Data.Int.Star
Goal:
n : ℕ
hn : Even n
x : ℤ
hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x
⊢ x = x.natAbs • HPow.hPow (α := ℤ) 1 n

Tactic:
simpa [eq_comm (a := x)] using hx

Premises used: eq_comm
-- Module: Mathlib.Data.Int.Star
Goal:
n : ℕ
hn : Even n
x : ℤ
hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x
⊢ x = x.natAbs • HPow.hPow (α := ℤ) 1 n

Tactic:
have : x = x.natAbs • 1 ^ n := by simpa [eq_comm (a := x)] using hx
-- Module: Mathlib.Data.Int.Star
Goal:
n : ℕ
hn : Even n
x : ℤ
hx : Membership.mem (γ := AddSubmonoid ℤ) (nonneg ℤ) x
this : x = x.natAbs • HPow.hPow (α := ℤ) 1 n
rw : Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) (x.natAbs • HPow.hPow (α := ℤ) 1 n)
⊢ Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x ^ n)) x

Tactic:
rw [this]
-- Module: Mathlib.Data.Int.Star
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.natAbs • HPow.hPow (α := ℤ) 1 n)

Tactic:
nsmul_mem (subset_closure <| mem_range_self _) _

Premises used: Set.mem_range_self, AddSubmonoid.subset_closure, nsmul_mem
-- Module: Mathlib.Data.Int.Star
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.natAbs • HPow.hPow (α := ℤ) 1 n)

Tactic:
exact nsmul_mem (subset_closure <| mem_range_self _) _

Premises used: Set.mem_range_self, AddSubmonoid.subset_closure, nsmul_mem
-- Module: Mathlib.Data.Int.Star
Goal:
⊢ Eq (α := AddSubmonoid ℤ) (closure (range fun (x : ℤ) ↦ x * x)) (nonneg ℤ)

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow even_two

Premises used: even_two, sq, Int.addSubmonoid_closure_range_pow
-- Module: Mathlib.Data.Int.Star
Goal:
a b : ℤ
⊢ a ≤ b ↔ ∃ (p : ℤ), Membership.mem (γ := AddSubmonoid ℤ) (closure (range fun (s : ℤ) ↦ star s * s)) p ∧ b = a + p

Tactic:
simp [eq_comm, le_iff_exists_nonneg_add (a := a)]

Premises used: eq_comm, le_iff_exists_nonneg_add
-- Module: Mathlib.Data.Int.SuccPred
Goal:
⊢ Order.succ = succ

Tactic:
rfl

Premises used: Order.succ, Int.succ, rfl
-- Module: Mathlib.Data.Int.SuccPred
Goal:
⊢ Order.pred = pred

Tactic:
rfl

Premises used: Int.pred, Order.pred, rfl
-- Module: Mathlib.Data.Int.SuccPred
Goal:
a b : ℤ
h : a ≤ b
rw : a + (↑(b - a).toNat : ℤ) = b
rw₁ : a + (b - a) = b
rw₂ : a + b - a = b
rw₃ rw₄ : b = b
⊢ Order.succ^[(b - a).toNat] a = b

Tactic:
rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]

Premises used: add_sub_assoc, add_sub_cancel_left, Int.toNat_sub_of_le, Order.succ_iterate
-- Module: Mathlib.Data.Int.SuccPred
Goal:
a b : ℤ
h : a ≤ b
rw : b - (↑(b - a).toNat : ℤ) = a
rw₁ : b - (b - a) = a
rw₂ rw₃ : a = a
⊢ Order.pred^[(b - a).toNat] b = a

Tactic:
rw [pred_iterate, toNat_sub_of_le h, sub_sub_cancel]

Premises used: Order.pred_iterate, Int.toNat_sub_of_le, sub_sub_cancel
-- Module: Mathlib.Data.Int.SuccPred
Goal:
a b : ℕ
rw : HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 = (↑b : ℤ) ↔ a + 1 = b
⊢ CovBy (α := ℤ) (↑a : ℤ) (↑b : ℤ) ↔ a ⋖ b

Tactic:
rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]

Premises used: Order.covBy_iff_add_one_eq
-- Module: Mathlib.Data.Int.SuccPred
Goal:
a b : ℕ
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 = (↑b : ℤ) ↔ a + 1 = b

Tactic:
Int.natCast_inj

Premises used: Int.add, Int.natCast_inj
-- Module: Mathlib.Data.Int.SuccPred
Goal:
a b : ℕ
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 = (↑b : ℤ) ↔ a + 1 = b

Tactic:
exact Int.natCast_inj

Premises used: Int.natCast_inj
-- Module: Mathlib.Data.Int.WithZero
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
rw₃ rw₄ : Eq (α := ℝ≥0) 1 1
⊢ Eq (α := ℝ≥0)
    (if hx : Eq (α := WithZero (Multiplicative ℤ)) 1 0 then 0
    else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ))
    1

Tactic:
rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]

Premises used: WithZero.unzero_coe, zpow_zero, toAdd_one, dif_neg, one_ne_zero
-- Module: Mathlib.Data.Int.WithZero
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) : ℤ))
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) : ℤ))
⊢ (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
-- Module: Mathlib.Data.Int.WithZero
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) : ℤ))
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) : ℤ))
⊢ (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

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.Data.Int.WithZero
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) : ℤ))
pos₂ pos₃ : Eq (α := ℝ≥0) 0 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:
rw [dif_pos hxy, dif_pos hx, zero_mul]

Premises used: MulZeroClass.zero_mul, dif_pos
-- Module: Mathlib.Data.Int.WithZero
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) : ℤ))
pos₁ :
  0 =
    HMul.hMul (α := ℝ≥0)
      (if hx : x = 0 then 0 else HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)) 0
pos₂ pos₃ : Eq (α := ℝ≥0) 0 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:
rw [dif_pos hxy, dif_pos hy, mul_zero]

Premises used: dif_pos, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
⊢ x ≠ 0

Tactic:
obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
⊢ y ≠ 0

Tactic:
obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg :
  HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hxy) : ℤ) =
    HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx * unzero hy) : ℤ)
⊢ (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:
rw [dif_neg hxy, dif_neg hx, dif_neg hy, ← zpow_add' (Or.inl he), ← toAdd_mul]

Premises used: toAdd_mul, zpow_add', dif_neg, Or.inl
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : unzero hxy = unzero hx * unzero hy
⊢ HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hxy) : ℤ) =
    HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx * unzero hy) : ℤ)

Tactic:
congr
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
neg : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = (↑(unzero hx * unzero hy) : WithZero (Multiplicative ℤ))
neg₁ :
  (↑(unzero hxy) : WithZero (Multiplicative ℤ)) =
    (↑(unzero hx) : WithZero (Multiplicative ℤ)) * (↑(unzero hy) : WithZero (Multiplicative ℤ))
neg₂ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * (↑(unzero hy) : WithZero (Multiplicative ℤ))
neg₃ : (↑(unzero hxy) : WithZero (Multiplicative ℤ)) = x * y
neg₄ neg₅ : x * y = x * y
⊢ unzero hxy = unzero hx * unzero hy

Tactic:
rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]

Premises used: WithZero.coe_inj, WithZero.coe_unzero, WithZero.coe_mul
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x : WithZero (Multiplicative ℤ)
hx : x = 0
⊢ Eq (α := ℝ≥0) ((toNNReal he : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [toNNReal, hx]

Premises used: WithZeroMulInt.toNNReal
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : e ≠ 0
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
⊢ (toNNReal he : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x =
    HPow.hPow (β := ℤ) e ((toAdd : (a : Multiplicative ℤ) → ℤ) (unzero hx) : ℤ)

Tactic:
simp [toNNReal, hx]

Premises used: WithZeroMulInt.toNNReal
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : e ≠ 0
hm : m ≠ 0
⊢ Ne (α := ℝ≥0) ((toNNReal he : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp only [ne_eq, map_eq_zero, hm, not_false_eq_true]

Premises used: map_eq_zero, ne_eq, not_false_eq_true
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : e ≠ 0
hm : m ≠ 0
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((toNNReal he : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0)

Tactic:
lt_of_le_of_ne zero_le' (toNNReal_ne_zero he hm).symm

Premises used: WithZeroMulInt.toNNReal_ne_zero, Ne.symm, zero_le', lt_of_le_of_ne
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : 1 < e
x y : WithZero (Multiplicative ℤ)
zero :
  x < 0 →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
coe :
  ∀ (a : Multiplicative ℤ),
    x < (↑a : WithZero (Multiplicative ℤ)) →
      LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
⊢ x < y →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) y : ℝ≥0)

Tactic:
cases y
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
⊢ x < 0 →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
a : Multiplicative ℤ
coe :
  0 < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
coe₁ :
  ∀ (a_1 : Multiplicative ℤ),
    (↑a_1 : WithZero (Multiplicative ℤ)) < (↑a : WithZero (Multiplicative ℤ)) →
      LT.lt (α := ℝ≥0)
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a_1 : WithZero (Multiplicative ℤ)) : ℝ≥0)
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)
⊢ x < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) x : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)

Tactic:
cases x
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : 1 < e
a : Multiplicative ℤ
⊢ 0 < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) 0 : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)

Tactic:
simpa using zpow_pos he.pos _

Premises used: LT.lt.pos, zpow_pos
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
he : 1 < e
a a_1 : Multiplicative ℤ
⊢ (↑a_1 : WithZero (Multiplicative ℤ)) < (↑a : WithZero (Multiplicative ℤ)) →
    LT.lt (α := ℝ≥0) ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a_1 : WithZero (Multiplicative ℤ)) : ℝ≥0)
      ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) (↑a : WithZero (Multiplicative ℤ)) : ℝ≥0)

Tactic:
simp [toNNReal, he]

Premises used: WithZeroMulInt.toNNReal
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
pos : ∀ (hm : m = 0), Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
neg :
  ∀ (hm : ¬m = 0), Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : m = 0
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1

Tactic:
simp only [hm, map_zero, zero_ne_one]

Premises used: map_zero, zero_ne_one
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1

Tactic:
⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩

Premises used: Eq.rec, map_one, Iff.intro, Eq.symm, WithZeroMulInt.toNNReal
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
neg : ∀ (h1 : Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)), m = 1
⊢ Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0) ↔ m = 1

Tactic:
refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : Eq (α := ℝ≥0) ((toNNReal he0 : (a : WithZero (Multiplicative ℤ)) → ℝ≥0) m : ℝ≥0) (1 : ℝ≥0)
⊢ unzero hm = 1

Tactic:
rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1

Premises used: zero_le, WithZeroMulInt.toNNReal_neg_apply, toAdd_eq_zero, zpow_eq_one_iff_right₀
-- Module: Mathlib.Data.Int.WithZero
Goal:
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
neg : (↑(unzero hm) : WithZero (Multiplicative ℤ)) = 1
neg₁ : Eq (α := WithZero (Multiplicative ℤ)) (↑1 : WithZero (Multiplicative ℤ)) 1
neg₂ neg₃ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
⊢ m = 1

Tactic:
rw [← WithZero.coe_unzero hm, h1, coe_one]

Premises used: WithZero.coe_unzero, WithZero.coe_one