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 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
rw : (f 1)⁻¹ = f 1
rw₁ : Eq.{u_2 + 1} (α := M₂) 1⁻¹ 1
⊢ f 1⁻¹ = f 1
have rw₂ : Eq.{u_2 + 1} (α := M₂) 1 1
Tactic: rw [inv, one, inv_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 : Injective 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 / y) = f (x * y⁻¹)
have rw : f x / f y = f (x * y⁻¹)
Tactic: rw [div, mul, inv, 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 : Injective 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 * y⁻¹)
⊢ f (x / y) = f (x * y⁻¹)
have rw₁ : f x / f y = f x * f y⁻¹
Tactic: rw [div, mul, inv, 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 : Injective 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 * y⁻¹)
rw₁ : f x / f y = f x * f y⁻¹
⊢ f (x / y) = f (x * y⁻¹)
have rw₂ : f x / f y = f x * (f y)⁻¹
Tactic: rw [div, mul, inv, 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 : Injective 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 * y⁻¹)
rw₁ : f x / f y = f x * f y⁻¹
rw₂ : f x / f y = f x * (f y)⁻¹
⊢ f (x / y) = f (x * y⁻¹)
have rw₃ : f x * (f y)⁻¹ = f x * (f y)⁻¹
Tactic: rw [div, mul, inv, 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 : Injective 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 (HPow.hPow (β := ℤ) x 0) = f 1
have rw : HPow.hPow (β := ℤ) (f x) 0 = 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) 0 = f 1
⊢ f (HPow.hPow (β := ℤ) x 0) = f 1
have rw₁ : 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) 0 = f 1
rw₁ : 1 = f 1
⊢ f (HPow.hPow (β := ℤ) x 0) = f 1
have rw₂ : Eq.{u_2 + 1} (α := M₂) 1 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 : Injective 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 (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw₁ : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
rw₁ : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw₂ : f x ^ n.succ = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
rw₁ : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f x ^ n.succ = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw₃ : f x ^ n * f x = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
rw₁ : HPow.hPow (β := ℤ) (f 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 * f x = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw₄ : f x ^ n * f x = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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 : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
rw₁ : HPow.hPow (β := ℤ) (f 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 * f x = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₄ : f x ^ n * f x = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
have rw₅ : f x ^ n * f x = f x ^ n * f x
Tactic: rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]
-- 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 : Injective 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) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
have rw : f x ^ Int.negSucc n = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
Tactic: rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]
-- 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 : Injective 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 = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
⊢ f (x ^ Int.negSucc n) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
have rw₁ : (f x ^ (n + 1))⁻¹ = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
Tactic: rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]
-- 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 : Injective 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 = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₁ : (f x ^ (n + 1))⁻¹ = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
⊢ f (x ^ Int.negSucc n) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
have rw₂ : (f x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
Tactic: rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]
-- 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 : Injective 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 = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₁ : (f x ^ (n + 1))⁻¹ = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₂ : (f x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
⊢ f (x ^ Int.negSucc n) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
have rw₃ : (f x ^ (n + 1))⁻¹ = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
Tactic: rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]
-- 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 : Injective 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 = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₁ : (f x ^ (n + 1))⁻¹ = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₂ : (f x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₃ : (f x ^ (n + 1))⁻¹ = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
⊢ f (x ^ Int.negSucc n) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
have rw₄ : (f x ^ (n + 1))⁻¹ = (f x ^ n.succ)⁻¹
Tactic: rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]
-- 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw : (f (x * y))⁻¹ = f (y⁻¹ * x⁻¹)
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y))⁻¹ = f (y⁻¹ * x⁻¹)
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y))⁻¹ = f (y⁻¹ * x⁻¹)
rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw₂ : (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y))⁻¹ = f (y⁻¹ * x⁻¹)
rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
rw₂ : (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw₃ : (f y)⁻¹ * (f x)⁻¹ = f y⁻¹ * f x⁻¹
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y))⁻¹ = f (y⁻¹ * x⁻¹)
rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
rw₂ : (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
rw₃ : (f y)⁻¹ * (f x)⁻¹ = f y⁻¹ * f x⁻¹
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw₄ : (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * f x⁻¹
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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 * y))⁻¹ = f (y⁻¹ * x⁻¹)
rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
rw₂ : (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
rw₃ : (f y)⁻¹ * (f x)⁻¹ = f y⁻¹ * f x⁻¹
rw₄ : (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * f x⁻¹
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
have rw₅ : (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * (f x)⁻¹
Tactic: rw [inv, mul, mul_inv_rev, mul, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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₁
h : x * y = 1
⊢ f x * f y = 1
have rw : f (x * y) = 1
Tactic: rw [← mul, h, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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₁
h : x * y = 1
rw : f (x * y) = 1
y₁ : M₁
rw₁ : f 1 = 1
⊢ f x * f y = 1
have rw₂ : Eq.{u_2 + 1} (α := M₂) 1 1
Tactic: rw [← mul, h, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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₁
h : x * y = 1
⊢ f x⁻¹ = f y
have rw : (f x)⁻¹ = f y
Tactic: rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, 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 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective 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₁
h : x * y = 1
rw : (f x)⁻¹ = f y
⊢ f x⁻¹ = f y
have rw₁ : f y = f y
Tactic: rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, 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 : Injective 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⁻¹ * x) = f 1
have rw : f x⁻¹ * f x = f 1
Tactic: rw [mul, inv, 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 : Injective 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 = f 1
⊢ f (x⁻¹ * x) = f 1
have rw₁ : (f x)⁻¹ * f x = f 1
Tactic: rw [mul, inv, 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 : Injective 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 = f 1
rw₁ : (f x)⁻¹ * f x = f 1
⊢ f (x⁻¹ * x) = f 1
have rw₂ : 1 = f 1
Tactic: rw [mul, inv, 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 : Injective 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 = f 1
rw₁ : (f x)⁻¹ * f x = f 1
rw₂ : 1 = f 1
⊢ f (x⁻¹ * x) = f 1
have rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
Tactic: rw [mul, inv, 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 : CommMagma M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f x * f y = f y * f x
have rw : f (x * y) = f y * f x
Tactic: rw [← mul, ← mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : CommMagma M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f (x * y) = f y * f x
⊢ f x * f y = f y * f x
have rw₁ : f (x * y) = f (y * x)
Tactic: rw [← mul, ← mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.InjSurj (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : CommMagma M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f (x * y) = f y * f x
rw₁ : f (x * y) = f (y * x)
⊢ f x * f y = f y * f x
have rw₂ : f (y * x) = f (y * x)
Tactic: rw [← mul, ← mul, mul_comm]