ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₁ : {w | w.IsComplex}.Nonempty<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<GOAL>∃ x ∈ ⋃ f, ⋃ (_ : f.natDegree ≤ D ∧ ∀ (i : ℕ), f.coeff i ∈ Set.Icc (-↑C) ↑C), ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset, ↑⟨K, hK₀⟩ = ℚ⟮x⟯
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₁ : {w | w.IsComplex}.Nonempty<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<GOAL>∃ x, (∃ i, ∃ (_ : i.natDegree ≤ D ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Set.Icc (-↑C) ↑C), x ∈ ↑(Polynomial.map (algebraMap ℤ A) i).roots.toFinset) ∧ K = ℚ⟮x⟯
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsComplex}<GOAL>minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this✝ : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsComplex}<VAR>this : 1 ≤ convexBodyLT'Factor ↥K<GOAL>minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
<VAR>K✝ : Type u_1<VAR>inst✝³ : Field K✝<VAR>inst✝² : NumberField K✝<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K✝| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<VAR>x✝¹ : { F // FiniteDimensional ℚ ↥F }<VAR>K : IntermediateField ℚ A<VAR>hK₀ : FiniteDimensional ℚ ↥K<VAR>x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}<VAR>hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N<VAR>this✝ : NumberField ↥K<VAR>w₀ : InfinitePlace ↥↑⟨K, hK₀⟩<VAR>hw₀ : w₀ ∈ {w | w.IsComplex}<VAR>this : 1 ≤ convexBodyLT'Factor ↥K<GOAL>minkowskiBound (↥K) 1 = (fun x => x * minkowskiBound (↥↑⟨K, hK₀⟩) 1) ↑1
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>Measurable fun y => map (fun x => (x, y)) μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (fun x => (x, b)) μ) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (map (fun x => (x, b)) μ) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => μ ((fun x => (x, b)) ⁻¹' s)
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>‖equivRealProd z‖ ≤ 1 * abs z
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ≤ᶠ[ae (μ.trim ⋯)] μ[f j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>0 ≤ᶠ[ae (μ.trim ⋯)] μ[f j|↑ℱ i] - f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>x✝ : (μ.trim ⋯) s < ⊤<GOAL>0 ≤ ∫ (x : Ω) in s, (μ[f j|↑ℱ i] - f i) x ∂μ.trim ⋯
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>x✝ : (μ.trim ⋯) s < ⊤<VAR>hf : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<GOAL>0 ≤ ∫ (x : Ω) in s, (μ[f j|↑ℱ i] - f i) x ∂μ.trim ⋯
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>x : ↑C<GOAL>(LocallyConstant.evalMonoidHom x) (eval C l) = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>x : ↑C<GOAL>(List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : CommMonoid β<VAR>inst✝² : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f✝ f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : MulEquivClass F α β<VAR>f : F<VAR>hfAB : BijOn (⇑f) A B<VAR>s t : Multiset α<VAR>x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>x✝¹ : card s = n<VAR>x✝ : card t = n<GOAL>(map (⇑f) s).prod = (map (⇑f) t).prod ↔ s.prod = t.prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Mul R<VAR>inst✝ : HasDistribNeg R<VAR>a x y : R<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy (-a) x y
<VAR>R : Type u_2<VAR>K : Type ?u.14465<VAR>L : Type ?u.14468<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a✝ : Nontrivial S<GOAL>(minpolyDiv R x).Monic
<VAR>R : Type u_2<VAR>K : Type ?u.14465<VAR>L : Type ?u.14468<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a✝ : Nontrivial S<VAR>this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff<GOAL>(minpolyDiv R x).Monic
<VAR>R : Type u_2<VAR>K : Type ?u.14465<VAR>L : Type ?u.14468<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a✝ : Nontrivial S<VAR>this : (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff = 1<GOAL>(minpolyDiv R x).Monic
<VAR>R : Type u_2<VAR>K : Type ?u.14465<VAR>L : Type ?u.14468<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a✝ : Nontrivial S<VAR>this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff<GOAL>(minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<VAR>a : { x // x ∈ s }<VAR>x✝¹ : a ∈ ↑s.attach<VAR>b : { x // x ∈ s }<VAR>x✝ : b ∈ ↑s.attach<VAR>hab : a ≠ b<VAR>x : γ<VAR>hxa : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) a<VAR>hxb : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<VAR>a : { x // x ∈ s }<VAR>x✝¹ : a ∈ ↑s.attach<VAR>b : { x // x ∈ s }<VAR>x✝ : b ∈ ↑s.attach<VAR>hab : a ≠ b<VAR>x : γ<VAR>hxa : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) a<VAR>hxb : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) b<VAR>xa : β<VAR>hfa : xa ∈ f ↑a<VAR>hga : x ∈ g xa<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<VAR>a : { x // x ∈ s }<VAR>x✝¹ : a ∈ ↑s.attach<VAR>b : { x // x ∈ s }<VAR>x✝ : b ∈ ↑s.attach<VAR>hab : a ≠ b<VAR>x : γ<VAR>hxa : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) a<VAR>hxb : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) b<VAR>xa : β<VAR>hfa : xa ∈ f ↑a<VAR>hga : x ∈ g xa<VAR>xb : β<VAR>hfb : xb ∈ f ↑b<VAR>hgb : x ∈ g xb<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<VAR>a : { x // x ∈ s }<VAR>x✝¹ : a ∈ ↑s.attach<VAR>b : { x // x ∈ s }<VAR>x✝ : b ∈ ↑s.attach<VAR>hab : a ≠ b<VAR>x : γ<VAR>hxa : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) a<VAR>hxb : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) b<VAR>xa : β<VAR>hfa : xa ∈ f ↑a<VAR>hga : x ∈ g xa<VAR>xb : β<VAR>hfb : xb ∈ f ↑b<VAR>hgb : x ∈ g xb<GOAL>xa ≠ xb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<VAR>a : { x // x ∈ s }<VAR>x✝¹ : a ∈ ↑s.attach<VAR>b : { x // x ∈ s }<VAR>x✝ : b ∈ ↑s.attach<VAR>hab : a ≠ b<VAR>x : γ<VAR>hxa : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) a<VAR>hxb : x ∈ (fun a => (f ↑a).disjiUnion g ⋯) b<VAR>xa : β<VAR>hfa : xa ∈ f ↑a<VAR>hga : x ∈ g xa<VAR>hfb : xa ∈ f ↑b<VAR>hgb : x ∈ g xa<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hn : 1 ≤ n<GOAL>?m.1078222 + 1 ≤ n
<VAR>n : ℤ<GOAL>(-n).bodd = n.bodd
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * ↑y₂) = f.toMap (x₂ * ↑y₁)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map prod.snd ((fiberBinaryProductEquiv F X Y).symm (x, y)) = y
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map prod.snd ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ((Types.binaryProductIso ↑(F.obj X) ↑(F.obj Y)).inv (x, y))) = y
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>((Types.binaryProductIso ↑(F.obj X) ↑(F.obj Y)).inv ≫ (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.snd) (x, y) = y
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<GOAL>mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<GOAL>mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<VAR>k' : ℕ<VAR>hk' : Δ'.len = Δ''.len + k' + 1<GOAL>mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<VAR>k' : ℕ<VAR>hk' : Δ'.len = Δ''.len + k' + 1<VAR>eq : Δ.len = Δ''.len + (k + k' + 2)<GOAL>mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<VAR>k' : ℕ<VAR>hk' : Δ'.len = Δ''.len + k' + 1<VAR>eq : Δ.len = Δ''.len + (k + k' + 2)<GOAL>mapMono K i ≫ mapMono K i' = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<VAR>k' : ℕ<VAR>hk' : Δ'.len = Δ''.len + k' + 1<VAR>eq : Δ.len = Δ''.len + (k + k' + 2)<GOAL>Δ ≠ Δ''
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>inst✝¹ : Mono i'<VAR>inst✝ : Mono i<VAR>h₁ : ¬Δ = Δ'<VAR>h₂ : ¬Δ' = Δ''<VAR>k : ℕ<VAR>hk : Δ.len = Δ'.len + k + 1<VAR>k' : ℕ<VAR>hk' : Δ'.len = Δ''.len + k' + 1<VAR>eq : Δ.len = Δ''.len + (k + k' + 2)<GOAL>¬Isδ₀ (i' ≫ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a✝ b✝ c d a b : α<VAR>n : ℤ<GOAL>(a / b) ^ n = a ^ n / b ^ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>nc : ¬IsCyclic α<GOAL>Nontrivial α
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>nc : ¬Nontrivial α<GOAL>IsCyclic α
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<GOAL>QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h2s : ν s = 0<GOAL>(map Prod.snd (μ.prod ν)) s = 0
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sin x * cos (2 * x) + cos x * sin (2 * x) = 3 * sin x - 4 * sin x ^ 3
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2<GOAL>sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2<GOAL>sin x * (2 * (1 - sin x ^ 2) - 1) + 2 * sin x * (1 - sin x ^ 2) = 3 * sin x - 4 * sin x ^ 3
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>a • insert 0 (interior A) ⊆ insert 0 (interior A)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>ha : ‖0‖ ≤ 1<GOAL>0 • insert 0 (interior A) ⊆ insert 0 (interior A)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>h : a ≠ 0<GOAL>a • insert 0 (interior A) ⊆ insert 0 (interior A)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ' : QuasiIso φ'<GOAL>QuasiIso (φ ≫ φ') ↔ QuasiIso φ
<VAR>a✝ b c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a c x✝ : ℕ<VAR>dvd : c + 1 ∣ a + 1<VAR>dvd2 : a + 1 ∣ x✝<GOAL>x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
<VAR>a✝ b c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a c x✝ : ℕ<VAR>dvd : c + 1 ∣ a + 1<VAR>dvd2 : a + 1 ∣ x✝<VAR>a_split : a + 1 ≠ 0<GOAL>x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
<VAR>a✝ b c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a c x✝ : ℕ<VAR>dvd : c + 1 ∣ a + 1<VAR>dvd2 : a + 1 ∣ x✝<VAR>a_split : a + 1 ≠ 0<VAR>c_split : c + 1 ≠ 0<GOAL>x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
<VAR>a✝ b c✝ d m n k✝ : ℕ<VAR>p q : ℕ → Prop<VAR>a c : ℕ<VAR>a_split : a + 1 ≠ 0<VAR>c_split : c + 1 ≠ 0<VAR>k k2 : ℕ<VAR>pr : a + 1 = (c + 1) * k2<VAR>k2_nonzero : k2 ≠ 0<GOAL>(a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<GOAL>∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PseudoMetrizableSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<GOAL>∃ K ⊆ U, IsClosed K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PseudoMetrizableSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<VAR>r : ℝ≥0∞<VAR>F : ℕ → Set X<VAR>F_closed : ∀ (n : ℕ), IsClosed (F n)<VAR>F_mono : Monotone F<VAR>hU : IsOpen (⋃ n, F n)<VAR>hr : r < μ (⋃ n, F n)<GOAL>∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K