case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), mrange (ϕ i)

case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ (⨆ (i : ι), mrange (ϕ i)) ≤ mrange (noncommPiCoprod ϕ hcomm)
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), mrange (ϕ i)
apply le_antisymm
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), mrange (ϕ i)
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), mrange (ϕ i)
rintro x ⟨f, rfl⟩
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), mrange (ϕ i)
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), mrange (ϕ i)
refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
case a.intro.hs
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => mrange (ϕ i)

case a.intro.a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ?a.intro.s✝

case a.intro.s
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ Submonoid M
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), mrange (ϕ i)
apply Submonoid.mem_sSup_of_mem
no goals
case a.intro.a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ (fun i => mrange (ϕ i)) i
simp
no goals
case a.intro.hs
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => mrange (ϕ i)
use i
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ (⨆ (i : ι), mrange (ϕ i)) ≤ mrange (noncommPiCoprod ϕ hcomm)
refine' iSup_le _
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y ∈ mrange (noncommPiCoprod ϕ hcomm)
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
rintro i x ⟨y, rfl⟩
no goals
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y ∈ mrange (noncommPiCoprod ϕ hcomm)
refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩