G : Type ?u.321013
G' : Type ?u.321016
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321025
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.321046
inst✝² : Group N
P : Type ?u.321052
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ (i : η), i ∈ univ → p i = 1
⊢ p = 1
G : Type ?u.321013
G' : Type ?u.321016
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321025
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.321046
inst✝² : Group N
P : Type ?u.321052
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : p ∈ pi univ fun i => ⊥
⊢ p = 1
simp only [mem_pi, mem_bot] at *
case h
G : Type ?u.321013
G' : Type ?u.321016
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321025
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.321046
inst✝² : Group N
P : Type ?u.321052
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ (i : η), i ∈ univ → p i = 1
j : η
⊢ p j = OfNat.ofNat 1 j
G : Type ?u.321013
G' : Type ?u.321016
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321025
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.321046
inst✝² : Group N
P : Type ?u.321052
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ (i : η), i ∈ univ → p i = 1
⊢ p = 1
ext j
no goals
case h
G : Type ?u.321013
G' : Type ?u.321016
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.321025
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.321046
inst✝² : Group N
P : Type ?u.321052
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ (i : η), i ∈ univ → p i = 1
j : η
⊢ p j = OfNat.ofNat 1 j
exact hp j trivial