-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem mulSingle_mem_pi [DecidableEq η] {I : Set η} {H : ∀ i, Subgroup (f i)} (i : η) (x : f i) :
    Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i

Proof state:
case mp
η : Type u_7
f : η → Type u_8
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

Tactic:
intro h hi

Result:
case mp
η : Type u_7
f : η → Type u_8
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

Proof state:
case pos
η : Type u_7
f : η → Type u_8
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

Tactic:
subst heq

Result:
case pos
η : Type u_7
f : η → Type u_8
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

Proof state:
case mpr
η : Type u_7
f : η → Type u_8
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

Tactic:
intro h j hj

Result:
case mpr
η : Type u_7
f : η → Type u_8
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

Proof state:
case mp
η : Type u_7
f : η → Type u_8
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

Tactic:
simpa using h i hi

Result:
no goals

Proof state:
η : Type u_7
f : η → Type u_8
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

Tactic:
constructor

Result:
case mp
η : Type u_7
f : η → Type u_8
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
η : Type u_7
f : η → Type u_8
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

Proof state:
case pos
η : Type u_7
f : η → Type u_8
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

Tactic:
simpa using h hj

Result:
no goals

Proof state:
case neg
η : Type u_7
f : η → Type u_8
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

Tactic:
simp [heq, one_mem]

Result:
no goals

Proof state:
case mpr
η : Type u_7
f : η → Type u_8
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

Tactic:
by_cases heq : j = i

Result:
case pos
η : Type u_7
f : η → Type u_8
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
η : Type u_7
f : η → Type u_8
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