ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<VAR>a : R<VAR>ha : a ∈ J<VAR>s : R<VAR>hs : s ∈ P.primeCompl<VAR>eq : (algebraMap R (Localization.AtPrime P)) (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<GOAL>False
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<VAR>a : R<VAR>ha : a ∈ J<VAR>s : R<VAR>hs : s ∈ P.primeCompl<VAR>eq✝ : (algebraMap R (Localization.AtPrime P)) (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<VAR>m : R<VAR>hm : m ∈ P.primeCompl<VAR>eq : ↑⟨m, hm⟩ * (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<GOAL>False
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<VAR>a : R<VAR>ha : a ∈ J<VAR>s : R<VAR>hs : s ∈ P.primeCompl<VAR>eq✝ : (algebraMap R (Localization.AtPrime P)) (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<VAR>m : R<VAR>hm : m ∈ P.primeCompl<VAR>eq : ↑⟨m, hm⟩ * (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<GOAL>s * m * x ∈ J
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<VAR>a : R<VAR>ha : a ∈ J<VAR>s : R<VAR>hs : s ∈ P.primeCompl<VAR>eq✝ : (algebraMap R (Localization.AtPrime P)) (x * ↑(⟨a, ha⟩, ⟨s, hs⟩).2 - ↑(⟨a, ha⟩, ⟨s, hs⟩).1) = 0<VAR>m : R<VAR>hm : m ∈ P.primeCompl<VAR>eq : s * (m * x) = m * a<GOAL>s * m * x ∈ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>S : Set (Subsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>S : Set (Subsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ‖∫ (y : Ω), f y ∂(condexpKernel μ m) ω‖) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ‖∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω‖) μ
<VAR>P : Type u_1<VAR>inst✝¹ : Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>inst✝ : Encodable ι<VAR>𝒟 : ι → Cofinal P<VAR>i : ι<GOAL>(match Encodable.decode (Encodable.encode i) with | none => sequenceOfCofinals p 𝒟 (Encodable.encode i) | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈ 𝒟 i
<VAR>P : Type u_1<VAR>inst✝¹ : Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>inst✝ : Encodable ι<VAR>𝒟 : ι → Cofinal P<VAR>i : ι<GOAL>(match some i with | none => sequenceOfCofinals p 𝒟 (Encodable.encode i) | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈ 𝒟 i
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t u v A B : Set E<GOAL>Balanced 𝕜 s ↔ Metric.closedBall 0 1 • s ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ x : α<VAR>hx : x ∈ Ici a<VAR>y : α<VAR>hy : y ∈ Ici a<VAR>hxy : x < y<GOAL>projIci a x < projIci a y
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r✝ : R[X]<VAR>inst✝ : SMulZeroClass S R<VAR>r : S<VAR>p : R[X]<VAR>i : ℕ<VAR>hi : i ∈ (r • p).support<GOAL>i ∈ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r✝ : R[X]<VAR>inst✝ : SMulZeroClass S R<VAR>r : S<VAR>p : R[X]<VAR>i : ℕ<VAR>hi : ¬r • p.coeff i = 0<GOAL>¬p.coeff i = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r✝ : R[X]<VAR>inst✝ : SMulZeroClass S R<VAR>r : S<VAR>p : R[X]<VAR>i : ℕ<VAR>hi : p.coeff i = 0<GOAL>r • p.coeff i = 0
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : Monoid M✝<VAR>inst✝⁴ : SetLike B M✝<VAR>inst✝³ : SubmonoidClass B M✝<VAR>S : B<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>m : Multiset ↥S<GOAL>(Multiset.map Subtype.val m).prod ∈ S
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : Monoid M✝<VAR>inst✝⁴ : SetLike B M✝<VAR>inst✝³ : SubmonoidClass B M✝<VAR>S : B<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>m : Multiset ↥S<GOAL>↑m.prod ∈ S
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ioo a b) (Ioo (a + d) (b + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))
<VAR>x : ℝ<GOAL>↑(Real.arctan x) = (↑x).arctan
<VAR>x : ℝ<GOAL>↑(Real.arctan x) = (↑(Real.tan (Real.arctan x))).arctan
<VAR>x : ℝ<GOAL>↑(Real.arctan x) ≠ ↑π / 2
<VAR>x : ℝ<GOAL>-(π / 2) < (↑(Real.arctan x)).re
<VAR>x : ℝ<GOAL>(↑(Real.arctan x)).re ≤ π / 2
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>pk : Prime k<VAR>dk : k ∣ n<VAR>dkk : ¬k * k ∣ n<VAR>o : Option ℕ<VAR>H : (n / k).MinSqFacProp o<GOAL>n.MinSqFacProp o
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>pk : Prime k<VAR>dk : k ∣ n<VAR>dkk : ¬k * k ∣ n<VAR>o : Option ℕ<VAR>H : (n / k).MinSqFacProp o<VAR>this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n<GOAL>n.MinSqFacProp o
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<GOAL>(a / b).toNNReal = a.toNNReal / b.toNNReal
<VAR>n m : ℕ<VAR>h : m ≤ n<GOAL>Ico n m = []
<VAR>n : ℕ<VAR>x✝ : Decidable (↑n).Dom<GOAL>(↑n).toWithTop = ↑n
<VAR>n : ℕ<VAR>x✝ : Decidable (↑n).Dom<GOAL>(↑n).toWithTop = (↑n).toWithTop
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>↑a.sqrt ≤ √↑a
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>↑a.sqrt ^ 2 ≤ ↑a
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>a.sqrt ^ 2 ≤ a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>inversion c R '' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : f ≤ g<VAR>n : ℕ<VAR>x : ℝ<GOAL>(f ^ n) x ≤ (g ^ n) x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(AddOpposite.unop (addOppositeEquiv x)).orderTop = x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : AddOpposite.unop (addOppositeEquiv x) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : ∀ (a : Γ), AddOpposite.unop (x.coeff a) = 0 a then ⊤ else ↑(⋯.min ⋯)) = if h : ∀ (a : Γ), x.coeff a = coeff 0 a then ⊤ else ↑(⋯.min ⋯)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>inst✝ : CompleteSpace E<GOAL>∃ N K, ContractingWith K FunSpace.next^[N]
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>inst✝ : CompleteSpace E<VAR>N : ℕ<VAR>hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1<GOAL>∃ N K, ContractingWith K FunSpace.next^[N]
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>inst✝ : CompleteSpace E<VAR>N : ℕ<VAR>hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1<VAR>this : 0 ≤ (↑v.L * v.tDist) ^ N / ↑N !<GOAL>∃ N K, ContractingWith K FunSpace.next^[N]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : (x : β) → Decidable (f x ≤ g x)<VAR>f' g' : β → γ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : ContinuousOn f' {x | f x ≤ g x}<VAR>hg' : ContinuousOn g' {x | g x ≤ f x}<VAR>hfg : ∀ (x : β), f x = g x → f' x = g' x<GOAL>Continuous fun x => if f x ≤ g x then f' x else g' x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : (x : β) → Decidable (f x ≤ g x)<VAR>f' g' : β → γ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : ContinuousOn f' {x | f x ≤ g x}<VAR>hg' : ContinuousOn g' {x | g x ≤ f x}<VAR>hfg : ∀ (x : β), f x = g x → f' x = g' x<GOAL>ContinuousOn f' (closure {x | f x ≤ g x})
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : (x : β) → Decidable (f x ≤ g x)<VAR>f' g' : β → γ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : ContinuousOn f' {x | f x ≤ g x}<VAR>hg' : ContinuousOn g' {x | g x ≤ f x}<VAR>hfg : ∀ (x : β), f x = g x → f' x = g' x<GOAL>closure {x | ¬f x ≤ g x} ⊆ {x | g x ≤ f x}
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<GOAL>ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n { byteIdx := utf8Len [] } = { byteIdx := utf8Len [] + utf8Len (List.take n m) }<GOAL>ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor l (List.take n m) (List.drop n m ++ r) { str := s.str, startPos := s.startPos, stopPos := s.startPos + { byteIdx := utf8Len (List.take n m) } }
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor l (List.take n m) (List.drop n m ++ r) { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor l (List.take n m) (List.drop n m ++ r) { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>{ str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }.str.data = l ++ List.take n m ++ (List.drop n m ++ r)
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>{ str := { data := l ++ (List.take n m ++ List.drop n m ++ r) }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) } }.str.data = l ++ List.take n m ++ (List.drop n m ++ r)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<VAR>j k : n<GOAL>(diagonal v).updateColumn i (Pi.single i x) j k = diagonal (Function.update v i x) j k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<VAR>j : n<GOAL>(diagonal v).updateColumn i (Pi.single i x) j j = diagonal (Function.update v i x) j j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<VAR>j k : n<VAR>hjk : j ≠ k<GOAL>(diagonal v).updateColumn i (Pi.single i x) j k = diagonal (Function.update v i x) j k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>e : r ≃r s<VAR>x : β<VAR>y : α<GOAL>r (e.symm x) y ↔ s x (e y)
<VAR>M : Type u_1<VAR>inst✝⁴ : Nonempty M<VAR>inst✝³ : Semigroup M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CompactSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}<GOAL>∃ N ∈ S, ∀ N' ∈ S, N' ⊆ N → N' = N
<VAR>M : Type u_1<VAR>inst✝⁴ : Nonempty M<VAR>inst✝³ : Semigroup M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CompactSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}<VAR>c : Set (Set M)<VAR>hcs : c ⊆ S<VAR>hc : IsChain (fun x x_1 => x ⊆ x_1) c<GOAL>∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
<VAR>M : Type u_1<VAR>inst✝⁴ : Nonempty M<VAR>inst✝³ : Semigroup M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CompactSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}<VAR>c : Set (Set M)<VAR>hcs : c ⊆ S<VAR>hc : IsChain (fun x x_1 => x ⊆ x_1) c<GOAL>(⋂₀ c).Nonempty
<VAR>M : Type u_1<VAR>inst✝⁴ : Nonempty M<VAR>inst✝³ : Semigroup M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CompactSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}<VAR>c : Set (Set M)<VAR>hcs : c ⊆ S<VAR>hc : IsChain (fun x x_1 => x ⊆ x_1) c<VAR>m : M<VAR>hm : m ∈ ⋂₀ c<VAR>m' : M<VAR>hm' : m' ∈ ⋂₀ c<GOAL>m * m' ∈ ⋂₀ c
<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>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<GOAL>(starRingEnd 𝕜) ⟪T x, y⟫_𝕜 = ⟪T y, x⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β → σ<VAR>h : α → γ → σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>hh : Primrec₂ h<VAR>a : α<GOAL>(bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2) else Option.map (g a) (decode (encode (f a)).div2)) = some (Sum.casesOn (f a) (g a) (h a))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m₁ : α → β → β'<VAR>m₂ : α → γ → γ'<VAR>n' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)<VAR>s : Set ε<VAR>t₁ : Set β'<VAR>u₁ : Set α<VAR>hu₁ : u₁ ∈ f<VAR>v : Set β<VAR>hv : v ∈ g<VAR>ht₁ : image2 m₁ u₁ v ⊆ t₁<VAR>t₂ : Set γ'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>u₂ : Set α<VAR>hu₂ : u₂ ∈ f<VAR>w : Set γ<VAR>hw : w ∈ h<VAR>ht₂ : image2 m₂ u₂ w ⊆ t₂<GOAL>s ∈ map₂ m f (map₂ n g h)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m₁ : α → β → β'<VAR>m₂ : α → γ → γ'<VAR>n' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)<VAR>s : Set ε<VAR>t₁ : Set β'<VAR>u₁ : Set α<VAR>hu₁ : u₁ ∈ f<VAR>v : Set β<VAR>hv : v ∈ g<VAR>ht₁ : image2 m₁ u₁ v ⊆ t₁<VAR>t₂ : Set γ'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>u₂ : Set α<VAR>hu₂ : u₂ ∈ f<VAR>w : Set γ<VAR>hw : w ∈ h<VAR>ht₂ : image2 m₂ u₂ w ⊆ t₂<GOAL>image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m₁ : α → β → β'<VAR>m₂ : α → γ → γ'<VAR>n' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)<VAR>s : Set ε<VAR>t₁ : Set β'<VAR>u₁ : Set α<VAR>hu₁ : u₁ ∈ f<VAR>v : Set β<VAR>hv : v ∈ g<VAR>ht₁ : image2 m₁ u₁ v ⊆ t₁<VAR>t₂ : Set γ'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>u₂ : Set α<VAR>hu₂ : u₂ ∈ f<VAR>w : Set γ<VAR>hw : w ∈ h<VAR>ht₂ : image2 m₂ u₂ w ⊆ t₂<GOAL>image2 m₁ (u₁ ∩ u₂) v ⊆ t₁
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m₁ : α → β → β'<VAR>m₂ : α → γ → γ'<VAR>n' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)<VAR>s : Set ε<VAR>t₁ : Set β'<VAR>u₁ : Set α<VAR>hu₁ : u₁ ∈ f<VAR>v : Set β<VAR>hv : v ∈ g<VAR>ht₁ : image2 m₁ u₁ v ⊆ t₁<VAR>t₂ : Set γ'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>u₂ : Set α<VAR>hu₂ : u₂ ∈ f<VAR>w : Set γ<VAR>hw : w ∈ h<VAR>ht₂ : image2 m₂ u₂ w ⊆ t₂<GOAL>image2 m₂ (u₁ ∩ u₂) w ⊆ t₂
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : CompleteSpace E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>L : E →L[𝕜] F<VAR>hf : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₂ <:+: l₁ ++ (l₂ ++ l₃)
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₂ <:+: l₁ ++ l₂ ++ l₃
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<GOAL>∃ p, p ∈ normalizedFactors x
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<VAR>p' : α<VAR>hp' : Irreducible p'<VAR>hp'x : p' ∣ x<GOAL>∃ p, p ∈ normalizedFactors x
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<VAR>p' : α<VAR>hp' : Irreducible p'<VAR>hp'x : p' ∣ x<VAR>p : α<VAR>hp : p ∈ normalizedFactors x<VAR>right✝ : p' ~ᵤ p<GOAL>∃ p, p ∈ normalizedFactors x
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<GOAL>(IsLocalization.map S' f ⋯).Finite