ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<GOAL>(single (h k) x) (h i) = (single k x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>i : κ<VAR>x : β (h i)<GOAL>(single (h i) x) (h i) = (single i x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<VAR>hik : i ≠ k<GOAL>(single (h k) x) (h i) = (single k x) i
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>J : LieIdeal R L<VAR>k l : ℕ<GOAL>D (k + l) (I + J) ≤ D k I + D l J
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>J : LieIdeal R L<VAR>k l : ℕ<VAR>D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }<GOAL>D (k + l) (I + J) ≤ D k I + D l J
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>J : LieIdeal R L<VAR>k l : ℕ<VAR>D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }<VAR>h₁ : ∀ (I J : LieIdeal R L), D₁ (I ⊔ J) ≤ D₁ I ⊔ J<GOAL>D (k + l) (I + J) ≤ D k I + D l J
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>J : LieIdeal R L<VAR>k l : ℕ<VAR>D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I => ⁅I, I⁆, monotone' := ⋯ }<VAR>h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (⇑D₁)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑D₁)^[n₁] a₁ ⊔ (⇑D₁)^[n₂] a₂<GOAL>D (k + l) (I + J) ≤ D k I + D l J
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁴ : SMul M X<VAR>inst✝³ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝² : SMul N Y<VAR>inst✝¹ : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝ : SMul P Z<VAR>f : X →ₑ[φ] Y<VAR>x : X<GOAL>(f.comp (MulActionHom.id M)) x = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>IsClosed (coborder s ↓∩ s)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(mulEquivOfQuotient f) (mk x y) = f.mk' x y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g✝ : G<VAR>H K : Subgroup G<VAR>g : G<GOAL>∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g✝ : G<VAR>H K : Subgroup G<VAR>g : G<VAR>this : mk H K (Quotient.out' (mk H K g)) = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out' (mk H K g) * k<GOAL>∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g✝ : G<VAR>H K : Subgroup G<VAR>g : G<VAR>this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out' (mk H K g) * k<GOAL>∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g✝ : G<VAR>H K : Subgroup G<VAR>g : G<VAR>this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out' (mk H K g) * k<VAR>h : G<VAR>h_h : h ∈ H<VAR>k : G<VAR>hk : k ∈ K<VAR>T : g = h * Quotient.out' (mk H K g) * k<GOAL>∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g✝ : G<VAR>H K : Subgroup G<VAR>g : G<VAR>this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out' (mk H K g) * k<VAR>h : G<VAR>h_h : h ∈ H<VAR>k : G<VAR>hk : k ∈ K<VAR>T : g = h * Quotient.out' (mk H K g) * k<GOAL>h * (Quotient.out' (mk H K g) * k) = g
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i j : I<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (β a)<VAR>inst✝ : (a : α) → (b : β a) → One (γ a b)<VAR>a : α<VAR>b : β a<VAR>x : γ a b<GOAL>uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>this : CompleteSpace ↑s<GOAL>∃ y ∈ s, IsFixedPt f y ∧ Tendsto (fun n => f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>this : CompleteSpace ↑s<VAR>y : ↑s<VAR>hfy : IsFixedPt (MapsTo.restrict f s s hsf) y<VAR>h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)<VAR>hle : ∀ (n : ℕ), edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤ edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)<GOAL>∃ y ∈ s, IsFixedPt f y ∧ Tendsto (fun n => f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>this : CompleteSpace ↑s<VAR>y : ↑s<VAR>hfy : IsFixedPt (MapsTo.restrict f s s hsf) y<VAR>h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)<VAR>hle : ∀ (n : ℕ), edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤ edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)<GOAL>Tendsto (fun n => f^[n] x) atTop (𝓝 ↑y)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hf : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>this : CompleteSpace ↑s<VAR>y : ↑s<VAR>hfy : IsFixedPt (MapsTo.restrict f s s hsf) y<VAR>h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)<VAR>hle : ∀ (n : ℕ), edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤ edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)<VAR>n : ℕ<GOAL>edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → α<VAR>h : MapsTo f s s<VAR>x : ↑s<VAR>k : ℕ<VAR>ih : ↑((restrict f s s h)^[k] x) = f^[k] ↑x<GOAL>↑((restrict f s s h)^[k + 1] x) = f^[k + 1] ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ℕ → α<GOAL>⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ℕ → α<GOAL>⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ {i | 0 < i}, f b
<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 '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (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>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ∈ Iic n<VAR>y : α<VAR>hy : y ∈ Iic n<VAR>hxy : x < y<GOAL>ψ x < ψ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ∈ Iic n<VAR>i : ℕ<VAR>hy : succ^[i] x ∈ Iic n<VAR>hxy : x < succ^[i] x<GOAL>ψ x < ψ (succ^[i] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ∈ Iic n<VAR>k : ℕ<VAR>ih : succ^[k + 1] x ∈ Iic n → x < succ^[k + 1] x → ψ x < ψ (succ^[k + 1] x)<VAR>hy : succ^[k + 1 + 1] x ∈ Iic n<VAR>hxy : x < succ^[k + 1 + 1] x<GOAL>ψ x < ψ (succ^[k + 1 + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ^[k + 1] x ≤ n → x < succ^[k + 1] x → ψ x < ψ (succ^[k + 1] x)<VAR>hy : succ^[k + 1 + 1] x ≤ n<VAR>hxy : x < succ^[k + 1 + 1] x<GOAL>ψ x < ψ (succ^[k + 1 + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))<VAR>hxy : x < succ (succ (succ^[k] x))<VAR>hy : succ (succ (succ^[k] x)) ≤ n<GOAL>ψ x < ψ (succ (succ (succ^[k] x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))<VAR>hxy : x < succ (succ (succ^[k] x))<VAR>hy : succ (succ (succ^[k] x)) ≤ n<VAR>hmax : ¬IsMax (succ^[k] x)<VAR>hmax' : ¬IsMax (succ (succ^[k] x))<GOAL>ψ x < ψ (succ (succ (succ^[k] x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))<VAR>hxy : x < succ (succ (succ^[k] x))<VAR>hy : succ (succ (succ^[k] x)) ≤ n<VAR>hmax : ¬IsMax (succ^[k] x)<VAR>hmax' : ¬IsMax (succ (succ^[k] x))<GOAL>ψ (succ (succ^[k] x)) < ψ (succ (succ (succ^[k] x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))<VAR>hxy : x < succ (succ (succ^[k] x))<VAR>hy : succ (succ (succ^[k] x)) ≤ n<VAR>hmax : ¬IsMax (succ^[k] x)<VAR>hmax' : ¬IsMax (succ (succ^[k] x))<GOAL>ψ (succ^[k.succ] x) < ψ (succ (succ^[k.succ] x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : Preorder β<VAR>ψ : α → β<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (succ m)<VAR>x : α<VAR>hx : x ≤ n<VAR>k : ℕ<VAR>ih : succ (succ^[k] x) ≤ n → x < succ (succ^[k] x) → ψ x < ψ (succ (succ^[k] x))<VAR>hxy : x < succ (succ (succ^[k] x))<VAR>hy : succ (succ (succ^[k] x)) ≤ n<VAR>hmax : ¬IsMax (succ^[k] x)<VAR>hmax' : ¬IsMax (succ (succ^[k] x))<GOAL>succ^[k.succ] x < succ (succ (succ^[k] x))
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m x : (i : ι) → E i<GOAL>‖(f + g) x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f g : α → δ<VAR>s : Set α<VAR>hfg : f =ᶠ[ae μ] g<GOAL>f =ᶠ[ae (μ.restrict s)] g
<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>f g : α → δ<VAR>s : Set α<VAR>hfg : f =ᶠ[ae μ] g<GOAL>ae (μ.restrict s) ≤ ae μ
<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>f g : α → δ<VAR>s : Set α<VAR>hfg : f =ᶠ[ae μ] g<GOAL>μ.restrict s ≪ μ
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.rotateL x r).dual = r.dual.rotateR x l.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<GOAL>(if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).dual = if l✝.size < ratio * r✝.size then r✝.dual.node3R x✝ l✝.dual x l.dual else r✝.dual.node4R x✝ l✝.dual x l.dual
<VAR>n m : ℕ<GOAL>(range' n (m - n)).Nodup
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<GOAL>(↑n).toReal = ↑n
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
<VAR>α : Type u_1<VAR>a b : PosNum<VAR>this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)<GOAL>Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
<VAR>α : Type u_1<VAR>a b : PosNum<VAR>this : Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b)<GOAL>Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ
<VAR>s x y : ℝ<VAR>hx₀ : 0 < x<VAR>hx₁ : x < 1 / (1 + s ^ 2)<VAR>hy : |y| < s * x<GOAL>√(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))
<VAR>s x y : ℝ<VAR>hx₀ : 0 < x<VAR>hx₁ : x < 1 / (1 + s ^ 2)<VAR>hy : |y| < s * x<VAR>H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2<GOAL>√(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<GOAL>(if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<GOAL>(∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1<GOAL>mk l₁ = mk l₂
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1<VAR>h : l₁.length ≤ l₂.length<GOAL>mk l₁ = mk l₂
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1<VAR>h : l₁.length ≤ l₂.length<GOAL>l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default
<VAR>Γ : Type u_1<VAR>i : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1<VAR>h : l₁.length ≤ l₂.length<GOAL>l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
<VAR>Γ : Type u_1<VAR>i✝ : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i : ℕ), (mk l₁).nth i = (mk l₂).nth i<VAR>h✝ : l₁.length ≤ l₂.length<VAR>i : ℕ<VAR>h : i < l₂.length<VAR>h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length<GOAL>(l₁ ++ List.replicate (l₂.length - l₁.length) default).get ⟨i, h₂⟩ = l₂.get ⟨i, h⟩
<VAR>Γ : Type u_1<VAR>i✝ : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i : ℕ), l₁.getI i = l₂.getI i<VAR>h✝ : l₁.length ≤ l₂.length<VAR>i : ℕ<VAR>h : i < l₂.length<VAR>h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length<GOAL>(l₁ ++ List.replicate (l₂.length - l₁.length) default).get ⟨i, h₂⟩ = l₂.get ⟨i, h⟩
<VAR>Γ : Type u_1<VAR>i✝ : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i : ℕ), l₁.getI i = l₂.getI i<VAR>h✝ : l₁.length ≤ l₂.length<VAR>i : ℕ<VAR>h : i < l₂.length<VAR>h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length<VAR>h' : i < l₁.length<GOAL>(l₁ ++ List.replicate (l₂.length - l₁.length) default).get ⟨i, h₂⟩ = l₂.get ⟨i, h⟩
<VAR>Γ : Type u_1<VAR>i✝ : Inhabited Γ<VAR>L₁ L₂ : ListBlank Γ<VAR>l₁ l₂ : List Γ<VAR>H : ∀ (i : ℕ), l₁.getI i = l₂.getI i<VAR>h✝ : l₁.length ≤ l₂.length<VAR>i : ℕ<VAR>h : i < l₂.length<VAR>h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length<VAR>h' : l₁.length ≤ i<GOAL>(l₁ ++ List.replicate (l₂.length - l₁.length) default).get ⟨i, h₂⟩ = l₂.get ⟨i, h⟩
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.boundaries.orderEmbOfFin ⋯ = c.boundary
<VAR>n : ℕ<VAR>c : Composition n<GOAL>∀ (x : Fin (c.length + 1)), c.boundary x ∈ c.boundaries
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>h₁' : x' < y' → P<VAR>h₂' : x' = y' → P<VAR>h₃' : y' < x' → P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : ∀ (h : x' < y'), h₁ ⋯ = h₁' h<VAR>hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h<VAR>hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h<GOAL>ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>h₁' : x' < y' → P<VAR>h₂' : x' = y' → P<VAR>h₃' : y' < x' → P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : ∀ (h : x' < y'), h₁ ⋯ = h₁' h<VAR>hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h<VAR>hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h<VAR>h : x < y<GOAL>h₁ h = ltByCases x' y' h₁' h₂' h₃'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>h₁' : x' < y' → P<VAR>h₂' : x' = y' → P<VAR>h₃' : y' < x' → P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : ∀ (h : x' < y'), h₁ ⋯ = h₁' h<VAR>hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h<VAR>hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h<VAR>h : x = y<GOAL>h₂ h = ltByCases x' y' h₁' h₂' h₃'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>h₁' : x' < y' → P<VAR>h₂' : x' = y' → P<VAR>h₃' : y' < x' → P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : ∀ (h : x' < y'), h₁ ⋯ = h₁' h<VAR>hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h<VAR>hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h<VAR>h : y < x<GOAL>h₃ h = ltByCases x' y' h₁' h₂' h₃'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X : J<VAR>tX : IsInitial X<VAR>F : J ⥤ C<VAR>j j' : J<VAR>k : j ⟶ j'<GOAL>𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z w : K<GOAL>normSq (z + w) = normSq z + normSq w + 2 * re (z * (starRingEnd K) w)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z w : K<GOAL>(re z + re w) * (re z + re w) + (im z + im w) * (im z + im w) = re z * re z + im z * im z + (re w * re w + im w * im w) + 2 * (re z * re w - im z * -im w)
<VAR>s n : Nat<VAR>step : optParam Nat 1<GOAL>range' s n step = range'TR s n step
<VAR>s✝ n✝ : Nat<VAR>step : optParam Nat 1<VAR>s n m : Nat<GOAL>range'TR.go step n (s + step * (n + 1) - step) ((s + step * (n + 1) - step) :: range' (s + step * (n + 1)) m step) = range' s (n + 1 + m) step
<VAR>s✝ n✝ : Nat<VAR>step : optParam Nat 1<VAR>s n m : Nat<GOAL>range'TR.go step n (s + step * n) ((s + step * n) :: range' (s + step * n + step) m step) = range' s (n + m + 1) step
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hI : M.Indep I<GOAL>M ↾ I = freeOn I