awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
i : ℕ
h : IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)
⊢ IsSquare (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1).sign ↔ 0 ≤ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1
have succ : IsSquare (sign (↑(i + 1) : ℤ)) ↔ 0 ≤ i + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
⊢ IsSquare (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1).sign ↔ 0 ≤ HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1
have pred : IsSquare (α := ℤ) (-1) ↔ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 ≤ 0
Tactic: rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
⊢ IsSquare (α := ℤ) (-1) ↔ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 ≤ 0
have pred : IsSquare (α := ℤ) (-1) ↔ i + 1 ≤ 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
⊢ IsSquare (α := ℤ) (-1) ↔ i + 1 ≤ 0
have pred : ¬IsSquare (α := ℤ) (-1)
Tactic: simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
z : ℤ
⊢ IsSquare z.sign ↔ 0 ≤ z
have zero : IsSquare (sign 0) ↔ LE.le (α := ℤ) 0 0
Tactic: induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
z : ℤ
zero : IsSquare (sign 0) ↔ LE.le (α := ℤ) 0 0
⊢ IsSquare z.sign ↔ 0 ≤ z
have succ : ∀ (i : ℕ),
  (IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)) →
    (IsSquare (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1).sign ↔ 0 ≤ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
Tactic: induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
z : ℤ
zero : IsSquare (sign 0) ↔ LE.le (α := ℤ) 0 0
succ :
  ∀ (i : ℕ),
    (IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)) →
      (IsSquare (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1).sign ↔ 0 ≤ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
⊢ IsSquare z.sign ↔ 0 ≤ z
have pred : ∀ (i : ℕ),
  (IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))) →
    (IsSquare (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1).sign ↔ 0 ≤ HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
Tactic: induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u : ℤˣ
⊢ (↑u : ℤ).natAbs * (↑u⁻¹ : ℤ).natAbs = 1
have rw : natAbs 1 = 1
Tactic: rw [← natAbs_mul, Units.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u : ℤˣ
⊢ (↑u⁻¹ : ℤ).natAbs * (↑u : ℤ).natAbs = 1
have rw : natAbs 1 = 1
Tactic: rw [← natAbs_mul, Units.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u ≠ v ↔ u = -v
have inl : ∀ (hu : IsUnit (M := ℤ) 1), 1 ≠ v ↔ 1 = -v
Tactic: obtain rfl | rfl := isUnit_eq_one_or hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
hu : IsUnit u
hv : IsUnit v
inl : ∀ (hu : IsUnit (M := ℤ) 1), 1 ≠ v ↔ 1 = -v
⊢ u ≠ v ↔ u = -v
have inr : ∀ (hu : IsUnit (M := ℤ) (-1)), -1 ≠ v ↔ -1 = -v
Tactic: obtain rfl | rfl := isUnit_eq_one_or hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) 1
⊢ 1 ≠ v ↔ 1 = -v
have inl : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) 1 1 ↔ Eq (α := ℤ) 1 (-1)
Tactic: obtain rfl | rfl := isUnit_eq_one_or hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) 1
inl : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) 1 1 ↔ Eq (α := ℤ) 1 (-1)
⊢ 1 ≠ v ↔ 1 = -v
have inl₁ : ∀ (hv : IsUnit (M := ℤ) (-1)), Ne (α := ℤ) 1 (-1) ↔ Eq (α := ℤ) 1 (- -1)
Tactic: obtain rfl | rfl := isUnit_eq_one_or hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) (-1)
⊢ -1 ≠ v ↔ -1 = -v
have inr : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) (-1) 1 ↔ Eq (α := ℤ) (-1) (-1)
Tactic: obtain rfl | rfl := isUnit_eq_one_or hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) (-1)
inr : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) (-1) 1 ↔ Eq (α := ℤ) (-1) (-1)
⊢ -1 ≠ v ↔ -1 = -v
have inr₁ : ∀ (hv : IsUnit (M := ℤ) (-1)), Ne (α := ℤ) (-1) (-1) ↔ Eq (α := ℤ) (-1) (- -1)
Tactic: obtain rfl | rfl := isUnit_eq_one_or hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1
have refine : ∀ (h : u = 1 ∨ u = -1), IsUnit u
Tactic: refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u : ℤ
h : u = 1 ∨ u = -1
⊢ IsUnit u
have inl : IsUnit (M := ℤ) 1
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u : ℤ
h : u = 1 ∨ u = -1
inl : IsUnit (M := ℤ) 1
⊢ IsUnit u
have inr : IsUnit (M := ℤ) (-1)
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (hypothesis)
Goal:
u v : ℤ
h : u * v = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
have h' : v * u = 1
Tactic: have h' : v * u = 1 := mul_comm u v ▸ h
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u * v = 1
h' : v * u = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
have inl : ∀ (h : 1 * v = 1) (h' : v * 1 = 1), Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h
Cleared hypotheses: u, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u * v = 1
h' : v * u = 1
inl : ∀ (h : 1 * v = 1) (h' : v * 1 = 1), Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
have inr : ∀ (h : -1 * v = 1) (h' : v * -1 = 1), Eq (α := ℤ) (-1) 1 ∧ v = 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = -1
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h
Cleared hypotheses: u, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
h : 1 * v = 1
h' : v * 1 = 1
⊢ Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1
have inl : ∀ (h h' : HMul.hMul (α := ℤ) 1 1 = 1), Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'
Cleared hypotheses: v, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
h : 1 * v = 1
h' : v * 1 = 1
inl : ∀ (h h' : HMul.hMul (α := ℤ) 1 1 = 1), Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
⊢ Eq (α := ℤ) 1 1 ∧ v = 1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = -1
have inl₁ : ∀ (h : HMul.hMul (α := ℤ) 1 (-1) = 1) (h' : HMul.hMul (α := ℤ) (-1) 1 = 1),
  Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) (-1)
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'
Cleared hypotheses: v, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
⊢ Eq (α := ℤ) (-1) 1 ∧ v = 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = -1
have inr : ∀ (h : HMul.hMul (α := ℤ) (-1) 1 = 1) (h' : HMul.hMul (α := ℤ) 1 (-1) = 1),
  Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 (-1)
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'
Cleared hypotheses: v, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
inr :
  ∀ (h : HMul.hMul (α := ℤ) (-1) 1 = 1) (h' : HMul.hMul (α := ℤ) 1 (-1) = 1),
    Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 (-1)
⊢ Eq (α := ℤ) (-1) 1 ∧ v = 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = -1
have inr₁ : ∀ (h h' : HMul.hMul (α := ℤ) (-1) (-1) = 1),
  Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)
Tactic: obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h'
Cleared hypotheses: v, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
h h' : HMul.hMul (α := ℤ) 1 1 = 1
⊢ Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
have inl : ¬(Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1) → Eq (α := ℤ) 1 (-1)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
h h' : HMul.hMul (α := ℤ) 1 1 = 1
inl inl₁ : ¬(Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1) → Eq (α := ℤ) 1 (-1)
⊢ Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)
have inl₂ : ¬Eq (α := ℤ) 1 1 → Eq (α := ℤ) 1 (-1)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
h h' : HMul.hMul (α := ℤ) (-1) (-1) = 1
⊢ Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)
have inr : ¬(Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1) → Eq (α := ℤ) (-1) (-1)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
h h' : HMul.hMul (α := ℤ) (-1) (-1) = 1
inr inr₁ : ¬(Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1) → Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)
have inr₂ : ¬Eq (α := ℤ) (-1) 1 → Eq (α := ℤ) (-1) (-1)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
have refine_1 : ∀ (h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1) (H : u = 1 ∧ v = 1), u * v = 1
Tactic: refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
refine_1 : ∀ (h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1) (H : u = 1 ∧ v = 1), u * v = 1
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
have refine_2 : ∀ (h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1) (H : u = -1 ∧ v = -1), u * v = 1
Tactic: refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = 1 ∧ v = 1
⊢ u * v = 1
have refine_1 : ∀ (h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) 1 1 ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) 1 (-1)), HMul.hMul (α := ℤ) 1 1 = 1
Tactic: obtain ⟨rfl, rfl⟩ := H
Cleared hypotheses: u, v, h, H
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = -1 ∧ v = -1
⊢ u * v = 1
have refine_2 : ∀ (h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) (-1) 1 ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) (-1) (-1)),
  HMul.hMul (α := ℤ) (-1) (-1) = 1
Tactic: obtain ⟨rfl, rfl⟩ := H
Cleared hypotheses: u, v, h, H
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u * v = -1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
have inl : ∀ (h : 1 * v = -1), Eq (α := ℤ) 1 1 ∧ v = -1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = 1
Tactic: obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u * v = -1
inl : ∀ (h : 1 * v = -1), Eq (α := ℤ) 1 1 ∧ v = -1 ∨ Eq (α := ℤ) 1 (-1) ∧ v = 1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
have inr : ∀ (h : -1 * v = -1), Eq (α := ℤ) (-1) 1 ∧ v = -1 ∨ Eq (α := ℤ) (-1) (-1) ∧ v = 1
Tactic: obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
have refine_1 : ∀ (h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1) (H : u = 1 ∧ v = -1), u * v = -1
Tactic: refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
refine_1 : ∀ (h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1) (H : u = 1 ∧ v = -1), u * v = -1
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
have refine_2 : ∀ (h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1) (H : u = -1 ∧ v = 1), u * v = -1
Tactic: refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = 1 ∧ v = -1
⊢ u * v = -1
have refine_1 : ∀ (h : Eq (α := ℤ) 1 1 ∧ Eq (α := ℤ) (-1) (-1) ∨ Eq (α := ℤ) 1 (-1) ∧ Eq (α := ℤ) (-1) 1),
  HMul.hMul (α := ℤ) 1 (-1) = -1
Tactic: obtain ⟨rfl, rfl⟩ := H
Cleared hypotheses: u, v, h, H
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (goal)
Goal:
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
⊢ u * v = -1
have refine_2 : ∀ (h : Eq (α := ℤ) (-1) 1 ∧ Eq (α := ℤ) 1 (-1) ∨ Eq (α := ℤ) (-1) (-1) ∧ Eq (α := ℤ) 1 1),
  HMul.hMul (α := ℤ) (-1) 1 = -1
Tactic: obtain ⟨rfl, rfl⟩ := H
Cleared hypotheses: u, v, h, H
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (hypothesis)
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
have ha₁ : a = 1 ∨ a = -1
Tactic: rw [isUnit_iff] at ha hb hc hd
Cleared hypotheses: ha, hb, hc, hd
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (hypothesis)
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
have hb₁ : b = 1 ∨ b = -1
Tactic: rw [isUnit_iff] at ha hb hc hd
Cleared hypotheses: ha, hb, hc, hd
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (hypothesis)
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
hb₁ : b = 1 ∨ b = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
have hc₁ : c = 1 ∨ c = -1
Tactic: rw [isUnit_iff] at ha hb hc hd
Cleared hypotheses: ha, hb, hc, hd
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Units (hypothesis)
Goal:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
ha₁ : a = 1 ∨ a = -1
hb₁ : b = 1 ∨ b = -1
hc₁ : c = 1 ∨ c = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
have hd₁ : d = 1 ∨ d = -1
Tactic: rw [isUnit_iff] at ha hb hc hd
Cleared hypotheses: ha, hb, hc, hd
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute a b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
  @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
Tactic: rw [h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
h : Commute b a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (b * a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _) =
  @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * (a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _)
Tactic: rw [h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1
Tactic: rw [mul_assoc, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [mul_assoc, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw₂ : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = a * 1
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
rw₂ : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = a * 1
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw₃ : 1 * a = a * 1
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
rw₂ : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = a * 1
rw₃ : 1 * a = a * 1
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw₄ : 1 * a = a
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible (a * b)
rw : a * (b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a)) = a * 1
rw₁ : a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = a * 1
rw₂ : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = a * 1
rw₃ : 1 * a = a * 1
rw₄ : 1 * a = a
⊢ b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a) = 1
have rw₅ : a = a
Tactic: rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw₂ : b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b)) = 1 * b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
rw₂ : b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b)) = 1 * b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw₃ : b * 1 = 1 * b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
rw₂ : b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b)) = 1 * b
rw₃ : b * 1 = 1 * b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw₄ : b = 1 * b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a * b = 1 * b
rw₁ : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b) = 1 * b
rw₂ : b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * (a * b)) = 1 * b
rw₃ : b * 1 = 1 * b
rw₄ : b = 1 * b
⊢ b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ * a = 1
have rw₅ : b = b
Tactic: rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
⊢ a * (b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _) = 1
have rw : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ = 1
Tactic: rw [← mul_assoc, mul_invOf_self]