ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : MeasurableSpace E<VAR>μ : Measure E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>b₀ : Basis ι ℝ E<VAR>this : FiniteDimensional ℝ E<GOAL>μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (fundamentalDomain b₀)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : MeasurableSpace E<VAR>μ : Measure E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>b₀ : Basis ι ℝ E<VAR>this : FiniteDimensional ℝ E<GOAL>fundamentalDomain b = ⇑(b.equiv b₀ (Equiv.refl ι)) ⁻¹' fundamentalDomain b₀
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : MeasurableSpace E<VAR>μ : Measure E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>b₀ : Basis ι ℝ E<VAR>this : FiniteDimensional ℝ E<GOAL>b₀.det ⇑b = LinearMap.det ↑(b.equiv b₀ (Equiv.refl ι)).symm
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>dg : q.natDegree < n<GOAL>(p - q).coeff n = p.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>dg : (-q).natDegree < n<GOAL>(p - q).coeff n = p.coeff n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<GOAL>∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (↑f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>nk : ¬∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (↑f j)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>nk : ¬∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (↑f j)<VAR>ε : α<VAR>ε0 : ε > 0<GOAL>∃ i, ∀ j ≥ i, abv (↑f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>ε : α<VAR>ε0 : ε > 0<VAR>nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_1 ≤ x_2), abv (↑f x_2) < x<GOAL>∃ i, ∀ j ≥ i, abv (↑f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>ε : α<VAR>ε0 : ε > 0<VAR>nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_1 ≤ x_2), abv (↑f x_2) < x<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<GOAL>∃ i, ∀ j ≥ i, abv (↑f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>ε : α<VAR>ε0 : ε > 0<VAR>nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_1 ≤ x_2), abv (↑f x_2) < x<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>j : ℕ<VAR>ij : i ≤ j<VAR>hj : abv (↑f j) < ε / 2<GOAL>∃ i, ∀ j ≥ i, abv (↑f j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this : (a : Prop) → Decidable a<VAR>ε : α<VAR>ε0 : ε > 0<VAR>nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_1 ≤ x_2), abv (↑f x_2) < x<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>j : ℕ<VAR>ij : i ≤ j<VAR>hj : abv (↑f j) < ε / 2<VAR>k : ℕ<VAR>jk : k ≥ j<GOAL>abv (↑f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>this✝ : (a : Prop) → Decidable a<VAR>ε : α<VAR>ε0 : ε > 0<VAR>nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_1 ≤ x_2), abv (↑f x_2) < x<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>j : ℕ<VAR>ij : i ≤ j<VAR>hj : abv (↑f j) < ε / 2<VAR>k : ℕ<VAR>jk : k ≥ j<VAR>this : abv (↑f k - ↑f j + ↑f j) < ε / 2 + ε / 2<GOAL>abv (↑f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>f : Filter β<VAR>u v : β → α<VAR>bu : α<VAR>hu : ∀ᶠ (x : β) in f, u x ≤ bu<VAR>bv : α<VAR>hv : ∀ᶠ (x : β) in f, v x ≤ bv<GOAL>∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>m : M<VAR>s : Set M<GOAL>m ∈ span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>m : M<VAR>s : Set M<GOAL>m ∈ span R (_root_.id '' s) ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : AddCommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : StarAddMonoid α<VAR>inst✝ : ContinuousStar α<VAR>f : β → α<VAR>a : α<VAR>h : HasSum f a<GOAL>HasSum (fun b => Star.star (f b)) (Star.star a)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>hk : M ^ k = 0<GOAL>IsUnit M.charpolyRev
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>hk : 1 - X • M.map ⇑C ∣ 1<GOAL>IsUnit M.charpolyRev
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>hk : 1 - X • M.map ⇑C ∣ 1<GOAL>M.charpolyRev ∣ 1
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>hk : 1 - X • M.map ⇑C ∣ 1<GOAL>M.charpolyRev ∣ det 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>s t : Set α<VAR>a b : α<GOAL>∀ (x : Set α), SupClosed ((fun s => {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}) x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>s t✝ : Set α<VAR>a b : α<VAR>s₁ s₂ : Set α<VAR>hs : s₁ ≤ s₂<VAR>h₂ : SupClosed s₂<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s₁<GOAL>t.sup' ht id ∈ s₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : OrderedSemiring α<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : MulActionWithZero α β<VAR>inst✝² : CeilDiv α β<VAR>a : α<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : PosSMulReflectLE α β<VAR>ha : 0 < a<VAR>b : β<GOAL>∀ (c : β), a • b ⌈/⌉ a ≤ c ↔ b ≤ c
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>hj : ¬c.Rel j (c.next j)<GOAL>inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>hj : ¬c.Rel j (c.next j)<GOAL>(inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (φ.f j ≫ inrX φ j) ≫ sndX φ j
<VAR>ι : Sort u_1<VAR>g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>f : ι → ℝ≥0<GOAL>(⨆ i, ↑(f i)).toNNReal = ⨆ i, ((fun i => ↑(f i)) i).toNNReal
<VAR>ι : Sort u_1<VAR>g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>f : ι → ℝ≥0<GOAL>(⨆ i, ↑(f i)).toNNReal = ⨆ i, f i
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>take 1 (drop n l) = [l.get ⟨n, h⟩]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>f : p → α<GOAL>⨆ (h : p), f h = if h : p then f h else sSup ∅
<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 : IsCompact s<GOAL>IsLindelof s
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>a₂ b₂ : σ₂<VAR>h : f₂ a₂ = f₂ b₂<GOAL>(match none with | some b₁ => Reaches₁ f₂ a₂ (tr b₁) | none => f₂ a₂ = none) ↔ match none with | some b₁ => Reaches₁ f₂ b₂ (tr b₁) | none => f₂ b₂ = none
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<GOAL>φ.nilRank ≤ finrank R M
<VAR>n : ℕ<VAR>hn : Even n<VAR>h : n ≠ 0<GOAL>StrictConvexOn ℝ univ fun x => x ^ n
<VAR>n : ℕ<VAR>hn : Even n<VAR>h : n ≠ 0<GOAL>StrictMono (deriv fun a => a ^ n)
<VAR>n : ℕ<VAR>hn : Even n<VAR>h : n ≠ 0<GOAL>StrictMono fun x => ↑n * x ^ (n - 1)
<VAR>n : ℕ<VAR>hn : Even n<VAR>h : 0 < n<GOAL>StrictMono fun x => ↑n * x ^ (n - 1)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<GOAL>ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toPartialHomeomorph)) (e.target ∩ e'.target)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet)<GOAL>ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toPartialHomeomorph)) (e.target ∩ e'.target)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet<GOAL>ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toPartialHomeomorph)) (e.target ∩ e'.target)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet<GOAL>∀ y ∈ e.target ∩ e'.target, ↑(e.symm ≫ₕ e'.toPartialHomeomorph) y = (y.1, e.coordChange e' y.1 y.2)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x✝ : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet<VAR>b : B<VAR>x : F<VAR>hb : (b, x) ∈ e.target ∩ e'.target<GOAL>↑(e.symm ≫ₕ e'.toPartialHomeomorph) (b, x) = ((b, x).1, e.coordChange e' (b, x).1 (b, x).2)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x✝ : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet<VAR>b : B<VAR>x : F<VAR>hb : (b, x) ∈ e.target ∩ e'.target<GOAL>(↑(e.symm ≫ₕ e'.toPartialHomeomorph) (b, x)).1 = ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x✝ : M<VAR>Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet<VAR>b : B<VAR>x : F<VAR>hb : (b, x) ∈ e.target ∩ e'.target<VAR>this : (↑e.symm (b, x)).proj ∈ e'.baseSet<GOAL>(↑(e.symm ≫ₕ e'.toPartialHomeomorph) (b, x)).1 = ((b, x).1, e.coordChange e' (b, x).1 (b, x).2).1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ<GOAL>SeparableSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ<VAR>this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε<GOAL>SeparableSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ<VAR>this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε<VAR>t : Set α<VAR>htc : t.Countable<VAR>ht : univ ⊆ closure t<GOAL>SeparableSpace α
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono f<GOAL>Mono (G.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono f<VAR>this : Mono (F.map f ≫ (α.app Y).hom)<GOAL>Mono (G.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono f<VAR>this : Mono (F.map f ≫ (α.app Y).hom)<GOAL>G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
<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 : γ → δ<GOAL>map n (map₂ m f g) = map₂ (fun a b => n (m a b)) f g
<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 : γ → δ<GOAL>map (n ∘ fun p => m p.1 p.2) (f ×ˢ g) = map (fun p => n (m p.1 p.2)) (f ×ˢ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<GOAL>(s ∪ t).ncard ≤ s.ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>h : (s ∪ t).Finite<GOAL>(s ∪ t).ncard ≤ s.ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>h : (s ∪ t).Infinite<GOAL>(s ∪ t).ncard ≤ s.ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>h : (s ∪ t).Infinite<GOAL>0 ≤ s.ncard + t.ncard