case intro
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x : FreeProduct fun i => G i
⊢ ↑(↑lift f) x ∈ s
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
⊢ MonoidHom.range (↑lift f) ≤ s
rintro _ ⟨x, rfl⟩
case intro.h_one
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
⊢ ↑(↑lift f) 1 ∈ s

case intro.h_of
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
i : ι
x : G i
⊢ ↑(↑lift f) (↑of x) ∈ s

case intro.h_mul
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x y : FreeProduct fun i => G i
hx : ↑(↑lift f) x ∈ s
hy : ↑(↑lift f) y ∈ s
⊢ ↑(↑lift f) (x * y) ∈ s
case intro
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x : FreeProduct fun i => G i
⊢ ↑(↑lift f) x ∈ s
induction' x using FreeProduct.induction_on with i x x y hx hy
no goals
case intro.h_one
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
⊢ ↑(↑lift f) 1 ∈ s
exact s.one_mem
case intro.h_of
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
i : ι
x : G i
⊢ ↑(f i) x ∈ s
case intro.h_of
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
i : ι
x : G i
⊢ ↑(↑lift f) (↑of x) ∈ s
simp only [lift_of, SetLike.mem_coe]
no goals
case intro.h_of
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
i : ι
x : G i
⊢ ↑(f i) x ∈ s
exact h i (Set.mem_range_self x)
case intro.h_mul
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x y : FreeProduct fun i => G i
hx : ↑(↑lift f) x ∈ s
hy : ↑(↑lift f) y ∈ s
⊢ ↑(↑lift f) x * ↑(↑lift f) y ∈ s
case intro.h_mul
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x y : FreeProduct fun i => G i
hx : ↑(↑lift f) x ∈ s
hy : ↑(↑lift f) y ∈ s
⊢ ↑(↑lift f) (x * y) ∈ s
simp only [map_mul, SetLike.mem_coe]
no goals
case intro.h_mul
ι : Type u_3
M : ι → Type ?u.337350
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.337361
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), MonoidHom.range (f i) ≤ s
x y : FreeProduct fun i => G i
hx : ↑(↑lift f) x ∈ s
hy : ↑(↑lift f) y ∈ s
⊢ ↑(↑lift f) x * ↑(↑lift f) y ∈ s
exact s.mul_mem hx hy