ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : R<VAR>f : ι → M<GOAL>c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : ι → M<GOAL>0 • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), 0 • f i
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : R<VAR>f : ι → M<VAR>hc : c ≠ 0<GOAL>c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b<GOAL>a ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b<GOAL>sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ a} ≤ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b}
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J : Ideal R<GOAL>RingHom.ker (quotQuotMk I J) = I ⊔ J
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>C : Set (Set α)<VAR>B : ℕ → Set α<VAR>hA : m0 = generateFrom C<VAR>hC : IsPiSystem C<VAR>h1B : ⋃ i, B i = univ<VAR>h2B : ∀ (i : ℕ), B i ∈ C<VAR>hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤<VAR>h_eq : ∀ s ∈ C, μ s = ν s<GOAL>μ = ν
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>C : Set (Set α)<VAR>B : ℕ → Set α<VAR>hA : m0 = generateFrom C<VAR>hC : IsPiSystem C<VAR>h1B : ⋃ i, B i = univ<VAR>h2B : ∀ (i : ℕ), B i ∈ C<VAR>hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤<VAR>h_eq : ∀ s ∈ C, μ s = ν s<GOAL>range B ⊆ C
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>C : Set (Set α)<VAR>B : ℕ → Set α<VAR>hA : m0 = generateFrom C<VAR>hC : IsPiSystem C<VAR>h1B : ⋃ i, B i = univ<VAR>h2B : ∀ (i : ℕ), B i ∈ C<VAR>hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤<VAR>h_eq : ∀ s ∈ C, μ s = ν s<GOAL>∀ s ∈ range B, μ s ≠ ⊤
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hx : x ∈ s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hx : x ∈ s ∧ (x ∉ s ∨ (↑(G.edgeDensity s t) - ε) * ↑t.card ≤ ↑(filter (G.Adj x) t).card) ∧ (x ∉ s ∨ (↑(G.edgeDensity s u) - ε) * ↑u.card ≤ ↑(filter (G.Adj x) u).card)<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hx : x ∈ s ∧ x ∉ s ∨ x ∈ s ∧ (↑(G.edgeDensity s t) - ε) * ↑t.card ≤ ↑(filter (G.Adj x) t).card ∧ (↑(G.edgeDensity s u) - ε) * ↑u.card ≤ ↑(filter (G.Adj x) u).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hx : x ∈ s ∧ ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card ∧ ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(image (fun x_1 => (x, x_1)) (filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u))<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(↑(G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u)).card / (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card))<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u)).card / (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card)<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u)).card / (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card)<VAR>hε : 0 ≤ ε<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(filter (fun x => match x with | (y, z) => G.Adj y z) (filter (G.Adj x) t ×ˢ filter (G.Adj x) u)).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u)).card / (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card)<VAR>hε : 0 ≤ ε<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ε * (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card)
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hxY : ↑t.card * (↑(G.edgeDensity s t) - ε) ≤ ↑(filter (G.Adj x) t).card<VAR>hsu : ↑u.card * (↑(G.edgeDensity s u) - ε) ≤ ↑(filter (G.Adj x) u).card<VAR>hY : ↑t.card * ε ≤ ↑(filter (G.Adj x) t).card<VAR>hZ : ↑u.card * ε ≤ ↑(filter (G.Adj x) u).card<VAR>this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε<VAR>this : ε ≤ ↑(G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u)).card / (↑(filter (G.Adj x) t).card * ↑(filter (G.Adj x) u).card)<VAR>hε : 0 ≤ ε<GOAL>ε ^ 3 * ↑t.card * ↑u.card = ε * (↑t.card * ε * (↑u.card * ε))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>h : gauge s x < a<GOAL>∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>h : gauge s x < a<VAR>b : ℝ<VAR>hba : b < a<VAR>hb : 0 < b<VAR>hx : x ∈ b • s<GOAL>∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ t<VAR>hst : _root_.Disjoint (s.erase a) t<GOAL>_root_.Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ t<VAR>hst : _root_.Disjoint (s.erase a) t<GOAL>a ∉ s.erase a ∧ _root_.Disjoint (s.erase a) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<GOAL>μ.restrict (toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>μ.restrict (toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<GOAL>μ.restrict (toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<VAR>A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<GOAL>μ.restrict (toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<VAR>A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<GOAL>s ⊆ ⋃ n, v n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<VAR>A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ ⋃ n, v n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<VAR>A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<VAR>x : α<VAR>hx : x ∈ s<VAR>this : 0 < ‖f x‖<GOAL>x ∈ ⋃ n, v n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}<VAR>A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<VAR>x : α<VAR>hx : x ∈ s<VAR>this : 0 < ‖f x‖<VAR>n : ℕ<VAR>hn : u n < ‖f x‖<GOAL>x ∈ ⋃ n, v n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>x✝ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : AddMonoid N<VAR>inst✝ : DistribMulAction R N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>c : R<VAR>v : α →₀ M<VAR>hsmul : ∀ (x : M), f (c • x) = c • f x<GOAL>mapRange f hf (c • v) = c • mapRange f hf v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>x✝ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : AddMonoid N<VAR>inst✝ : DistribMulAction R N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>c : R<VAR>v : α →₀ M<VAR>hsmul : ∀ (x : M), f (c • x) = c • f x<GOAL>mapRange (f ∘ fun x => c • x) ?h v = c • mapRange f hf v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>x✝ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : AddMonoid N<VAR>inst✝ : DistribMulAction R N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>c : R<VAR>v : α →₀ M<VAR>hsmul : ∀ (x : M), f (c • x) = c • f x<GOAL>(f ∘ fun x => c • x) 0 = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>(H ⊓ K).relindex K = H.relindex K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise Commute<GOAL>noncommFold (fun x x_1 => x * x_1) (↑l) comm 1 = l.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>l : List α<VAR>comm : {x | x ∈ ↑l}.Pairwise Commute<GOAL>List.foldr (fun x x_1 => x * x_1) 1 l = l.prod
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : Y<VAR>y z : X<GOAL>glueDist Φ Ψ ε (Sum.inr x) (Sum.inl z) ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inl z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : Y<VAR>y z : X<GOAL>glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inl z).swap ≤ glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inl y).swap + glueDist Ψ Φ ε (Sum.inl y).swap (Sum.inl z).swap
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x y : Y<VAR>z : X<GOAL>glueDist Φ Ψ ε (Sum.inr x) (Sum.inl z) ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x y : X<VAR>z : Y<GOAL>glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : Y<VAR>y : X<VAR>z : Y<GOAL>glueDist Φ Ψ ε (Sum.inr x) (Sum.inr z) ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : Y<VAR>y : X<VAR>z : Y<GOAL>glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inr z).swap ≤ glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inl y).swap + glueDist Ψ Φ ε (Sum.inl y).swap (Sum.inr z).swap