ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<VAR>hk0 : k ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<VAR>hk0 : k ≠ 0<VAR>hj2 : r ^ 2 = j ^ 4<VAR>hk2 : s ^ 2 = k ^ 4<VAR>hh : i ^ 2 = j ^ 4 + k ^ 4<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<VAR>hk0 : k ≠ 0<VAR>hj2 : r ^ 2 = j ^ 4<VAR>hk2 : s ^ 2 = k ^ 4<VAR>hh : i ^ 2 = j ^ 4 + k ^ 4<VAR>hn : n ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<VAR>hk0 : k ≠ 0<VAR>hj2 : r ^ 2 = j ^ 4<VAR>hk2 : s ^ 2 = k ^ 4<VAR>hh : i ^ 2 = j ^ 4 + k ^ 4<VAR>hn : n ≠ 0<VAR>hic : i.natAbs < c.natAbs<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : s.gcd r = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<VAR>k : ℤ<VAR>hk : s = k ^ 2 ∨ s = -k ^ 2<VAR>hk0 : k ≠ 0<VAR>hj2 : r ^ 2 = j ^ 4<VAR>hk2 : s ^ 2 = k ^ 4<VAR>hh : i ^ 2 = j ^ 4 + k ^ 4<VAR>hn : n ≠ 0<VAR>hic : i.natAbs < c.natAbs<VAR>hic' : c.natAbs ≤ i.natAbs<GOAL>False
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<GOAL>(interpolate s v) 1 = 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<GOAL>∑ x ∈ s, Lagrange.basis s v x = 1
<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 α<GOAL>μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t
<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 α<GOAL>μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)
<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>hs : μ.restrict s = ν.restrict s<VAR>ht : μ.restrict t = ν.restrict t<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>(μ.restrict (s ∪ t)) u = (ν.restrict (s ∪ t)) u
<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>hs : μ.restrict s = ν.restrict s<VAR>ht : μ.restrict t = ν.restrict t<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)
<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>hs : μ.restrict s = ν.restrict s<VAR>ht : μ.restrict t = ν.restrict t<VAR>u : Set α<VAR>hu : MeasurableSet u<VAR>US : Set α<VAR>hsub : u ∩ s ⊆ US<VAR>hm : MeasurableSet US<VAR>hμ : μ US = μ (u ∩ s)<VAR>hν : ν US = ν (u ∩ s)<GOAL>μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>P : Ideal α<VAR>hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal<VAR>J : Ideal α<VAR>hPJ : P < J<GOAL>J = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>P : Ideal α<VAR>hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal<VAR>J : Ideal α<VAR>hPJ : P < J<VAR>hnonmax : ¬J = ⊤<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>P : Ideal α<VAR>hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal<VAR>J : Ideal α<VAR>hPJ : P < J<VAR>hnonmax : ¬J = ⊤<VAR>M : Ideal α<VAR>hM1 : M.IsMaximal<VAR>hM2 : J ≤ M<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f g : α → β → σ<VAR>hg : Primrec₂ f<VAR>H : ∀ (a : α) (b : β), f a b = g a b<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f g : α → β → σ<VAR>hg : Primrec₂ f<VAR>H : ∀ (a : α) (b : β), f a b = g a b<VAR>a : α<VAR>b : β<GOAL>f a b = g a b
<VAR>x : ℂ<VAR>n : ℕ<GOAL>x ^ ↑n = x ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>H : (𝓤 α).HasBasis p s<GOAL>CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>H : (𝓤 α).HasBasis p s<VAR>h : ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i<VAR>i : γ<VAR>hi : p i<GOAL>∃ N, ∀ n ≥ N, (u n, u N) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>H : (𝓤 α).HasBasis p s<VAR>h : ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i<VAR>i : γ<VAR>hi : p i<GOAL>∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiable I' I'' g<VAR>hf : MDifferentiable I I' f<VAR>p : TangentBundle I M<GOAL>tangentMap I I'' (g ∘ f) p = (tangentMap I' I'' g ∘ tangentMap I I' f) p
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<GOAL>(∀ (i' : ℝ), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | dist p.1 p.2 < i} ⊆ {p | dist p.1 p.2 < i'}) ↔ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>(∃ j, G.moveRight j ≈ 0) ↔ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>hn : G ‖ 0<GOAL>∃ j, G.moveRight j ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>hn : ∃ j, G.moveRight j ≤ 0<GOAL>∃ j, G.moveRight j ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>i : G.RightMoves<VAR>hi : G.moveRight i ≤ 0<GOAL>∃ j, G.moveRight j ≈ 0
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q✝ : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<VAR>q : ℚ<GOAL>↑|q| = |↑q|
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>μ ({x} + r • s) / μ ({y} + r • t) = ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s * (ENNReal.ofReal (|r| ^ finrank ℝ E) * μ t)⁻¹
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s * (ENNReal.ofReal (|r| ^ finrank ℝ E) * μ t)⁻¹ = ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ * (μ s * (μ t)⁻¹)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s * ((ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ * (μ t)⁻¹) = ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ * (μ s * (μ t)⁻¹)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0 ∨ μ t ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ⊤ ∨ μ t ≠ 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ * (μ s * (μ t)⁻¹) = μ s / μ t
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x y : E<VAR>s t : Set E<GOAL>ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ⊤
<VAR>n : ℕ<GOAL>harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹
<VAR>n : ℕ<GOAL>∑ x ∈ Finset.Ico (0 + 1) (n + 1), (↑x)⁻¹ = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<GOAL>MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<GOAL>MeasureTheory.SignedMeasure.ExistsOneDivLT s i (Nat.find ⋯)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℤ<GOAL>(1 / A) ^ n = 1 / A ^ n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f : X → ℝ<VAR>s✝ s : Set X<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hfi : Integrable f μ<GOAL>∫ (x : X) in {y | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f : X → ℝ<VAR>s✝ s : Set X<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hfi : Integrable f μ<GOAL>∫ (x : X), {a | f a ≤ 0}.indicator f x ∂μ ≤ ∫ (x : X), s.indicator f x ∂μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in atTop, Disjoint (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<GOAL>∀ᶠ (n : ℕ) in atTop, Disjoint (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>ker (f ^ m) ⊓ range (f ^ m) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>∀ x ∈ ker (f ^ n) ⊓ range (f ^ m), x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>x : M<VAR>hx : (f ^ m) x ∈ ↑(ker (f ^ n))<GOAL>(f ^ m) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>x : M<VAR>hx : (f ^ m) x ∈ ↑(ker (f ^ n))<GOAL>(f ^ n) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>x : M<VAR>hx : x ∈ ker (f ^ (n + m))<GOAL>(f ^ n) x = 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>x✝ : A ⊗[R] M<VAR>x : A<VAR>y : M<GOAL>(basisAux A b) (a • x ⊗ₜ[R] y) = a • (basisAux A b) (x ⊗ₜ[R] y)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<GOAL>Continuous fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<GOAL>∀ (x : X × ℝ), ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) x