awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (hypothesis)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
⊢ a + b = b + a
have h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
Tactic: have h₁ : (1 + 1 : R) * (a + b) = a + (a + b) + b := by
      rw [left_distrib]
      simp only [right_distrib, one_mul, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
⊢ HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
have rw : 1 * (a + b) + 1 * (a + b) = a + (b + a) + b
Tactic: rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (hypothesis)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
⊢ a + b = b + a
have h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
Tactic: have h₂ : (1 + 1 : R) * (a + b) = a + (b + a) + b := by
      rw [right_distrib]
      simp only [left_distrib, one_mul, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (hypothesis)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
⊢ a + b = b + a
have this₁ : a + (a + b) + b = a + (b + a) + b
Tactic: have := h₁.symm.trans h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
this : a + (a + b) + b = a + (b + a) + b
⊢ a + b = b + a
have rwa : ∀ (this : a + (a + b) = a + (b + a)), a + b = b + a
Tactic: rwa [add_left_inj, add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
this : a + (a + b) + b = a + (b + a) + b
rwa : ∀ (this : a + (a + b) = a + (b + a)), a + b = b + a
⊢ a + b = b + a
have rwa₁ : ∀ (this : a + b = b + a), a + b = b + a
Tactic: rwa [add_left_inj, add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = HAdd.hAdd (α := R) 0 0 * a
have rw : 0 * a = 0 * a
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ HAdd.hAdd (α := R) 0 0 * a = 0 * a + 0 * a
have rw : 0 * a + 0 * a = 0 * a + 0 * a
Tactic: rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (hypothesis)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = 0
have this₁ : 0 * a = 0 * a + 0 * a
Tactic: have : 0 * a = 0 * a + 0 * a :=
      calc 0 * a = (0 + 0) * a := by rw [zero_add]
      _ = 0 * a + 0 * a := by rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
⊢ 0 * a = 0
have rwa : ∀ (this : 0 * a = 0), 0 * a = 0
Tactic: rwa [left_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = a * HAdd.hAdd (α := R) 0 0
have rw : a * 0 = a * 0
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * HAdd.hAdd (α := R) 0 0 = a * 0 + a * 0
have rw : a * 0 + a * 0 = a * 0 + a * 0
Tactic: rw [left_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (hypothesis)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = 0
have this₁ : a * 0 = a * 0 + a * 0
Tactic: have : a * 0 = a * 0 + a * 0 :=
      calc a * 0 = a * (0 + 0) := by rw [zero_add]
      _ = a * 0 + a * 0 := by rw [left_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
⊢ a * 0 = 0
have rwa : ∀ (this : a * 0 = 0), a * 0 = 0
Tactic: rwa [left_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
⊢ a * 1 = a
have rw : 1 * a = a
Tactic: rw [mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
rw : 1 * a = a
⊢ a * 1 = a
have rw₁ : a = a
Tactic: rw [mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
⊢ (a + b) * c = a * c + b * c
have rw : c * (a + b) = a * c + b * c
Tactic: rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
rw : c * (a + b) = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₁ : c * a + c * b = a * c + b * c
Tactic: rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₂ : a * c + c * b = a * c + b * c
Tactic: rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : a * c + c * b = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₃ : a * c + c * b = a * c + c * b
Tactic: rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
⊢ (n + 1).negOnePow = -n.negOnePow
have rw : n.negOnePow * negOnePow 1 = -n.negOnePow
Tactic: rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
rw : n.negOnePow * negOnePow 1 = -n.negOnePow
⊢ (n + 1).negOnePow = -n.negOnePow
have rw₁ : n.negOnePow * -1 = -n.negOnePow
Tactic: rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
rw : n.negOnePow * negOnePow 1 = -n.negOnePow
rw₁ : n.negOnePow * -1 = -n.negOnePow
⊢ (n + 1).negOnePow = -n.negOnePow
have rw₂ : -(n.negOnePow * 1) = -n.negOnePow
Tactic: rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
rw : n.negOnePow * negOnePow 1 = -n.negOnePow
rw₁ : n.negOnePow * -1 = -n.negOnePow
rw₂ : -(n.negOnePow * 1) = -n.negOnePow
⊢ (n + 1).negOnePow = -n.negOnePow
have rw₃ : -n.negOnePow = -n.negOnePow
Tactic: rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
hn : Even n
⊢ n.negOnePow = 1
have obtain : ∀ (k : ℤ), (k + k).negOnePow = 1
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
k : ℤ
⊢ (k + k).negOnePow = 1
have rw : k.negOnePow * k.negOnePow = 1
Tactic: rw [negOnePow_add, units_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
k : ℤ
rw : k.negOnePow * k.negOnePow = 1
⊢ (k + k).negOnePow = 1
have rw₁ : Eq (α := ℤˣ) 1 1
Tactic: rw [negOnePow_add, units_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
hn : Odd n
⊢ n.negOnePow = -1
have obtain : ∀ (k : ℤ), (2 * k + 1).negOnePow = -1
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
⊢ n.negOnePow = 1 ↔ Even n
have mp : n.negOnePow = 1 → Even n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
mp : n.negOnePow = 1 → Even n
⊢ n.negOnePow = 1 ↔ Even n
have mpr : Even n → n.negOnePow = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
h : n.negOnePow = 1
⊢ Even n
have mp : ¬Odd n
Tactic: rw [← Int.not_odd_iff_even]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (hypothesis)
Goal:
n : ℤ
h : n.negOnePow = 1
h' : Odd n
⊢ False
have h₁ : Eq (α := ℤˣ) (-1) 1
Tactic: simp only [negOnePow_odd _ h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n
have mp : n.negOnePow = -1 → Odd n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
mp : n.negOnePow = -1 → Odd n
⊢ n.negOnePow = -1 ↔ Odd n
have mpr : Odd n → n.negOnePow = -1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
h : n.negOnePow = -1
⊢ Odd n
have mp : ¬Even n
Tactic: rw [← Int.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (hypothesis)
Goal:
n : ℤ
h : n.negOnePow = -1
h' : Even n
⊢ False
have h₁ : Eq (α := ℤˣ) 1 (-1)
Tactic: rw [negOnePow_even _ h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
⊢ |(↑n.negOnePow : ℤ)| = 1
have rw : Eq (α := ℤ) (↑(↑n.negOnePow : ℤ).natAbs : ℤ) 1
Tactic: rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(↑n.negOnePow : ℤ).natAbs : ℤ) 1
⊢ |(↑n.negOnePow : ℤ)| = 1
have rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
Tactic: rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(↑n.negOnePow : ℤ).natAbs : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ |(↑n.negOnePow : ℤ)| = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
⊢ |n|.negOnePow = n.negOnePow
have inl : ∀ (h : |n| = n), |n|.negOnePow = n.negOnePow
Tactic: obtain h | h := abs_choice n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n : ℤ
inl : ∀ (h : |n| = n), |n|.negOnePow = n.negOnePow
⊢ |n|.negOnePow = n.negOnePow
have inr : ∀ (h : |n| = -n), |n|.negOnePow = n.negOnePow
Tactic: obtain h | h := abs_choice n
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
have pos : ∀ (h₂ : Even n₂), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
Tactic: by_cases h₂ : Even n₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
pos : ∀ (h₂ : Even n₂), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
have neg : ∀ (h₂ : ¬Even n₂), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
Tactic: by_cases h₂ : Even n₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
have pos : Even n₁ ↔ (Even n₁ ↔ Even n₂)
Tactic: rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
have pos : Even n₁ → (Even n₁ ↔ Even n₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ → (Even n₁ ↔ Even n₂)
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
have pos₁ : (Even n₁ ↔ Even n₂) → Even n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ → (Even n₁ ↔ Even n₂)
pos₁ : (Even n₁ ↔ Even n₂) → Even n₁
pos₂ pos₃ : Even n₁ → (Even n₁ ↔ Even n₂)
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
have pos₄ : Even n₁ → Even n₁ → Even n₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ → (Even n₁ ↔ Even n₂)
pos₁ : (Even n₁ ↔ Even n₂) → Even n₁
pos₂ pos₃ : Even n₁ → (Even n₁ ↔ Even n₂)
pos₄ : Even n₁ → Even n₁ → Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
have pos₅ : Even n₁ → Even n₂ → Even n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ → (Even n₁ ↔ Even n₂)
pos₁ : (Even n₁ ↔ Even n₂) → Even n₁
pos₂ pos₃ : Even n₁ → (Even n₁ ↔ Even n₂)
pos₄ : Even n₁ → Even n₁ → Even n₂
pos₅ pos₆ : Even n₁ → Even n₂ → Even n₁
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)
have pos₇ : ¬Even n₁ → ¬Even n₂ → Even n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (hypothesis)
Goal:
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
have h₃ : Odd n₂
Tactic: rw [Int.not_even_iff_odd] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
have neg : Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
Tactic: rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₅ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₅ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₆ : ¬Odd n₁ → ¬Odd n₂ → Odd n₁
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.NegOnePow (goal)
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₅ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
neg₆ : ¬Odd n₁ → ¬Odd n₂ → Odd n₁
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
have neg₇ : ¬¬Odd n₁ → ¬¬Odd n₂ → Odd n₁
Tactic: tauto