ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>hb_lt_one : b' < 1<VAR>hb : b' ∈ Set.Ioo 0 1<VAR>hb' : ∀ (i : α), b' ≤ b i<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>hq_poly : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b' * x) x, (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)<VAR>h_tendsto : Tendsto (fun x => b' * x) atTop atTop<VAR>n : ℕ<VAR>hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)<VAR>h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)<VAR>h_ge_n₀ : R.n₀ ≤ n<VAR>h_n_pos : 0 < n<VAR>h_bn : 1 < b' * ↑n<GOAL>b i * ↑n ∈ Set.Icc (b' * ↑n) ↑n
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a ∣ b * ↑u ↔ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>l : List (Option α)<GOAL>(some x :: l).reduceOption = x :: l.reduceOption
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>hl : l.HasBasis (fun x => True) b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ blimsup u l p<GOAL>∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>hl : l.HasBasis (fun x => True) b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ blimsup u l p<VAR>f : ↑{i | True} → β<VAR>hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i<GOAL>∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<GOAL>∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<GOAL>∀ (ss : WSeq α), a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>ss : WSeq α<VAR>h : a ∈ ss<GOAL>∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>ss✝ : WSeq α<VAR>h : a ∈ ss✝<VAR>b : α<VAR>ss : WSeq α<VAR>o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s<VAR>s : WSeq α<VAR>S : WSeq (WSeq α)<GOAL>s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>ss✝ : WSeq α<VAR>h : a ∈ ss✝<VAR>ss : WSeq α<VAR>IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s<VAR>s : WSeq α<VAR>S : WSeq (WSeq α)<GOAL>s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y : ℝ≥0∞<VAR>hp : (x, y) ∈ {p | p ≠ (⊤, ⊤)}<GOAL>ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y : ℝ≥0∞<VAR>hp : ¬(x = ⊤ ∧ y = ⊤)<GOAL>ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)
<VAR>ι : Type u_1<VAR>κ✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>κ : ι → Type u_6<VAR>t : (i : ι) → Finset (κ i)<VAR>f : ((i : ι) → i ∈ univ → κ i) → β<GOAL>∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a x_1 => x a
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>Even (∑ i ∈ s, f i) ↔ Even (filter (fun x => Odd (f x)) s).card
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>(Even (∑ x ∈ filter (fun x => Even (f x)) s, f x) ↔ Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x)) ↔ Even (filter (fun x => Odd (f x)) s).card
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>Even (∑ x ∈ filter (fun x => ¬Even (f x)) s, f x) ↔ Even (filter (fun x => Odd (f x)) s).card
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>(∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) % 2 = 0 ↔ Even (filter (fun x => Odd (f x)) s).card
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>(∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even (filter (fun x => Odd (f x)) s).card
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>inst✝ : CountableInterFilter f<VAR>hstf : f ≤ 𝓟 (s ∩ t)<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>inst✝ : CountableInterFilter f<VAR>hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>inst✝ : CountableInterFilter f<VAR>hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t<VAR>x : X<VAR>hsx : x ∈ s<VAR>hx : ClusterPt x f<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>inst✝ : CountableInterFilter f<VAR>hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t<VAR>x : X<VAR>hsx : x ∈ s<VAR>hx : ClusterPt x f<VAR>hxt : x ∈ t<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : ℕ → E''<GOAL>(∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖1‖) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
<VAR>b n : ℕ<GOAL>log b n ≤ clog b n
<VAR>b n : ℕ<VAR>hb : b ≤ 1<GOAL>log b n ≤ clog b n
<VAR>b n : ℕ<VAR>hb : 1 < b<GOAL>log b n ≤ clog b n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>s : Set α<GOAL>(uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>s : Set α<GOAL>↑(Finset.filter (fun x => x ∈ s) Finset.univ).card / ↑Finset.univ.card = ↑(Finset.filter (fun x => x ∈ s) Finset.univ).card / ↑(Fintype.card α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set (Set α)<GOAL>⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₁'}<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁'p₂ : p₁' ≠ p₂<VAR>hp₃p₂ : ¬p₃ = p₂<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₁'}<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁'p₂ : p₁' ≠ p₂<VAR>hp₃p₂ : ¬p₃ = p₂<VAR>hw : Wbtw ℝ p₁ p₂ p₁'<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₁'}<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁'p₂ : p₁' ≠ p₂<VAR>hp₃p₂ : ¬p₃ = p₂<VAR>hw : Wbtw ℝ p₂ p₁' p₁<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₁'}<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁'p₂ : p₁' ≠ p₂<VAR>hp₃p₂ : ¬p₃ = p₂<VAR>hw : Wbtw ℝ p₁' p₁ p₂<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>(∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>n : Type u_1<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : (toMatrix' Q).PosDef<GOAL>PosDef Q
<VAR>n : Type u_1<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : (toMatrix' Q).PosDef<GOAL>(LinearMap.BilinMap.toQuadraticMap ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I I' : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis' I R<VAR>hI' : M.Basis' I' R<GOAL>∃ x ∈ I' \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I I' : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>hI' : M.Basis I' (R ∩ M.E)<GOAL>∃ x ∈ I' \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M.Basis (B' ∩ (R ∩ M.E)) (R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M.Basis (B' ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M✶.Basis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M✶.Basis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M✶.Basis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hI' : M✶.Basis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>B : Set α<VAR>hI' : M.Basis (B ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J✝ X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>B : Set α<VAR>hI' : M.Basis (B ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<VAR>J : Set α<VAR>hJ : M.Basis J (B ∩ (R ∩ M.E))<VAR>hIJ : I ⊆ J<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>B : Set α<VAR>hI' : M.Basis (B ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<VAR>hJ : M.Basis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))<VAR>hIJ : I ⊆ B ∩ (R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>B : Set α<VAR>hI' : M.Basis (B ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<VAR>hJ : M.Basis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))<VAR>hIJ : I ⊆ B ∩ (R ∩ M.E)<VAR>hIJ' : I ⊂ B ∩ (R ∩ M.E)<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : M.Indep I<VAR>hIY : I ⊆ R<VAR>hIn : ¬M.Basis I (R ∩ M.E)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>B : Set α<VAR>hI' : M.Basis (B ∩ (R ∩ M.E)) (R ∩ M.E)<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<VAR>hBIB' : B ⊆ I ∪ B'<VAR>hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)<VAR>hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))<VAR>h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)<VAR>hJ : M.Basis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))<VAR>hIJ : I ⊆ B ∩ (R ∩ M.E)<VAR>hIJ' : I ⊂ B ∩ (R ∩ M.E)<VAR>e : α<VAR>he : e ∈ B ∩ (R ∩ M.E) ∧ e ∉ I<GOAL>∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, (fun I => M.Indep I ∧ I ⊆ R) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J X Y : Set α<VAR>M : Matroid α<VAR>R A : Set α<VAR>hAX : A ⊆ R<VAR>I : Set α<VAR>hI : M.Indep I<VAR>right✝ : I ⊆ R<VAR>hIA : I ⊆ A<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => M.Indep I ∧ I ⊆ R) Y ∧ I ⊆ Y ∧ Y ⊆ A}).Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J✝ X Y : Set α<VAR>M : Matroid α<VAR>R A : Set α<VAR>hAX : A ⊆ R<VAR>I : Set α<VAR>hI : M.Indep I<VAR>right✝ : I ⊆ R<VAR>hIA : I ⊆ A<VAR>J : Set α<VAR>hJ : M.Basis' J A<VAR>hIJ : I ⊆ J<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => M.Indep I ∧ I ⊆ R) Y ∧ I ⊆ Y ∧ Y ⊆ A}).Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J✝ X Y : Set α<VAR>M : Matroid α<VAR>R A : Set α<VAR>hAX : A ⊆ R<VAR>I : Set α<VAR>hI : M.Indep I<VAR>right✝ : I ⊆ R<VAR>hIA : I ⊆ A<VAR>J : Set α<VAR>hJ : M.Basis' J A<VAR>hIJ : I ⊆ J<GOAL>J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => M.Indep I ∧ I ⊆ R) Y ∧ I ⊆ Y ∧ Y ⊆ A}
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I✝ J✝ X Y : Set α<VAR>M : Matroid α<VAR>R A : Set α<VAR>hAX : A ⊆ R<VAR>I : Set α<VAR>hI : M.Indep I<VAR>right✝ : I ⊆ R<VAR>hIA : I ⊆ A<VAR>J : Set α<VAR>hJ : M.Basis' J A<VAR>hIJ : I ⊆ J<GOAL>∀ ⦃y : Set α⦄, (fun I => M.Indep I ∧ I ⊆ R) y ∧ I ⊆ y ∧ y ⊆ A → J ⊆ y → J = y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<GOAL>cfc f a = (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }
<VAR>θ : Angle<GOAL>(↑(π / 2) - θ).sin = θ.cos
<VAR>x✝ : ℝ<GOAL>(↑(π / 2) - ↑x✝).sin = (↑x✝).cos
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ => ‖φ x‖₊
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>J.plusMap η ≫ J.plusLift γ hR = J.plusLift (η ≫ γ) hR
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>J.toPlus P ≫ J.plusMap η ≫ J.plusLift γ hR = η ≫ γ
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>X : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>Y ⊆ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → Y ⊆ F
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>Hf✝ : Monotone f<VAR>a✝ : α<VAR>s : Set α<VAR>Hf : Monotone f<VAR>a : α<VAR>ha : a ∈ upperBounds s<GOAL>f a ∈ upperBounds (f '' s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<GOAL>sSup S = ringConGen fun x y => ∃ c ∈ S, c x y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<GOAL>sSup S = sInf {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<VAR>x✝ : RingCon R<GOAL>x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(M.whiskerLeft (𝟙 N)).hom = (𝟙 (M.tensorBimod N)).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (𝟙 N)).hom = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (𝟙 (M.tensorBimod N)).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ 𝟙 N.X) (M.X ◁ 𝟙 N.X) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ 𝟙 (TensorBimod.X M N)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ 𝟙 (TensorBimod.X M N)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B f f
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : NoMaxOrder α<VAR>b : α<VAR>h : IsSuccLimit (succ b)<GOAL>False