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_1 : S → R
hf_1 : Injective f_1
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 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)
have rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
Tactic: rw [natCast, Nat.cast_succ, add, one, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
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 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)
have rw₁ : HAdd.hAdd (α := R) (↑n : R) 1 = f (HAdd.hAdd (α := S) (↑n : S) 1)
Tactic: rw [natCast, Nat.cast_succ, add, one, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
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 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₁ : HAdd.hAdd (α := R) (↑n : R) 1 = f (HAdd.hAdd (α := S) (↑n : S) 1)
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)
have rw₂ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + f 1
Tactic: rw [natCast, Nat.cast_succ, add, one, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
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 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₁ : HAdd.hAdd (α := R) (↑n : R) 1 = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₂ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + f 1
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)
have rw₃ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + 1
Tactic: rw [natCast, Nat.cast_succ, add, one, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
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 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₁ : HAdd.hAdd (α := R) (↑n : R) 1 = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₂ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + f 1
rw₃ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + 1
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)
have rw₄ : HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [natCast, Nat.cast_succ, add, one, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
⊢ f (↑(↑n : ℤ) : S) = f (↑n : S)
have rw : f (↑(↑n : ℤ) : S) = (↑n : R)
Tactic: rw [natCast, intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : f (↑(↑n : ℤ) : S) = (↑n : R)
⊢ f (↑(↑n : ℤ) : S) = f (↑n : S)
have rw₁ : Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (↑n : R)
Tactic: rw [natCast, intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : f (↑(↑n : ℤ) : S) = (↑n : R)
rw₁ : Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (↑n : R)
⊢ f (↑(↑n : ℤ) : S) = f (↑n : S)
have rw₂ : Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
Tactic: rw [natCast, intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
⊢ f (↑(Int.negSucc n) : S) = f (-(↑(n + 1) : S))
have rw : (↑(Int.negSucc n) : R) = f (-(↑(n + 1) : S))
Tactic: rw [intCast, neg, natCast, Int.cast_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(Int.negSucc n) : R) = f (-(↑(n + 1) : S))
⊢ f (↑(Int.negSucc n) : S) = f (-(↑(n + 1) : S))
have rw₁ : (↑(Int.negSucc n) : R) = -f (↑(n + 1) : S)
Tactic: rw [intCast, neg, natCast, Int.cast_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(Int.negSucc n) : R) = f (-(↑(n + 1) : S))
rw₁ : (↑(Int.negSucc n) : R) = -f (↑(n + 1) : S)
⊢ f (↑(Int.negSucc n) : S) = f (-(↑(n + 1) : S))
have rw₂ : Eq.{u_1 + 1} (α := R) (↑(Int.negSucc n) : R) (-(↑(n + 1) : R))
Tactic: rw [intCast, neg, natCast, Int.cast_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(Int.negSucc n) : R) = f (-(↑(n + 1) : S))
rw₁ : (↑(Int.negSucc n) : R) = -f (↑(n + 1) : S)
rw₂ : Eq.{u_1 + 1} (α := R) (↑(Int.negSucc n) : R) (-(↑(n + 1) : R))
⊢ f (↑(Int.negSucc n) : S) = f (-(↑(n + 1) : S))
have rw₃ : Eq.{u_1 + 1} (α := R) (-(↑(n + 1) : R)) (-(↑(n + 1) : R))
Tactic: rw [intCast, neg, natCast, Int.cast_negSucc]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ -f x * f y = -(f x * f y)
have rw : f (-x) * f y = -(f x * f y)
Tactic: rw [← neg, ← mul, neg_mul, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f (-x) * f y = -(f x * f y)
⊢ -f x * f y = -(f x * f y)
have rw₁ : f (-x * y) = -(f x * f y)
Tactic: rw [← neg, ← mul, neg_mul, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f (-x) * f y = -(f x * f y)
rw₁ : f (-x * y) = -(f x * f y)
⊢ -f x * f y = -(f x * f y)
have rw₂ : f (-(x * y)) = -(f x * f y)
Tactic: rw [← neg, ← mul, neg_mul, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f (-x) * f y = -(f x * f y)
rw₁ : f (-x * y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
⊢ -f x * f y = -(f x * f y)
have rw₃ : -f (x * y) = -(f x * f y)
Tactic: rw [← neg, ← mul, neg_mul, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f (-x) * f y = -(f x * f y)
rw₁ : f (-x * y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
rw₃ : -f (x * y) = -(f x * f y)
⊢ -f x * f y = -(f x * f y)
have rw₄ : -(f x * f y) = -(f x * f y)
Tactic: rw [← neg, ← mul, neg_mul, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * -f y = -(f x * f y)
have rw : f x * f (-y) = -(f x * f y)
Tactic: rw [← neg, ← mul, mul_neg, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f x * f (-y) = -(f x * f y)
⊢ f x * -f y = -(f x * f y)
have rw₁ : f (x * -y) = -(f x * f y)
Tactic: rw [← neg, ← mul, mul_neg, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f x * f (-y) = -(f x * f y)
rw₁ : f (x * -y) = -(f x * f y)
⊢ f x * -f y = -(f x * f y)
have rw₂ : f (-(x * y)) = -(f x * f y)
Tactic: rw [← neg, ← mul, mul_neg, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f x * f (-y) = -(f x * f y)
rw₁ : f (x * -y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
⊢ f x * -f y = -(f x * f y)
have rw₃ : -f (x * y) = -(f x * f y)
Tactic: rw [← neg, ← mul, mul_neg, neg, mul]
-- 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 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f x * f (-y) = -(f x * f y)
rw₁ : f (x * -y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
rw₃ : -f (x * y) = -(f x * f y)
⊢ f x * -f y = -(f x * f y)
have rw₄ : -(f x * f y) = -(f x * f y)
Tactic: rw [← neg, ← mul, mul_neg, neg, mul]
-- 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
⊢ Eq.{u_2 + 1} (α := S) (↑0 : S) 0
have rw : f (↑0 : R) = 0
Tactic: rw [← natCast, Nat.cast_zero, zero]
-- 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
rw : f (↑0 : R) = 0
rw₁ : f 0 = 0
⊢ Eq.{u_2 + 1} (α := S) (↑0 : S) 0
have rw₂ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← natCast, Nat.cast_zero, zero]
-- 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1
have rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [← natCast, Nat.cast_succ, add, one, 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1
have rw₁ : f (HAdd.hAdd (α := R) (↑n : R) 1) = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [← natCast, Nat.cast_succ, add, one, 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
rw₁ : f (HAdd.hAdd (α := R) (↑n : R) 1) = HAdd.hAdd (α := S) (↑n : S) 1
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1
have rw₂ : f (↑n : R) + f 1 = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [← natCast, Nat.cast_succ, add, one, 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
rw₁ : f (HAdd.hAdd (α := R) (↑n : R) 1) = HAdd.hAdd (α := S) (↑n : S) 1
rw₂ : f (↑n : R) + f 1 = HAdd.hAdd (α := S) (↑n : S) 1
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1
have rw₃ : f (↑n : R) + 1 = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [← natCast, Nat.cast_succ, add, one, 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 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
rw₁ : f (HAdd.hAdd (α := R) (↑n : R) 1) = HAdd.hAdd (α := S) (↑n : S) 1
rw₂ : f (↑n : R) + f 1 = HAdd.hAdd (α := S) (↑n : S) 1
rw₃ : f (↑n : R) + 1 = HAdd.hAdd (α := S) (↑n : S) 1
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1
have rw₄ : HAdd.hAdd (α := S) (↑n : S) 1 = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [← natCast, Nat.cast_succ, add, one, 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) (↑(↑n : ℤ) : S) (↑n : S)
have rw : f (↑(↑n : ℤ) : R) = (↑n : S)
Tactic: rw [← intCast, Int.cast_natCast, natCast]