ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x✝ : X<VAR>s✝ : Set X<VAR>B : Set (Set X)<VAR>hB : IsTopologicalBasis B<VAR>x : X<VAR>s : Set X<VAR>h : s ∈ 𝓝 x<GOAL>∃ t ∈ B, x ∈ t ∧ closure t ⊆ s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>motive : HNNExtension G A B φ → Prop<VAR>x : HNNExtension G A B φ<VAR>of : ∀ (g : G), motive (HNNExtension.of g)<VAR>t : motive HNNExtension.t<VAR>mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)<VAR>inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹<VAR>S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<GOAL>motive x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>motive : HNNExtension G A B φ → Prop<VAR>x : HNNExtension G A B φ<VAR>of : ∀ (g : G), motive (HNNExtension.of g)<VAR>t : motive HNNExtension.t<VAR>mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)<VAR>inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹<VAR>S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<VAR>f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯<GOAL>motive x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>motive : HNNExtension G A B φ → Prop<VAR>x : HNNExtension G A B φ<VAR>of : ∀ (g : G), motive (HNNExtension.of g)<VAR>t : motive HNNExtension.t<VAR>mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)<VAR>inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹<VAR>S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<VAR>f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯<VAR>hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)<GOAL>motive x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>motive : HNNExtension G A B φ → Prop<VAR>x : HNNExtension G A B φ<VAR>of : ∀ (g : G), motive (HNNExtension.of g)<VAR>t : motive HNNExtension.t<VAR>mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)<VAR>inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹<VAR>S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<VAR>f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯<VAR>hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)<GOAL>motive ((S.subtype.comp f) x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)<VAR>i : Fin (n + 1)<VAR>e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm<GOAL>MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (Measure.pi μ) ((μ i).prod (Measure.pi fun j => μ (i.succAbove j)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)<VAR>i : Fin (n + 1)<VAR>e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm<GOAL>MeasurePreserving (⇑e) ((μ i).prod (Measure.pi fun j => μ (i.succAbove j))) (Measure.pi μ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)<VAR>i : Fin (n + 1)<VAR>e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm<VAR>s : (i : Fin (n + 1)) → Set (α i)<VAR>x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)<GOAL>(Measure.map (⇑e) ((μ i).prod (Measure.pi fun j => μ (i.succAbove j)))) (univ.pi s) = ∏ i : Fin (n + 1), (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)<VAR>i : Fin (n + 1)<VAR>e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm<VAR>s : (i : Fin (n + 1)) → Set (α i)<VAR>x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)<GOAL>((μ i).prod (Measure.pi fun j => μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) = ((μ i).prod (Measure.pi fun i_1 => μ (i.succAbove i_1))) (s i ×ˢ univ.pi fun i_1 => s (i.succAbove i_1))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>m : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>μ : (i : Fin (n + 1)) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)<VAR>i : Fin (n + 1)<VAR>e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm<VAR>s : (i : Fin (n + 1)) → Set (α i)<VAR>x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)<VAR>x : α i<VAR>f : (j : Fin n) → α (i.succAbove j)<GOAL>(x, f) ∈ ⇑e ⁻¹' univ.pi s ↔ (x, f) ∈ s i ×ˢ univ.pi fun i_1 => s (i.succAbove i_1)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<GOAL>cardPowDegree (x - z) < a
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<GOAL>cardPowDegree (x - z) < a
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : ¬x = y<VAR>hyz' : ¬y = z<VAR>hxz' : ¬x = z<GOAL>cardPowDegree (x - z) < a
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<GOAL>cardPowDegree (x - z) < a
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<GOAL>cardPowDegree (x - z) ≤ max (cardPowDegree (x - y)) (cardPowDegree (y - z))
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<GOAL>↑(Fintype.card Fq) ^ (x - z).natDegree ≤ max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<VAR>this : 1 ≤ ↑(Fintype.card Fq)<GOAL>↑(Fintype.card Fq) ^ (x - z).natDegree ≤ max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<VAR>this : 1 ≤ ↑(Fintype.card Fq)<GOAL>↑(Fintype.card Fq) ^ (x - z).natDegree ≤ ↑(Fintype.card Fq) ^ (x - y).natDegree ∨ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤ ↑(Fintype.card Fq) ^ (y - z).natDegree
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<VAR>this : 1 ≤ ↑(Fintype.card Fq)<GOAL>(x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<VAR>this : 1 ≤ ↑(Fintype.card Fq)<GOAL>(x - z).degree ≤ max (x - y).degree (y - z).degree
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>x y z : Fq[X]<VAR>a : ℤ<VAR>hxy : cardPowDegree (x - y) < a<VAR>hyz : cardPowDegree (y - z) < a<VAR>ha : 0 < a<VAR>hxy' : x - y ≠ 0<VAR>hyz' : y - z ≠ 0<VAR>hxz' : x - z ≠ 0<VAR>this : 1 ≤ ↑(Fintype.card Fq)<GOAL>x - z = x - y + (y - z)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompactSpace α<VAR>w : ∀ (x : α), dist (f x) (g x) < C<VAR>c : Continuous fun x => dist (f x) (g x)<GOAL>dist f g < C
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x✝ : α<VAR>C : ℝ<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompactSpace α<VAR>w : ∀ (x : α), dist (f x) (g x) < C<VAR>c : Continuous fun x => dist (f x) (g x)<VAR>x : α<VAR>le : IsMaxOn (fun x => dist (f x) (g x)) univ x<GOAL>dist f g < C
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NeZero μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NeZero μ<VAR>hg : ConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>ht_mem : ∀ᵐ (x : α) ∂μ, (f x, g (f x)) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}<GOAL>(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℤ<GOAL>f (n • a) = f 0 + n • b
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M₁<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Module.rank R M ≤ Module.rank R' M₁
<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✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ ↑f.support<GOAL>(Finsupp.total ι M R v) f ≠ v x
<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✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ ↑f.support<VAR>p : v x ∉ span R (v '' ↑f.support)<GOAL>(Finsupp.total ι M R v) f ≠ v x
<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✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ ↑f.support<VAR>p : (Finsupp.total ι M R v) f ∉ span R (v '' ↑f.support)<VAR>w : (Finsupp.total ι M R v) f = v x<GOAL>False
<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✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ ↑f.support<VAR>p : (Finsupp.total ι M R v) f ∉ Submodule.map (Finsupp.total ι M R v) (Finsupp.supported R R ↑f.support)<VAR>w : (Finsupp.total ι M R v) f = v x<GOAL>False
<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✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ ↑f.support<VAR>w : (Finsupp.total ι M R v) f = v x<VAR>p : ∀ x ∈ Finsupp.supported R R ↑f.support, ¬(Finsupp.total ι M R v) x = (Finsupp.total ι M R v) f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a = s.indicator (⇑p) a * (∑' (a' : α), s.indicator (⇑p) a')⁻¹
<VAR>k : Type u<VAR>inst✝³ : Field k<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : IsAlgClosed K<VAR>inst✝ : Algebra k K<VAR>p q : k[X]<GOAL>IsCoprime p q ↔ ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
<VAR>k : Type u<VAR>inst✝³ : Field k<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : IsAlgClosed K<VAR>inst✝ : Algebra k K<VAR>p q : k[X]<VAR>h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0<GOAL>¬(p = 0 ∧ q = 0)
<VAR>k : Type u<VAR>inst✝³ : Field k<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : IsAlgClosed K<VAR>inst✝ : Algebra k K<VAR>p q : k[X]<VAR>h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0<VAR>x : k[X]<VAR>hu : x ∈ nonunits k[X]<VAR>h0 : x ≠ 0<GOAL>x ∣ p → ¬x ∣ q
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<GOAL>s ⊂ {a} ↔ s = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<VAR>hs : s ⊂ {a}<VAR>b : α<VAR>hb : b ∈ s<GOAL>{a} ⊆ s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<VAR>a : α<GOAL>s = 0 → s ⊂ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝¹ : Finset α<VAR>t✝ : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq γ<VAR>f : α → β<VAR>s✝ : Finset α<VAR>t : β → Finset γ<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>x✝ : a ∉ s<VAR>ih : (image f s).biUnion t = s.biUnion fun a => t (f a)<GOAL>(image f (insert a s)).biUnion t = (insert a s).biUnion fun a => t (f a)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝¹ : Coreflective j<VAR>A : D<VAR>inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)<VAR>ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit<GOAL>A ∈ j.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝¹ : Coreflective j<VAR>A : D<VAR>inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)<VAR>ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit<VAR>this : IsIso (ε.app (j.obj ((coreflector j).obj A)))<GOAL>A ∈ j.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝¹ : Coreflective j<VAR>A : D<VAR>inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)<VAR>ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit<VAR>this✝ : IsIso (ε.app (j.obj ((coreflector j).obj A)))<VAR>this : Mono (ε.app A)<GOAL>A ∈ j.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝¹ : Coreflective j<VAR>A : D<VAR>inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)<VAR>ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit<VAR>this✝¹ : IsIso (ε.app (j.obj ((coreflector j).obj A)))<VAR>this✝ : Mono (ε.app A)<VAR>this : IsIso (ε.app A)<GOAL>A ∈ j.essImage
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A * B = 1<VAR>g : A * C = 1<GOAL>B = C
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝³ : Semiring A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : TopologicalSemiring A<VAR>inst✝ : Algebra R A<VAR>f : A →A[R] A<GOAL>↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
<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>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>hf : Injective2 f<GOAL>image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(quotQuotEquivComm I f) ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)
<VAR>x y : ℝ<GOAL>mk 0 = 0
<VAR>x y : ℝ<GOAL>mk 0 = { cauchy := 0 }
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>e.r i' = none
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi'✝ : ∀ (i : ι), e.f i ≠ i'<VAR>hi' : e.r i' = none<GOAL>e.r i' = none
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<VAR>i : ι<VAR>hi : e.r i' = some i<GOAL>e.r i' = none
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>p : β → Bool<VAR>l : List α<VAR>f : α → List β<GOAL>countP p (l.bind f) = (map (countP p ∘ f) l).sum
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε δ : ℝ<VAR>h : ε ≤ δ<VAR>x : E<VAR>r' : ℝ<VAR>r'r : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<GOAL>x ∈ A f L r δ
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε δ : ℝ<VAR>h : ε ≤ δ<VAR>x : E<VAR>r' : ℝ<VAR>r'r : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<VAR>y : E<VAR>hy : y ∈ ball x r'<VAR>z : E<VAR>hz : z ∈ ball x r'<GOAL>0 ≤ r
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>l : E →ₗ.[R] F<VAR>hl : l ∈ c<VAR>x : ↥l.domain<GOAL>↑l x = ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>l : E →ₗ.[R] F<VAR>hl : l ∈ c<VAR>x : ↥l.domain<GOAL>↑x = ↑⟨↑x, ⋯⟩