G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1) ↔ ∀ (i : η) (x : f i), x ∈ H i → x = 1
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
simp only [eq_bot_iff_forall]
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1) → ∀ (i : η) (x : f i), x ∈ H i → x = 1

case mpr
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (i : η) (x : f i), x ∈ H i → x = 1) → ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1) ↔ ∀ (i : η) (x : f i), x ∈ H i → x = 1
constructor
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
i : η
x : f i
hx : x ∈ H i
⊢ x = 1
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1) → ∀ (i : η) (x : f i), x ∈ H i → x = 1
intro h i x hx
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
i : η
x : f i
hx : x ∈ H i
this : ↑(MonoidHom.single f i) x = 1
⊢ x = 1
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
i : η
x : f i
hx : x ∈ H i
⊢ x = 1
have : MonoidHom.single f i x = 1 :=
  h (MonoidHom.single f i x) ((mulSingle_mem_pi i x).mpr fun _ => hx)
no goals
case mp
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
h : ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
i : η
x : f i
hx : x ∈ H i
this : ↑(MonoidHom.single f i) x = 1
⊢ x = 1
simpa using congr_fun this i
no goals
case mpr
G : Type ?u.330176
G' : Type ?u.330179
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.330188
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.330209
inst✝² : Group N
P : Type ?u.330215
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (∀ (i : η) (x : f i), x ∈ H i → x = 1) → ∀ (x : (i : η) → f i), x ∈ pi univ H → x = 1
exact fun h x hx => funext fun i => h _ _ (hx i trivial)