[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
x y z : M
x✝¹ : y ∈ powers x
x✝ : z ∈ powers x
n₁ : ℕ
h₁ : x ^ n₁ = y
n₂ : ℕ
h₂ : x ^ n₂ = z
⊢ x ^ (n₁ + n₂) = y * z
[PROOFSTEP]
simp only [pow_add, *]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ IsSubmonoid Set.univ
[PROOFSTEP]
constructor
[GOAL]
case one_mem
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ 1 ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
case mul_mem
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a * b ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ f 1 ∈ s
[PROOFSTEP]
rw [IsMonoidHom.map_one hf]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ 1 ∈ s
[PROOFSTEP]
exact hs.one_mem
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f (a * b) ∈ s
[PROOFSTEP]
rw [IsMonoidHom.map_mul' hf]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f a * f b ∈ s
[PROOFSTEP]
exact hs.mul_mem ha hb
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
s : Set M
hs : IsSubmonoid s
a b : γ
x✝¹ : a ∈ f '' s
x✝ : b ∈ f '' s
x : M
hx : x ∈ s ∧ f x = a
y : M
hy : y ∈ s ∧ f y = b
⊢ f (x * y) = a * b
[PROOFSTEP]
rw [hf.map_mul, hx.2, hy.2]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
⊢ IsSubmonoid (Set.range f)
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
⊢ IsSubmonoid (f '' Set.univ)
[PROOFSTEP]
exact Univ.isSubmonoid.image hf
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ a ^ 0 ∈ s
[PROOFSTEP]
rw [pow_zero]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact hs.one_mem
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s
[PROOFSTEP]
rw [pow_succ]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s
[PROOFSTEP]
exact hs.mul_mem h (IsSubmonoid.pow_mem hs h)
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
⊢ a ∈ s ∧ ∀ (x : M), x ∈ l → x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
this : a * List.prod l ∈ s
⊢ List.prod (a :: l) ∈ s
[PROOFSTEP]
simpa
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
⊢ (∀ (a : M), a ∈ m → a ∈ s) → Multiset.prod m ∈ s
[PROOFSTEP]
refine' Quotient.inductionOn m fun l hl => _
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ Multiset.prod (Quotient.mk (List.isSetoid M) l) ∈ s
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe, Multiset.coe_prod]
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ List.prod l ∈ s
[PROOFSTEP]
exact list_prod_mem hs hl
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
M : Type u_3
A : Type u_4
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
f : A → M
m : Multiset A
hm : Multiset.Nodup m
x✝ : ∀ (b : A), b ∈ { val := m, nodup := hm } → f b ∈ s
⊢ ∀ (a : M), a ∈ Multiset.map (fun b => f b) { val := m, nodup := hm }.val → a ∈ s
[PROOFSTEP]
simpa
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a : M
ha : a ∈ Closure s
⊢ a ∈ t
[PROOFSTEP]
induction ha
[GOAL]
case basic
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a a✝¹ : M
a✝ : a✝¹ ∈ s
⊢ a✝¹ ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a : M
⊢ 1 ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : a✝² ∈ t
a_ih✝ : b✝ ∈ t
⊢ a✝² * b✝ ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
⊢ f '' Closure s ≤ Closure (f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
hx : x ∈ Closure s
⊢ f x ∈ Closure (f '' s)
[PROOFSTEP]
induction' hx with z hz
[GOAL]
case intro.intro.basic
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x z : M
hz : z ∈ s
⊢ f z ∈ Closure (f '' s)
[PROOFSTEP]
solve_by_elim [subset_closure, Set.mem_image_of_mem]
[GOAL]
case intro.intro.one
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ f 1 ∈ Closure (f '' s)
[PROOFSTEP]
rw [hf.map_one]
[GOAL]
case intro.intro.one
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ 1 ∈ Closure (f '' s)
[PROOFSTEP]
apply IsSubmonoid.one_mem (closure.isSubmonoid (f '' s))
[GOAL]
case intro.intro.mul
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f (a✝² * b✝) ∈ Closure (f '' s)
[PROOFSTEP]
rw [hf.map_mul]
[GOAL]
case intro.intro.mul
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f a✝² * f b✝ ∈ Closure (f '' s)
[PROOFSTEP]
solve_by_elim [(closure.isSubmonoid _).mul_mem]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
h : a ∈ Closure s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
induction h
[GOAL]
case basic
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝¹ : M
a✝ : a✝¹ ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝¹
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case basic a ha => exists [a]; simp [ha]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
case basic a ha => exists [a]; simp [ha]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
exists [a]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ (∀ (x : M), x ∈ [a] → x ∈ s) ∧ List.prod [a] = a
[PROOFSTEP]
simp [ha]
[GOAL]
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case one => exists []; simp
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
[PROOFSTEP]
case one => exists []; simp
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
[PROOFSTEP]
exists []
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ (∀ (x : M), x ∈ [] → x ∈ s) ∧ List.prod [] = 1
[PROOFSTEP]
simp
[GOAL]
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case mul a b _ _ ha hb =>
  rcases ha with ⟨la, ha, eqa⟩
  rcases hb with ⟨lb, hb, eqb⟩
  exists la ++ lb
  simp [eqa.symm, eqb.symm, or_imp]
  exact fun a => ⟨ha a, hb a⟩
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
ha : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
case mul a b _ _ ha hb =>
  rcases ha with ⟨la, ha, eqa⟩
  rcases hb with ⟨lb, hb, eqb⟩
  exists la ++ lb
  simp [eqa.symm, eqb.symm, or_imp]
  exact fun a => ⟨ha a, hb a⟩
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
ha : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
rcases ha with ⟨la, ha, eqa⟩
[GOAL]
case intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
rcases hb with ⟨lb, hb, eqb⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
exists la ++ lb
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ (∀ (x : M), x ∈ la ++ lb → x ∈ s) ∧ List.prod (la ++ lb) = a * b
[PROOFSTEP]
simp [eqa.symm, eqb.symm, or_imp]
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ ∀ (x : M), (x ∈ la → x ∈ s) ∧ (x ∈ lb → x ∈ s)
[PROOFSTEP]
exact fun a => ⟨ha a, hb a⟩
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_3
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
hs : hd ∈ s
⊢ hd * y * z = List.prod (hd :: tl)
[PROOFSTEP]
rw [mul_assoc, List.prod_cons, ← hyzx]
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_3
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
ht : hd ∈ t
⊢ y * (z * hd) = List.prod (hd :: tl)
[PROOFSTEP]
rw [← mul_assoc, List.prod_cons, ← hyzx, mul_comm hd]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
S : Submonoid M
⊢ IsSubmonoid ↑S
[PROOFSTEP]
refine' ⟨S.2, S.1.2⟩


[GOAL]
α : Type u
β : Type v
inst✝² : Mul α
inst✝¹ : Mul β
γ : Type u_1
inst✝ : Mul γ
f : α → β
g : β → γ
hf : IsMulHom f
hg : IsMulHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp only [Function.comp, hf.map_mul, hg.map_mul]
[GOAL]
α✝ : Type u
β✝ : Type v
inst✝⁴ : Mul α✝
inst✝³ : Mul β✝
γ : Type u_1
inst✝² : Mul γ
α : Type u_2
β : Type u_3
inst✝¹ : Semigroup α
inst✝ : CommSemigroup β
f g : α → β
hf : IsMulHom f
hg : IsMulHom g
a b : α
⊢ f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOFSTEP]
simp only [hf.map_mul, hg.map_mul, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u
β : Type v
inst✝¹ : MulOneClass α
inst✝ : Group β
f : α → β
hf : IsMulHom f
⊢ ?m.13736 hf * f 1 = ?m.13736 hf
[PROOFSTEP]
rw [← hf.map_mul, one_mul]
[GOAL]
α : Type u
β : Type v
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
f : α → β
hf : IsMonoidHom f
γ : Type u_1
inst✝ : MulOneClass γ
g : β → γ
hg : IsMonoidHom g
src✝ : IsMulHom (g ∘ f) := IsMulHom.comp hf.toIsMulHom hg.toIsMulHom
⊢ g (f 1) = 1
[PROOFSTEP]
rw [hf.map_one, hg.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f : α → β
hf✝ hf : IsGroupHom f
a : α
⊢ f a⁻¹ * f a = 1
[PROOFSTEP]
rw [← hf.map_mul, inv_mul_self, hf.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f : α → β
hf✝ hf : IsGroupHom f
a b : α
⊢ f (a / b) = f a / f b
[PROOFSTEP]
simp_rw [div_eq_mul_inv, hf.map_mul, hf.map_inv]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : Function.Injective f
x✝ : α
⊢ f x✝ = 1 → x✝ = 1
[PROOFSTEP]
rw [← hf.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : Function.Injective f
x✝ : α
⊢ f x✝ = f 1 → x✝ = 1
[PROOFSTEP]
exact @h _ _
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : ∀ (a : α), f a = 1 → a = 1
x y : α
hxy : f x = f y
⊢ f (x / y) = 1
[PROOFSTEP]
rwa [hf.map_div, div_eq_one]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup α
inst✝ : AddCommGroup β
f g : α → β
hf : IsAddGroupHom f
hg : IsAddGroupHom g
⊢ IsAddGroupHom fun a => f a - g a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg