Last active
April 7, 2026 21:59
-
-
Save kbuzzard/766fa711cefb620e10048c9587d89318 to your computer and use it in GitHub Desktop.
to_additive trace on fcdb939
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [attribute] [5722493.000000] ✅️ applying [to_additive] ▼ | |
| [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inl) a | |
| [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inr) b | |
| [translate_detail] [4256341.000000] ✅️ translating the value fun {α} {β} {M} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f} | |
| {a b} h₁ h₂ ↦ | |
| have this := | |
| Eq.mpr | |
| (id | |
| (congrArg (fun _a ↦ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) _a (𝓝 (a * b))) | |
| (OrderIso.map_atTop sumEquiv))) | |
| (Eq.mpr | |
| (id | |
| (congrArg (fun _a ↦ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) _a (𝓝 (a * b))) | |
| (Eq.symm prod_atTop_atTop_eq))) | |
| (Eq.mpr | |
| (eq_of_heq | |
| ((fun α β f f' e'_3 l₁ l₁' e'_4 l₂ ↦ | |
| Eq.casesOn (motive := fun a x ↦ f' = a → e'_3 ≍ x → Tendsto f l₁ l₂ ≍ Tendsto f' l₁' l₂) e'_3 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun f' ↦ | |
| ∀ (e_3 : f = f'), e_3 ≍ Eq.refl f → Tendsto f l₁ l₂ ≍ Tendsto f' l₁' l₂) | |
| (fun e_3 h ↦ | |
| Eq.casesOn (motive := fun a x ↦ l₁' = a → e'_4 ≍ x → Tendsto f l₁ l₂ ≍ Tendsto f l₁' l₂) | |
| e'_4 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun l₁' ↦ | |
| ∀ (e_4 : l₁ = l₁'), e_4 ≍ Eq.refl l₁ → Tendsto f l₁ l₂ ≍ Tendsto f l₁' l₂) | |
| (fun e_4 h ↦ HEq.refl (Tendsto f l₁ l₂)) (Eq.symm h) e'_4) | |
| (Eq.refl l₁') (HEq.refl e'_4)) | |
| (Eq.symm h) e'_3) | |
| (Eq.refl f') (HEq.refl e'_3)) | |
| (Finset α × Finset β) M ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) | |
| ((fun p ↦ p.1 * p.2) ∘ | |
| Prod.map (fun s ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun s ↦ ∏ b ∈ s, (f ∘ Sum.inr) b) | |
| (funext fun s ↦ | |
| of_eq_true | |
| (Eq.trans | |
| (congr (congrArg Eq (prod_disjSum s.1 s.2 f)) | |
| (congrFun' | |
| (congrArg (comp fun p ↦ p.1 * p.2) | |
| (congr | |
| (congrArg Prod.map | |
| (funext fun s ↦ prod_congr (Eq.refl s) fun x a ↦ Eq.refl (f (Sum.inl x)))) | |
| (funext fun s ↦ prod_congr (Eq.refl s) fun x a ↦ Eq.refl (f (Sum.inr x))))) | |
| s)) | |
| (eq_self ((∏ x ∈ s.1, f (Sum.inl x)) * ∏ x ∈ s.2, f (Sum.inr x))))) | |
| (atTop ×ˢ atTop) | |
| ((SummationFilter.unconditional α).filter ×ˢ (SummationFilter.unconditional β).filter) | |
| (eq_of_heq | |
| ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 ↦ | |
| Eq.casesOn (motive := fun a_2 x ↦ a' = a_2 → e'_5 ≍ x → a ×ˢ a_1 ≍ a' ×ˢ a'_1) e'_5 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun a' ↦ ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a ×ˢ a_1 ≍ a' ×ˢ a'_1) | |
| (fun e_5 h ↦ | |
| Eq.casesOn (motive := fun a_2 x ↦ a'_1 = a_2 → e'_6 ≍ x → a ×ˢ a_1 ≍ a ×ˢ a'_1) e'_6 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun a' ↦ | |
| ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a ×ˢ a_1 ≍ a ×ˢ a') | |
| (fun e_6 h ↦ HEq.refl (a ×ˢ a_1)) (Eq.symm h) e'_6) | |
| (Eq.refl a'_1) (HEq.refl e'_6)) | |
| (Eq.symm h) e'_5) | |
| (Eq.refl a') (HEq.refl e'_5)) | |
| (Filter (Finset α)) (Filter (Finset β)) (Filter (Finset α × Finset β)) Filter.instSProd atTop | |
| (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) | |
| e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } | |
| (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop | |
| (SummationFilter.unconditional α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| α { filter := atTop } | |
| (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| α atTop | |
| (SummationFilter.unconditional | |
| α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 h ↦ | |
| HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') | |
| (HEq.refl e'_2)) | |
| α { filter := atTop } | |
| (SummationFilter.unconditional α) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := | |
| fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun filter' ↦ | |
| ∀ | |
| (e_2 : | |
| filter = filter'), | |
| e_2 ≍ | |
| Eq.refl filter → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { | |
| filter := | |
| filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') | |
| (HEq.refl e'_2)) | |
| α atTop | |
| (SummationFilter.unconditional | |
| α).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := | |
| fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun self' ↦ | |
| ∀ | |
| (e_2 : | |
| self = self'), | |
| e_2 ≍ | |
| Eq.refl | |
| self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') | |
| (HEq.refl e'_2)) | |
| α { filter := atTop } | |
| (SummationFilter.unconditional | |
| α) | |
| (eq_of_heq | |
| ((fun β filter filter' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec | |
| (motive := | |
| fun filter' ↦ | |
| ∀ | |
| (e_2 : | |
| filter = | |
| filter'), | |
| e_2 ≍ | |
| Eq.refl | |
| filter → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { | |
| filter := | |
| filter }) | |
| (Eq.symm h) | |
| e'_2) | |
| (Eq.refl filter') | |
| (HEq.refl e'_2)) | |
| α atTop | |
| (SummationFilter.unconditional | |
| α).filter | |
| (eq_of_heq | |
| ((fun β self self' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec | |
| (motive := | |
| fun | |
| self' ↦ | |
| ∀ | |
| (e_2 : | |
| self = | |
| self'), | |
| e_2 ≍ | |
| Eq.refl | |
| self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 | |
| h ↦ | |
| HEq.refl | |
| self.filter) | |
| (Eq.symm | |
| h) | |
| e'_2) | |
| (Eq.refl | |
| self') | |
| (HEq.refl | |
| e'_2)) | |
| α | |
| { | |
| filter := | |
| atTop } | |
| (SummationFilter.unconditional | |
| α) | |
| (eq_of_heq | |
| ((fun β filter | |
| filter' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| ⋯) e'_2 ⋯ | |
| (Eq.refl | |
| filter') | |
| (HEq.refl | |
| e'_2)) | |
| α atTop | |
| (SummationFilter.unconditional | |
| α).filter | |
| (eq_of_heq | |
| (⋯ α | |
| { | |
| filter := | |
| atTop } | |
| (SummationFilter.unconditional | |
| α) | |
| ⋯)))))))))))))))))))))))))))))))))))))))))) | |
| atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → e'_2 ≍ x → self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) (Eq.symm h) | |
| e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } | |
| (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop | |
| (SummationFilter.unconditional β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ self'.filter) | |
| (fun e_2 h ↦ HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') (HEq.refl e'_2)) | |
| β { filter := atTop } | |
| (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun filter' ↦ | |
| ∀ (e_2 : filter = filter'), | |
| e_2 ≍ Eq.refl filter → | |
| { filter := filter } ≍ | |
| { filter := filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { filter := filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') (HEq.refl e'_2)) | |
| β atTop | |
| (SummationFilter.unconditional | |
| β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun self' ↦ | |
| ∀ (e_2 : self = self'), | |
| e_2 ≍ Eq.refl self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 h ↦ | |
| HEq.refl self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') | |
| (HEq.refl e'_2)) | |
| β { filter := atTop } | |
| (SummationFilter.unconditional β) | |
| (eq_of_heq | |
| ((fun β filter filter' e'_2 ↦ | |
| Eq.casesOn (motive := | |
| fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { filter := filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun filter' ↦ | |
| ∀ | |
| (e_2 : | |
| filter = filter'), | |
| e_2 ≍ | |
| Eq.refl filter → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { | |
| filter := | |
| filter }) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl filter') | |
| (HEq.refl e'_2)) | |
| β atTop | |
| (SummationFilter.unconditional | |
| β).filter | |
| (eq_of_heq | |
| ((fun β self self' e'_2 ↦ | |
| Eq.casesOn (motive := | |
| fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec (motive := | |
| fun self' ↦ | |
| ∀ | |
| (e_2 : | |
| self = self'), | |
| e_2 ≍ | |
| Eq.refl | |
| self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| self.filter) | |
| (Eq.symm h) e'_2) | |
| (Eq.refl self') | |
| (HEq.refl e'_2)) | |
| β { filter := atTop } | |
| (SummationFilter.unconditional | |
| β) | |
| (eq_of_heq | |
| ((fun β filter filter' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| fun a x ↦ | |
| filter' = a → | |
| e'_2 ≍ x → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec | |
| (motive := | |
| fun filter' ↦ | |
| ∀ | |
| (e_2 : | |
| filter = | |
| filter'), | |
| e_2 ≍ | |
| Eq.refl | |
| filter → | |
| { | |
| filter := | |
| filter } ≍ | |
| { | |
| filter := | |
| filter' }) | |
| (fun e_2 h ↦ | |
| HEq.refl | |
| { | |
| filter := | |
| filter }) | |
| (Eq.symm h) | |
| e'_2) | |
| (Eq.refl filter') | |
| (HEq.refl e'_2)) | |
| β atTop | |
| (SummationFilter.unconditional | |
| β).filter | |
| (eq_of_heq | |
| ((fun β self self' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| fun a x ↦ | |
| self' = a → | |
| e'_2 ≍ x → | |
| self.filter ≍ | |
| self'.filter) | |
| e'_2 | |
| (fun h ↦ | |
| Eq.ndrec | |
| (motive := | |
| fun | |
| self' ↦ | |
| ∀ | |
| (e_2 : | |
| self = | |
| self'), | |
| e_2 ≍ | |
| Eq.refl | |
| self → | |
| self.filter ≍ | |
| self'.filter) | |
| (fun e_2 | |
| h ↦ | |
| HEq.refl | |
| self.filter) | |
| (Eq.symm | |
| h) | |
| e'_2) | |
| (Eq.refl | |
| self') | |
| (HEq.refl | |
| e'_2)) | |
| β | |
| { | |
| filter := | |
| atTop } | |
| (SummationFilter.unconditional | |
| β) | |
| (eq_of_heq | |
| ((fun β filter | |
| filter' | |
| e'_2 ↦ | |
| Eq.casesOn | |
| (motive := | |
| ⋯) e'_2 ⋯ | |
| (Eq.refl | |
| filter') | |
| (HEq.refl | |
| e'_2)) | |
| β atTop | |
| (SummationFilter.unconditional | |
| β).filter | |
| (eq_of_heq | |
| (⋯ β | |
| { | |
| filter := | |
| atTop } | |
| (SummationFilter.unconditional | |
| β) | |
| ⋯)))))))))))))))))))))))))))))))))))))))))))) | |
| (𝓝 (a * b)))) | |
| (Tendsto.comp tendsto_mul (Eq.symm nhds_prod_eq ▸ Tendsto.prodMap h₁ h₂)))); | |
| Eq.mp | |
| (congrFun' | |
| (congrArg LE.le | |
| (Eq.trans | |
| (Eq.trans | |
| (congrArg (Filter.map ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm)) (OrderIso.map_atTop sumEquiv)) | |
| (Eq.symm Filter.map_map)) | |
| (congrArg (Filter.map fun x ↦ ∏ b ∈ x, f b) (OrderIso.map_atTop sumEquiv.symm)))) | |
| (𝓝 (a * b))) | |
| this ▶ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment