ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>s : Set E<VAR>inst✝ : SeparableSpace ↑s<VAR>hs : range f ∪ {0} ⊆ s<GOAL>∀ᵐ (x : α) ∂μ, f x ∈ closure s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N : L.Substructure M<VAR>h : N.FG<GOAL>N.CG
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>hf : s.Finite<VAR>h : ((closure L).toFun s).FG<GOAL>((closure L).toFun s).CG
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<GOAL>(last n).insertNth x p = snoc (fun j => _root_.cast ⋯ (p j)) x
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<GOAL>p = (last n).removeNth (snoc (fun j => _root_.cast ⋯ (p j)) x)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<VAR>j : Fin n<GOAL>p j = (last n).removeNth (snoc (fun j => _root_.cast ⋯ (p j)) x) j
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<VAR>j : Fin n<GOAL>HEq (p j) ((last n).removeNth (snoc (fun j => _root_.cast ⋯ (p j)) x) j)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<VAR>j : Fin n<GOAL>HEq (p j) (snoc (fun j => _root_.cast ⋯ (p j)) x j.castSucc)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α (last n)<VAR>p : (j : Fin n) → α ((last n).succAbove j)<VAR>j : Fin n<GOAL>HEq (snoc (fun j => _root_.cast ⋯ (p j)) x j.castSucc) ((last n).removeNth (snoc (fun j => _root_.cast ⋯ (p j)) x) j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : NormedRing E<VAR>inst✝² : StarRing E<VAR>inst✝¹ : CstarRing E<VAR>inst✝ : Nontrivial E<GOAL>‖1‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : NormedRing E<VAR>inst✝² : StarRing E<VAR>inst✝¹ : CstarRing E<VAR>inst✝ : Nontrivial E<VAR>this : 0 < ‖1‖<GOAL>‖1‖ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<GOAL>μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<GOAL>⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>A : Set α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>r : ℝ≥0∞<VAR>hr : μ A < r<GOAL>⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U < r
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>s : (i : κ) → κ' i → HomogeneousIdeal 𝒜<GOAL>(⨅ i, ⨅ j, s i j).toIdeal = ⨅ i, ⨅ j, (s i j).toIdeal
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<GOAL>(stdBasisMatrix i i c).trace = c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp F 2 μ)<GOAL>eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp F 2 μ)<VAR>h_two : ENNReal.ofReal 2 = 2<GOAL>eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp F 2 μ)<VAR>h_two : ENNReal.ofReal 2 = 2<GOAL>eLpNorm (↑↑f) 2 μ ^ 2 < ⊤
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>_hn : n ≠ 0<VAR>hmn : m.Coprime n<GOAL>1 (m * n) = 1 m * 1 n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>n : ℕ<VAR>_hn : n ≠ 0<VAR>hm : 1 ≠ 0<VAR>hmn : Coprime 1 n<GOAL>1 (1 * n) = 1 1 * 1 n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>_hn : n ≠ 0<VAR>hmn : m.Coprime n<VAR>hm' : m ≠ 1<GOAL>1 (m * n) = 1 m * 1 n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>_hn : n ≠ 0<VAR>hmn : m.Coprime n<VAR>hm' : m ≠ 1<GOAL>m * n ≠ 1
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>_hn : n ≠ 0<VAR>hmn : m.Coprime n<VAR>hm' : m ≠ 1<GOAL>¬m = 1 ∨ ¬n = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K 1 < volume (convexBodyLT' K f w₀)<GOAL>∃ a, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧ |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K 1 < volume (convexBodyLT' K f w₀)<VAR>w✝ : K<VAR>h_mem : w✝ ∈ ↑1<VAR>h_nz : w✝ ≠ 0<VAR>h_bd : (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w w✝ < ↑(f w)) ∧ |((↑w₀).embedding w✝).re| < 1 ∧ |((↑w₀).embedding w✝).im| < ↑(f ↑w₀) ^ 2<GOAL>∃ a, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧ |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K 1 < volume (convexBodyLT' K f w₀)<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_bd : (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ((algebraMap (𝓞 K) K) a) < ↑(f w)) ∧ |((↑w₀).embedding ((algebraMap (𝓞 K) K) a)).re| < 1 ∧ |((↑w₀).embedding ((algebraMap (𝓞 K) K) a)).im| < ↑(f ↑w₀) ^ 2<GOAL>∃ a, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧ |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame < b.toPGame → a < b
<VAR>a b : Ordinal.{u_1}<GOAL>¬a < b → ¬a.toPGame < b.toPGame
<VAR>a b : Ordinal.{u_1}<GOAL>b ≤ a → ¬a.toPGame < b.toPGame
<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✝¹ : NonUnitalSemiring α<VAR>inst✝ : Fintype n<VAR>A B C : Matrix n n α<VAR>i j : n<GOAL>(A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
<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✝¹ : NonUnitalSemiring α<VAR>inst✝ : Fintype n<VAR>A B C : Matrix n n α<VAR>i j : n<GOAL>(A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
<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✝¹ : NonUnitalSemiring α<VAR>inst✝ : Fintype n<VAR>A B C : Matrix n n α<VAR>i j : n<GOAL>∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(lift G f P g Hg)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<VAR>h✝ : IsEmpty ι<GOAL>Function.Injective ⇑(lift G f P g Hg)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<VAR>h✝ : Nonempty ι<GOAL>Function.Injective ⇑(lift G f P g Hg)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<GOAL>∀ (a : DirectLimit G f), (lift G f P g Hg) a = 0 → a = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<VAR>z : DirectLimit G f<VAR>hz : (lift G f P g Hg) z = 0<GOAL>z = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g✝ : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (lift G f P g✝ Hg) ((of G f i✝) g) = 0<GOAL>(of G f i✝) g = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g✝ : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>h✝ : Nonempty ι<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (g✝ i✝) g = 0<GOAL>(of G f i✝) g = 0
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝¹ : X → ↑F X<VAR>xs : Path F<VAR>a a' : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a'<VAR>f✝ : F.B a' → F.M<VAR>a✝ : IsPath xs (f✝ i)<VAR>h : M.mk ⟨a, f⟩ = M.mk ⟨a', f✝⟩<GOAL>a = a'
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>xs : Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<VAR>a✝ : IsPath xs (f i)<VAR>h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩<GOAL>a = a
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>{ length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun (↑↑(Fin.natAdd p.length i) + 1) = q.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>Fin.append p.toFun q.toFun (Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = q.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>Fin.cast ⋯ (↑(p.length + ↑i) + 1) = Fin.natAdd (p.length + 1) i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>↑(Fin.cast ⋯ (↑(p.length + ↑i) + 1)) = ↑(Fin.natAdd (p.length + 1) i)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>↑(↑(p.length + ↑i) + 1) = p.length + 1 + ↑i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>↑(↑(p.length + ↑i) + 1) = p.length + ↑i + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>((p.length + ↑i) % (p.length + q.length + 1 + 1) + 1 % ({ length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.length + 1)) % (p.length + q.length + 1 + 1) = p.length + ↑i + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>p.length + ↑i + 1 < (p.length + q.length + 1).succ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>-(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>h : ∀ (w : M), ∃ c, c • v = w<GOAL>finrank R M ≤ 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>h : ∀ (w : M), ∃ c, c • v = w<VAR>this : Nontrivial R<GOAL>finrank R M ≤ 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>this : Nontrivial R<VAR>h : ∀ (w : M), ∃ c, c • 0 = w<GOAL>finrank R M ≤ 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>h : ∀ (w : M), ∃ c, c • v = w<VAR>this : Nontrivial R<VAR>hn : v ≠ 0<GOAL>finrank R M ≤ 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → Zero (β i)<VAR>inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝¹ : CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>h : (i : ι) → β i → γ<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((subtypeDomain p v).prod fun i b => h (↑i) b) = v.prod h
<VAR>n m n✝ : ℕ<VAR>a b : Fin (n✝ + 1 + 1)<VAR>h : a < b<GOAL>∃ k < b, k + 1 ≤ b ∧ b = a + k + 1
<VAR>n m n✝ : ℕ<VAR>a b : Fin (n✝ + 1 + 1)<VAR>h : a < b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k + 1<GOAL>∃ k < b, k + 1 ≤ b ∧ b = a + k + 1
<VAR>n m n✝ : ℕ<VAR>a b : Fin (n✝ + 1 + 1)<VAR>h : a < b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k + 1<VAR>hkb : k < ↑b<GOAL>∃ k < b, k + 1 ≤ b ∧ b = a + k + 1
<VAR>n m n✝ : ℕ<VAR>a b : Fin (n✝ + 1 + 1)<VAR>h : a < b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k + 1<VAR>hkb : k < ↑b<GOAL>⟨k, ⋯⟩ + 1 ≤ b
<VAR>n m n✝ : ℕ<VAR>a b : Fin (n✝ + 1 + 1)<VAR>h : a < b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k + 1<VAR>hkb : k < ↑b<GOAL>b = a + ⟨k, ⋯⟩ + 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.104131, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p : ℤ<GOAL>(δ (-1) 0 (inl φ)).v p p ⋯ = (Cochain.ofHom (φ ≫ inr φ)).v p p ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>hf : Injective f<VAR>x y z : α<GOAL>f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>hf : Injective f<VAR>x y z : α<GOAL>f ((Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
<GOAL>Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>κ.restrict hs ⊗ₖ η = (κ ⊗ₖ η).restrict ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>κ.restrict hs ⊗ₖ η = κ.restrict ?hs ⊗ₖ η.restrict ?ht
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet Set.univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
<VAR>p : ℕ → Bool<VAR>m : ℕ<VAR>pm : p m = true<VAR>this : true ∈ ↑p m<VAR>n : ℕ<VAR>hn : n ∈ rfind ↑p<VAR>h : m < n<GOAL>False
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i j : α<VAR>x : γ<GOAL>update f (inl i) x (inl j) = update (f ∘ inl) i x j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : UniformSpace X<VAR>s : Set X<VAR>h : ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)<VAR>V : Set (X × X)<VAR>V_in : V ∈ 𝓤 X<GOAL>∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : UniformSpace X<VAR>s : Set X<VAR>V : Set (X × X)<VAR>V_in : V ∈ 𝓤 X<VAR>h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}<GOAL>∃ x, (∀ (n : ℕ), x n ∈ s) ∧ ∀ a ∈ s, ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : UniformSpace X<VAR>s : Set X<VAR>V : Set (X × X)<VAR>V_in : V ∈ 𝓤 X<VAR>h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}<VAR>u : ℕ → X<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V<GOAL>∃ x, (∀ (n : ℕ), x n ∈ s) ∧ ∀ a ∈ s, ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : UniformSpace X<VAR>s : Set X<VAR>V : Set (X × X)<VAR>V_in : V ∈ 𝓤 X<VAR>h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}<VAR>u : ℕ → X<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V<VAR>x : X<VAR>x✝ : x ∈ s<VAR>φ : ℕ → ℕ<VAR>hφ : StrictMono φ<VAR>huφ : Tendsto (u ∘ φ) atTop (𝓝 x)<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : UniformSpace X<VAR>s : Set X<VAR>V : Set (X × X)<VAR>V_in : V ∈ 𝓤 X<VAR>h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}<VAR>u : ℕ → X<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V<VAR>x : X<VAR>x✝ : x ∈ s<VAR>φ : ℕ → ℕ<VAR>hφ : StrictMono φ<VAR>huφ : Tendsto (u ∘ φ) atTop (𝓝 x)<VAR>N : ℕ<VAR>hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V<GOAL>False
<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' : δ<VAR>h : s.Nonempty<GOAL>image2 (fun x y => y) s t = t
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R<VAR>i : σ<GOAL>(pderiv i) (C a * f) = C a * (pderiv i) f
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>i j : ι<VAR>hij : i < j<GOAL>succFn i ≤ j
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>i j : ι<VAR>hij : i < j<VAR>h : IsGLB (Set.Ioi i) (succFn i)<GOAL>succFn i ≤ j
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>i j : ι<VAR>hij : i < j<VAR>h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))<GOAL>succFn i ≤ j