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