[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Mul M₁ := inst✝¹
x y z : M₁
⊢ f (x * y * z) = f (x * (y * z))
[PROOFSTEP]
erw [mul, mul, mul, mul, mul_assoc]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : CommSemigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Semigroup M₁ := Injective.semigroup f hf mul
x y : M₁
⊢ f (x * y) = f (y * x)
[PROOFSTEP]
erw [mul, mul, mul_comm]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : LeftCancelSemigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Semigroup M₁ := Injective.semigroup f hf mul
x y z : M₁
H : x * y = x * z
⊢ f x * f y = f x * f z
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : RightCancelSemigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Semigroup M₁ := Injective.semigroup f hf mul
x y z : M₁
H : x * y = z * y
⊢ f x * f y = f z * f y
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝¹ : One M₁ := inst✝¹
src✝ : Mul M₁ := inst✝²
x : M₁
⊢ f (1 * x) = f x
[PROOFSTEP]
erw [mul, one, one_mul]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝¹ : One M₁ := inst✝¹
src✝ : Mul M₁ := inst✝²
x : M₁
⊢ f (x * 1) = f x
[PROOFSTEP]
erw [mul, one, mul_one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective 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
src✝¹ : MulOneClass M₁ := Injective.mulOneClass f hf one mul
src✝ : Semigroup M₁ := Injective.semigroup f hf mul
x : M₁
⊢ f ((fun n x => x ^ n) 0 x) = f 1
[PROOFSTEP]
erw [npow, one, pow_zero]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective 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
src✝¹ : MulOneClass M₁ := Injective.mulOneClass f hf one mul
src✝ : Semigroup M₁ := Injective.semigroup f hf mul
n : ℕ
x : M₁
⊢ f ((fun n x => x ^ n) (n + 1) x) = f (x * (fun n x => x ^ n) n x)
[PROOFSTEP]
erw [npow, pow_succ, mul, npow]
[GOAL]
M₁✝ : Type u_1
M₂ : Type u_2
inst✝⁸ : Mul M₁✝
inst✝⁷ : One M₁✝
inst✝⁶ : Pow M₁✝ ℕ
M₁ : Type ?u.7086
inst✝⁵ : Zero M₁
inst✝⁴ : One M₁
inst✝³ : Add M₁
inst✝² : SMul ℕ M₁
inst✝¹ : NatCast M₁
inst✝ : AddMonoidWithOne M₂
f : M₁ → M₂
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝ : AddMonoid M₁ := Injective.addMonoid f hf zero add nsmul
⊢ f (NatCast.natCast 0) = f 0
[PROOFSTEP]
erw [nat_cast, Nat.cast_zero, zero]
[GOAL]
M₁✝ : Type u_1
M₂ : Type u_2
inst✝⁸ : Mul M₁✝
inst✝⁷ : One M₁✝
inst✝⁶ : Pow M₁✝ ℕ
M₁ : Type ?u.7086
inst✝⁵ : Zero M₁
inst✝⁴ : One M₁
inst✝³ : Add M₁
inst✝² : SMul ℕ M₁
inst✝¹ : NatCast M₁
inst✝ : AddMonoidWithOne M₂
f : M₁ → M₂
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝ : AddMonoid M₁ := Injective.addMonoid f hf zero add nsmul
n : ℕ
⊢ f (NatCast.natCast (n + 1)) = f (NatCast.natCast n + 1)
[PROOFSTEP]
erw [nat_cast, Nat.cast_succ, add, one, nat_cast]
[GOAL]
M₁✝ : Type u_1
M₂ : Type u_2
inst✝⁴ : Mul M₁✝
inst✝³ : One M₁✝
inst✝² : Pow M₁✝ ℕ
M₁ : Type u_3
inst✝¹ : Inv M₁
inst✝ : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x⁻¹⁻¹ = f x
[PROOFSTEP]
rw [inv, inv, inv_inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : Mul M₁
inst✝³ : One M₁
inst✝² : Pow M₁ ℕ
inst✝¹ : Inv M₁
inst✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
src✝¹ : One M₁ := inst✝³
src✝ : Inv M₁ := inst✝¹
⊢ f 1⁻¹ = f 1
[PROOFSTEP]
erw [inv, one, inv_one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝² : Monoid M₁ := Injective.monoid f hf one mul npow
src✝¹ : Inv M₁ := inst✝³
src✝ : Div M₁ := inst✝²
x y : M₁
⊢ f (x / y) = f (x * y⁻¹)
[PROOFSTEP]
erw [div, mul, inv, div_eq_mul_inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝² : Monoid M₁ := Injective.monoid f hf one mul npow
src✝¹ : Inv M₁ := inst✝³
src✝ : Div M₁ := inst✝²
x : M₁
⊢ f ((fun n x => x ^ n) 0 x) = f 1
[PROOFSTEP]
erw [zpow, zpow_zero, one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝² : Monoid M₁ := Injective.monoid f hf one mul npow
src✝¹ : Inv M₁ := inst✝³
src✝ : Div M₁ := inst✝²
n : ℕ
x : M₁
⊢ f ((fun n x => x ^ n) (Int.ofNat (Nat.succ n)) x) = f (x * (fun n x => x ^ n) (Int.ofNat n) x)
[PROOFSTEP]
erw [zpow, mul, zpow_ofNat, pow_succ, zpow, zpow_ofNat]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝² : Monoid M₁ := Injective.monoid f hf one mul npow
src✝¹ : Inv M₁ := inst✝³
src✝ : Div M₁ := inst✝²
n : ℕ
x : M₁
⊢ f ((fun n x => x ^ n) (Int.negSucc n) x) = f ((fun n x => x ^ n) (↑(Nat.succ n)) x)⁻¹
[PROOFSTEP]
erw [zpow, zpow_negSucc, inv, zpow, zpow_ofNat]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝¹ : DivInvMonoid M₁ := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : InvolutiveInv M₁ := Injective.involutiveInv f hf inv
x y : M₁
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)
[PROOFSTEP]
erw [inv, mul, mul_inv_rev, mul, inv, inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝¹ : DivInvMonoid M₁ := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : InvolutiveInv M₁ := Injective.involutiveInv f hf inv
x y : M₁
h : x * y = 1
⊢ f x⁻¹ = f y
[PROOFSTEP]
erw [inv, inv_eq_of_mul_eq_one_right (by erw [← mul, h, one])]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝¹ : DivInvMonoid M₁ := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : InvolutiveInv M₁ := Injective.involutiveInv f hf inv
x y : M₁
h : x * y = 1
⊢ f x * ?m.28665 = 1
[PROOFSTEP]
erw [← mul, h, one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : 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
src✝ : DivInvMonoid M₁ := Injective.divInvMonoid f hf one mul inv div npow zpow
x : M₁
⊢ f (x⁻¹ * x) = f 1
[PROOFSTEP]
erw [mul, inv, mul_left_inv, one]
[GOAL]
M₁✝ : Type u_1
M₂ : Type u_2
inst✝¹⁵ : Mul M₁✝
inst✝¹⁴ : One M₁✝
inst✝¹³ : Pow M₁✝ ℕ
inst✝¹² : Inv M₁✝
inst✝¹¹ : Div M₁✝
inst✝¹⁰ : Pow M₁✝ ℤ
M₁ : Type ?u.34880
inst✝⁹ : Zero M₁
inst✝⁸ : One M₁
inst✝⁷ : Add M₁
inst✝⁶ : SMul ℕ M₁
inst✝⁵ : Neg M₁
inst✝⁴ : Sub M₁
inst✝³ : SMul ℤ M₁
inst✝² : NatCast M₁
inst✝¹ : IntCast M₁
inst✝ : AddGroupWithOne M₂
f : M₁ → M₂
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
neg : ∀ (x : M₁), f (-x) = -f x
sub : ∀ (x y : M₁), f (x - y) = f x - f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : AddGroup M₁ := Injective.addGroup f hf zero add neg sub nsmul zsmul
src✝ : AddMonoidWithOne M₁ := Injective.addMonoidWithOne f hf zero one add nsmul nat_cast
n : ℕ
⊢ f (IntCast.intCast ↑n) = f ↑n
[PROOFSTEP]
rw [nat_cast, ← Int.cast, int_cast, Int.cast_ofNat]
[GOAL]
M₁✝ : Type u_1
M₂ : Type u_2
inst✝¹⁵ : Mul M₁✝
inst✝¹⁴ : One M₁✝
inst✝¹³ : Pow M₁✝ ℕ
inst✝¹² : Inv M₁✝
inst✝¹¹ : Div M₁✝
inst✝¹⁰ : Pow M₁✝ ℤ
M₁ : Type ?u.34880
inst✝⁹ : Zero M₁
inst✝⁸ : One M₁
inst✝⁷ : Add M₁
inst✝⁶ : SMul ℕ M₁
inst✝⁵ : Neg M₁
inst✝⁴ : Sub M₁
inst✝³ : SMul ℤ M₁
inst✝² : NatCast M₁
inst✝¹ : IntCast M₁
inst✝ : AddGroupWithOne M₂
f : M₁ → M₂
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
neg : ∀ (x : M₁), f (-x) = -f x
sub : ∀ (x y : M₁), f (x - y) = f x - f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : AddGroup M₁ := Injective.addGroup f hf zero add neg sub nsmul zsmul
src✝ : AddMonoidWithOne M₁ := Injective.addMonoidWithOne f hf zero one add nsmul nat_cast
n : ℕ
⊢ f (IntCast.intCast (Int.negSucc n)) = f (-↑(n + 1))
[PROOFSTEP]
erw [int_cast, neg, nat_cast, Int.cast_negSucc]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₂
inst✝ : Semigroup M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Mul M₂ := inst✝¹
x y z : M₁
⊢ f x * f y * f z = f x * (f y * f z)
[PROOFSTEP]
simp only [← mul, mul_assoc]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₂
inst✝ : CommSemigroup M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝ : Semigroup M₂ := Surjective.semigroup f hf mul
x y : M₁
⊢ f x * f y = f y * f x
[PROOFSTEP]
erw [← mul, ← mul, mul_comm]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝¹ : One M₂ := inst✝¹
src✝ : Mul M₂ := inst✝²
x : M₁
⊢ 1 * f x = f x
[PROOFSTEP]
erw [← one, ← mul, one_mul]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
src✝¹ : One M₂ := inst✝¹
src✝ : Mul M₂ := inst✝²
x : M₁
⊢ f x * 1 = f x
[PROOFSTEP]
erw [← one, ← mul, mul_one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₂
inst✝² : One M₂
inst✝¹ : Pow M₂ ℕ
inst✝ : 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
src✝¹ : Semigroup M₂ := Surjective.semigroup f hf mul
src✝ : MulOneClass M₂ := Surjective.mulOneClass f hf one mul
x : M₁
⊢ (fun n x => x ^ n) 0 (f x) = 1
[PROOFSTEP]
dsimp only
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₂
inst✝² : One M₂
inst✝¹ : Pow M₂ ℕ
inst✝ : 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
src✝¹ : Semigroup M₂ := Surjective.semigroup f hf mul
src✝ : MulOneClass M₂ := Surjective.mulOneClass f hf one mul
x : M₁
⊢ f x ^ 0 = 1
[PROOFSTEP]
erw [← npow, pow_zero, ← one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₂
inst✝² : One M₂
inst✝¹ : Pow M₂ ℕ
inst✝ : 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
src✝¹ : Semigroup M₂ := Surjective.semigroup f hf mul
src✝ : MulOneClass M₂ := Surjective.mulOneClass f hf one mul
n : ℕ
x : M₁
⊢ (fun n x => x ^ n) (n + 1) (f x) = f x * (fun n x => x ^ n) n (f x)
[PROOFSTEP]
dsimp only
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₂
inst✝² : One M₂
inst✝¹ : Pow M₂ ℕ
inst✝ : 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
src✝¹ : Semigroup M₂ := Surjective.semigroup f hf mul
src✝ : MulOneClass M₂ := Surjective.mulOneClass f hf one mul
n : ℕ
x : M₁
⊢ f x ^ (n + 1) = f x * f x ^ n
[PROOFSTEP]
erw [← npow, pow_succ, ← npow, ← mul]
[GOAL]
M₁ : Type u_1
M₂✝ : Type u_2
inst✝⁸ : Mul M₂✝
inst✝⁷ : One M₂✝
inst✝⁶ : Pow M₂✝ ℕ
M₂ : Type ?u.46065
inst✝⁵ : Zero M₂
inst✝⁴ : One M₂
inst✝³ : Add M₂
inst✝² : SMul ℕ M₂
inst✝¹ : NatCast M₂
inst✝ : AddMonoidWithOne M₁
f : M₁ → M₂
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝ : AddMonoid M₂ := Surjective.addMonoid f hf zero add nsmul
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
rw [← Nat.cast, ← nat_cast, Nat.cast_zero, zero]
[GOAL]
M₁ : Type u_1
M₂✝ : Type u_2
inst✝⁸ : Mul M₂✝
inst✝⁷ : One M₂✝
inst✝⁶ : Pow M₂✝ ℕ
M₂ : Type ?u.46065
inst✝⁵ : Zero M₂
inst✝⁴ : One M₂
inst✝³ : Add M₂
inst✝² : SMul ℕ M₂
inst✝¹ : NatCast M₂
inst✝ : AddMonoidWithOne M₁
f : M₁ → M₂
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝ : AddMonoid M₂ := Surjective.addMonoid f hf zero add nsmul
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
rw [← Nat.cast, ← nat_cast, Nat.cast_succ, add, one, nat_cast]
[GOAL]
M₁ : Type u_1
M₂✝ : Type u_2
inst✝⁴ : Mul M₂✝
inst✝³ : One M₂✝
inst✝² : Pow M₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x)⁻¹⁻¹ = f x
[PROOFSTEP]
erw [← inv, ← inv, inv_inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
x y : M₁
⊢ f x / f y = f x * (f y)⁻¹
[PROOFSTEP]
erw [← inv, ← mul, ← div, div_eq_mul_inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
x : M₁
⊢ (fun n x => x ^ n) 0 (f x) = 1
[PROOFSTEP]
dsimp only
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
x : M₁
⊢ f x ^ 0 = 1
[PROOFSTEP]
erw [← zpow, zpow_zero, ← one]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
n : ℕ
x : M₁
⊢ (fun n x => x ^ n) (Int.ofNat (Nat.succ n)) (f x) = f x * (fun n x => x ^ n) (Int.ofNat n) (f x)
[PROOFSTEP]
dsimp only
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
n : ℕ
x : M₁
⊢ f x ^ Int.ofNat (Nat.succ n) = f x * f x ^ Int.ofNat n
[PROOFSTEP]
erw [← zpow, ← zpow, zpow_ofNat, zpow_ofNat, pow_succ, ← mul]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
n : ℕ
x : M₁
⊢ (fun n x => x ^ n) (Int.negSucc n) (f x) = ((fun n x => x ^ n) (↑(Nat.succ n)) (f x))⁻¹
[PROOFSTEP]
dsimp only
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝² : Monoid M₂ := Surjective.monoid f hf one mul npow
src✝¹ : Div M₂ := inst✝²
src✝ : Inv M₂ := inst✝³
n : ℕ
x : M₁
⊢ f x ^ Int.negSucc n = (f x ^ ↑(Nat.succ n))⁻¹
[PROOFSTEP]
erw [← zpow, ← zpow, zpow_negSucc, zpow_ofNat, inv]
[GOAL]
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : 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
src✝ : DivInvMonoid M₂ := Surjective.divInvMonoid f hf one mul inv div npow zpow
x : M₁
⊢ (f x)⁻¹ * f x = 1
[PROOFSTEP]
erw [← inv, ← mul, mul_left_inv, one]
[GOAL]
M₁ : Type u_1
M₂✝ : Type u_2
inst✝¹⁵ : Mul M₂✝
inst✝¹⁴ : One M₂✝
inst✝¹³ : Pow M₂✝ ℕ
inst✝¹² : Inv M₂✝
inst✝¹¹ : Div M₂✝
inst✝¹⁰ : Pow M₂✝ ℤ
M₂ : Type ?u.57344
inst✝⁹ : Zero M₂
inst✝⁸ : One M₂
inst✝⁷ : Add M₂
inst✝⁶ : Neg M₂
inst✝⁵ : Sub M₂
inst✝⁴ : SMul ℕ M₂
inst✝³ : SMul ℤ M₂
inst✝² : NatCast M₂
inst✝¹ : IntCast M₂
inst✝ : AddGroupWithOne M₁
f : M₁ → M₂
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
neg : ∀ (x : M₁), f (-x) = -f x
sub : ∀ (x y : M₁), f (x - y) = f x - f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : AddMonoidWithOne M₂ := Surjective.addMonoidWithOne f hf zero one add nsmul nat_cast
src✝ : AddGroup M₂ := Surjective.addGroup f hf zero add neg sub nsmul zsmul
n : ℕ
⊢ IntCast.intCast ↑n = ↑n
[PROOFSTEP]
rw [← Int.cast, ← int_cast, Int.cast_ofNat, nat_cast]
[GOAL]
M₁ : Type u_1
M₂✝ : Type u_2
inst✝¹⁵ : Mul M₂✝
inst✝¹⁴ : One M₂✝
inst✝¹³ : Pow M₂✝ ℕ
inst✝¹² : Inv M₂✝
inst✝¹¹ : Div M₂✝
inst✝¹⁰ : Pow M₂✝ ℤ
M₂ : Type ?u.57344
inst✝⁹ : Zero M₂
inst✝⁸ : One M₂
inst✝⁷ : Add M₂
inst✝⁶ : Neg M₂
inst✝⁵ : Sub M₂
inst✝⁴ : SMul ℕ M₂
inst✝³ : SMul ℤ M₂
inst✝² : NatCast M₂
inst✝¹ : IntCast M₂
inst✝ : AddGroupWithOne M₁
f : M₁ → M₂
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : M₁), f (x + y) = f x + f y
neg : ∀ (x : M₁), f (-x) = -f x
sub : ∀ (x y : M₁), f (x - y) = f x - f y
nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : AddMonoidWithOne M₂ := Surjective.addMonoidWithOne f hf zero one add nsmul nat_cast
src✝ : AddGroup M₂ := Surjective.addGroup f hf zero add neg sub nsmul zsmul
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
rw [← Int.cast, ← int_cast, Int.cast_negSucc, neg, nat_cast]
