ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<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✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<VAR>B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i => chooseBasis R (φ i)<VAR>b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) := Pi.basis fun i => B i<GOAL>Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>IsOpen (⇑h '' s) ↔ IsOpen s
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<VAR>hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<VAR>hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<VAR>hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x<VAR>hdg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>g : Filter β<VAR>i : γ → α<VAR>h : range i ∈ f<GOAL>Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>g : Filter β<VAR>i : γ → α<VAR>h : range i ∈ f<GOAL>(map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s✝ t s : Set α<GOAL>sInf s⁻¹ = (sSup s)⁻¹
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s✝ t s : Set α<GOAL>⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hT : FinMeasAdditive μ T<GOAL>FinMeasAdditive (c • μ) T
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hT : FinMeasAdditive μ T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s = ⊤<GOAL>(c • μ) s = ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hT : FinMeasAdditive μ T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s = ⊤<GOAL>c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hT : FinMeasAdditive μ T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s = ⊤<GOAL>μ s = ⊤ ∨ c = ⊤ ∧ ¬μ s = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMonoOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictMonoOn f s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J : Ideal R<GOAL>(quotQuotEquivComm I J).symm = quotQuotEquivComm J I
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J : Ideal R<GOAL>(((quotQuotEquivQuotSup I J).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup J I).symm).symm = ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup I J).symm
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<VAR>A : MeasurableEmbedding fun x => -x<GOAL>∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<VAR>A : MeasurableEmbedding fun x => -x<VAR>this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)<GOAL>∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<VAR>A : MeasurableEmbedding fun x => -x<VAR>this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)<GOAL>∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : C(X, Y)<VAR>hfs : Function.Surjective f.toFun<VAR>a b : LocallyConstant Y Z<VAR>h : comap f a = comap f b<VAR>y : Y<VAR>x : X<VAR>hx : f.toFun x = y<GOAL>a y = b y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>x✝ : Option α × Perm α<VAR>x : Option α<VAR>σ : Perm α<GOAL>(fun σ => (σ none, removeNone σ)) ((fun i => swap none i.1 * optionCongr i.2) (x, σ)) = (x, σ)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>x✝ : Option α × Perm α<VAR>x : Option α<VAR>σ : Perm α<VAR>this : removeNone (swap none x * optionCongr σ) = σ<GOAL>(fun σ => (σ none, removeNone σ)) ((fun i => swap none i.1 * optionCongr i.2) (x, σ)) = (x, σ)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<GOAL>x = y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>M' : Submodule R S<VAR>hM : M' ≤ M<VAR>hFG : Module.Finite R ↥M'<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))<GOAL>x = y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>M' : Submodule R S<VAR>hM : M' ≤ M<VAR>hFG : M'.FG<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))<GOAL>x = y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>M' : Submodule R S<VAR>hM : M' ≤ M<VAR>hFG : M'.FG<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))<VAR>x' : ↥M' ⊗[R] ↥N<VAR>hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x<VAR>y' : ↥M' ⊗[R] ↥N<VAR>hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y<GOAL>x' = y'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hc : ChainClosure r c<GOAL>IsChain r c
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>a b : α<VAR>na : ℕ<VAR>na' : α<VAR>p : IsNat ((↑n - 1) * a) na<VAR>pa : ↑na = na'<GOAL>-(a * b) = na' * b
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>a b : α<VAR>na : ℕ<VAR>na' : α<VAR>p : IsNat ((↑n - 1) * a) na<VAR>pa : ↑na = na'<GOAL>-1 * (a * b) = (↑n - 1) * a * b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y✝ : ι → ℝ<VAR>δ : ℝ<VAR>x y : ι → ℝ<GOAL>dist (x ⊓ y) (x ⊔ y) = dist x y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝¹ y✝ : ι → ℝ<VAR>δ : ℝ<VAR>x y : ι → ℝ<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>S : Set α<VAR>a b : α<GOAL>swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>S : Set α<VAR>a b : α<GOAL>(∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>S : Set α<VAR>a b : α<GOAL>(∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>a : α<VAR>l : List α<GOAL>(a :: l).inits = (map reverse (a :: l).reverse.tails).reverse
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : F<VAR>w : E<VAR>hw : ∀ (x : ↥T.domain), ⟪w, ↑x⟫_𝕜 = ⟪y, ↑T x⟫_𝕜<GOAL>y ∈ T†.domain
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : F<VAR>w : E<VAR>hw : ∀ (x : ↥T.domain), ⟪w, ↑x⟫_𝕜 = ⟪y, ↑T x⟫_𝕜<GOAL>Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : F<VAR>w : E<VAR>hw : ∀ (x : ↥T.domain), ⟪w, ↑x⟫_𝕜 = ⟪y, ↑T x⟫_𝕜<VAR>this : Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)<GOAL>⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun) = ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<VAR>hm : MeasurableSet t<VAR>h_fin : μ t ≠ ⊤<GOAL>μ (s \ t) + μ t = μ (s ∪ t)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p ≤ r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p ≤ r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hw : Wbtw ℝ p₁ p₂ p₃<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p ≤ r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hw : Wbtw ℝ p₂ p₃ p₁<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p ≤ r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hw : Wbtw ℝ p₃ p₁ p₂<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.I * (-Complex.I * (o.kahler x) y) = (o.kahler x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * b ≤ a ↔ a * b ≤ a * 1
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝¹ b✝¹ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b / min a b = mabs (a / b)
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝¹ b✝¹ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ab : a ≤ b<GOAL>max a b / min a b = mabs (a / b)
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝¹ b✝¹ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ba : b ≤ a<GOAL>max a b / min a b = mabs (a / b)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<VAR>F G : Filter X<GOAL>AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f✝ g : C(α, β)<VAR>f : C(β, γ)<VAR>g₁ g₂ : C(α, β)<VAR>hf : Injective ⇑f<VAR>h : f.comp g₁ = f.comp g₂<VAR>a : α<GOAL>f (g₁ a) = f (g₂ a)
<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>X Y : F<VAR>h : W.Nonsingular ![X, Y, 1]<GOAL>toAffine W ![X, Y, 1] = Affine.Point.some ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictAnti (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictAnti f
<VAR>m n : ℤ<GOAL>Even n.natAbs ↔ Even n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<GOAL>(∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<GOAL>(∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<GOAL>(∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<GOAL>(∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ p⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<VAR>x : α<GOAL>↑‖‖f x‖ ^ q‖₊ ^ p = ↑‖f x‖₊ ^ (p * q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q✝ : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<VAR>x : α<GOAL>ENNReal.ofReal ‖‖f x‖ ^ q‖ ^ p = ENNReal.ofReal ‖f x‖ ^ (p * q)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<GOAL>supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<GOAL>supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<GOAL>supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<GOAL>LinearMap.range ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) ≤ ⨆ i, supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<GOAL>⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<VAR>l : α →₀ M<GOAL>l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<VAR>l : α →₀ M<GOAL>0 ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>δ : Type u_7<VAR>s : δ → Set α<VAR>this : DecidablePred fun x => x ∈ ⋃ i, s i<VAR>l : α →₀ M<GOAL>∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → f ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i)) → single a b + f ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>(∃ a w, w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>h : ¬G.IsAcyclic<GOAL>∃ a w, w.IsCycle ∧ G.girth = w.length
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>h : ¬G.IsAcyclic<VAR>w✝¹ : α<VAR>w✝ : G.Walk w✝¹ w✝¹<VAR>h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length<GOAL>∃ a w, w.IsCycle ∧ G.girth = w.length