ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>((Option.map (fun n => F a (ofNat Code n)) (List.range (n + 4))[m]?).bind fun a_1 => (Option.map (fun n => F a (ofNat Code n)) (List.range (n + 4))[(unpair m).1]?).bind fun a_2 => Option.map ((fun s₂ => bif n.bodd then bif n.div2.bodd then rf a (ofNat Code m, a_1) else pc a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂) else bif n.div2.bodd then co a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂) else pr a (ofNat Code (unpair m).1, ofNat Code (unpair m).2, a_2, s₂)) ∘ fun n => F a (ofNat Code n)) (List.range (n + 4))[(unpair m).2]?) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>m1 : (unpair m).1 < n + 4<VAR>m2 : (unpair m).2 < n + 4<GOAL>(bif n.bodd then bif n.div2.bodd then rf a (ofNat Code n.div2.div2, F a (ofNat Code n.div2.div2)) else pc a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2)) else bif n.div2.bodd then co a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2)) else pr a (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2))) = F a (ofNat Code (n + 4))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : CommRing B<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra A K<VAR>inst✝¹² : Algebra B L<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : IsScalarTower A B L<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsFractionRing A K<VAR>inst✝⁴ : IsIntegralClosure B A L<VAR>inst✝³ : IsFractionRing B L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsDomain B<VAR>I J : Submodule B L<GOAL>I ≤ Jᵛ ↔ J ≤ Iᵛ
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<VAR>this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x✝ : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<VAR>this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯<VAR>x y : α<GOAL>dist x y ≤ ↑(Kf⁻¹ - Kg)⁻¹ * dist (f x * g x) (f y * g y)
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x✝ : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<VAR>this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯<VAR>x y : α<GOAL>dist x y ≤ dist (f x * g x) (f y * g y) / ↑(Kf⁻¹ - Kg)
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x✝ : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<VAR>this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯<VAR>x y : α<GOAL>dist x y * ↑(Kf⁻¹ - Kg) ≤ dist (f x * g x) (f y * g y)
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x✝ : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<VAR>this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯<VAR>x y : α<GOAL>↑Kf⁻¹ * dist x y - ↑Kg * dist x y ≤ dist (f x * g x) (f y * g y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<GOAL>HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<VAR>e_1✝ : HomogeneousLocalization 𝒜 (Submonoid.powers f) = ↑(CommRingCat.of (A⁰_ f))<GOAL>HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<VAR>e_1✝ : HomogeneousLocalization 𝒜 (Submonoid.powers f) = ↑(CommRingCat.of (A⁰_ f))<GOAL>Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<VAR>e_1✝ : HomogeneousLocalization 𝒜 (Submonoid.powers f) = ↑(CommRingCat.of (A⁰_ f))<GOAL>Localization.mk 0 ⟨f ^ i, ⋯⟩ = 0
<VAR>x y : ℝ<GOAL>range arcsin = Icc (-(π / 2)) (π / 2)
<VAR>x y : ℝ<GOAL>Subtype.val '' range (IccExtend arcsin.proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<GOAL>μ (⋃ b, s b) = μ (⋃ b, t b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<VAR>b : β<VAR>hb : μ (t b) = ⊤<GOAL>μ (⋃ b, s b) = μ (⋃ b, t b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<VAR>htop : ¬∃ b, μ (t b) = ⊤<GOAL>μ (⋃ b, s b) = μ (⋃ b, t b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<VAR>htop : ∀ (b : β), μ (t b) ≠ ⊤<GOAL>μ (⋃ b, s b) = μ (⋃ b, t b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<VAR>htop : ∀ (b : β), μ (t b) ≠ ⊤<GOAL>μ (⋃ b, t b) ≤ μ (⋃ b, s b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>inst✝ : Countable β<VAR>s t : β → Set α<VAR>hsub : ∀ (b : β), s b ⊆ t b<VAR>h_le : ∀ (b : β), μ (t b) ≤ μ (s b)<VAR>htop : ∀ (b : β), μ (t b) ≠ ⊤<VAR>M : Set α → Set α := toMeasurable μ<VAR>H : ∀ (b : β), M (t b) ∩ M (⋃ b, s b) =ᶠ[ae μ] M (t b)<GOAL>μ (⋃ b, t b) ≤ μ (⋃ b, s b)
<GOAL>2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = ⊥
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤ ⊥
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤ LinearMap.ker (((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasCoproducts C<VAR>inst✝ : HasImages C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, g ≤ f<GOAL>sSup s ≤ f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasCoproducts C<VAR>inst✝ : HasImages C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, g ≤ f<GOAL>underlying.obj (sSup s) ⟶ underlying.obj f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasCoproducts C<VAR>inst✝ : HasImages C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>k : ∀ g ∈ s, g ≤ f<GOAL>?f ≫ f.arrow = (sSup s).arrow
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<GOAL>(μ (t ∩ s)).toReal • 1 = (μ (t ∩ s)).toReal
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>(G.nonuniformWitnesses ε s t).1 ⊆ s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>(⋯.choose, ⋯.choose).1 ⊆ s
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>a ∈ LocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>a ∈ nonunits ↥A ↔ A.valuation ↑a < 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>¬IsUnit a ↔ A.valuation ↑a < 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>¬A.valuation ↑a = 1 ↔ A.valuation ↑a < 1
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<GOAL>Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<GOAL>ContinuousOn (fun b => ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)) ((a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<GOAL>↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) = a.coordChange he he' b