awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(↑n : ℤ) : R) = (↑n : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(↑n : ℤ) : S) (↑n : S)
have rw₁ : f (↑n : R) = (↑n : S)
Tactic: rw [← intCast, Int.cast_natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(↑n : ℤ) : R) = (↑n : S)
rw₁ : f (↑n : R) = (↑n : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(↑n : ℤ) : S) (↑n : S)
have rw₂ : Eq.{u_2 + 1} (α := S) (↑n : S) (↑n : S)
Tactic: rw [← intCast, Int.cast_natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (↑(Int.negSucc n) : S) (-(↑(n + 1) : S))
have rw : f (↑(Int.negSucc n) : R) = -(↑(n + 1) : S)
Tactic: rw [← intCast, Int.cast_negSucc, neg, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(Int.negSucc n) : R) = -(↑(n + 1) : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(Int.negSucc n) : S) (-(↑(n + 1) : S))
have rw₁ : f (-(↑(n + 1) : R)) = -(↑(n + 1) : S)
Tactic: rw [← intCast, Int.cast_negSucc, neg, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(Int.negSucc n) : R) = -(↑(n + 1) : S)
rw₁ : f (-(↑(n + 1) : R)) = -(↑(n + 1) : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(Int.negSucc n) : S) (-(↑(n + 1) : S))
have rw₂ : -f (↑(n + 1) : R) = -(↑(n + 1) : S)
Tactic: rw [← intCast, Int.cast_negSucc, neg, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(Int.negSucc n) : R) = -(↑(n + 1) : S)
rw₁ : f (-(↑(n + 1) : R)) = -(↑(n + 1) : S)
rw₂ : -f (↑(n + 1) : R) = -(↑(n + 1) : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(Int.negSucc n) : S) (-(↑(n + 1) : S))
have rw₃ : Eq.{u_2 + 1} (α := S) (-(↑(n + 1) : S)) (-(↑(n + 1) : S))
Tactic: rw [← intCast, Int.cast_negSucc, neg, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have inl : ∀ (m : ℕ) (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
Tactic: obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℤ
inl : ∀ (m : ℕ) (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have inr : ∀ (m : ℕ) (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)
Tactic: obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
have inl : ∀ (n : ℤ), (↑((↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑0 : ℤ) : α) (↑n : α)
Tactic: induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
inl : ∀ (n : ℤ), (↑((↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑0 : ℤ) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
have inl₁ : ∀ (m : ℕ) (ih : ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)) (n : ℤ),
  (↑((↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑(m + 1) : ℤ) : α) (↑n : α)
Tactic: induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)
have inr : ∀ (n : ℤ), (↑(-(↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑0 : ℤ)) : α) (↑n : α)
Tactic: induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
inr : ∀ (n : ℤ), (↑(-(↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑0 : ℤ)) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)
have inr₁ : ∀ (m : ℕ) (ih : ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)) (n : ℤ),
  (↑(-(↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑(m + 1) : ℤ)) : α) (↑n : α)
Tactic: induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℤ
m : ℕ
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
have zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Defs (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℤ
m : ℕ
zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
have succ : ∀ (n_1 : ℕ),
  (↑(n ^ n_1) : R) = HPow.hPow (α := R) (↑n : R) n_1 → (↑(n ^ (n_1 + 1)) : R) = HPow.hPow (α := R) (↑n : R) (n_1 + 1)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
n : ℤ
⊢ ∃ (k : ℤ), Xor (n = 2 * k) (n = 2 * k + 1)
have inl : ∀ (k : ℤ), ∃ (k_1 : ℤ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
Tactic: rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
n : ℤ
inl : ∀ (k : ℤ), ∃ (k_1 : ℤ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
⊢ ∃ (k : ℤ), Xor (n = 2 * k) (n = 2 * k + 1)
have inr : ∀ (k : ℤ), ∃ (k_1 : ℤ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Tactic: rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
k : ℤ
⊢ ∃ (k_1 : ℤ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
have h : Xor (k + k = 2 * k) (k + k = 2 * k + 1)
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
k : ℤ
⊢ ∃ (k_1 : ℤ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
have h : Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
n : ℕ
⊢ IsSquare (α := ℤ) (↑n : ℤ) ↔ IsSquare n
have mp : IsSquare (α := ℤ) (↑n : ℤ) → IsSquare n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
n : ℕ
mp : IsSquare (α := ℤ) (↑n : ℤ) → IsSquare n
⊢ IsSquare (α := ℤ) (↑n : ℤ) ↔ IsSquare n
have mpr : IsSquare n → IsSquare (α := ℤ) (↑n : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (hypothesis)
Goal:
b p : ℕ
w : 0 < b
⊢ (↑(b ^ p - 1) : ℤ) = HPow.hPow (α := ℤ) (↑b : ℤ) p - 1
have this : 1 ≤ b ^ p
Tactic: have : 1 ≤ b ^ p := Nat.one_le_pow p b w
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
⊢ (↑(b ^ p - 1) : ℤ) = HPow.hPow (α := ℤ) (↑b : ℤ) p - 1
have norm_cast : b ^ p - 1 = b ^ p - 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n
have obtain : ∀ (k : ℤ), (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)
have ofNat : (-a) ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) = -a ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)
Tactic: rw [Int.ofNat_eq_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) = -a ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)
have ofNat : (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)
have negSucc : ((-a) ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹ = -(a ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹
Tactic: simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ ((-a) ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹ = -(a ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹
have negSucc : ((-a) ^ (1 + k * 2))⁻¹ = -(a ^ (1 + k * 2))⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℤ
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
have ofNat : ∀ (k : ℕ), (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)
Tactic: cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℤ
ofNat : ∀ (k : ℕ), (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
have negSucc : ∀ (k : ℕ), (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)
Tactic: cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Odd n
⊢ HPow.hPow (α := α) (-1) n = -1
have rw : -HPow.hPow (α := α) 1 n = -1
Tactic: rw [h.neg_zpow, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Int.Parity (goal)
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Odd n
rw : -HPow.hPow (α := α) 1 n = -1
⊢ HPow.hPow (α := α) (-1) n = -1
have rw₁ : Eq.{u_1 + 1} (α := α) (-1) (-1)
Tactic: rw [h.neg_zpow, one_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (↑(-x) : R) * (↑y : R) = (↑x : R) * (↑(-y) : R)
have rw : (↑(-x.mulRight (↑y : R)) : R) = (↑x : R) * (↑(-y) : R)
Tactic: rw [← neg_eq_val_neg, ← val_neg_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (↑(-x.mulRight (↑y : R)) : R) = (↑x : R) * (↑(-y) : R)
have h : (↑x : R) * (↑(-y) : R) + (↑(x.mulRight (↑y : R)) : R) = 0
Tactic: apply AddUnits.neg_eq_of_add_eq_zero_left
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (↑(-x) : R) * (↑(-y) : R) = (↑x : R) * (↑y : R)
have rw : y.mulLeft (↑(-x) : R) = -y.mulLeft (↑x : R)
Tactic: rw [← val_mulLeft, ← val_mulLeft, ← AddUnits.ext_iff, ← neg_inj, ← y.neg_mulLeft, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ y.mulLeft (↑(-x) : R) = -y.mulLeft (↑x : R)
have huv : (↑(y.mulLeft (↑(-x) : R)) : R) = (↑(-y.mulLeft (↑x : R)) : R)
Tactic: apply AddUnits.ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
have rw : HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
  HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
Tactic: rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
rw :
  HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
have rw₁ : HMul.hMul (α := R) 2 1 - 1 = 1
Tactic: rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
rw :
  HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
rw₁ : HMul.hMul (α := R) 2 1 - 1 = 1
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
have rw₂ : HSub.hSub (α := R) 2 1 = 1
Tactic: rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
rw :
  HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
rw₁ : HMul.hMul (α := R) 2 1 - 1 = 1
rw₂ : HSub.hSub (α := R) 2 1 = 1
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
have rw₃ : HAdd.hAdd (α := R) 1 1 - 1 = 1
Tactic: rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
rw :
  HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
rw₁ : HMul.hMul (α := R) 2 1 - 1 = 1
rw₂ : HSub.hSub (α := R) 2 1 = 1
rw₃ : HAdd.hAdd (α := R) 1 1 - 1 = 1
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Invertible (α := R) 2
⊢ HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    1
have rw : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = 1
Tactic: rw [← two_mul, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Invertible (α := R) 2
rw : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = 1
⊢ HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← two_mul, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₂ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]