ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<GOAL>cthickening δ (closure E) = ⋃ x ∈ closure E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ (closure E)<GOAL>x ∈ ⋃ x ∈ closure E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ (closure E)<VAR>y : α<VAR>yE : y ∈ closure E<VAR>hy : infDist x (closure E) = dist x y<GOAL>x ∈ ⋃ x ∈ closure E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ (closure E)<VAR>y : α<VAR>yE : y ∈ closure E<VAR>hy : dist x y ≤ δ<GOAL>x ∈ ⋃ x ∈ closure E, closedBall x δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝ : LE α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ →+* ℂ<VAR>hf : Continuous ⇑f<GOAL>f = RingHom.id ℂ ∨ f = starRingEnd ℂ
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>g : α → α<VAR>x y : α<VAR>hx : IsFixedPt f x<VAR>hy : IsFixedPt g y<VAR>C : ℝ<VAR>hfg : ∀ (z : α), dist (f z) (g z) ≤ C<GOAL>dist y (f y) / (1 - ↑K) = dist (f y) (g y) / (1 - ↑K)
<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>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α → α'<VAR>g : M →ₗ[R] M'<VAR>h : ∀ (i : α), g (v i) = v' (f i)<VAR>l : α<GOAL>((Finsupp.total α' M' R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l) 1 = ((g ∘ₗ Finsupp.total α M R v) ∘ₗ lsingle l) 1
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a = b + c<GOAL>a - b = c
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : S ∈ leftTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : S ∈ leftTransversals ↑H<GOAL>Finite (G ⧸ H) ↔ H.FiniteIndex
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<GOAL>(∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i => (φ i).vars
<VAR>R✝ : Type u<VAR>A✝ : Type v<VAR>B : Type w<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Algebra R✝ A✝<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R✝ B<VAR>S✝ : Subalgebra R✝ A✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>(algebraMap (↥S) A).range = S.toSubring
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>n : G<VAR>hn : n ∈ s<VAR>g : G<GOAL>g * n * g⁻¹ ∈ s
<VAR>this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>hf : _root_.Partrec f<VAR>g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)<GOAL>Partrec' f
<VAR>f : ℕ →. ℕ<VAR>hf : Partrec f<GOAL>Partrec' fun v => f v.head
<VAR>c : Code<VAR>hf : Partrec c.eval<GOAL>Partrec' fun v => c.eval v.head
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : β → Set α<VAR>h₁ : Unbounded r (⋃ x, s x)<VAR>h₂ : #β < StrictOrder.cof r<GOAL>∃ x, Unbounded r (s x)
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : β → Set α<VAR>h₁ : Unbounded r (⋃₀ range s)<VAR>h₂ : #β < StrictOrder.cof r<GOAL>∃ x, Unbounded r (s x)
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : β → Set α<VAR>h₁ : Unbounded r (⋃₀ range s)<VAR>h₂ : #β < StrictOrder.cof r<VAR>x : β<VAR>u : Unbounded r (s x)<GOAL>∃ x, Unbounded r (s x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>q : ι → Prop<VAR>hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i<GOAL>l.HasBasis (fun i => p i ∧ q i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>q : ι → Prop<VAR>hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i<VAR>t : Set α<VAR>ht : t ∈ l<GOAL>∃ i, (p i ∧ q i) ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i✝ : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>q : ι → Prop<VAR>hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i<VAR>t : Set α<VAR>ht : t ∈ l<VAR>i : ι<VAR>hpi : p i<VAR>hti : s i ⊆ t<GOAL>∃ i, (p i ∧ q i) ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hφ : Integrable φ μ<VAR>hf : Memℒp f ⊤ μ<GOAL>Integrable (φ • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hφ : Memℒp φ 1 μ<VAR>hf : Memℒp f ⊤ μ<GOAL>Memℒp (φ • f) 1 μ
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a b : α<VAR>m : Multiset α<GOAL>{a} = b ::ₘ m ↔ a = b ∧ m = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a b : α<VAR>m : Multiset α<GOAL>(a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝² : Zero β<VAR>inst✝¹ : Zero γ<VAR>inst✝ : DecidableEq n<VAR>f : α → β → γ<VAR>hf : ∀ (a : α), f a 0 = 0<VAR>A : Matrix l m α<VAR>b : n → β<VAR>i₁ : l<VAR>i₂ : n<VAR>j₁ : m<VAR>j₂ : n<GOAL>kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => A.map fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>a ^ (n + 1) ≤ xn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>a ^ n * a ≤ xn a1 n * a + Pell.d a1 * yn a1 n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>s : Set ι<GOAL>LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total ι M R v))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>LiftRel R ca cb.think ↔ LiftRel R ca cb
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<GOAL>LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>(∃ z, b = a + z • p) → toIocMod hp a b = a + p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h : toIocMod hp a b = a + p<GOAL>b = a + (toIocDiv hp a b + 1) • p
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inr g₁ g₂ ≫ pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₁ g₂ ≫ pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯ = pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Sheaf J A<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>inst✝ : J.HasSheafCompose (forget A)<VAR>F G : Sheaf J (Type w)<VAR>f : F ⟶ G<GOAL>Presheaf.IsLocallySurjective J f.val ↔ IsIso (imageSheafι f)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Sheaf J A<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>inst✝ : J.HasSheafCompose (forget A)<VAR>F G : Sheaf J (Type w)<VAR>f : F ⟶ G<GOAL>IsIso (Subpresheaf.sheafify J (imagePresheaf f.val)).ι ↔ IsIso { val := (Subpresheaf.sheafify J (imagePresheaf f.val)).ι }
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a))
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous reflTransSymmAux
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous fun x => ↑x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous fun x => 1 / 2
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous fun x => ↑x.1 * 2 * ↑x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous fun x => ↑x.1 * (2 - 2 * ↑x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>x : ↑I × ↑I<VAR>hx : ↑x.2 = 1 / 2<GOAL>↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>x : α<VAR>y : β<VAR>s t : Set β<VAR>h : ContinuousWithinAt f (f ⁻¹' s) x<VAR>ht : t ∈ 𝓝[s] f x<VAR>hxy : y = f x<GOAL>f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<GOAL>(Aᵀ * Aᵀ.adjugate)ᵀ = A.det • 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (thickening ε s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (ball 1 ε * s)
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.237519}<VAR>α : Type u_1<VAR>h : 3 ≤ #α<VAR>x y : α<VAR>this : ↑3 ≤ #α<GOAL>∃ z, z ≠ x ∧ z ≠ y
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.237519}<VAR>α : Type u_1<VAR>h : 3 ≤ #α<VAR>x y : α<VAR>this✝ : ↑3 ≤ #α<VAR>this : ↑2 < #α<GOAL>∃ z, z ≠ x ∧ z ≠ y
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.237519}<VAR>α : Type u_1<VAR>h : 3 ≤ #α<VAR>x y : α<VAR>this✝¹ : ↑3 ≤ #α<VAR>this✝ : ↑2 < #α<VAR>this : ∃ z, z ∉ [x, y]<GOAL>∃ z, z ≠ x ∧ z ≠ y
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>p : γ → Prop<GOAL>(∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>((η.withDensity (κ.rnDeriv η)) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>((η.withDensity (κ.rnDeriv η)) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>∫⁻ (b : γ) in s, ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>Measurable (Function.uncurry fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>Measurable (Function.uncurry fun a x => (1 - κ.rnDerivAux (κ + η) a x).toNNReal)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>Measurable (Function.uncurry (κ.rnDeriv η))
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<GOAL>∫⁻ (b : γ) in s, ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>this : η.withDensity (κ.rnDeriv η) = ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)<VAR>hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1<GOAL>∫⁻ (b : γ) in s, ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η) a = (κ a) s
<VAR>M : Type u<VAR>inst✝⁹ : Monoid M<VAR>G✝ : Type u<VAR>inst✝⁸ : Group G✝<VAR>F✝ : Type v<VAR>inst✝⁷ : Field F✝<VAR>inst✝⁶ : MulSemiringAction M F✝<VAR>inst✝⁵ : MulSemiringAction G✝ F✝<VAR>m : M<VAR>G : Type u<VAR>F : Type v<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Field F<VAR>inst✝² : Finite G<VAR>inst✝¹ : MulSemiringAction G F<VAR>inst✝ : FaithfulSMul G F<GOAL>Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
<VAR>M : Type u<VAR>inst✝⁹ : Monoid M<VAR>G✝ : Type u<VAR>inst✝⁸ : Group G✝<VAR>F✝ : Type v<VAR>inst✝⁷ : Field F✝<VAR>inst✝⁶ : MulSemiringAction M F✝<VAR>inst✝⁵ : MulSemiringAction G✝ F✝<VAR>m : M<VAR>G : Type u<VAR>F : Type v<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Field F<VAR>inst✝² : Finite G<VAR>inst✝¹ : MulSemiringAction G F<VAR>inst✝ : FaithfulSMul G F<VAR>val✝ : Fintype G<GOAL>Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
<VAR>M : Type u<VAR>inst✝⁹ : Monoid M<VAR>G✝ : Type u<VAR>inst✝⁸ : Group G✝<VAR>F✝ : Type v<VAR>inst✝⁷ : Field F✝<VAR>inst✝⁶ : MulSemiringAction M F✝<VAR>inst✝⁵ : MulSemiringAction G✝ F✝<VAR>m : M<VAR>G : Type u<VAR>F : Type v<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Field F<VAR>inst✝² : Finite G<VAR>inst✝¹ : MulSemiringAction G F<VAR>inst✝ : FaithfulSMul G F<VAR>val✝ : Fintype G<GOAL>Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0
<VAR>α : Type u_1<VAR>inst✝ : AddGroup α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(↑n)⁻¹.val • n • a = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>v : E<GOAL>v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫_𝕜 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<VAR>hlim : ¬IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<VAR>hlim : ¬IsSuccLimit (sSup s)<VAR>y : α<VAR>hy : y ⋖ sSup s<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<VAR>hlim : ¬IsSuccLimit (sSup s)<VAR>y : α<VAR>hy : y ⋖ sSup s<VAR>i : α<VAR>his : i ∈ s<VAR>hi : y < i<GOAL>sSup s ∈ s
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<GOAL>⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<VAR>h✝ : IsEmpty ι<GOAL>⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<VAR>h✝ : Nonempty ι<GOAL>⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1
<VAR>f g : Code<VAR>k : Cont'<GOAL>codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)
<VAR>f g : Code<VAR>k : Cont'<GOAL>trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) = trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y