awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f x
have rw : f 1 * f x = f x
Tactic: rw [← one, ← mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
⊢ 1 * f x = f x
have rw₁ : f (1 * x) = f x
Tactic: rw [← one, ← mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
rw₁ : f (1 * x) = f x
⊢ 1 * f x = f x
have rw₂ : f x = f x
Tactic: rw [← one, ← mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f x
have rw : f x * f 1 = f x
Tactic: rw [← one, ← mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
⊢ f x * 1 = f x
have rw₁ : f (x * 1) = f x
Tactic: rw [← one, ← mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
rw₁ : f (x * 1) = f x
⊢ f x * 1 = f x
have rw₂ : f x = f x
Tactic: rw [← one, ← mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ HPow.hPow (β := ℕ) (f x) 0 = 1
have rw : f (HPow.hPow (β := ℕ) x 0) = 1
Tactic: rw [← npow, pow_zero, ← one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
rw : f (HPow.hPow (β := ℕ) x 0) = 1
rw₁ : f 1 = 1
⊢ HPow.hPow (β := ℕ) (f x) 0 = 1
have rw₂ : f 1 = f 1
Tactic: rw [← npow, pow_zero, ← one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ (n + 1) = f x ^ n * f x
have rw : f (x ^ (n + 1)) = f x ^ n * f x
Tactic: rw [← npow, pow_succ, ← npow, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ (n + 1)) = f x ^ n * f x
⊢ f x ^ (n + 1) = f x ^ n * f x
have rw₁ : f (x ^ n * x) = f x ^ n * f x
Tactic: rw [← npow, pow_succ, ← npow, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ (n + 1)) = f x ^ n * f x
rw₁ : f (x ^ n * x) = f x ^ n * f x
⊢ f x ^ (n + 1) = f x ^ n * f x
have rw₂ : f (x ^ n * x) = f (x ^ n) * f x
Tactic: rw [← npow, pow_succ, ← npow, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ (n + 1)) = f x ^ n * f x
rw₁ : f (x ^ n * x) = f x ^ n * f x
rw₂ : f (x ^ n * x) = f (x ^ n) * f x
⊢ f x ^ (n + 1) = f x ^ n * f x
have rw₃ : f (x ^ n * x) = f (x ^ n * x)
Tactic: rw [← npow, pow_succ, ← npow, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂_1 : Type u_2
inst : Mul M₂_1
inst_1 : One M₂_1
inst_2 : Pow M₂_1 ℕ
M₂ : Type u_3
inst_3 : Inv M₂
inst_4 : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x)⁻¹⁻¹ = f x
have rw : (f x⁻¹)⁻¹ = f x
Tactic: rw [← inv, ← inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂_1 : Type u_2
inst : Mul M₂_1
inst_1 : One M₂_1
inst_2 : Pow M₂_1 ℕ
M₂ : Type u_3
inst_3 : Inv M₂
inst_4 : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
⊢ (f x)⁻¹⁻¹ = f x
have rw₁ : f x⁻¹⁻¹ = f x
Tactic: rw [← inv, ← inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂_1 : Type u_2
inst : Mul M₂_1
inst_1 : One M₂_1
inst_2 : Pow M₂_1 ℕ
M₂ : Type u_3
inst_3 : Inv M₂
inst_4 : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
rw₁ : f x⁻¹⁻¹ = f x
⊢ (f x)⁻¹⁻¹ = f x
have rw₂ : f x = f x
Tactic: rw [← inv, ← inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f x / f y = f x * (f y)⁻¹
have rw : f x / f y = f x * f y⁻¹
Tactic: rw [← inv, ← mul, ← div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : f x / f y = f x * f y⁻¹
⊢ f x / f y = f x * (f y)⁻¹
have rw₁ : f x / f y = f (x * y⁻¹)
Tactic: rw [← inv, ← mul, ← div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : f x / f y = f x * f y⁻¹
rw₁ : f x / f y = f (x * y⁻¹)
⊢ f x / f y = f x * (f y)⁻¹
have rw₂ : f (x / y) = f (x * y⁻¹)
Tactic: rw [← inv, ← mul, ← div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : f x / f y = f x * f y⁻¹
rw₁ : f x / f y = f (x * y⁻¹)
rw₂ : f (x / y) = f (x * y⁻¹)
⊢ f x / f y = f x * (f y)⁻¹
have rw₃ : f (x * y⁻¹) = f (x * y⁻¹)
Tactic: rw [← inv, ← mul, ← div, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ HPow.hPow (β := ℤ) (f x) 0 = 1
have rw : f (HPow.hPow (β := ℤ) x 0) = 1
Tactic: rw [← zpow, zpow_zero, ← one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f (HPow.hPow (β := ℤ) x 0) = 1
rw₁ : f 1 = 1
⊢ HPow.hPow (β := ℤ) (f x) 0 = 1
have rw₂ : f 1 = f 1
Tactic: rw [← zpow, zpow_zero, ← one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw₂ : f (x ^ n.succ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f (x ^ n.succ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw₃ : f (x ^ n.succ) = f (x ^ n) * f x
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f (x ^ n.succ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₃ : f (x ^ n.succ) = f (x ^ n) * f x
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw₄ : f (x ^ n * x) = f (x ^ n) * f x
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f (x ^ n.succ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₃ : f (x ^ n.succ) = f (x ^ n) * f x
rw₄ : f (x ^ n * x) = f (x ^ n) * f x
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
have rw₅ : f (x ^ n * x) = f (x ^ n * x)
Tactic: rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
have rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
Tactic: rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
have rw₁ : f (x ^ Int.negSucc n) = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
Tactic: rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
rw₁ : f (x ^ Int.negSucc n) = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
have rw₂ : f (x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
Tactic: rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
rw₁ : f (x ^ Int.negSucc n) = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₂ : f (x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
have rw₃ : f (x ^ (n + 1))⁻¹ = (f (x ^ n.succ))⁻¹
Tactic: rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
rw₁ : f (x ^ Int.negSucc n) = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₂ : f (x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₃ : f (x ^ (n + 1))⁻¹ = (f (x ^ n.succ))⁻¹
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
have rw₄ : (f (x ^ (n + 1)))⁻¹ = (f (x ^ n.succ))⁻¹
Tactic: rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : Group M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ (f x)⁻¹ * f x = 1
have rw : f x⁻¹ * f x = 1
Tactic: rw [← inv, ← mul, inv_mul_cancel, one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : Group M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f x⁻¹ * f x = 1
⊢ (f x)⁻¹ * f x = 1
have rw₁ : f (x⁻¹ * x) = 1
Tactic: rw [← inv, ← mul, inv_mul_cancel, one]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : Group M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f x⁻¹ * f x = 1
rw₁ : f (x⁻¹ * x) = 1
rw₂ : f 1 = 1
⊢ (f x)⁻¹ * f x = 1
have rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
Tactic: rw [← inv, ← mul, inv_mul_cancel, one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Defs (goal)
Goal:
n : ℕ
x : ℤ
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * x = (↑n : ℤ) * x + x
have rw : (↑n : ℤ) * x + 1 * x = (↑n : ℤ) * x + x
Tactic: rw [Int.add_mul, Int.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Defs (goal)
Goal:
n : ℕ
x : ℤ
rw : (↑n : ℤ) * x + 1 * x = (↑n : ℤ) * x + x
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * x = (↑n : ℤ) * x + x
have rw₁ : (↑n : ℤ) * x + x = (↑n : ℤ) * x + x
Tactic: rw [Int.add_mul, Int.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m_1 n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m
have simp_rw : IsSquare m ↔ ∃ (n : ℤ), n * n = m
Tactic: simp_rw [← exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m_1 n m : ℤ
simp_rw : IsSquare m ↔ ∃ (n : ℤ), n * n = m
⊢ IsSquare m ↔ sqrt m * sqrt m = m
have simp_rw₁ : (∃ (r : ℤ), m = r * r) ↔ ∃ (n : ℤ), n * n = m
Tactic: simp_rw [← exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one m with h₁ | h₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr : ∀ (h₁ : m % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one m with h₁ | h₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
h₁ : m % 2 = 0
inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m n : ℤ
h₁ : m % 2 = 1
inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases emod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
have zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
m : ℤ
n : ℕ
zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
have succ : ∀ (n : ℕ), (Even (m ^ n) ↔ Even m ∧ n ≠ 0) → (Even (m ^ (n + 1)) ↔ Even m ∧ n + 1 ≠ 0)
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Int.Even (goal)
Goal:
n : ℕ
⊢ Even (α := ℤ) (↑n : ℤ) ↔ Even n
have rw_mod_cast : HMod.hMod (α := ℤ) (↑n : ℤ) 2 = 0 ↔ Even n
Tactic: rw_mod_cast [even_iff, Nat.even_iff]