ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ (⨆ (i : ι), MonoidHom.range (f i)) ≤ MonoidHom.range (↑lift f)
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ MonoidHom.range (↑lift f) = ⨆ (i : ι), MonoidHom.range (f i)
apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), MonoidHom.range (f i) ≤ MonoidHom.range (↑lift f)
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ (⨆ (i : ι), MonoidHom.range (f i)) ≤ MonoidHom.range (↑lift f)
apply iSup_le _
case intro
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ ↑(f i) x ∈ MonoidHom.range (↑lift f)
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), MonoidHom.range (f i) ≤ MonoidHom.range (↑lift f)
rintro i _ ⟨x, rfl⟩
no goals
case intro
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ ↑(f i) x ∈ MonoidHom.range (↑lift f)
exact ⟨of x, by simp only [lift_of]⟩
no goals
ι : Type u_3
M : ι → Type ?u.342946
inst✝³ : (i : ι) → Monoid (M i)
N✝ : Type ?u.342957
inst✝² : Monoid N✝
G : ι → Type u_2
inst✝¹ : (i : ι) → Group (G i)
N : Type u_1
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ ↑(↑lift f) (↑of x) = ↑(f i) x
simp only [lift_of]