ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<VAR>s : Set (α × ℝ)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), (ρ.condKernel a) (Prod.mk a ⁻¹' (Prod.map id (embeddingReal Ω) ⁻¹' s)) ∂ρ.fst = ∫⁻ (a : α), ((ρ.condKernel.map f ⋯) a) (Prod.mk a ⁻¹' s) ∂ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<VAR>s : Set (α × ℝ)<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>o : Option α<GOAL>a ∈ o.toFinset ↔ a ∈ o
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<GOAL>k * 0 = 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>l : Multiset S[X]<GOAL>∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max ⋯ 0 (Multiset.map natDegree ⟦a⟧)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : End X<GOAL>α.symm.conj (α.conj f) = f
<VAR>θ : Angle<GOAL>0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
<VAR>θ : Angle<GOAL>0 ≤ (↑θ.toReal).cos ↔ |θ.toReal| ≤ π / 2
<VAR>θ : Angle<GOAL>0 ≤ Real.cos θ.toReal ↔ -(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2
<VAR>θ : Angle<VAR>h : 0 ≤ Real.cos θ.toReal<GOAL>-(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2
<VAR>θ : Angle<VAR>h : 0 ≤ Real.cos θ.toReal<VAR>hn : ¬(-(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2)<GOAL>False
<VAR>θ : Angle<VAR>h : 0 ≤ Real.cos θ.toReal<VAR>hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal<GOAL>False
<VAR>θ : Angle<VAR>h : 0 ≤ Real.cos θ.toReal<VAR>hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal<GOAL>Real.cos θ.toReal < 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>m : M<VAR>p : Submonoid M<GOAL>closure {m} ≤ p ↔ m ∈ p
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : H₁.Normal<VAR>hH₂ : H₂.Normal<VAR>hdis : Disjoint H₁ H₂<VAR>x y : G<VAR>hx : x ∈ H₁<VAR>hy : y ∈ H₂<GOAL>x * y * x⁻¹ * y⁻¹ = 1
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : H₁.Normal<VAR>hH₂ : H₂.Normal<VAR>hdis : Disjoint H₁ H₂<VAR>x y : G<VAR>hx : x ∈ H₁<VAR>hy : y ∈ H₂<GOAL>x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h : 0 < x<GOAL>logb b x < 0 ↔ 1 < x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommSemiring R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1164305) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommSemiring R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>this : 0 ≤ cfcₙ id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x<GOAL>0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x
<VAR>x y : ℝ<VAR>a b : Cauchy abs<GOAL>(Real.add { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy + { cauchy := b }.cauchy
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<GOAL>f ∈ closure S ↔ (fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ orbit (↥(closure S)) x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<VAR>hf : f ∈ closure S<GOAL>(fixedBy α f)ᶜ.Finite
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<GOAL>((fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ orbit (↥(closure S)) x) → f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x<VAR>supp : Set α := (fixedBy α f)ᶜ<VAR>fin : supp.Finite<VAR>supp_eq : supp = (fixedBy α f)ᶜ<GOAL>f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x<VAR>supp : Set α := (fixedBy α f)ᶜ<VAR>fin : supp.Finite<VAR>supp_eq : supp = (fixedBy α f)ᶜ<GOAL>(fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<GOAL>∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<GOAL>∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ ∅ → f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<GOAL>∀ {a : α} {s : Set α}, a ∉ s → s.Finite → (∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S) → ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ insert a s → f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<VAR>a : α<VAR>s : Set α<VAR>ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x<VAR>supp_subset : (fixedBy α f)ᶜ ⊆ insert a s<GOAL>f ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<VAR>a : α<VAR>s : Set α<VAR>ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x<VAR>supp_subset : (fixedBy α f)ᶜ ⊆ insert a s<VAR>b : α<GOAL>(swap (f a) a * f) b ∈ orbit (↥(closure S)) b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>supp : Set α<VAR>fin : supp.Finite<VAR>a : α<VAR>s : Set α<VAR>ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x<VAR>supp_subset : (fixedBy α f)ᶜ ⊆ insert a s<VAR>b : α<VAR>hb : b ∈ (fixedBy α (swap (f a) a * f))ᶜ<GOAL>b ∈ s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>m n : ℕ<GOAL>constantCoeff (wittNSMul p m n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>m n : ℕ<GOAL>constantCoeff (m • X 0) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>‖x‖ = ↑p ^ (-x.valuation)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>↑x ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : ↑x = 0<GOAL>x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<GOAL>x ∈ image Eq s ↔ x ∈ s
<VAR>n m l : ℕ<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
<VAR>n m l : ℕ<VAR>hml : m ≤ l<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
<VAR>n m l : ℕ<VAR>hlm : l ≤ m<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<VAR>this : Iₚ ≠ ⊤<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<VAR>this : Iₚ ≠ ⊤<VAR>M : Ideal Sₚ<VAR>hM : M.IsMaximal<VAR>hM' : Iₚ ≤ M<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<VAR>this : Iₚ ≠ ⊤<VAR>M : Ideal Sₚ<VAR>hM : M.IsMaximal<VAR>hM' : Iₚ ≤ M<GOAL>comap (algebraMap R S) (comap (algebraMap S Sₚ) M) ≤ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<VAR>this : Iₚ ≠ ⊤<VAR>M : Ideal Sₚ<VAR>hM : M.IsMaximal<VAR>hM' : Iₚ ≤ M<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R S) (comap (algebraMap S Sₚ) M)<GOAL>x ∈ P
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hI : comap (algebraMap R S) I ≤ P<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I<VAR>hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I<VAR>this : Iₚ ≠ ⊤<VAR>M : Ideal Sₚ<VAR>hM : M.IsMaximal<VAR>hM' : Iₚ ≤ M<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R S) (comap (algebraMap S Sₚ) M)<VAR>hx' : x ∉ P<GOAL>False
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<GOAL>Tendsto (fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<GOAL>Tendsto (fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<GOAL>Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<VAR>f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast<GOAL>Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<VAR>f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast<VAR>cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<GOAL>Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<VAR>f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast<VAR>cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<VAR>hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<GOAL>Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<VAR>f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast<VAR>cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<VAR>hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<VAR>hf₂ : ClosedEmbedding ⇑(lcRow0Extend hcd)<GOAL>Tendsto (mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, -↑1], Int.cast ∘ cd]<VAR>hmB : Continuous mB<VAR>f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => (↑g).map Int.cast<VAR>cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m => m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<VAR>hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))<VAR>hf₂ : ClosedEmbedding ⇑(lcRow0Extend hcd)<GOAL>(mB ∘ fun g => (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) = ⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a => ↑a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x y : E<GOAL>⟪(adjoint T * T) x, y⟫_𝕜 = ⟪x, (adjoint T * T) y⟫_𝕜
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hm : m.Sized<VAR>hr : r.Sized<GOAL>(l.node4L x m y r).Sized
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>Tendsto (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>(fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>h_ae_eq : f i =ᶠ[ae μ] f' i<GOAL>μ {x | ε ≤ dist (f' i x) (g' x)} = μ {x | ε ≤ dist (f i x) (g x)}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>h_ae_eq : f i =ᶠ[ae μ] f' i<GOAL>{x | ε ≤ dist (f' i x) (g' x)} =ᶠ[ae μ] {x | ε ≤ dist (f i x) (g x)}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>h_ae_eq : f i =ᶠ[ae μ] f' i<VAR>x : α<VAR>hxf : f i x = f' i x<VAR>hxg : g x = g' x<GOAL>{x | ε ≤ dist (f' i x) (g' x)} x = {x | ε ≤ dist (f i x) (g x)} x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>h_ae_eq : f i =ᶠ[ae μ] f' i<VAR>x : α<VAR>hxf : f i x = f' i x<VAR>hxg : g x = g' x<GOAL>{x | ε ≤ dist (f' i x) (g' x)} x ↔ {x | ε ≤ dist (f i x) (g x)} x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Dist E<VAR>l : Filter ι<VAR>f f' : ι → α → E<VAR>g g' : α → E<VAR>h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i<VAR>h_right : g =ᶠ[ae μ] g'<VAR>h_tendsto : TendstoInMeasure μ f l g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>h_ae_eq : f i =ᶠ[ae μ] f' i<VAR>x : α<VAR>hxf : f i x = f' i x<VAR>hxg : g x = g' x<GOAL>ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 1<VAR>hab : b ≤ a<GOAL>mabs a ≤ mabs b
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 1<VAR>hab : b ≤ a<GOAL>a⁻¹ ≤ b⁻¹
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData = leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>op x • ↑s = op y • ↑s ↔ y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<VAR>x✝¹ x✝ : R<GOAL>(algebraMap R ℍ[R,c₁,c₂]) x✝¹ = (algebraMap R ℍ[R,c₁,c₂]) x✝ → x✝¹ = x✝
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>filter p (n • s) = n • filter p s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>filter p (n • 0) = n • filter p 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>a : α<VAR>m : M<VAR>n : N<VAR>a' : α<GOAL>(zipWith f hf (single a m) (single a n)) a' = (single a (f m n)) a'