ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t u : Set α<VAR>hs : s ∈ 𝓝 a<VAR>h₂ : t ∩ s = u ∩ s<GOAL>𝓝[t] a = 𝓝[u] a
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>s : ι → Finset α<VAR>hs : ∀ (t : Finset α), ∃ i, t ⊆ s i<GOAL>∑' (a : α), f a = ⨆ i, ∑ a ∈ s i, f a
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>s : ι → Finset α<VAR>hs : ∀ (t : Finset α), ∃ i, t ⊆ s i<GOAL>⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a
<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>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>s : ι → Finset α<VAR>hs : ∀ (t : Finset α), ∃ i, t ⊆ s i<GOAL>⨆ i, (fun t => ∑ a ∈ t, f a) (s i) = ⨆ s, ∑ a ∈ s, f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>HasSum (fun n => r ^ n) (1 - r)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<GOAL>((Finset.erase b m).erase (m.1, m.2 - 1)).card + 2 = Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<GOAL>(Finset.erase b m).card - 1 + 2 = Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<GOAL>Finset.card b - 1 - 1 + 2 = Finset.card b
<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>s : Finset ι<VAR>f : ι → α → β<GOAL>(mulSupport fun x => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)
<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>s : Finset ι<VAR>f : ι → α → β<GOAL>∀ (x : α), (∀ x_1 ∈ s, f x_1 x = 1) → ∏ i ∈ s, f i x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b<VAR>ha : a ∈ Ici a<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<VAR>b : β<VAR>hb : b < f a<GOAL>∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<VAR>b : β<VAR>hb : b > f a<GOAL>∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>rootSpace H (2 • ⇑α) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h✝ : Subsingleton L<GOAL>rootSpace H (2 • ⇑α) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h✝ : Nontrivial L<GOAL>rootSpace H (2 • ⇑α) = ⊥
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<GOAL>∃ ι f, lsub f = o ∧ #ι = o.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<GOAL>∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}
<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>h : G.IsSRGWith n k ℓ μ<VAR>hn : 0 < n<VAR>this : DecidableEq V := Classical.decEq V<GOAL>k * (k - ℓ - 1) = (n - k - 1) * μ
<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>h : G.IsSRGWith n k ℓ μ<VAR>hn : Nonempty V<VAR>this : DecidableEq V := Classical.decEq V<GOAL>k * (k - ℓ - 1) = (n - k - 1) * μ
<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>h : G.IsSRGWith n k ℓ μ<VAR>this : DecidableEq V := Classical.decEq V<VAR>v : V<GOAL>k * (k - ℓ - 1) = (n - k - 1) * μ
<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>h : G.IsSRGWith n k ℓ μ<VAR>this : DecidableEq V := Classical.decEq V<VAR>v : V<GOAL>k = (G.neighborFinset v).card
<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>h : G.IsSRGWith n k ℓ μ<VAR>this : DecidableEq V := Classical.decEq V<VAR>v : V<GOAL>n - k - 1 = (Gᶜ.neighborFinset v).card
<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>h : G.IsSRGWith n k ℓ μ<VAR>this : DecidableEq V := Classical.decEq V<VAR>v : V<GOAL>∀ a ∈ G.neighborFinset v, (bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a).card = k - ℓ - 1
<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>h : G.IsSRGWith n k ℓ μ<VAR>this : DecidableEq V := Classical.decEq V<VAR>v : V<GOAL>∀ b ∈ Gᶜ.neighborFinset v, (bipartiteBelow G.Adj (G.neighborFinset v) b).card = μ
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : ∃ n, lowerCentralSeries H n = ⊥<GOAL>∃ n, lowerCentralSeries G n = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>n : ℕ<VAR>hn : lowerCentralSeries H n = ⊥<GOAL>∃ n, lowerCentralSeries G n = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>n : ℕ<VAR>hn : lowerCentralSeries H n = ⊥<GOAL>lowerCentralSeries G (n + 1) = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>n : ℕ<VAR>hn : lowerCentralSeries H n = ⊥<GOAL>Subgroup.map f (lowerCentralSeries G n) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>x : Sigma γ<VAR>i : ι<VAR>a : α i<VAR>j : ι<VAR>b : β j<GOAL>x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>x : Sigma γ<VAR>i : ι<VAR>a : α i<VAR>b : β i<GOAL>x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>x : Sigma γ<VAR>i : ι<VAR>a : α i<VAR>j : ι<VAR>b : β j<VAR>h : i ≠ j<GOAL>x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : t ∈ 𝓝[s] x<GOAL>ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball 1 δ / s = thickening δ s⁻¹
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>v : ι →₀ R<GOAL>b.repr ((Finsupp.total ι M R ⇑b) v) = v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>v : ι →₀ R<GOAL>b.repr (↑b.repr.symm v) = v
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : V<VAR>f : A ⟶ B<GOAL>(single V c j ⋙ eval V c j).map f ≫ (singleObjXSelf c j B).hom = (singleObjXSelf c j A).hom ≫ (𝟭 V).map f
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<VAR>y : A × ↥M<VAR>hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<VAR>y : A × ↥M<VAR>hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1<VAR>this : z * w * (algebraMap A S) ↑y.2 * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1 * (algebraMap A S) y.1<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<VAR>y : A × ↥M<VAR>hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1<VAR>this : 0 = (algebraMap A S) (x.1 * y.1)<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<VAR>y : A × ↥M<VAR>hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1<VAR>this : 0 = (algebraMap A S) (x.1 * y.1)<VAR>H : x.1 = 0<GOAL>z = 0 ∨ w = 0
<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>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<VAR>z w : S<VAR>h : z * w = 0<VAR>x : A × ↥M<VAR>hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1<VAR>y : A × ↥M<VAR>hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1<VAR>this : 0 = (algebraMap A S) (x.1 * y.1)<VAR>H : y.1 = 0<GOAL>z = 0 ∨ w = 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : Monotone f<VAR>hx : x ≤ f x<VAR>n : ℕ<GOAL>f^[n] x ≤ f^[n + 1] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : Monotone f<VAR>hx : x ≤ f x<VAR>n : ℕ<GOAL>f^[n] x ≤ f^[n] (f x)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<GOAL>oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>h₀ : ↑(oreDenom r₁ s₂) * r₁ = oreNum r₁ s₂ * ↑s₂<GOAL>oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<GOAL>v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<GOAL>v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>v • r₂ /ₒ (u * s₁) = v₀ • r₂ /ₒ (u₀ * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>∃ u_1 v_1, u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ ↑u_1 * ↑(u₀ * s₁) = v_1 * ↑(u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>∃ v_1, (s₄ * s₃) • v₀ • r₂ = v_1 • v • r₂ ∧ ↑(s₄ * s₃) * ↑(u₀ * s₁) = v_1 * ↑(u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>(s₄ * s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂ ∧ ↑(s₄ * s₃) * ↑(u₀ * s₁) = ↑s₄ * r₃ * ↑(u * s₁)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<VAR>v₀ : R := oreNum r₁ s₂<VAR>u₀ : ↥S := oreDenom r₁ s₂<VAR>h₀ : ↑u₀ * r₁ = v₀ * ↑s₂<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u<VAR>this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂<VAR>s₄ : ↥S<VAR>hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)<GOAL>(↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂ ∧ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>↑S.card = ∏ i : α, (P i - N i + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>∏ i : α, ↑(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺)).card = ∏ i : α, (P i - N i + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>i : α<GOAL>↑(Icc (∑ j : β, ↑B * -(A i j)⁻) (∑ j : β, ↑B * (A i j)⁺)).card = P i - N i + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>i : α<GOAL>P i + 1 - N i = P i - N i + 1
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : β<VAR>p : Fin n → β<GOAL>(last n).insertNth x p = snoc p x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K✝ L : Subgroup G<VAR>f : G →* G'<VAR>K : Subgroup G<GOAL>f.ker.relindex K = Nat.card ↑(⇑f '' ↑K)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K✝ L : Subgroup G<VAR>f : G →* G'<VAR>K : Subgroup G<GOAL>Nat.card ↥(map f K) = Nat.card ↑(⇑f '' ↑K)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>ha : a ≠ 0<VAR>x✝ : p ∣ C a * q<VAR>r : R[X]<VAR>hr : C a * q = p * r<GOAL>q = p * (C a⁻¹ * r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Ioo a b ↔ False
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n✝ : ℤ<VAR>n : ℕ<GOAL>0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n✝ : ℤ<VAR>n : ℕ<VAR>this : -↑n < 1<GOAL>0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ t₁ : List α<VAR>h : l₁ ~ l₂<GOAL>l₁ ∪ t₁ ~ l₂ ∪ t₁