ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<VAR>S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)<VAR>i : Fin N<VAR>hi : μ s / (↑N + 1) < μ (s ∩ v i)<VAR>B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))<VAR>w : Finset ↑(u i)<VAR>hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<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>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<GOAL>Measure.map (⇑e) μ = ν ↔ Measure.map (⇑e.symm) ν = μ
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>γ : SL(2, ℤ)<VAR>z : ℍ<GOAL>(eisensteinSeries a k ∣[k] γ) z = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>γ : SL(2, ℤ)<VAR>z : ℍ<GOAL>denom (↑γ) z ^ k * ∑' (x : ↑(gammaSet N a)), eisSummand k (↑x ᵥ* ↑γ) z = denom (↑γ) z ^ k * ∑' (x : ↑(gammaSet N (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)<VAR>h' : Module.rank R N < ℵ₀<GOAL>finrank R M ≤ finrank R N
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>⟪y, x⟫_ℝ = 0
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<GOAL>∃ m, n * m % k = n.gcd k
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<VAR>hk' : ↑k ≠ 0<GOAL>∃ m, n * m % k = n.gcd k
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<VAR>hk' : ↑k ≠ 0<VAR>key : (fun m => (m % ↑k).toNat) ↑(n.gcd k) = (fun m => (m % ↑k).toNat) (↑n * n.gcdA k + ↑k * n.gcdB k)<GOAL>∃ m, n * m % k = n.gcd k
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<VAR>hk' : ↑k ≠ 0<VAR>key : (↑(n.gcd k) % ↑k).toNat = ((↑n * n.gcdA k + ↑k * n.gcdB k) % ↑k).toNat<GOAL>∃ m, n * m % k = n.gcd k
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<VAR>hk' : ↑k ≠ 0<VAR>key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat<GOAL>∃ m, n * m % k = n.gcd k
<VAR>k n : ℕ<VAR>hk : n.gcd k < k<VAR>hk' : ↑k ≠ 0<VAR>key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat<GOAL>Int.ofNat (n * (n.gcdA k % ↑k).toNat % k) = Int.ofNat (↑n * n.gcdA k % ↑k).toNat
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' univ x<VAR>hf : HasDerivWithinAt f f' univ x<GOAL>HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) univ x
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Subsemigroup.closure s)<GOAL>0 * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Subsemigroup.closure s)<GOAL>0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Subsemigroup.closure s)<VAR>p₁ p₂ : R<VAR>ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<GOAL>p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f✝ : R →ₙ+* S<VAR>s : Set R<VAR>x✝¹ : R<VAR>h : x✝¹ ∈ closure s<VAR>x✝ y : R<VAR>hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Subsemigroup.closure s)<VAR>x : R<VAR>hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>f : -x * q = -(x * q)<GOAL>-(x * q) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<GOAL>x * 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<GOAL>0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>q₁ q₂ : R<VAR>ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<GOAL>x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f✝ : R →ₙ+* S<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>z : R<VAR>hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)<VAR>f : x * -z = -(x * z)<GOAL>-(x * z) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<VAR>m : ℕ<GOAL>WittVector.ghostFun (x ^ m) = WittVector.ghostFun x ^ m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>inst✝ : CharZero R<VAR>x✝² x✝¹ : ℕ<VAR>x✝ : ↑x✝² = ↑x✝¹<GOAL>f ↑x✝² = f ↑x✝¹
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : BorelSpace E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : TendstoInMeasure μ f u g<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : BorelSpace E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : TendstoInMeasure μ f u g<VAR>ns : ℕ → ι<VAR>hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))<GOAL>AEMeasurable g μ
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ (-1) = -1<GOAL>ψ (-x) = -ψ x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ (-1) = -1<GOAL>ψ (-1) * ψ x = -ψ x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.leftOp<VAR>j : Jᵒᵖ<GOAL>((coconeLeftOpOfCone c).ι.app j ≫ (fun s => (hc.lift (coneOfCoconeLeftOp s)).unop) s).op = (s.ι.app j).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.leftOp<VAR>m : (coconeLeftOpOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => (hc.lift (coneOfCoconeLeftOp s)).unop) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.leftOp<VAR>m : (coconeLeftOpOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j<VAR>j : J<GOAL>(m.op ≫ c.π.app j).unop = (((fun s => (hc.lift (coneOfCoconeLeftOp s)).unop) s).op ≫ c.π.app j).unop
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : IsSeparable s<GOAL>IsSeparable (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : IsSeparable s<GOAL>IsSeparable ((fun x => f ↑x) '' univ)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X✝<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X✝ → E<VAR>s✝ t : Set X✝<VAR>μ✝ ν : Measure X✝<VAR>l l' : Filter X✝<VAR>X : Type u_5<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>hm : m ≤ m0<VAR>f : X → E<VAR>hf_meas : StronglyMeasurable f<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm
<VAR>n : ℕ<GOAL>antidiagonal (n + 1) = cons (n + 1, 0) (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯
<VAR>n : ℕ<GOAL>(antidiagonal (n + 1)).val = (cons (n + 1, 0) (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯).val
<VAR>n : ℕ<GOAL>(antidiagonal (n + 1)).val = (n + 1, 0) ::ₘ Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })) (antidiagonal n).val
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderTop α<GOAL>Ico a b ⊆ Ici a
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>b : n<VAR>c : R<VAR>M : Matrix n n R<GOAL>(transvection i j c * M) i b = M i b + c * M j b
<VAR>M₀✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero M₀✝<VAR>M₀ : Type u_2<VAR>inst✝ : CommMonoidWithZero M₀<VAR>a : M₀<GOAL>Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰
<VAR>M₀✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero M₀✝<VAR>M₀ : Type u_2<VAR>inst✝ : CommMonoidWithZero M₀<VAR>a : M₀<GOAL>(¬∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ¬∀ (x : M₀), x * a = 0 → x = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : (RightFraction.mk α.s ⋯ β.s).f ≫ γ.s = (RightFraction.mk α.s ⋯ β.s).s ≫ γ.f<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.s ≫ γ.s = α.s ≫ γ.f<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.s ≫ γ.s = α.s ≫ γ.f<VAR>ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.s ≫ γ.s = α.s ≫ γ.f<VAR>ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯<VAR>this : IsIso (L.map β.s)<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.s ≫ γ.s = α.s ≫ γ.f<VAR>ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' f'' : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>hα : f = α.fst.map L ⋯<VAR>hα' : f' = α.snd.map L ⋯<VAR>β : W.LeftFraction X Y<VAR>hβ : f'' = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.s ≫ γ.s = α.s ≫ γ.f<VAR>ψ : W.LeftFraction₃ X Y := LeftFraction₃.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.f ≫ γ.s) (β.s ≫ γ.s) ⋯<VAR>this✝¹ : IsIso (L.map β.s)<VAR>this✝ : IsIso (L.map γ.s)<VAR>this : IsIso (L.map (β.s ≫ γ.s))<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>𝕜 : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝¹¹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝¹⁰ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝⁵ : TopologicalSpace N<VAR>inst✝⁴ : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝³ : TopologicalSpace N'<VAR>inst✝² : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<GOAL>UniqueMDiffOn J (⇑h '' s)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝¹¹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝¹⁰ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝⁵ : TopologicalSpace N<VAR>inst✝⁴ : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝³ : TopologicalSpace N'<VAR>inst✝² : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>hn : 1 ≤ n<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<GOAL>⇑h '' s = h.toHomeomorph.toPartialHomeomorph.target ∩ ↑h.toHomeomorph.toPartialHomeomorph.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s t : Set α<VAR>n : ℕ<GOAL>0 < n.succ
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<VAR>x✝ : r * x ∣ r * y<VAR>z : R'<VAR>h✝ : r * y = r * x * z<GOAL>y = x * z
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<VAR>x✝ : x ∣ y<VAR>z : R'<VAR>h : y = x * z<GOAL>r * y = r * x * z
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
<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✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace G<VAR>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪x, (adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>d : α<GOAL>(fun o => o.getD d) '' range l.get? = insert d {x | x ∈ l}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulWithZero α β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>ht : t.Nonempty<GOAL>0 ⊆ 0 • t