ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>↑(cs.length (w₁ * w₂)) = ↑(cs.length w₁) + ↑(cs.length w₂)
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>denom 0 = 1
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<VAR>this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atBot<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : AddAction Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>b : Γ'<GOAL>((of R).symm ((x * y) • z)).coeff b = ((of R).symm (x • y • z)).coeff b
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : AddAction Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>b : Γ'<GOAL>∑ ij ∈ VAddAntidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 • ((of R).symm z).coeff ij.2 = ∑ ij ∈ VAddAntidiagonal ⋯ ⋯ b, x.coeff ij.1 • ((of R).symm (y • z)).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : AddAction Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>b : Γ'<GOAL>∑ x_1 ∈ (VAddAntidiagonal ⋯ ⋯ b).sigma fun a => addAntidiagonal ⋯ ⋯ a.1, (x.coeff x_1.snd.1 * y.coeff x_1.snd.2) • ((of R).symm z).coeff x_1.fst.2 = ∑ x_1 ∈ (VAddAntidiagonal ⋯ ⋯ b).sigma fun a => VAddAntidiagonal ⋯ ⋯ a.2, x.coeff x_1.fst.1 • y.coeff x_1.snd.1 • ((of R).symm z).coeff x_1.snd.2
<VAR>𝕜 : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜 F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜 F'<VAR>inst✝⁴ : CompleteSpace 𝕜<VAR>α : Type u_1<VAR>inst✝³ : PseudoMetricSpace α<VAR>E' : Type u_2<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<VAR>s : Set α<VAR>f : α → E'<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')<VAR>A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv<GOAL>∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
<VAR>𝕜 : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜 F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜 F'<VAR>inst✝⁴ : CompleteSpace 𝕜<VAR>α : Type u_1<VAR>inst✝³ : PseudoMetricSpace α<VAR>E' : Type u_2<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<VAR>s : Set α<VAR>f : α → E'<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')<VAR>A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv<VAR>LA : LipschitzWith ‖↑A‖₊ ⇑A<GOAL>∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
<VAR>𝕜 : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜 F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜 F'<VAR>inst✝⁴ : CompleteSpace 𝕜<VAR>α : Type u_1<VAR>inst✝³ : PseudoMetricSpace α<VAR>E' : Type u_2<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<VAR>s : Set α<VAR>f : α → E'<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')<VAR>A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv<VAR>LA : LipschitzWith ‖↑A‖₊ ⇑A<VAR>L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s<GOAL>∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
<VAR>𝕜 : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜 F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜 F'<VAR>inst✝⁴ : CompleteSpace 𝕜<VAR>α : Type u_1<VAR>inst✝³ : PseudoMetricSpace α<VAR>E' : Type u_2<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<VAR>s : Set α<VAR>f : α → E'<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')<VAR>A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv<VAR>LA : LipschitzWith ‖↑A‖₊ ⇑A<VAR>L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s<VAR>g : α → ι → ℝ<VAR>hg : LipschitzWith (‖↑A‖₊ * K) g<VAR>gs : EqOn (⇑A ∘ f) g s<GOAL>∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>(rename g) (eval₂ C (X ∘ f) p) = (rename (g ∘ f)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) = (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)).comp C) (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p = (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>eval₂ ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) (fun x => X (g (f x))) p = (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g (f x))) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<GOAL>(eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C = algebraMap R (MvPolynomial α R)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>g : τ → α<VAR>p : MvPolynomial σ R<VAR>x✝ : R<GOAL>((eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)).comp C) x✝ = (algebraMap R (MvPolynomial α R)) x✝
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<GOAL>l = ⟨term I ho :: ↑l.Tail, hlc⟩
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<GOAL>l = ⟨↑l, ⋯⟩
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(singleObjHomologySelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom = ((single C c j).obj A).homologyι j
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ (variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Nonsingular 0 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>(variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧ (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔ (variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.a₆ = 0 ∧ (1 ^ 3 * (W.a₃ + { u := 1, r := x, s := 0, t := y }.r * W.a₁ + 2 * { u := 1, r := x, s := 0, t := y }.t) ≠ 0 ∨ 1 ^ 4 * (W.a₄ - { u := 1, r := x, s := 0, t := y }.s * W.a₃ + 2 * { u := 1, r := x, s := 0, t := y }.r * W.a₂ - ({ u := 1, r := x, s := 0, t := y }.t + { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.s) * W.a₁ + 3 * { u := 1, r := x, s := 0, t := y }.r ^ 2 - 2 * { u := 1, r := x, s := 0, t := y }.s * { u := 1, r := x, s := 0, t := y }.t) ≠ 0)
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>F' : MonoFactorisation f<VAR>x : ↑(image f)<GOAL>(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) ⋯) = (ι f) x
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>F' : MonoFactorisation f<VAR>x : ↑(image f)<GOAL>↑x = (ι f) x
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>u : Mˣ<VAR>n : ℕ<GOAL>↑(u ^ ↑n) = ↑u ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>u : Mˣ<VAR>k : ℕ<GOAL>↑(u ^ -[k+1]) = ↑u ^ -[k+1]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : SetLike S R<VAR>hSR : NonUnitalSubsemiringClass S R<VAR>s : S<GOAL>(unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : SetLike S R<VAR>hSR : NonUnitalSubsemiringClass S R<VAR>s : S<VAR>this : SMulMemClass S ℕ R<GOAL>(unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ κ : Kernel α β<VAR>h : IsSFiniteKernel κ<VAR>a : α<GOAL>(Measure.sum fun n => (κ.seq n) a) = κ a
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsClosed (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsOpen (⋃ i_1, s i_1 \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i j : ι<GOAL>IsOpen (s j \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsOpen (s i \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i j : ι<VAR>h_ne : i ≠ j<GOAL>IsOpen (s j \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f✝ : Perm α<VAR>inst✝ : DecidablePred p<VAR>a : α<VAR>f : Perm (Subtype p)<VAR>x : α<VAR>h : p x<GOAL>p x ↔ p ((ofSubtype f) x)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f✝ : Perm α<VAR>inst✝ : DecidablePred p<VAR>a : α<VAR>f : Perm (Subtype p)<VAR>x : α<VAR>h : ¬p x<GOAL>p x ↔ p ((ofSubtype f) x)
<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>inst✝ : AffineSpace V P<VAR>s₁ s₂ : Set P<GOAL>affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
<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>inst✝ : AffineSpace V P<VAR>s₁ s₂ : Set P<GOAL>affineSpan k s₁ ∥ affineSpan k s₂ ↔ (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Icc ↑a ↑b)<GOAL>∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x ∈ Finset.Ico a b, -f ↑x
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<GOAL>F.map ((exp.coev A).app B) ≫ (expComparison F A).app (A ⨯ B) = (exp.coev (F.obj A)).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<VAR>e_1✝ : (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) = (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))<VAR>e_4✝ : (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))<VAR>e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))<VAR>e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))<VAR>e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)<GOAL>inv (prodComparison F A B) = (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<VAR>e_1✝ : (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) = (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))<VAR>e_4✝ : (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))<VAR>e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))<VAR>e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))<VAR>e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)<GOAL>prodComparison F A B ≫ (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B) = 𝟙 (F.obj (A ⨯ B))
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>x : List α<GOAL>x ∈ M.accepts ↔ M.eval x ∈ M.accept
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>i : Fin (n + 1)<VAR>x : α<VAR>p : Fin n → α<GOAL>i.insertNth x p ∘ rev = i.rev.insertNth x (p ∘ rev)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>i : Fin (n + 1)<VAR>x✝ : α<VAR>p : Fin n → α<VAR>x : Fin (n + 1)<GOAL>(i.insertNth x✝ p ∘ rev) x = i.rev.insertNth x✝ (p ∘ rev) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Zero α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f✝ g✝ : ι →₀ α<VAR>i✝ : ι<VAR>a : α<VAR>f g : ι →₀ α<VAR>i : ι<GOAL>i ∈ f.support ∪ g.support ↔ (fun i => Icc (f i) (g i)) i ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Zero α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f✝ g✝ : ι →₀ α<VAR>i✝ : ι<VAR>a : α<VAR>f g : ι →₀ α<VAR>i : ι<GOAL>f i = 0 ∧ g i = 0 ↔ (fun i => Icc (f i) (g i)) i = 0
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<VAR>h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<VAR>h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q<VAR>h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<VAR>h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q<VAR>h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)<GOAL>‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - ‖p -ᵥ q‖ ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>hq : dist a q = dist b q<VAR>m : P := midpoint ℝ a b<VAR>hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<VAR>h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q<VAR>h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)<GOAL>‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b p q : P<VAR>m : P := midpoint ℝ a b<VAR>hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖<VAR>hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))<VAR>h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p<VAR>h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q<VAR>h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q<VAR>h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)<GOAL>‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hs : s ⊆ f.source<GOAL>map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' s] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hs : s ⊆ f.source<GOAL>s ⊆ (f.extend I).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLinearOrder β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (f ⊓ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLinearOrder β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>c : Chain α<VAR>z : β<GOAL>(f ⊓ g) (ωSup c) ≤ z ↔ ωSup (c.map (f ⊓ g)) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLinearOrder β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>c : Chain α<VAR>z : β<GOAL>(∀ (x x_1 : ℕ), f (c x_1) ≤ z ∨ g (c x) ≤ z) ↔ ∀ (i : ℕ), f (c i) ≤ z ∨ g (c i) ≤ z
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>o % b ^ log b o < o
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>o % 0 ^ log 0 o < o
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : b ≠ 0<GOAL>o % b ^ log b o < o