ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<VAR>c : M₂<GOAL>c ∈ ker (pi f) ↔ c ∈ ⨅ i, ker (f i)
<VAR>x y : ℝ<GOAL>√x ≤ 1 ↔ x ≤ 1
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑((S.leftInvEquiv hS).symm x) * ↑x = 1
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a ≤ 1 / b ↔ b ≤ 1 / a
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>z : ℂ<GOAL>↑x ^ (↑y * z) = ↑(x ^ y) ^ z
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>z : ℂ<GOAL>-π < (log ↑x * ↑y).im
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>z : ℂ<GOAL>(log ↑x * ↑y).im ≤ π
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F))).obj (X₁.tensorObj Y₁).rel ≤ (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (X₂.tensorObj Y₂).tgt))).obj (X₂.tensorObj Y₂).rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F))).obj ((Subobject.pullback (prod.map π₁ π₁)).obj X₁.rel) ⊓ (Subobject.pullback π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F))).obj ((Subobject.pullback (prod.map π₂ π₂)).obj Y₁.rel) ≤ (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (X₂.tgt ⨯ Y₂.tgt)))).obj ((Subobject.pullback (prod.map π₁ π₁)).obj X₂.rel) ⊓ (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (X₂.tgt ⨯ Y₂.tgt)))).obj ((Subobject.pullback (prod.map π₂ π₂)).obj Y₂.rel)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(Subobject.pullback (π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) ≫ prod.map π₁ π₁)).obj X₁.rel ≤ (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (X₂.tgt ⨯ Y₂.tgt)) ≫ prod.map π₁ π₁)).obj X₂.rel
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(Subobject.pullback (π(π₁, π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)) ≫ prod.map π₂ π₂)).obj Y₁.rel ≤ (Subobject.pullback (prod.map (prod.map f.f g.f) (𝟙 (X₂.tgt ⨯ Y₂.tgt)) ≫ prod.map π₂ π₂)).obj Y₂.rel
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε r : ℝ<VAR>hr : 0 < r<GOAL>r • ball 0 1 = ball 0 r
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : β<GOAL>const abv x⁻¹ = if h : (const abv x).LimZero then 0 else (const abv x).inv h
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>h0 : 0 < type r<VAR>a : α<GOAL>¬r a (enum r 0 h0)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>h0 : 0 < type r<VAR>a : α<GOAL>0 ≤ typein r a
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>∃ r, ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = r
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M.V ≅ N.V<VAR>comm : autoParam (∀ (g : ↑G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g) _auto✝<VAR>g : ↑G<GOAL>N.ρ g ≫ f.inv = f.inv ≫ M.ρ g
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M.V ≅ N.V<VAR>comm : autoParam (∀ (g : ↑G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g) _auto✝<VAR>g : ↑G<VAR>w : (M.ρ g ≫ f.hom) ≫ f.inv = (f.hom ≫ N.ρ g) ≫ f.inv<GOAL>N.ρ g ≫ f.inv = f.inv ≫ M.ρ g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>(∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R[ℕ]<GOAL>{ toFinsupp := a } = 0 ↔ a = 0
<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>s : Set α<VAR>f g : α → E<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>eLpNormEssSup (s.piecewise f g) μ = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))
<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>s : Set α<VAR>f g : α → E<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>essSup (fun x => ↑‖s.piecewise f g x‖₊) μ = essSup (s.piecewise (fun x => ↑‖f x‖₊) fun x => ↑‖g x‖₊) μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>x * x⋆ ≠ 0 ↔ x ≠ 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>(ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ (ℬ Y₁ Y₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂))) (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom = (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ (ℬ Y₂ Y₃).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>∀ (j : Discrete WalkingPair), ((ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ (ℬ Y₁ Y₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂))) (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫ (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app j = ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ (ℬ Y₂ Y₃).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫ (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app j
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<GOAL>∃ i T, Substructure.map (of L ι G f i).toHom T = S
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<VAR>i : ι<VAR>y : { x // x ∈ A } → G i<VAR>eq_y : (fun a => ↑a) = fun a => ⟦Structure.Sigma.mk f i (y a)⟧<GOAL>∃ i T, Substructure.map (of L ι G f i).toHom T = S
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<VAR>i : ι<VAR>y : { x // x ∈ A } → G i<VAR>eq_y : (fun a => ↑a) = fun a => ⟦Structure.Sigma.mk f i (y a)⟧<GOAL>∃ T, Substructure.map (of L ι G f i).toHom T = S
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<VAR>i : ι<VAR>y : { x // x ∈ A } → G i<VAR>eq_y : (fun a => ↑a) = fun a => ⟦Structure.Sigma.mk f i (y a)⟧<GOAL>Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (range y)) = S
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<VAR>i : ι<VAR>y : { x // x ∈ A } → G i<VAR>eq_y : (fun a => ↑a) = fun a => ⟦Structure.Sigma.mk f i (y a)⟧<GOAL>(Substructure.closure L).toFun (⇑(of L ι G f i).toHom '' range y) = S
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : Nonempty ι<VAR>S : L.Substructure (DirectLimit G f)<VAR>S_fg : S.FG<VAR>A : Finset (DirectLimit G f)<VAR>A_closure : (Substructure.closure L).toFun ↑A = S<VAR>i : ι<VAR>y : { x // x ∈ A } → G i<VAR>eq_y : (fun a => ↑a) = fun a => ⟦Structure.Sigma.mk f i (y a)⟧<GOAL>(Substructure.closure L).toFun ((fun a => ⟦Structure.Sigma.mk f i a⟧) '' range y) = S
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iInf f).toReal = ⨅ i, (f i).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<GOAL>IntegrableOn f univ μ ↔ Integrable f μ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>k : ℤ<VAR>h : k + k ≠ 0<GOAL>0 < a ^ (k + k) ↔ a ≠ 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this : IsNoetherian K V<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this.extend ⋯)) K V := Basis.extend this<VAR>b_eq : b = Basis.extend this<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this.extend ⋯)) K V := Basis.extend this<VAR>b_eq : b = Basis.extend this<VAR>i1 : Fintype ↑(this.extend ⋯) := ⋯.fintype<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this.extend ⋯)) K V := Basis.extend this<VAR>b_eq : b = Basis.extend this<VAR>i1 : Fintype ↑(this.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this.extend ⋯)) K V := Basis.extend this<VAR>b_eq : b = Basis.extend this<VAR>i1 : Fintype ↑(this.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝¹ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this✝ : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝<VAR>b_eq : b = Basis.extend this✝<VAR>i1 : Fintype ↑(this✝.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝¹ : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this✝ : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝<VAR>b_eq : b = Basis.extend this✝<VAR>i1 : Fintype ↑(this✝.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯<GOAL>S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝² : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this✝¹ : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹<VAR>b_eq : b = Basis.extend this✝¹<VAR>i1 : Fintype ↑(this✝¹.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯<VAR>this : span K (Set.range ⇑bS) = ⊤<GOAL>S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : finrank K ↥S = finrank K V<VAR>this✝² : IsNoetherian K V<VAR>bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S<VAR>bS_eq : bS = Basis.ofVectorSpace K ↥S<VAR>this✝¹ : LinearIndependent (ι := { x // x ∈ Subtype.val '' Basis.ofVectorSpaceIndex K ↥S }) K Subtype.val<VAR>b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹<VAR>b_eq : b = Basis.extend this✝¹<VAR>i1 : Fintype ↑(this✝¹.extend ⋯) := ⋯.fintype<VAR>i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype<VAR>this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯<VAR>this : span K (Basis.ofVectorSpaceIndex K ↥S) = ⊤<GOAL>S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.adjustToOrientation x).toBasis.orientation = x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>(e.toBasis.adjustToOrientation x).orientation = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>E : Type u_5<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : MetrizableSpace E<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>NullMeasurableSet {x | f x = g x} μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>E : Type u_5<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : MetrizableSpace E<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>{x | AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x} =ᶠ[ae μ] {x | f x = g x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>E : Type u_5<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : MetrizableSpace E<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>x : α<VAR>hfx : f x = AEStronglyMeasurable.mk f hf x<VAR>hgx : g x = AEStronglyMeasurable.mk g hg x<GOAL>{x | AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x} x = {x | f x = g x} x
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : BorelSpace G<VAR>g : G<GOAL>μ {g} = μ {1}
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : BorelSpace G<VAR>g : G<GOAL>{g} = (fun h => g⁻¹ * h) ⁻¹' {1}
<VAR>f : Code → Code<VAR>hf : Computable f<VAR>g : ℕ → ℕ → Part ℕ := fun x y => do let b ← (ofNat Code x).eval x (ofNat Code b).eval y<VAR>this✝ : Partrec₂ g<VAR>cg : Code<VAR>eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => g p.1 p.2) a)<VAR>eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)<VAR>F : ℕ → Code := fun x => f (cg.curry x)<VAR>this : Computable F<VAR>cF : Code<VAR>eF : cF.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (↑F a)<VAR>eF' : cF.eval (encode cF) = Part.some (encode (F (encode cF)))<VAR>n : ℕ<GOAL>(f (cg.curry (encode cF))).eval n = (cg.curry (encode cF)).eval n