case mp
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ Pi.mulSingle i x ∈ pi I H → i ∈ I → x ∈ H i

case mpr
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ (i ∈ I → x ∈ H i) → Pi.mulSingle i x ∈ pi I H
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i
constructor
case mp
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : Pi.mulSingle i x ∈ pi I H
hi : i ∈ I
⊢ x ∈ H i
case mp
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ Pi.mulSingle i x ∈ pi I H → i ∈ I → x ∈ H i
intro h hi
no goals
case mp
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : Pi.mulSingle i x ∈ pi I H
hi : i ∈ I
⊢ x ∈ H i
simpa using h i hi
case mpr
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
case mpr
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ (i ∈ I → x ∈ H i) → Pi.mulSingle i x ∈ pi I H
intro h j hj
case pos
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
heq : j = i
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j

case neg
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
heq : ¬j = i
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
case mpr
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
by_cases heq : j = i
case pos
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
j : η
hj : j ∈ I
x : f j
h : j ∈ I → x ∈ H j
⊢ Pi.mulSingle j x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
case pos
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
heq : j = i
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
subst heq
no goals
case pos
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
j : η
hj : j ∈ I
x : f j
h : j ∈ I → x ∈ H j
⊢ Pi.mulSingle j x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
simpa using h hj
no goals
case neg
G : Type ?u.323215
G' : Type ?u.323218
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.323227
inst✝⁴ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.323248
inst✝³ : Group N
P : Type ?u.323254
inst✝² : Group P
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
h : i ∈ I → x ∈ H i
j : η
hj : j ∈ I
heq : ¬j = i
⊢ Pi.mulSingle i x j ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) j
simp [heq, one_mem]