ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<GOAL>smul α φ r 0 = 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<GOAL>∀ (Y : C) (f : Y ⟶ Opposite.unop X), (Presheaf.imageSieve α r).arrows f → (A.val.map f.op) (smul α φ r 0) = (A.val.map f.op) 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop X<VAR>r₀ : (forget RingCat).obj (R₀.obj (Opposite.op Y))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.val.map f.op) r<GOAL>(A.val.map f.op) (smul α φ r 0) = (A.val.map f.op) 0
<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>inst✝³ : SFinite μ<VAR>δ : Type u_7<VAR>inst✝² : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : Measure α<VAR>μc : Measure γ<VAR>inst✝¹ : SFinite μa<VAR>inst✝ : SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)
<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>inst✝³ : SFinite μ<VAR>δ : Type u_7<VAR>inst✝² : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : Measure α<VAR>μc : Measure γ<VAR>inst✝¹ : SFinite μa<VAR>inst✝ : SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(sum fun p => (map f (sFiniteSeq μa p.1)).prod (map g (sFiniteSeq μc p.2))) = sum fun i => map (Prod.map f g) ((sFiniteSeq μa i.1).prod (sFiniteSeq μc i.2))
<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>inst✝³ : SFinite μ<VAR>δ : Type u_7<VAR>inst✝² : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : Measure α<VAR>μc : Measure γ<VAR>inst✝¹ : SFinite μa<VAR>inst✝ : SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>i : ℕ × ℕ<GOAL>(map f (sFiniteSeq μa i.1)).prod (map g (sFiniteSeq μc i.2)) = map (Prod.map f g) ((sFiniteSeq μa i.1).prod (sFiniteSeq μc i.2))
<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>inst✝³ : SFinite μ<VAR>δ : Type u_7<VAR>inst✝² : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : Measure α<VAR>μc : Measure γ<VAR>inst✝¹ : SFinite μa<VAR>inst✝ : SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>i : ℕ × ℕ<VAR>s : Set β<VAR>t : Set δ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(map (Prod.map f g) ((sFiniteSeq μa i.1).prod (sFiniteSeq μc i.2))) (s ×ˢ t) = (map f (sFiniteSeq μa i.1)) s * (map g (sFiniteSeq μc i.2)) t
<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>inst✝³ : SFinite μ<VAR>δ : Type u_7<VAR>inst✝² : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>μa : Measure α<VAR>μc : Measure γ<VAR>inst✝¹ : SFinite μa<VAR>inst✝ : SFinite μc<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>i : ℕ × ℕ<VAR>s : Set β<VAR>t : Set δ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>((sFiniteSeq μa i.1).prod (sFiniteSeq μc i.2)) (Prod.map f g ⁻¹' s ×ˢ t) = (sFiniteSeq μa i.1) (f ⁻¹' s) * (sFiniteSeq μc i.2) (g ⁻¹' t)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : F (Fix F)<GOAL>rec (Functor.map mk) (mk x) = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : F (Fix F)<GOAL>(mk ∘ dest) <$> x = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : F (Fix F)<GOAL>(mk ∘ dest) <$> x = id <$> x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x✝ : F (Fix F)<VAR>x : Fix F<GOAL>(mk ∘ dest) x = id x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>x✝ : N<GOAL>x✝ ∈ map f H.normalizer → x✝ ∈ (map f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>x✝ : N<GOAL>∀ (x : G), (∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H) → f x = x✝ → ∀ (h : N), (∃ x ∈ H, f x = h) ↔ ∃ x ∈ H, f x = x✝ * h * x✝⁻¹
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m m₁ m₂ : OuterMeasure α<GOAL>m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r✝ x y z : R<VAR>a b c : ℍ[R]<VAR>r : R<VAR>q : ℍ[R]<GOAL>normSq (r • q) = r ^ 2 * normSq q
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<VAR>hm : ∀ (i : ι), ‖m i‖ ≠ 0<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<VAR>hm : ∀ (i : ι), ‖m i‖ ≠ 0<VAR>δ : ι → 𝕜<VAR>hδ0 : ∀ (i : ι), δ i ≠ 0<VAR>hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i<VAR>hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖<VAR>a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<VAR>hm : ∀ (i : ι), ‖m i‖ ≠ 0<VAR>δ : ι → 𝕜<VAR>hδ0✝ : ∀ (i : ι), δ i ≠ 0<VAR>hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i<VAR>hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖<VAR>a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖<VAR>hδ0 : 0 < ∏ i : ι, ‖δ i‖<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x✝ : α × α<VAR>a : α<VAR>h : Disjoint s t<VAR>x : α × α<GOAL>x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x✝ : α × α<VAR>a : α<VAR>h : Disjoint s t<VAR>x : α × α<GOAL>(x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
<VAR>a x✝ z x y : ℂ<GOAL>↑x.arg = ↑y.arg ↔ x.arg = y.arg
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Ioi a * Ici b ⊆ Ioi (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.11614) (N : Type ?u.11613) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Ioi a * Ici b ⊆ Ioi (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.11614) (N : Type ?u.11613) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : y ∈ Ioi a<VAR>z : α<VAR>hzb : z ∈ Ici b<GOAL>(fun x x_1 => x * x_1) y z ∈ Ioi (a * b)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : ¬x = 0<GOAL>0 ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : ¬x = 0<VAR>h : 1 < ↑p<GOAL>0 ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : ¬x = 0<VAR>h : 1 < ↑p<GOAL>↑p ^ (-x.valuation) ≤ ↑p ^ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : ¬x = 0<VAR>h : 1 < ↑p<GOAL>‖x‖ ≤ ↑p ^ 0
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : K<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : K<VAR>s : Subfield K := let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯; { toSubring := __spread.0, inv_mem' := ⋯ }<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : K<VAR>s : Subfield K := let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯; { toSubring := __spread.0, inv_mem' := ⋯ }<VAR>this : iSup S = s<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>z : G<GOAL>z ∈ center G ↔ ∀ (g : G), g * z = z * g
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>z : G<GOAL>z ∈ center G ↔ z ∈ Set.center G
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<VAR>this : NeZero m<GOAL>¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<VAR>this : NeZero m<GOAL>¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<VAR>this : NeZero m<VAR>h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0<GOAL>¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<VAR>this : NeZero m<VAR>h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0<GOAL>¬Summable fun n => {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n
<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>k : ZMod m<VAR>this : NeZero m<VAR>h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0<GOAL>¬Summable fun n => 1 / ↑(n + 1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>n : M<VAR>hn : (mk' S) n = (mk' S) m<VAR>hn' : ‖n‖ < ‖(mk' S) m‖ + ε<GOAL>∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>n : M<VAR>hn : -m + n ∈ S<VAR>hn' : ‖n‖ < ‖(mk' S) m‖ + ε<GOAL>∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>n : M<VAR>hn : -m + n ∈ S<VAR>hn' : ‖n‖ < ‖(mk' S) m‖ + ε<GOAL>‖m + (-m + n)‖ < ‖(mk' S) m‖ + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<GOAL>s = ⊤ ↔ ∀ (x y : α), s.Rel x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Setoid α<GOAL>(∀ {x y : α}, ⊤ x y → s.Rel x y) ↔ ∀ (x y : α), s.Rel x y
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>n : ℕ<VAR>h : c ≤ ↑n<GOAL>∃ m ≤ n, c = ↑m
<VAR>α β : Type u<VAR>n c : ℕ<VAR>h : ↑c ≤ ↑n<GOAL>∃ m ≤ n, ↑c = ↑m
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : CommMonoid P<VAR>f✝ : M →* P<VAR>g : N →* P<VAR>f : M × N →* P<VAR>x : M × N<GOAL>((f.comp (inl M N)).coprod (f.comp (inr M N))) x = f x
<VAR>M : Type u_1<VAR>inst✝ : Group M<VAR>S : Submonoid M<VAR>x : ↥S.leftInv<GOAL>↑(S.fromLeftInv x) = (↑x)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : ℝ<GOAL>dist x 0 = |x|
<VAR>a b : ℕ+<VAR>hab : a < b<GOAL>a ≤ b - 1
<VAR>a b : ℕ+<VAR>hab : a < b<GOAL>↑a ≤ if 1 < b then ↑b - ↑1 else 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>deriv ε x = -x⁻¹ / log x ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : 1 < x<VAR>this : log x ≠ 0<GOAL>deriv ε x = -x⁻¹ / log x ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : 1 < x<VAR>this : log x ≠ 0<GOAL>deriv (fun z => 1 / log z) x = -x⁻¹ / log x ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsNilpotent ((aeval x) P)<VAR>h' : IsUnit ((aeval x) (derivative P))<GOAL>∃! r, IsNilpotent (x - r) ∧ (aeval r) P = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsNilpotent ((aeval x) P)<VAR>h' : IsUnit ((aeval x) (derivative P))<GOAL>∃! r, IsNilpotent (r - x) ∧ (aeval r) P = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsNilpotent ((aeval x) P)<VAR>h' : IsUnit ((aeval x) (derivative P))<GOAL>∃ x_1, IsNilpotent (x_1 - x) ∧ (aeval x_1) P = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsNilpotent ((aeval x) P)<VAR>h' : IsUnit ((aeval x) (derivative P))<VAR>r₁ r₂ : S<VAR>x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0<VAR>x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0<VAR>hr₁ : IsNilpotent (r₁ - x)<VAR>hr₁' : (aeval r₁) P = 0<VAR>hr₂ : IsNilpotent (r₂ - x)<VAR>hr₂' : (aeval r₂) P = 0<GOAL>r₁ = r₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>c : Ordinal.{u_2}<VAR>hc : ℵ₀ < c.cof<VAR>hf : ∀ i < c, f i < c<VAR>a : Ordinal.{u_2}<GOAL>Cardinal.lift.{u_2, 0} #Unit < c.cof
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Prime ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(maximalIdeal ℤ_[p]).IsPrime
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑p ≠ 0
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto (fun a => a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : μ sᶜ = 0<GOAL>(fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : s ∈ ae μ<GOAL>(fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : s ∈ ae μ<GOAL>∀ a ∈ s, (if a ∈ s then f a else g a) = f a
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>int_nonzero : ∫ (x : G), f x ∂μ ≠ 0<GOAL>↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>int_nonzero : ∫ (x : G), f x ∂μ ≠ 0<VAR>this : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ<GOAL>↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>int_nonzero : ∫ (x : G), f x ∂μ ≠ 0<VAR>this : ∫ (x : G), f x ∂μ' = μ'.haarScalarFactor μ • ∫ (x : G), f x ∂μ<GOAL>↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>1 + m ≤ n ↔ m < n
<VAR>ι✝ : Type u_1<VAR>R✝ : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : Finite ι✝<VAR>inst✝⁸ : CommSemiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ N<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : Fintype ι<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>w : ι → R<GOAL>((piEquiv ι R M) v) w = ∑ i : ι, w i • v i
<VAR>ι✝ : Type u_1<VAR>R✝ : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : Finite ι✝<VAR>inst✝⁸ : CommSemiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ N<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>inst✝³ : Fintype ι<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>w : ι → R<GOAL>∑ x : ι, ((Pi.basisFun R ι).repr w) x • v x = ∑ i : ι, w i • v i
<VAR>a b : Prop<GOAL>Xor' a b ↔ (¬a ↔ b)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>this : dist x y ≤ dist x (f x) + dist y (f y) + ↑K * dist x y<GOAL>dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<GOAL>Set.range ⇑(s.orderEmbOfFin h) = ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>p : A<VAR>hp : p ∈ restrictScalars R (span S t)<VAR>s0 : S<VAR>y : A<VAR>hy : y ∈ t<GOAL>s0 • y ∈ span R (s • t)