[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]


[GOAL]
G : Type u_1
M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂
[PROOFSTEP]
rintro @⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ @⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩
  ⟨rfl⟩
      -- FIXME (See https://github.com/leanprover/lean4/issues/1711)
        -- congr
[GOAL]
case mk.mk.mk.mk.mk.mk.refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
suffices one₁ = one₂ by cases this; rfl
[GOAL]
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
cases this
[GOAL]
case refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.mk.mk.mk.mk.refl
G : Type u_1
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ one₁ = one₂
[PROOFSTEP]
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)
[GOAL]
G : Type u_1
M : Type u
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c
[PROOFSTEP]
rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
[GOAL]
G : Type u_1
inst✝ : DivInvMonoid G
a✝ b a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
[PROOFSTEP]
rw [← zpow_ofNat]
[GOAL]
G : Type u_1
inst✝ : DivInvMonoid G
a✝ b a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' n a
[GOAL]
G✝ : Type u_1
inst✝¹ : DivInvMonoid G✝
a✝ b : G✝
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)
[PROOFSTEP]
rw [← ofNat_zsmul]
[GOAL]
G✝ : Type u_1
inst✝¹ : DivInvMonoid G✝
a✝ b : G✝
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)
[PROOFSTEP]
exact SubNegMonoid.zsmul_neg' n a
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b c a : G
⊢ a * a⁻¹ = 1
[PROOFSTEP]
rw [← mul_left_inv a⁻¹, inv_eq_of_mul (mul_left_inv a)]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a⁻¹ * (a * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_left_inv, one_mul]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * (a⁻¹ * b) = b
[PROOFSTEP]
rw [← mul_assoc, mul_right_inv, one_mul]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b * b⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, mul_right_inv, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b⁻¹ * b = a
[PROOFSTEP]
rw [mul_assoc, mul_left_inv, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c a b : G
⊢ a * b * (b⁻¹ * a⁻¹) = 1
[PROOFSTEP]
rw [mul_assoc, mul_inv_cancel_left, mul_right_inv]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ : G
src✝ : Group G := inst✝
a b c : G
h : a * b = a * c
⊢ b = c
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left]
[GOAL]
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ : G
src✝ : Group G := inst✝
a b c : G
h : a * b = c * b
⊢ a = c
[PROOFSTEP]
rw [← mul_inv_cancel_right a b, h, mul_inv_cancel_right]
[GOAL]
G✝ : Type u_1
G : Type u_2
⊢ Injective (@toDivInvMonoid G)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.refl
G✝ : Type u_1
G : Type u_2
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝¹ mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
⊢ mk mul_left_inv✝¹ = mk mul_left_inv✝
[PROOFSTEP]
rfl
[GOAL]
G✝ : Type u_1
G : Type u
⊢ Injective (@toGroup G)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.refl
G✝ : Type u_1
G : Type u
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝
[PROOFSTEP]
rfl


[GOAL]
G✝ : Type u_1
H : Type u_2
inst✝² : Mul G✝
inst✝¹ : Mul H
A✝ B✝ : Finset G✝
a0✝ b0✝ : G✝
G : Type u_3
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ ≠ a0 ∨ x✝ ≠ b0
⊢ x✝¹ * x✝ ≠ a0 * b0
[PROOFSTEP]
contrapose! k
[GOAL]
G✝ : Type u_1
H : Type u_2
inst✝² : Mul G✝
inst✝¹ : Mul H
A✝ B✝ : Finset G✝
a0✝ b0✝ : G✝
G : Type u_3
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ * x✝ = a0 * b0
⊢ x✝¹ = a0 ∧ x✝ = b0
[PROOFSTEP]
exact h ha hb k
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ Set.Subsingleton {ab | ab.fst ∈ A ∧ ab.snd ∈ B ∧ ab.fst * ab.snd = a0 * b0}
[PROOFSTEP]
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩ (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)
[GOAL]
case mk.mk
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ (x1, y1) = (x2, y2)
[PROOFSTEP]
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
[GOAL]
case mk.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : G
A B : Finset G
x1 y1 x2 y2 : G
h : UniqueMul A B x1 y1
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
⊢ (x1, y1) = (x2, y2)
[PROOFSTEP]
rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
[GOAL]
case mk.mk.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0 b0 : G
A B : Finset G
x2 y2 : G
h : UniqueMul A B x2 y2
hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2
⊢ (x2, y2) = (x2, y2)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : (a0, b0) ∈ A ×ˢ B), (fun x => (a0, b0).fst * (a0, b0).snd = a0 * b0) y → y = (_ : (a0, b0) ∈ A ×ˢ B)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun ab => ∃! x, ab.fst * ab.snd = a0 * b0) y → y = (a0, b0)
[PROOFSTEP]
simpa
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B →
      x.fst * x.snd = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = x) → UniqueMul A B a0 b0
[PROOFSTEP]
rintro ⟨x1, x2⟩ _ _ J x y hx hy l
[GOAL]
case mk
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x1 x2 : G
h✝ : (x1, x2) ∈ A ×ˢ B
a✝ : (x1, x2).fst * (x1, x2).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0
[PROOFSTEP]
rcases Prod.mk.inj_iff.mp (J (a0, b0) (Finset.mk_mem_product aA bB) rfl) with ⟨rfl, rfl⟩
[GOAL]
case mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab x, ab.fst * ab.snd = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
h✝ : (a0, b0) ∈ A ×ˢ B
a✝ : (a0, b0).fst * (a0, b0).snd = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B → y.fst * y.snd = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0
[PROOFSTEP]
exact Prod.mk.inj_iff.mp (J (x, y) (Finset.mk_mem_product hx hy) l)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
g : G
h : ∃! ab x, ab.fst * ab.snd = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
have h' := h
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
g : G
h h' : ∃! ab x, ab.fst * ab.snd = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
[GOAL]
case intro.mk.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
cases' Finset.mem_product.mp hab with ha hb
[GOAL]
case intro.mk.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
x✝ : ∃ g, ∃! ab x, ab.fst * ab.snd = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab x, ab.fst * ab.snd = (a, b).fst * (a, b).snd
ha : (a, b).fst ∈ A
hb : (a, b).snd ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
⊢ UniqueMul (Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A)))
    (Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))) a0 b0
[PROOFSTEP]
intro a b ha hb ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← hf.eq_iff, ← hf.eq_iff]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : a * b = a0 * b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [← hf.eq_iff, map_mul, map_mul] at ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A✝ B✝ : Finset G
a0✝ b0✝ : G
f : G →ₙ* H
hf : Function.Injective ↑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (↑f a0) (↑f b0)
a b : G
ha : a ∈ Finset.preimage A ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑A))
hb : b ∈ Finset.preimage B ↑f (_ : Set.InjOn (↑f) (↑f ⁻¹' ↑B))
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
⊢ UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
⊢ UniqueMul A B a0 b0
[PROOFSTEP]
intro a b ha hb ab
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← hf.eq_iff, ← hf.eq_iff]
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [← hf.eq_iff, map_mul, map_mul] at ab
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
exact h (Finset.mem_image.mpr ⟨_, ha, rfl⟩) (Finset.mem_image.mpr ⟨_, hb, rfl⟩) ab
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
⊢ UniqueMul (Finset.image (↑f) A) (Finset.image (↑f) B) (↑f a0) (↑f b0)
[PROOFSTEP]
intro a b aA bB ab
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a b : H
aA : a ∈ Finset.image (↑f) A
bB : b ∈ Finset.image (↑f) B
ab : a * b = ↑f a0 * ↑f b0
⊢ a = ↑f a0 ∧ b = ↑f b0
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ : ∃ a' ∈ A, f a' = a := Finset.mem_image.mp aA
[GOAL]
case refine'_2.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
b : H
bB : b ∈ Finset.image (↑f) B
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
ab : ↑f a * b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ b = ↑f b0
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ : ∃ b' ∈ B, f b' = b := Finset.mem_image.mp bB
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ ↑f a = ↑f a0 ∧ ↑f b = ↑f b0
[PROOFSTEP]
rw [hf.eq_iff, hf.eq_iff]
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : ↑f a * ↑f b = ↑f a0 * ↑f b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
rw [← map_mul, ← map_mul, hf.eq_iff] at ab
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ↑f
h : UniqueMul A B a0 b0
a : G
ha : a ∈ A
aA : ↑f a ∈ Finset.image (↑f) A
b : G
hb : b ∈ B
bB : ↑f b ∈ Finset.image (↑f) B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
exact h ha hb ab
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ UniqueMul (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
classical convert @mulHom_image_iff G H _ _ A B a0 b0 _ ⟨f, mul⟩ f.2 using 2 <;>
  · ext
    simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ UniqueMul (Finset.map f A) (Finset.map f B) (↑f a0) (↑f b0) ↔ UniqueMul A B a0 b0
[PROOFSTEP]
convert @mulHom_image_iff G H _ _ A B a0 b0 _ ⟨f, mul⟩ f.2 using 2
[GOAL]
case h.e'_1.h.e'_3
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ Finset.map f A = Finset.image (↑{ toFun := ↑f, map_mul' := mul }) A
[PROOFSTEP]
ext
[GOAL]
case h.e'_1.h.e'_3.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f A ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) A
[PROOFSTEP]
simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
case h.e'_1.h.e'_4
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ Finset.map f B = Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
[PROOFSTEP]
ext
[GOAL]
case h.e'_1.h.e'_4.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f B ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
[PROOFSTEP]
simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
let A' : Finset M := A
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
have hA' : A'.Nonempty := hA
[GOAL]
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
obtain ⟨a0, hA0, b0, hB0, J⟩ := UniqueSums.uniqueAdd_of_nonempty hA' hB
[GOAL]
case intro.intro.intro.intro
M : Type ?u.148083
inst✝¹ : Add M
inst✝ : UniqueSums M
A B : Finset (Multiplicative M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
a0 : M
hA0 : a0 ∈ A'
b0 : M
hB0 : b0 ∈ B
J : UniqueAdd A' B a0 b0
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueMul A B a0 b0
[PROOFSTEP]
exact ⟨ofAdd a0, hA0, ofAdd b0, hB0, fun a b aA bB H ↦ J aA bB H⟩
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
let A' : Finset M := A
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
have hA' : A'.Nonempty := hA
[GOAL]
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
obtain ⟨a0, hA0, b0, hB0, J⟩ := UniqueProds.uniqueMul_of_nonempty hA' hB
[GOAL]
case intro.intro.intro.intro
M : Type ?u.148565
inst✝¹ : Mul M
inst✝ : UniqueProds M
A B : Finset (Additive M)
hA : Finset.Nonempty A
hB : Finset.Nonempty B
A' : Finset M := A
hA' : Finset.Nonempty A'
a0 : M
hA0 : a0 ∈ A'
b0 : M
hB0 : b0 ∈ B
J : UniqueMul A' B a0 b0
⊢ ∃ a0, a0 ∈ A ∧ ∃ b0, b0 ∈ B ∧ UniqueAdd A B a0 b0
[PROOFSTEP]
exact ⟨ofMul a0, hA0, ofMul b0, hB0, fun a b aA bB H ↦ J aA bB H⟩