ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<VAR>this : Mono S.f<GOAL>((forget₂ C Ab).map (S.f.f k)) (((forget₂ C Ab).map (S.X₁.d j k)) x₁) = ((forget₂ C Ab).map (S.f.f k)) 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<GOAL>((forget₂ C Ab).map (hS.δ i j hij)) (((forget₂ C Ab).map (S.X₃.homologyπ i)) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) = ((forget₂ C Ab).map (S.X₁.homologyπ j)) (S.X₁.cyclesMk x₁ k hk ⋯)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<GOAL>((forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i)) (((forget₂ C Ab).map (S.X₂.pOpcycles i)) x₂) = ((forget₂ C Ab).map (S.X₃.homologyι i)) (((forget₂ C Ab).map (S.X₃.homologyπ i)) (S.X₃.cyclesMk x₃ j ⋯ hx₃))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))<VAR>hx₃ : ((forget₂ C Ab).map (S.X₃.d i j)) x₃ = 0<VAR>x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))<VAR>hx₂ : ((forget₂ C Ab).map (S.g.f i)) x₂ = x₃<VAR>x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))<VAR>hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂<VAR>k : ι<VAR>hk : c.next j = k<GOAL>((forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j)) (S.X₁.cyclesMk x₁ k hk ⋯) = ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)) (((forget₂ C Ab).map (S.X₂.pOpcycles i)) x₂)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.odd.get n = s.get (2 * n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.tail.get (2 * n) = s.get (2 * n + 1)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>X_emp : ¬IsEmpty Ω<GOAL>∃ As, (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>X_emp : Nonempty Ω<GOAL>∃ As, (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>X_emp : Nonempty Ω<VAR>xs : ℕ → Ω<VAR>xs_dense : DenseRange xs<GOAL>∃ As, (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>X_emp : Nonempty Ω<VAR>xs : ℕ → Ω<VAR>xs_dense : DenseRange xs<VAR>half_ε_pos : 0 < ε / 2<GOAL>∃ As, (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : Module.End R R<GOAL>IsIdempotentElem (f 1) ↔ IsIdempotentElem f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : Module.End R R<GOAL>f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : Module.End R R<GOAL>f (f 1) = f 1 ↔ ∀ (x : R), f (f x) = f x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => Commute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>⨅ z ∈ s, edist y z + edist x y = (⨅ z ∈ s, edist y z) + edist x y
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>mkHom f.hom i ≫ mkHom f.inv i' = 𝟙 (of ↑M)
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>↑(mkHom f.hom i ≫ mkHom f.inv i') = ↑(𝟙 (of ↑M))
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>mkHom f.inv i' ≫ mkHom f.hom i = 𝟙 (of ↑N)
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>↑(mkHom f.inv i' ≫ mkHom f.hom i) = ↑(𝟙 (of ↑N))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<GOAL>(p.scaleRoots s).Monic ↔ p.Monic
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<GOAL>sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
<VAR>k : Type u<VAR>inst✝¹¹ : CommRing k<VAR>G : Type u<VAR>inst✝¹⁰ : Group G<VAR>V : Type v<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module k V<VAR>inst✝⁷ : Module (MonoidAlgebra k G) V<VAR>inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>inst✝⁵ : AddCommGroup W<VAR>inst✝⁴ : Module k W<VAR>inst✝³ : Module (MonoidAlgebra k G) W<VAR>inst✝² : IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : W<GOAL>(equivariantProjection G π) v = ⅟↑(Fintype.card G) • ∑ g : G, (π.conjugate g) v
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>I : Ideal R<VAR>inst✝ : IsPrincipal I<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∣ generator I ↔ I = Ideal.span {x}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>I : Ideal R<VAR>inst✝ : IsPrincipal I<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∣ generator I ↔ span R {generator I} = Ideal.span {x}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>I : Ideal R<VAR>inst✝ : IsPrincipal I<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∣ generator I ↔ x ∈ I ∧ x ∣ generator I
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a b : α<VAR>hab : a ∣ b<VAR>hba : b ∣ a<VAR>a✝ : Nontrivial α<GOAL>normalize a = normalize b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>a✝ : Nontrivial α<VAR>u : αˣ<VAR>hab : a ∣ a * ↑u<VAR>hba : a * ↑u ∣ a<GOAL>normalize a = normalize (a * ↑u)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>a✝ : Nontrivial α<VAR>u : αˣ<VAR>hab : a ∣ a * ↑u<VAR>hba : a * ↑u ∣ a<VAR>ha : a ≠ 0<GOAL>normalize a = normalize (a * ↑u)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>a✝ : Nontrivial α<VAR>u : αˣ<VAR>hab : a ∣ a * ↑u<VAR>hba : a * ↑u ∣ a<VAR>ha : a ≠ 0<GOAL>a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<GOAL>Continuous fun p => p.1 * p.2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<GOAL>∀ (x : M × M), ContinuousAt (fun p => p.1 * p.2) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<VAR>x₀ y₀ : M<VAR>key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1<GOAL>ContinuousAt (fun p => p.1 * p.2) (x₀, y₀)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<VAR>x₀ y₀ : M<VAR>key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1<VAR>key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x<GOAL>ContinuousAt (fun p => p.1 * p.2) (x₀, y₀)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<GOAL>ContDiffOn 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<GOAL>ContDiffOn 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) (↑I.symm ⁻¹' (f'.symm ≫ₕ f).source ∩ range ↑I)
<VAR>α : Type u_1<VAR>I : Type ?u.61695<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<GOAL>IsRelPrime (x ^ m) y ↔ IsRelPrime x y
<VAR>α : Type u_1<VAR>I : Type ?u.61695<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>h : IsRelPrime (x ^ m) y<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>I : Type ?u.61695<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>h : IsRelPrime (∏ _x ∈ Finset.range m, x) y<GOAL>IsRelPrime x y
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : MapsTo h s t'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = h x<GOAL>derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s : ↥S<GOAL>mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Zero N<VAR>f✝ g✝ f g : α →₀ N<VAR>h : f = g<GOAL>f.neLocus f = ∅
<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>π : α → Type u_11<VAR>t : (i : α) → Set (π i)<GOAL>univ.pi t = ⋂ i, eval i ⁻¹' t i
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>β : Type u<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>q : BallPackage β α<GOAL>∃ s, (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧ range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>β : Type u<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>q : BallPackage β α<VAR>h✝ : IsEmpty β<GOAL>∃ s, (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧ range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>β : Type u<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>q : BallPackage β α<VAR>h✝ : Nonempty β<GOAL>∃ s, (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧ range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>this : DecidableEq α<GOAL>(powersetAux l₁).revzip ~ (powersetAux l₂).revzip
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>this : DecidableEq α<GOAL>List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>f.toMap x * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y)⁻¹ * f.toMap ↑y = f.toMap x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>card { x // p x } = (filter p univ).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>∀ (x : α), x ∈ filter p univ ↔ p x
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set (OnePoint X)<VAR>t s : Set X<GOAL>IsOpen (some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set (OnePoint X)<VAR>t s : Set X<GOAL>∞ ∈ (some '' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a - (b + c) = a - c - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a - (c + b) = a - c - b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>M✶.Coindep X ↔ M.Indep X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.11640, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = S.g ≫ x<GOAL>S.f ≫ k = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = S.g ≫ x<GOAL>h.descQ k ⋯ = h.g' ≫ x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<GOAL>Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ n, s n, f a ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ n, s n, f a ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>Tendsto (fun i => ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ n, s n, f a ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>Tendsto (fun i => ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (x : α), (⋂ b, s b).indicator f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>Integrable bound μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : IntegrableOn f (s 0) μ<VAR>bound : α → ℝ := (s 0).indicator fun a => ‖f a‖<VAR>h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ<GOAL>∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a