ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0<VAR>f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this<VAR>ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re<GOAL>Tendsto (fun g => (↑g • z).re) cofinite (cocompact ℝ)
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0<VAR>f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this<VAR>ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re<VAR>e_1✝ : ↑((fun g => ↑g 1) ⁻¹' {p}) = { g // ↑g 1 = p }<VAR>g : ↑((fun g => ↑g 1) ⁻¹' {p})<GOAL>(↑g • z).re = (⇑(f.trans ff) ∘ fun g => (lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) g
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0<VAR>f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this<VAR>ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re<VAR>e_1✝ : ↑((fun g => ↑g 1) ⁻¹' {p}) = { g // ↑g 1 = p }<VAR>g : ↑((fun g => ↑g 1) ⁻¹' {p})<GOAL>(↑g • z).re = (lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁' l₂' : List α<VAR>h : (a :: l).split = (l₁', l₂')<VAR>l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<GOAL>a :: l ~ l₁' ++ l₂'
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁' l₂' : List α<VAR>h : (a :: l).split = (l₁', l₂')<VAR>l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<VAR>fst_eq✝ : a :: l₂ = l₁'<VAR>snd_eq✝ : l₁ = l₂'<GOAL>a :: l ~ l₁' ++ l₂'
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<VAR>h : (a :: l).split = (a :: l₂, l₁)<GOAL>a :: l ~ a :: l₂ ++ l₁
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α✝ : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<GOAL>↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑0
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α✝ : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<GOAL>↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = (aeval α) (minpoly F α)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α✝ : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<GOAL>↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = (aeval ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α))) (minpoly F α)
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(-(m ^ 2 - n ^ 2)).natAbs.gcd (m ^ 2 + n ^ 2).natAbs = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 0<GOAL>(n ^ 2 - m ^ 2).natAbs.gcd (n ^ 2 + m ^ 2).natAbs = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>x : α<GOAL>x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>x : α<GOAL>pred a < x ↔ a = x ∨ a < x
<VAR>f g : CircleDeg1Lift<GOAL>dist (f 0 + g 0) (f (g 0)) < 1
<VAR>f g : CircleDeg1Lift<GOAL>f 0 + g 0 - 1 < f (g 0) ∧ f (g 0) < f 0 + g 0 + 1
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<GOAL>x ^ y < x ^ z ↔ y < z
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>inst✝¹ : Finite l<VAR>inst✝ : DecidableEq m<VAR>A : Matrix l m R<VAR>B : Matrix m n R<VAR>x : M₁<GOAL>((toLin v₁ v₃) (A * B)) x = ((toLin v₂ v₃) A) (((toLin v₁ v₂) B) x)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>a : K<VAR>nth_partNum_eq : (of v).partNums.get? n = some a<GOAL>a = 1
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>a : K<VAR>nth_partNum_eq : (of v).partNums.get? n = some a<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>gp_a_eq_a_n : gp.a = a<GOAL>a = 1
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>a : K<VAR>nth_partNum_eq : (of v).partNums.get? n = some a<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>gp_a_eq_a_n : gp.a = a<VAR>this : gp.a = 1<GOAL>a = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>P.parts.Nonempty ↔ a ≠ ⊥
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<GOAL>μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>hf : AntilipschitzWith 0 f<GOAL>μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<GOAL>μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<GOAL>μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<GOAL>⨆ r, ⨆ (_ : 0 < r), ⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ⨆ i, ⨆ (_ : 0 < i), ⨅ i_1, ⨅ (_ : s ⊆ ⋃ n, i_1 n), ⨅ (_ : ∀ (n : ℕ), diam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑K ^ d * diam (i_1 i) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ⨆ i, ⨆ (_ : 0 < i), ⨅ i_1, ⨅ (_ : s ⊆ ⋃ n, i_1 n), ⨅ (_ : ∀ (n : ℕ), diam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑K ^ d * diam (i_1 i) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ⨅ i, ⨅ (_ : s ⊆ ⋃ n, i n), ⨅ (_ : ∀ (n : ℕ), diam (i n) ≤ ε / ↑K), ∑' (i_1 : ℕ), ⨆ (_ : (i i_1).Nonempty), ↑K ^ d * diam (i i_1) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<VAR>t : ℕ → Set Y<VAR>hst : s ⊆ ⋃ n, t n<VAR>htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K<GOAL>⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<VAR>t : ℕ → Set Y<VAR>htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K<VAR>hst : f ⁻¹' s ⊆ f ⁻¹' ⋃ n, t n<GOAL>⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<VAR>t : ℕ → Set Y<VAR>htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K<VAR>hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i<GOAL>⨅ t, ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<VAR>t : ℕ → Set Y<VAR>htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K<VAR>hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i<VAR>n : ℕ<GOAL>diam (f ⁻¹' t n) ≤ ε
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<VAR>h0 : K ≠ 0<VAR>hKd0 : ↑K ^ d ≠ 0<VAR>hKd : ↑K ^ d ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<VAR>t : ℕ → Set Y<VAR>htε : ∀ (n : ℕ), diam (t n) ≤ ε / ↑K<VAR>hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i<GOAL>∑' (n : ℕ), ⨆ (_ : (f ⁻¹' t n).Nonempty), diam (f ⁻¹' t n) ^ d ≤ ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * diam (t i) ^ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x₁ x₂ : α<VAR>y : β<GOAL>dist (x₁, y) (x₂, y) = dist x₁ x₂
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype β<VAR>f : α → β<VAR>inst✝ : Fintype ↑(ker f).classes<GOAL>Fintype.card ↑(ker f).classes ≤ Fintype.card β
<VAR>n a b : ℕ<VAR>t : List ℕ<GOAL>ofDigits (-1) (a :: b :: t) = (List.map (fun n => ↑n) (a :: b :: t)).alternatingSum
<VAR>n a b : ℕ<VAR>t : List ℕ<GOAL>↑a + -1 * (↑b + -1 * (List.map (fun n => ↑n) t).alternatingSum) = ↑a + -↑b + (List.map (fun n => ↑n) t).alternatingSum
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>T_gen p F a = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<GOAL>Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), a ⩿ b → f a ≤ f b<VAR>a b : α<VAR>hab : a ≤ b<GOAL>f a ≤ f b
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>φ : MvPolynomial σ R<GOAL>join₂ ((map f) φ) = (bind₂ f) φ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle (-x) y + o.oangle (-y) x = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<VAR>hp : Continuous fun y => (a.1, y)<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<VAR>hp : Continuous fun y => (a.1, y)<VAR>V : Set Y := {y | (a.1, y) ∈ W}<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<VAR>hp : Continuous fun y => (a.1, y)<VAR>V : Set Y := {y | (a.1, y) ∈ W}<VAR>hV : IsCompact V<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<VAR>hp : Continuous fun y => (a.1, y)<VAR>V : Set Y := {y | (a.1, y) ∈ W}<VAR>hV : IsCompact V<VAR>U : Set X := {x | MapsTo (Prod.mk x) V ↑W}<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompactSpace Y<VAR>W : Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<VAR>hp : Continuous fun y => (a.1, y)<VAR>V : Set Y := {y | (a.1, y) ∈ W}<VAR>hV : IsCompact V<VAR>U : Set X := {x | MapsTo (Prod.mk x) V ↑W}<VAR>hUV : U ×ˢ V ⊆ ↑W<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>n : ℕ<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : z ^ n + z ^ 2 = 0<GOAL>False
<VAR>n : ℕ<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : z ^ n + z ^ 2 = 0<VAR>h3 : z ^ 3 = 1<GOAL>False
<VAR>n : ℕ<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : z ^ n + z ^ 2 = 0<VAR>h3 : z ^ 3 = 1<VAR>key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2<GOAL>False
<VAR>n : ℕ<VAR>z : ℂ<VAR>h1 : z ^ n = z + 1<VAR>h2 : z ^ n + z ^ 2 = 0<VAR>h3 : z ^ 3 = 1<VAR>key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2<VAR>z_ne_zero : z ≠ 0<GOAL>False
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring α<VAR>inst✝² : Semiring β<VAR>inst✝¹ : Algebra R α<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>i j : n<GOAL>diagonal ((Pi.constRingHom n α) (Algebra.toRingHom r)) i j = if i = j then Algebra.toRingHom r else 0
<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>l l' : Filter α<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedAddCommGroup 𝕜<VAR>inst✝¹ : SMulZeroClass 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → E<VAR>c : 𝕜<VAR>s : Set α<VAR>sl : s ∈ l<VAR>hs : IntegrableOn f s μ<GOAL>IntegrableAtFilter (c • f) l μ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝¹ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>x x✝ : X<GOAL>x✝ ∈ thickening δ {x} ↔ x✝ ∈ ball x δ
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx : x ∈ f.domain<VAR>y : E<VAR>hy : y ∈ g.domain<VAR>hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩<GOAL>↑f ⟨x, hx⟩ = ↑g ⟨y, hy⟩
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx : x ∈ f.domain<VAR>y : E<VAR>hy : y ∈ g.domain<VAR>hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩<GOAL>(y, ↑f ⟨x, hx⟩) ∈ g.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx : x ∈ f.domain<VAR>y : E<VAR>hy : y ∈ g.domain<VAR>hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩<GOAL>(y, ↑f ⟨x, hx⟩) ∈ f.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx : x ∈ f.domain<VAR>y : E<VAR>hy : y ∈ g.domain<VAR>hxy : x = y<GOAL>(y, ↑f ⟨x, hx⟩) ∈ f.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx✝ : x ∈ f.domain<VAR>y : E<VAR>hx : y ∈ f.domain<VAR>hy : y ∈ g.domain<VAR>hxy : x = y<GOAL>(y, ↑f ⟨x, hx✝⟩) ∈ f.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<VAR>x : E<VAR>hx✝ : x ∈ f.domain<VAR>y : E<VAR>hx : y ∈ f.domain<VAR>hy : y ∈ g.domain<VAR>hxy : x = y<GOAL>↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>w✝ : Rˣ<GOAL>(fun m => m • Q) w✝ z = 0 ↔ Q z = 0
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>c c' : A →ₗ[R] CharacterModule B<VAR>x : A ⊗[R] B<GOAL>((fun c => liftAddHom c.toAddMonoidHom ⋯) (c + c')) x = ((fun c => liftAddHom c.toAddMonoidHom ⋯) c + (fun c => liftAddHom c.toAddMonoidHom ⋯) c') x
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>r : R<VAR>c : A →ₗ[R] CharacterModule B<VAR>x : A ⊗[R] B<GOAL>({ toFun := fun c => liftAddHom c.toAddMonoidHom ⋯, map_add' := ⋯ }.toFun (r • c)) 0 = ((RingHom.id R) r • { toFun := fun c => liftAddHom c.toAddMonoidHom ⋯, map_add' := ⋯ }.toFun c) 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α✝ → E<VAR>g✝ : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<GOAL>f =O[l] g ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x / g x‖