ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsOpen s<GOAL>MeasurableSet (f ⁻¹' sᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsOpen s<GOAL>IsClosed sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsOpen s<GOAL>IsOpen s
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>(1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>(1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ∑ x ∈ A.product B, ↑↑(G.interedges x.1 x.2).card / (↑(↑x.1.card * ↑x.2.card) * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>∑ x ∈ A ×ˢ B, ↑↑(interedges G.Adj x.1 x.2).card * ((1 - ε ^ 5 / 50) / ↑(↑(A.sup id).card * ↑(B.sup id).card)) ≤ ∑ x ∈ A.product B, ↑↑(G.interedges x.1 x.2).card / (↑(↑x.1.card * ↑x.2.card) * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>∑ x ∈ A ×ˢ B, ↑(interedges G.Adj x.1 x.2).card * ((1 - ε ^ 5 / 50) / (↑(A.sup id).card * ↑(B.sup id).card)) ≤ ∑ x ∈ A.product B, ↑(G.interedges x.1 x.2).card / (↑x.1.card * ↑x.2.card * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>∀ i ∈ A ×ˢ B, ↑(interedges G.Adj i.1 i.2).card * ((1 - ε ^ 5 / 50) / (↑(A.sup id).card * ↑(B.sup id).card)) ≤ ↑(G.interedges i.1 i.2).card / (↑i.1.card * ↑i.2.card * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<GOAL>∀ (a b : Finset α), a ∈ A → b ∈ B → ↑(interedges G.Adj a b).card * ((1 - ε ^ 5 / 50) / (↑(A.sup id).card * ↑(B.sup id).card)) ≤ ↑(G.interedges a b).card / (↑a.card * ↑b.card * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>↑(interedges G.Adj x y).card * ((1 - ε ^ 5 / 50) / (↑(A.sup id).card * ↑(B.sup id).card)) ≤ ↑(G.interedges x y).card / (↑x.card * ↑y.card * (↑A.card * ↑B.card))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>↑(interedges G.Adj x y).card * ((1 - ε ^ 5 / 50) / (↑(A.sup id).card * ↑(B.sup id).card) * (↑A.card * ↑x.card * (↑B.card * ↑y.card))) ≤ ↑(G.interedges x y).card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>0 < ↑A.card * ↑x.card * (↑B.card * ↑y.card)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>A.Nonempty
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>x.Nonempty
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>B.Nonempty
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<VAR>this : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))<VAR>x y : Finset α<VAR>hx : x ∈ A<VAR>hy : y ∈ B<GOAL>y.Nonempty
<VAR>k : Type u_1<VAR>inst✝¹⁰ : Field k<VAR>K : Type u_2<VAR>inst✝⁹ : Field K<VAR>F : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra k K<VAR>inst✝⁶ : Algebra k F<VAR>inst✝⁵ : Algebra K F<VAR>inst✝⁴ : IsScalarTower k K F<VAR>inst✝³ : NumberField k<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsGalois k K<VAR>inst✝ : IsUnramifiedAtInfinitePlaces k K<GOAL>Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K
<VAR>k : Type u_1<VAR>inst✝¹⁰ : Field k<VAR>K : Type u_2<VAR>inst✝⁹ : Field K<VAR>F : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra k K<VAR>inst✝⁶ : Algebra k F<VAR>inst✝⁵ : Algebra K F<VAR>inst✝⁴ : IsScalarTower k K F<VAR>inst✝³ : NumberField k<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsGalois k K<VAR>inst✝ : IsUnramifiedAtInfinitePlaces k K<GOAL>Finset.univᶜ = ∅
<VAR>k : Type u_1<VAR>inst✝¹⁰ : Field k<VAR>K : Type u_2<VAR>inst✝⁹ : Field K<VAR>F : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra k K<VAR>inst✝⁶ : Algebra k F<VAR>inst✝⁵ : Algebra K F<VAR>inst✝⁴ : IsScalarTower k K F<VAR>inst✝³ : NumberField k<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsGalois k K<VAR>inst✝ : IsUnramifiedAtInfinitePlaces k K<GOAL>∀ x ∈ Finset.univ, InfinitePlace.IsUnramifiedIn K x
<VAR>k : Type u_1<VAR>inst✝¹⁰ : Field k<VAR>K : Type u_2<VAR>inst✝⁹ : Field K<VAR>F : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra k K<VAR>inst✝⁶ : Algebra k F<VAR>inst✝⁵ : Algebra K F<VAR>inst✝⁴ : IsScalarTower k K F<VAR>inst✝³ : NumberField k<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsGalois k K<VAR>inst✝ : IsUnramifiedAtInfinitePlaces k K<GOAL>∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : Associates α<GOAL>p ≤ 1 ↔ p = 1
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<GOAL>(basisDivisor x x).degree = ⊥
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>R : α → β → Bool<VAR>as : List α<VAR>bs : List β<GOAL>takeWhile₂ R as bs = takeWhile₂TR R as bs
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>R : α → β → Bool<VAR>as : List α<VAR>bs : List β<GOAL>takeWhile₂ R as bs = takeWhile₂TR.go R as bs [] []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 8 → β<GOAL>∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 8 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) * f (last 7) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f✝ : Filter τ<VAR>ϕ✝ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>α' : Type u_5<VAR>ϕ : τ → α' → β<VAR>f : Filter τ<VAR>g : α → α'<GOAL>ω f ϕ (g '' s) = ω f (fun t x => ϕ t (g x)) s
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>a : G<VAR>x : k[G]<GOAL>of' k G a * x /ᵒᶠ a = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>a : G<VAR>x : k[G]<VAR>x✝ : G<GOAL>(of' k G a * x /ᵒᶠ a) x✝ = x x✝
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>a : G<VAR>x : k[G]<VAR>x✝ : G<GOAL>∀ (a_1 : G), a + a_1 = a + x✝ ↔ a_1 = x✝
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>a : G<VAR>x : k[G]<VAR>x✝ c : G<GOAL>a + c = a + x✝ ↔ c = x✝
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>inst✝⁷ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<GOAL>SmoothOn I I (↑f) f.source
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>inst✝⁷ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<GOAL>∀ x ∈ f.source, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I ⊤ (↑f) (f.source ∩ u)
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>inst✝⁷ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I ⊤ (↑f) (f.source ∩ u)
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>inst✝⁷ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>inst✝⁷ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<GOAL>ContMDiffOn I I ⊤ (↑f) (f.source ∩ s)