awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
q : ℚ≥0
a : K
rw : q • f a = f ((↑q : K) * a)
rw₁ : (↑q : L) * f a = f ((↑q : K) * a)
rw₂ : (↑q : L) * f a = f (↑q : K) * f a
⊢ f (q • a) = f ((↑q : K) * a)
have rw₃ : (↑q : L) * f a = (↑q : L) * f a
Tactic: rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
Tactic: rw [ratCast, div, intCast, natCast, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₁ : (↑q : L) = f (↑q.num : K) / f (↑q.den : K)
Tactic: rw [ratCast, div, intCast, natCast, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₁ : (↑q : L) = f (↑q.num : K) / f (↑q.den : K)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₂ : (↑q : L) = (↑q.num : L) / f (↑q.den : K)
Tactic: rw [ratCast, div, intCast, natCast, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₁ : (↑q : L) = f (↑q.num : K) / f (↑q.den : K)
rw₂ : (↑q : L) = (↑q.num : L) / f (↑q.den : K)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₃ : (↑q : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
Tactic: rw [ratCast, div, intCast, natCast, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₁ : (↑q : L) = f (↑q.num : K) / f (↑q.den : K)
rw₂ : (↑q : L) = (↑q.num : L) / f (↑q.den : K)
rw₃ : (↑q : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₄ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
Tactic: rw [ratCast, div, intCast, natCast, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
a : K
⊢ f (q • a) = f ((↑q : K) * a)
have rw : q • f a = f ((↑q : K) * a)
Tactic: rw [qsmul, mul, Rat.smul_def, ratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
a : K
rw : q • f a = f ((↑q : K) * a)
⊢ f (q • a) = f ((↑q : K) * a)
have rw₁ : q • f a = f (↑q : K) * f a
Tactic: rw [qsmul, mul, Rat.smul_def, ratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
a : K
rw : q • f a = f ((↑q : K) * a)
rw₁ : q • f a = f (↑q : K) * f a
⊢ f (q • a) = f ((↑q : K) * a)
have rw₂ : (↑q : L) * f a = f (↑q : K) * f a
Tactic: rw [qsmul, mul, Rat.smul_def, ratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
a : K
rw : q • f a = f ((↑q : K) * a)
rw₁ : q • f a = f (↑q : K) * f a
rw₂ : (↑q : L) * f a = f (↑q : K) * f a
⊢ f (q • a) = f ((↑q : K) * a)
have rw₃ : (↑q : L) * f a = (↑q : L) * f a
Tactic: rw [qsmul, mul, Rat.smul_def, ratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Defs (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
⊢ HSMul.hSMul (β := K) q 1 = (↑q : K)
have rw : HMul.hMul (α := K) (↑q : K) 1 = (↑q : K)
Tactic: rw [NNRat.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.Defs (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
rw : HMul.hMul (α := K) (↑q : K) 1 = (↑q : K)
⊢ HSMul.hSMul (β := K) q 1 = (↑q : K)
have rw₁ : Eq.{u_1 + 1} (α := K) (↑q : K) (↑q : K)
Tactic: rw [NNRat.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.Defs (goal)
Goal:
A : Type u_2
inst : DivisionRing A
m : ℚ
⊢ HSMul.hSMul (β := A) m 1 = (↑m : A)
have rw : HMul.hMul (α := A) (↑m : A) 1 = (↑m : A)
Tactic: rw [Rat.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.Defs (goal)
Goal:
A : Type u_2
inst : DivisionRing A
m : ℚ
rw : HMul.hMul (α := A) (↑m : A) 1 = (↑m : A)
⊢ HSMul.hSMul (β := A) m 1 = (↑m : A)
have rw₁ : Eq.{u_2 + 1} (α := A) (↑m : A) (↑m : A)
Tactic: rw [Rat.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.Equiv (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : Semiring A
inst_1 : Semiring B
inst_2 : FunLike F A B
inst_3 : MonoidWithZeroHomClass F A B
f : F
inst_4 : IsLocalHom.{u_1, u_2, u_3} (R := A) (S := B) f
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hB : IsField B
x y : A
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (x * y) : B) ((f : (a : A) → B) (y * x) : B)
have rw : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) = (f : (a : A) → B) (y * x)
Tactic: rw [map_mul, map_mul, hB.mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Equiv (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : Semiring A
inst_1 : Semiring B
inst_2 : FunLike F A B
inst_3 : MonoidWithZeroHomClass F A B
f : F
inst_4 : IsLocalHom.{u_1, u_2, u_3} (R := A) (S := B) f
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hB : IsField B
x y : A
rw : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) = (f : (a : A) → B) (y * x)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (x * y) : B) ((f : (a : A) → B) (y * x) : B)
have rw₁ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
Tactic: rw [map_mul, map_mul, hB.mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Equiv (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : Semiring A
inst_1 : Semiring B
inst_2 : FunLike F A B
inst_3 : MonoidWithZeroHomClass F A B
f : F
inst_4 : IsLocalHom.{u_1, u_2, u_3} (R := A) (S := B) f
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hB : IsField B
x y : A
rw : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) = (f : (a : A) → B) (y * x)
rw₁ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (x * y) : B) ((f : (a : A) → B) (y * x) : B)
have rw₂ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
Tactic: rw [map_mul, map_mul, hB.mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
have this : x - y ≠ 0
Tactic: have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
have rw : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
Tactic: rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
rw : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
have rw₁ : Eq.{u_2 + 1} (α := K) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
Tactic: rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)
have this : x - 1 ≠ 0
Tactic: have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)
have rw : ∑ i ∈ range n, x ^ i = (∑ i ∈ range n, x ^ i) * (x - 1) / (x - 1)
Tactic: rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
rw : ∑ i ∈ range n, x ^ i = (∑ i ∈ range n, x ^ i) * (x - 1) / (x - 1)
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)
have rw₁ : Eq.{u_2 + 1} (α := K) (∑ i ∈ range n, x ^ i) (∑ i ∈ range n, x ^ i)
Tactic: rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
have this : x - y ≠ 0
Tactic: have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
have rw : ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
Tactic: rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
rw : ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
have rw₁ : Eq.{u_2 + 1} (α := K) (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i))
Tactic: rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ x⁻¹ ≠ 1
have rwa : 1 / x ≠ 1
Tactic: rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
rwa : 1 / x ≠ 1
⊢ x⁻¹ ≠ 1
have rwa₁ : ¬1 / x = 1
Tactic: rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
rwa : 1 / x ≠ 1
rwa₁ : ¬1 / x = 1
⊢ x⁻¹ ≠ 1
have rwa₂ : ¬1 * x = 1
Tactic: rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
rwa : 1 / x ≠ 1
rwa₁ : ¬1 / x = 1
rwa₂ : ¬1 * x = 1
⊢ x⁻¹ ≠ 1
have rwa₃ : ¬x = 1
Tactic: rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
have h₁ : x⁻¹ ≠ 1
Tactic: have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
have h₂ : x⁻¹ - 1 ≠ 0
Tactic: have h₂ : x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
have h₃ : x - 1 ≠ 0
Tactic: have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Lean 4 proof step from Mathlib.Algebra.Field.GeomSum (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x
have rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
Tactic: rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]