ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>hs : s.Nonempty<VAR>Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i<GOAL>∃ i ∈ s, f i ≤ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>hs : s.Nonempty<VAR>Hlt : ∀ i ∈ s, g i < f i<GOAL>∏ i ∈ s, g i < ∏ i ∈ s, f i
<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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>s t : Set β<VAR>ht : MeasurableSet t<GOAL>((Measure.map f μ).restrict s) t = (Measure.map f (μ.restrict (f ⁻¹' s))) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<GOAL>¬Irreducible 1
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>m : M<VAR>a : α<GOAL>m ^ period m a • a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<GOAL>Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>l : ℝ≥0∞<VAR>hl : l < μ (⋂ r, ⋂ (_ : r > a), s r)<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, l < (⇑μ ∘ s) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>L : ℝ≥0∞<VAR>hL : L > μ (⋂ r, ⋂ (_ : r > a), s r)<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, (⇑μ ∘ s) b < L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>L : ℝ≥0∞<VAR>hL : L > μ (⋂ r, ⋂ (_ : r > a), s r)<VAR>u : ℕ → ι<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), a < u n<VAR>u_lim : Tendsto u atTop (𝓝 a)<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, (⇑μ ∘ s) b < L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>L : ℝ≥0∞<VAR>hL : L > μ (⋂ r, ⋂ (_ : r > a), s r)<VAR>u : ℕ → ι<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), a < u n<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : Tendsto (⇑μ ∘ s ∘ u) atTop (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))<VAR>B : ⋂ n, s (u n) = ⋂ r, ⋂ (_ : r > a), s r<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, (⇑μ ∘ s) b < L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>L : ℝ≥0∞<VAR>hL : L > μ (⋂ r, ⋂ (_ : r > a), s r)<VAR>u : ℕ → ι<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), a < u n<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : Tendsto (⇑μ ∘ s ∘ u) atTop (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))<VAR>B : ⋂ n, s (u n) = ⋂ r, ⋂ (_ : r > a), s r<VAR>n : ℕ<VAR>hn : μ (s (u n)) < L<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, (⇑μ ∘ s) b < L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>ι : Type u_8<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : DenselyOrdered ι<VAR>inst✝ : FirstCountableTopology ι<VAR>s : ι → Set α<VAR>a : ι<VAR>hs : ∀ r > a, MeasurableSet (s r)<VAR>hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j<VAR>hf : ∃ r > a, μ (s r) ≠ ⊤<VAR>L : ℝ≥0∞<VAR>hL : L > μ (⋂ r, ⋂ (_ : r > a), s r)<VAR>u : ℕ → ι<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), a < u n<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : Tendsto (⇑μ ∘ s ∘ u) atTop (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))<VAR>B : ⋂ n, s (u n) = ⋂ r, ⋂ (_ : r > a), s r<VAR>n : ℕ<VAR>hn : μ (s (u n)) < L<VAR>this : Ioc a (u n) ∈ 𝓝[>] a<GOAL>∀ᶠ (b : ι) in 𝓝[>] a, (⇑μ ∘ s) b < L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : δ → β<GOAL>(fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(T⁻¹ • z).im = z.im
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (X ^ p - C a)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this : ¬IsUnit (X ^ p - C a)<GOAL>Irreducible (X ^ p - C a)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this : ¬IsUnit (X ^ p - C a)<VAR>g : K[X]<VAR>hg : Irreducible g<VAR>hg' : g ∣ X ^ p - C a<GOAL>Irreducible (X ^ p - C a)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this : ¬IsUnit (X ^ p - C a)<VAR>g : K[X]<VAR>hg : Irreducible g<VAR>hg' : g ∣ X ^ p - C a<GOAL>g.natDegree = p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this : ¬IsUnit (X ^ p - C a)<VAR>g : K[X]<VAR>hg : Irreducible g<VAR>hg' : g ∣ X ^ p - C a<VAR>h : ¬g.natDegree = p<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this✝ : ¬IsUnit (X ^ p - C a)<VAR>g : K[X]<VAR>hg : Irreducible g<VAR>hg' : g ∣ X ^ p - C a<VAR>h : ¬g.natDegree = p<VAR>this : Fact (Irreducible g)<VAR>key : (Algebra.norm K) (root g) ^ p = a ^ g.natDegree<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>this✝¹ : ¬IsUnit (X ^ p - C a)<VAR>g : K[X]<VAR>hg : Irreducible g<VAR>hg' : g ∣ X ^ p - C a<VAR>h : ¬g.natDegree = p<VAR>this✝ : Fact (Irreducible g)<VAR>key : (Algebra.norm K) (root g) ^ p = a ^ g.natDegree<VAR>this : p.Coprime g.natDegree<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fintype (ZMod p)ˣ<GOAL>Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
<VAR>p : ℕ<VAR>inst✝ : Fintype (ZMod p)ˣ<VAR>hp : p = 0<GOAL>Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
<VAR>p : ℕ<VAR>inst✝ : Fintype (ZMod p)ˣ<VAR>hp : NeZero p<GOAL>Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<GOAL>(eval₂Hom f g) p = f (constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<GOAL>(eval₂Hom f g) (∑ v ∈ p.support, (monomial v) (coeff v p)) = f (constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<GOAL>(∑ x ∈ p.support, f (coeff x p) * x.prod fun i k => g i ^ k) = f (constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<VAR>h0 : constantCoeff p = 0<GOAL>(∑ x ∈ p.support, f (coeff x p) * x.prod fun i k => g i ^ k) = f (constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<VAR>h0 : ¬constantCoeff p = 0<GOAL>(∑ x ∈ p.support, f (coeff x p) * x.prod fun i k => g i ^ k) = f (constantCoeff p)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<VAR>h0 : constantCoeff p = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p.support<GOAL>(f (coeff d p) * d.prod fun i k => g i ^ k) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<VAR>h0 : ¬constantCoeff p = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p.support<VAR>hd0 : d ≠ 0<GOAL>(f (coeff d p) * d.prod fun i k => g i ^ k) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<VAR>p : MvPolynomial σ R<VAR>hp : ∀ i ∈ p.vars, g i = 0<VAR>h0 : ¬constantCoeff p = 0<GOAL>0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : ↑(G.cliqueFinset 3).card < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3<GOAL>∃ G' ≤ G, ∃ x, ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : ↑(G.cliqueFinset 3).card < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3<VAR>h : ∀ G' ≤ G, ∀ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : ↑(G.cliqueFinset 3).card < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3<VAR>h : ∀ G' ≤ G, ∀ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3<GOAL>∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG✝ : ↑(G.cliqueFinset 3).card < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3<VAR>h : ∀ G' ≤ G, ∀ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3<VAR>G' : SimpleGraph α<VAR>inst✝ : DecidableRel G'.Adj<VAR>hG : G' ≤ G<VAR>hG' : G'.CliqueFree 3<GOAL>ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑G'.edgeFinset.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>Ico a b \ Ico a c = Ico (max a c) b
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : K.X j ⟶ A<VAR>hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0<GOAL>(if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ (singleObjXIsoOfEq c j A j hi).inv else 0) = φ ≫ (singleObjXSelf c j A).inv
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : K.X j ⟶ A<VAR>hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0<GOAL>φ ≫ (singleObjXIsoOfEq c j A j ⋯).inv = φ ≫ (singleObjXSelf c j A).inv
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝¹ : (i : ι) → Sub (α i)<VAR>inst✝ : ∀ (i : ι), OrderedSub (α i)<VAR>f✝ g✝ : Π₀ (i : ι), α i<VAR>i✝ : ι<VAR>a b : α i✝<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<GOAL>(f - g) i = (⇑f - ⇑g) i
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<GOAL>μ (f '' s) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<GOAL>∀ (R : ℝ), μ (f '' (s ∩ closedBall 0 R)) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<GOAL>μ (f '' (s ∩ closedBall 0 R)) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<VAR>A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)<GOAL>μ (f '' (s ∩ closedBall 0 R)) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<VAR>A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)<VAR>B : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)<GOAL>μ (f '' (s ∩ closedBall 0 R)) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<VAR>A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)<VAR>B : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)<GOAL>μ (f '' (s ∩ closedBall 0 R)) ≤ 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<VAR>A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)<VAR>B : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)<GOAL>∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, μ (f '' (s ∩ closedBall 0 R)) ≤ ↑c * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>R : ℝ<VAR>A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)<VAR>B : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)<GOAL>∀ a ∈ Ioi 0, μ (f '' (s ∩ closedBall 0 R)) ≤ ↑a * μ (closedBall 0 R)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<VAR>u' : ℤˣ<VAR>g' : G<VAR>h' : (u', g') ∈ { head := g, toList := (u, w.head) :: w.toList, chain := ⋯ }.toList<GOAL>g' ∈ d.set u'
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<VAR>u' : ℤˣ<VAR>g' : G<VAR>h' : u' = u ∧ g' = w.head ∨ (u', g') ∈ w.toList<GOAL>g' ∈ d.set u'
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<GOAL>List.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ((u, w.head) :: w.toList)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<GOAL>∀ y ∈ w.toList.head?, (u, w.head).2 ∈ toSubgroup A B (u, w.head).1 → (u, w.head).1 = y.1
<VAR>m n : ℕ<GOAL>↑m = ↑n ↔ m = n
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a b : G<VAR>m : ℤ<GOAL>a * b * b ^ m = a * b ^ (m + 1)
<VAR>x✝ : ℕ<VAR>hk : x✝ ≤ 0<GOAL>choose 0 x✝ * x✝! * (0 - x✝)! = 0!
<VAR>n k : ℕ<VAR>hk : k.succ ≤ n + 1<GOAL>(n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
<VAR>n k : ℕ<VAR>hk : k.succ ≤ n + 1<VAR>hk₁ : k.succ < n + 1<GOAL>(n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
<VAR>n k : ℕ<VAR>hk : k.succ ≤ n + 1<VAR>hk₁ : k.succ = n + 1<GOAL>(n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<GOAL>Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⇔ ⊤ = a
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty<VAR>h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty<VAR>h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t<VAR>h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty<VAR>h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t<VAR>h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t<VAR>h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty<GOAL>IsPreconnected (⋃ n ∈ t, s n)