ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>aux2 : ((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>hgt : Disjoint t (g⁻¹ • t)<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>aux2 : ((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>hgt : (t ∩ g⁻¹ • t).Nonempty<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>aux2 : ((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>hgt : (t ∩ g⁻¹ • t).Nonempty<VAR>hstg : (s, t).1.card + (s, t).2.card ≤ (mulETransformLeft g (s, t)).1.card + (mulETransformLeft g (s, t)).2.card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>aux2 : ((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>hgt : (t ∩ g⁻¹ • t).Nonempty<VAR>hstg : (s, t).1.card + (s, t).2.card < (mulETransformRight g (s, t)).1.card + (mulETransformRight g (s, t)).2.card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>h : minkowskiBound K 1 < volume (convexBodyLT K f)<GOAL>∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>h : minkowskiBound K 1 < volume (convexBodyLT K f)<VAR>w✝ : K<VAR>h_mem : w✝ ∈ ↑1<VAR>h_nz : w✝ ≠ 0<VAR>h_bd : ∀ (w : InfinitePlace K), w w✝ < ↑(f w)<GOAL>∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>h : minkowskiBound K 1 < volume (convexBodyLT K f)<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_bd : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) a) < ↑(f w)<GOAL>∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>(z₁.comp 0 h).v p q hpq = v 0 p q hpq
<VAR>w x✝ y✝ z x y : ℝ<VAR>hx : 0 ≤ x<GOAL>↑‖x ^ y‖₊ = ↑(‖x‖₊ ^ y)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w a✝ : V<GOAL>a✝ ∈ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔ a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w a✝ : V<GOAL>a✝ ∉ (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) ↔ a✝ ∉ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<GOAL>TopologicalGroup G
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<VAR>x₀ : G<GOAL>𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) * λ ^ (3 * S.multiplicity - 2) + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * λ * ↑η + FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * ↑η ^ 2 = 0
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>S.a + S.b + (S.a + ↑η * S.b) * ↑η + (S.a + (-↑η - 1) * S.b) * (-↑η - 1) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<GOAL>Fintype.card (ClassGroup R) = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<GOAL>∃ x, ∀ (y : ClassGroup R), y = x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<GOAL>∀ (y : ClassGroup R), y = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>ClassGroup.mk I = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → α<VAR>n : ℕ<GOAL>image f^[n] = (image f)^[n]
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝² : SeminormedAddCommGroup M<VAR>inst✝¹ : SeminormedAddCommGroup N✝<VAR>N : Type u_3<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>fb : f.NormNoninc<VAR>x : M ⧸ S<GOAL>‖(lift S f hf) x‖ ≤ ‖x‖
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>inst✝² : SeminormedAddCommGroup M<VAR>inst✝¹ : SeminormedAddCommGroup N✝<VAR>N : Type u_3<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>fb : f.NormNoninc<VAR>x : M ⧸ S<VAR>fb' : ‖f‖ ≤ ↑1<GOAL>‖(lift S f hf) x‖ ≤ ‖x‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤<GOAL>⨆ i, ↑‖g i‖₊ < ⊤
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤<GOAL>UniformEquicontinuous (DFunLike.coe ∘ g)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤<VAR>x✝ : Fin 1<VAR>x : E<GOAL>BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>eq : #α = #β<GOAL>#(α ≃ β) = 2 ^ #α
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<GOAL>(T n).degree = (C 1 * T n).degree
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<GOAL>(D R R[X]) P = derivative P • (D R R[X]) X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Ici a) → β<GOAL>range (IciExtend f) = range f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ f g : ι →₀ α<VAR>h : f ≤ g<VAR>a : ι<VAR>ha : a ∈ f.support<GOAL>a ∈ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ f g : ι →₀ α<VAR>h : f ≤ g<VAR>a : ι<VAR>ha : 0 < f a<GOAL>0 < g a
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a✝ b✝ c d a b : α<GOAL>a / b < a ↔ 1 < b
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.135628, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>x₃ : A ⟶ S.X₃.X i<VAR>hx₃ : x₃ ≫ S.X₃.d i j = 0<VAR>x₂ : A ⟶ S.X₂.X i<VAR>hx₂ : x₂ ≫ S.g.f i = x₃<VAR>x₁ : A ⟶ S.X₁.X j<VAR>hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j<VAR>k : ι<VAR>hk : c.next j = k<GOAL>x₁ ≫ S.X₁.d j k = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.135628, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>x₃ : A ⟶ S.X₃.X i<VAR>hx₃ : x₃ ≫ S.X₃.d i j = 0<VAR>x₂ : A ⟶ S.X₂.X i<VAR>hx₂ : x₂ ≫ S.g.f i = x₃<VAR>x₁ : A ⟶ S.X₁.X j<VAR>hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j<VAR>k : ι<VAR>hk : c.next j = k<VAR>this : Mono S.f<GOAL>x₁ ≫ S.X₁.d j k = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>A : C<VAR>x₃ : A ⟶ S.X₃.X i<VAR>hx₃ : x₃ ≫ S.X₃.d i j = 0<VAR>x₂ : A ⟶ S.X₂.X i<VAR>hx₂ : x₂ ≫ S.g.f i = x₃<VAR>x₁ : A ⟶ S.X₁.X j<VAR>hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j<VAR>k : ι<VAR>hk : c.next j = k<GOAL>S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = S.X₁.liftCycles x₁ k hk ⋯ ≫ S.X₁.homologyπ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<GOAL>a \ limsup u f = liminf (fun b => a \ u b) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<GOAL>(a \ limsup u f)ᶜ = (liminf (fun b => a \ u b) f)ᶜ
<VAR>c : Cardinal.{u}<GOAL>𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<GOAL>M✶.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<GOAL>M✶.Indep (M.E \ B ∩ (M.E \ X))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))<GOAL>M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<GOAL>M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<GOAL>∀ (B_1 : Set α), M.Base B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hem : B' ⊆ B ∪ X ∧ e ∉ B'<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hem : B' ⊆ B ∪ X ∧ e ∉ B'<VAR>f : α<VAR>hfb : f ∈ B' \ B<VAR>hBf : M.Base (insert f (B \ {e}))<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<VAR>e : α<VAR>he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hem : B' ⊆ B ∪ X ∧ e ∉ B'<VAR>f : α<VAR>hfb : f ∈ B' \ B<VAR>hBf : M.Base (insert f (B \ {e}))<VAR>hi : M.Indep (insert f (B ∩ X))<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<GOAL>((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i) 1 = (((k + l).choose k • hasseDeriv (k + l)) ∘ₗ monomial i) 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<GOAL>(monomial (i - (k + l))) (↑((i - l).choose k) * ↑(i.choose l)) = (monomial (i - (k + l))) ((k + l).choose k • ↑(i.choose (k + l)))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<GOAL>(monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) = (monomial (i - (k + l))) (↑((k + l).choose k) * ↑(i.choose (k + l)))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<GOAL>(monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) = (monomial (i - (k + l))) ↑((k + l).choose k * i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<GOAL>(i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<GOAL>↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<GOAL>↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<GOAL>↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<VAR>h3 : k ≤ k + l<GOAL>↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<VAR>h3 : k ≤ k + l<GOAL>↑((i - l).choose k) * ↑(i.choose l) = ↑((k + l).choose k) * ↑(i.choose (k + l))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<VAR>h3 : k ≤ k + l<GOAL>↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) = ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - (k + l))!))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<VAR>h3 : k ≤ k + l<GOAL>↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) = ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f : R[X]<VAR>k l i : ℕ<VAR>hikl : k + l ≤ i<VAR>h1 : l ≤ i<VAR>h2 : k ≤ i - l<VAR>h3 : k ≤ k + l<GOAL>↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) = ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R✝ S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing Rₘ<VAR>M : Submonoid R<VAR>hM : 0 ∉ M<VAR>hR : IsField R<VAR>inst✝¹ : Algebra R Rₘ<VAR>inst✝ : IsLocalization M Rₘ<VAR>this : Field R := hR.toField<GOAL>Bijective ⇑(algebraMap R Rₘ)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R✝ S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing Rₘ<VAR>M : Submonoid R<VAR>hR : IsField R<VAR>inst✝¹ : Algebra R Rₘ<VAR>inst✝ : IsLocalization M Rₘ<VAR>this : Field R := hR.toField<VAR>hM : M ≤ nonZeroDivisors R<GOAL>Bijective ⇑(algebraMap R Rₘ)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R✝ S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing Rₘ<VAR>M : Submonoid R<VAR>hR : IsField R<VAR>inst✝¹ : Algebra R Rₘ<VAR>inst✝ : IsLocalization M Rₘ<VAR>this : Field R := hR.toField<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : Rₘ<GOAL>∃ a, (algebraMap R Rₘ) a = x
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R✝ S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing Rₘ<VAR>M : Submonoid R<VAR>hR : IsField R<VAR>inst✝¹ : Algebra R Rₘ<VAR>inst✝ : IsLocalization M Rₘ<VAR>this : Field R := hR.toField<VAR>hM : M ≤ nonZeroDivisors R<VAR>r m : R<VAR>hm : m ∈ M<GOAL>∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R✝ S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing Rₘ<VAR>M : Submonoid R<VAR>hR : IsField R<VAR>inst✝¹ : Algebra R Rₘ<VAR>inst✝ : IsLocalization M Rₘ<VAR>this : Field R := hR.toField<VAR>hM : M ≤ nonZeroDivisors R<VAR>r m : R<VAR>hm : m ∈ M<VAR>n : R<VAR>hn : m * n = 1<GOAL>∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t✝ : ι → α<VAR>a b : α<VAR>f : β → γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k✝ : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>h : μ.IsEverywherePos k<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<GOAL>IsGδ k
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k✝ : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>h : μ.IsEverywherePos k<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>u : ℕ → ℝ≥0∞<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>IsGδ k
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k✝ : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>h : μ.IsEverywherePos k<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>u : ℕ → ℝ≥0∞<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>this : ∀ (n : ℕ), ∃ W, IsOpen W ∧ 1 ∈ W ∧ ∀ g ∈ W * W, μ (g • k \ k) < u n<GOAL>IsGδ k