ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<VAR>dXY : (Disjoint on id) s Y<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<VAR>dXY : (Disjoint on id) s Y<VAR>dXZ : (Disjoint on id) s Z<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<VAR>dXY : (Disjoint on id) s Y<VAR>dXZ : (Disjoint on id) s Z<VAR>dYZ : (Disjoint on id) Y Z<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<VAR>dXY : (Disjoint on id) s Y<VAR>dXZ : (Disjoint on id) s Z<VAR>dYZ : (Disjoint on id) Y Z<VAR>that : 2 * (ε / 8) = ε / 4<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<VAR>dXY : (Disjoint on id) s Y<VAR>dXZ : (Disjoint on id) s Z<VAR>dYZ : (Disjoint on id) Y Z<VAR>that : 2 * (ε / 8) = ε / 4<VAR>this : 0 ≤ 1 - 2 * (ε / 8)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>this : Invertible 1<GOAL>(fromBlocks A B C 1).det = (A - B * C).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>count s = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>n : ℕ<GOAL>↑n ≤ count s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : s.Infinite<VAR>t : Finset α<VAR>ht : ↑t ⊆ s<GOAL>↑t.card ≤ count s
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : ¬((∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤)<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤<VAR>this : ↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) ≤ ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) ^ p⁻¹)<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤<VAR>this : ↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) ≤ ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹)) * ↑((∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) ^ p⁻¹)<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤<VAR>this : ∑ x ∈ s, ↑(w x * f x).toNNReal ≤ ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹)) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ≥0∞<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0∞<VAR>hp : 1 < p<VAR>hp₀ : 0 < p<VAR>hp₁ : p⁻¹ < 1<VAR>H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0<VAR>H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤<VAR>this : ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ a ∈ s, ↑(w a).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>h : f x = 2<GOAL>(preReflection x f) x = -x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>h : f x = 2<GOAL>x - (x + x) = -x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : RCLike K<VAR>z✝ : K<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<VAR>z : K<GOAL>re (OfNat.ofNat n * z) = OfNat.ofNat n * re z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<GOAL>∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<GOAL>∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<VAR>b : β<VAR>hb : (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧ ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y<GOAL>∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<VAR>b : β<VAR>hb : (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧ ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y<GOAL>∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this✝ : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<VAR>b : β<VAR>hb : (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧ ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y<VAR>p1 : α<VAR>p2 : β<VAR>hp : (p1, p2) ∈ ↑f<VAR>this : p1 ≠ a<GOAL>cmp (p1, p2).1 a = cmp (p1, p2).2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this✝ : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<VAR>b : β<VAR>hb : (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧ ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y<VAR>p1 : α<VAR>p2 : β<VAR>hp : (p1, p2) ∈ ↑f<VAR>this : p1 ≠ a<VAR>hl : p1 < a<GOAL>cmp (p1, p2).1 a = cmp (p1, p2).2 b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>f : PartialIso α β<VAR>a : α<VAR>h : ¬∃ b, (a, b) ∈ ↑f<VAR>this✝ : ∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), x < y<VAR>b : β<VAR>hb : (∀ x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.1 < a) ↑f), x < b) ∧ ∀ y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.1) ↑f), b < y<VAR>p1 : α<VAR>p2 : β<VAR>hp : (p1, p2) ∈ ↑f<VAR>this : p1 ≠ a<VAR>hr : p1 > a<GOAL>cmp (p1, p2).1 a = cmp (p1, p2).2 b
<VAR>T : Type u<VAR>inst✝¹ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<GOAL>inv sq.left ≫ f.hom ≫ sq.right = g.hom
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<GOAL>b.parallelepiped = PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (PositiveCompacts.piIcc01 ι)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>0 ≤ f' y
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : K<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : K<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : (i : ι) → AddCommMonoid (π i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (π i)<VAR>s : Set ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x₁ x₂ : π i<VAR>y : (i : ι) → π i<GOAL>update y i '' [x₁-[𝕜]x₂] = [update y i x₁-[𝕜]update y i x₂]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : (i : ι) → AddCommMonoid (π i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (π i)<VAR>s : Set ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x₁ x₂ : π i<VAR>y : (i : ι) → π i<GOAL>(fun x => update y i (x.1 • x₁ + x.2 • x₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = (fun p => p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : (i : ι) → AddCommMonoid (π i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (π i)<VAR>s : Set ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x₁ x₂ : π i<VAR>y : (i : ι) → π i<VAR>a : 𝕜 × 𝕜<VAR>ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}<GOAL>update y i (a.1 • x₁ + a.2 • x₂) = a.1 • update y i x₁ + a.2 • update y i x₂
<VAR>R✝ : Type u<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>toFinsupp✝ : R[ℕ]<GOAL>(-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>W : Type u₂<VAR>inst✝ : Quiver W<VAR>F_obj : V → W<VAR>map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)<VAR>h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X<VAR>h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝ }.map f))<GOAL>map✝¹ = map✝
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>W : Type u₂<VAR>inst✝ : Quiver W<VAR>F_obj : V → W<VAR>map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)<VAR>h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X<VAR>h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝ }.map f))<VAR>X Y : V<VAR>f : X ⟶ Y<GOAL>map✝¹ f = map✝ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>h : x < y<GOAL>∃ u v, StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>h : x < y<VAR>u : ℕ → α<VAR>hu_anti : StrictAnti u<VAR>hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y<VAR>hux : Tendsto u atTop (𝓝 x)<GOAL>∃ u v, StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>h : x < y<VAR>u : ℕ → α<VAR>hu_anti : StrictAnti u<VAR>hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y<VAR>hux : Tendsto u atTop (𝓝 x)<VAR>v : ℕ → α<VAR>hv_mono : StrictMono v<VAR>hv_mem : ∀ (n : ℕ), v n ∈ Ioo (u 0) y<VAR>hvy : Tendsto v atTop (𝓝 y)<GOAL>∃ u v, StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>M' : LieSubmodule R L M<GOAL>M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
<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>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<GOAL>ContDiff ℝ n fun x => ‖x‖ ^ 2
<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>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>x✝ : E<GOAL>‖x✝‖ ^ 2 = (⇑reCLM ∘ fun x => ⟪id x, id x⟫_𝕜) x✝
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<GOAL>p I
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : Box ι<VAR>hle : J ≤ I<VAR>hs : ∀ (s : Set ι), p (J.splitCenterBox s)<VAR>J' : Box ι<VAR>h' : J' ∈ splitCenter J<GOAL>p J'
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : Box ι<VAR>hle : J ≤ I<VAR>hs : ∀ (s : Set ι), p (J.splitCenterBox s)<VAR>s : Set ι<VAR>h' : J.splitCenterBox s ∈ splitCenter J<GOAL>p (J.splitCenterBox s)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk u w<VAR>r : G.Walk w x<GOAL>(p.reverseAux q).append r = p.reverseAux (q.append r)
<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>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>Summable fun i => ‖⟪v i, x⟫_𝕜‖ ^ 2
<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>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>HasSum (fun i => ‖⟪v i, x⟫_𝕜‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2)
<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>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>∀ (i : ι), 0 ≤ ‖⟪v i, x⟫_𝕜‖ ^ 2
<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>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>IsLUB (Set.range fun s => ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>X : C<VAR>f : T.obj₂ ⟶ X<VAR>hf : T.mor₁ ≫ f = 0<GOAL>∃ g, f = T.mor₂ ≫ g