case mp
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H → ∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i

case mpr
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i) → J ≤ pi I H
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H ↔ ∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i
constructor
case mp
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
⊢ map (Pi.evalMonoidHom f i) J ≤ H i
case mp
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H → ∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i
intro h i hi
case mp.intro.intro
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
x : (i : η) → f i
hx : x ∈ ↑J
⊢ ↑(Pi.evalMonoidHom f i) x ∈ H i
case mp
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
⊢ map (Pi.evalMonoidHom f i) J ≤ H i
rintro _ ⟨x, hx, rfl⟩
no goals
case mp.intro.intro
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
x : (i : η) → f i
hx : x ∈ ↑J
⊢ ↑(Pi.evalMonoidHom f i) x ∈ H i
exact (h hx) _ hi
case mpr
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : ∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i
x : (i : η) → f i
hx : x ∈ J
i : η
hi : i ∈ I
⊢ x i ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) i
case mpr
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i) → J ≤ pi I H
intro h x hx i hi
no goals
case mpr
G : Type ?u.321783
G' : Type ?u.321786
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321795
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.321816
inst✝² : Group N
P : Type ?u.321822
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : ∀ (i : η), i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i
x : (i : η) → f i
hx : x ∈ J
i : η
hi : i ∈ I
⊢ x i ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) i
refine' h i hi ⟨_, hx, rfl⟩