α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (¬x ∈ ⋃ (i : ι), mulSupport (f i)) → (⨆ (i : ι), f i x) = 1
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), mulSupport (f i)
rw [mulSupport_subset_iff']
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → (⨆ (i : ι), f i x) = 1
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (¬x ∈ ⋃ (i : ι), mulSupport (f i)) → (⨆ (i : ι), f i x) = 1
simp only [mem_iUnion, not_exists, nmem_mulSupport]
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ (⨆ (i : ι), f i x) = 1
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → (⨆ (i : ι), f i x) = 1
intro x hx
no goals
α : Type u_3
β : Type ?u.13009
A : Type ?u.13012
B : Type ?u.13015
M : Type u_1
N : Type ?u.13021
P : Type ?u.13024
R : Type ?u.13027
S : Type ?u.13030
G : Type ?u.13033
M₀ : Type ?u.13036
G₀ : Type ?u.13039
ι : Sort u_2
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ (⨆ (i : ι), f i x) = 1
simp only [hx, ciSup_const]