awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₄ : (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₄ : (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₅ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₄ : (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₅ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₆ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * (x⁻¹ * x)
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₄ : (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₅ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x
rw₆ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * (x⁻¹ * x)
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₇ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * 1
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
Tactic: have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
    Nat.recOn n (by simp) fun n h => by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
have rw : 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
Tactic: rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc,
    mul_inv_cancel₀ h₃]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
have simp : (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
Tactic: simp only [inv_pow, sub_eq_add_neg, mul_add, one_mul, mul_neg, add_mul, mul_inv_cancel₀ hx0,
    neg_mul, mul_assoc, mul_one, add_comm, neg_add_rev, neg_neg, h₄, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
have rw : -x + (x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
Tactic: rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : -x + (x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
have rw₁ : -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
Tactic: rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : -x + (x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
rw₁ : -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
have rw₂ : -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1))
Tactic: rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x x_1 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
⊢ x = x_1
have obtain : ∀ (x_2 : R) (hx : a * x_2 = 1), x = x_1
Tactic: obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x x_1 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
⊢ x = x_1
have obtain : ∀ (x_2 : R) (hx : a * x_2 = 1), x = x_1
Tactic: obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) ⋯) = 1
have h₁ : (if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) sorry) = choose (p := fun (x : R) ↦ a * x = 1) sorry
Tactic: convert! Classical.choose_spec (h.mul_inv_cancel ha)
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y : R, x * y = 1
have hex : ∃ (x_1 : R), x * x_1 = 1
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
hex : ∃ (x_1 : R), x * x_1 = 1
⊢ ∃! y : R, x * y = 1
have hunique : ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)
have rw : y = y * 1
Tactic: rw [hxz, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : y = y * 1
⊢ y = y * (x * z)
have rw₁ : y = y
Tactic: rw [hxz, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z
have rw : y * x * z = x * y * z
Tactic: rw [← mul_assoc, hf.mul_comm y x]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : y * x * z = x * y * z
⊢ y * (x * z) = x * y * z
have rw₁ : x * y * z = x * y * z
Tactic: rw [← mul_assoc, hf.mul_comm y x]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z
have rw : 1 * z = z
Tactic: rw [hxy, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : 1 * z = z
⊢ x * y * z = z
have rw₁ : z = z
Tactic: rw [hxy, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
have y₁ : y = y * (x * z)
Tactic: calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
y₁ : y = y * (x * z)
⊢ y = z
have y₂ : y * (x * z) = x * y * z
Tactic: calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.IsField (goal)
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
y₁ : y = y * (x * z)
y₂ : y * (x * z) = x * y * z
⊢ y = z
have y₃ : x * y * z = z
Tactic: calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.ModEq (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]
have rw : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p * c⁻¹]
Tactic: rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.ModEq (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
rw : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p * c⁻¹]
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]
have rw₁ : a * c ≡ b * c [PMOD p] ↔ a / c⁻¹ ≡ b / c⁻¹ [PMOD p]
Tactic: rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.ModEq (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
rw : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p * c⁻¹]
rw₁ : a * c ≡ b * c [PMOD p] ↔ a / c⁻¹ ≡ b / c⁻¹ [PMOD p]
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]
have rw₂ : a * c ≡ b * c [PMOD p] ↔ a * c ≡ b / c⁻¹ [PMOD p]
Tactic: rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.ModEq (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
rw : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p * c⁻¹]
rw₁ : a * c ≡ b * c [PMOD p] ↔ a / c⁻¹ ≡ b / c⁻¹ [PMOD p]
rw₂ : a * c ≡ b * c [PMOD p] ↔ a * c ≡ b / c⁻¹ [PMOD p]
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]
have rw₃ : a * c ≡ b * c [PMOD p] ↔ a * c ≡ b * c [PMOD p]
Tactic: rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.NegOnePow (goal)
Goal:
K : Type u_1
n : ℤ
inst : DivisionRing K
⊢ (↑(↑n.negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) n
have inl : ∀ (k : ℤ), (↑(↑(2 * k).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k)
Tactic: rcases even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Field.NegOnePow (goal)
Goal:
K : Type u_1
n : ℤ
inst : DivisionRing K
inl : ∀ (k : ℤ), (↑(↑(2 * k).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k)
⊢ (↑(↑n.negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) n
have inr : ∀ (k : ℤ), (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k + 1)
Tactic: rcases even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Field.NegOnePow (goal)
Goal:
K : Type u_1
inst : DivisionRing K
k : ℤ
⊢ (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k + 1)
have inr : (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (β := ℕ) (-1) 2 ^ k * -1
Tactic: rw [zpow_add_one₀ (by simp), zpow_mul, zpow_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₃ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₅ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₅ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₆ : HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₅ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₅ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
have rw₆ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₂ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (unop (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]