ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegral
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegral
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegral
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegralElem p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<VAR>p' q : R[X] ⧸ P<VAR>hq : q ∈ M'<VAR>hp : p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨q, hq⟩).2 = (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨q, hq⟩).1<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegralElem p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<VAR>p' q : R[X] ⧸ P<VAR>hq : q ∈ M'<VAR>hp : p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨q, hq⟩).2 = (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨q, hq⟩).1<GOAL>φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<VAR>p' q : R[X] ⧸ P<VAR>hq : q ∈ M'<VAR>hp : p * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'<GOAL>φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<VAR>p' q : R[X] ⧸ P<VAR>hq : q ∈ M'<VAR>hp : p * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'<GOAL>∀ x ∈ ⇑((algebraMap (R[X] ⧸ P) Sₘ).comp (Quotient.mk P)) '' insert X {p | p.degree ≤ 0}, φ'.IsIntegralElem x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯<VAR>hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C<VAR>p : Sₘ<VAR>p' q : R[X] ⧸ P<VAR>hq : q ∈ M'<VAR>hp : p * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'<GOAL>(algebraMap (R[X] ⧸ P) Sₘ) p' ∈ Subring.closure (⇑((algebraMap (R[X] ⧸ P) Sₘ).comp (Quotient.mk P)) '' insert X {p | p.degree ≤ 0})
<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>N i ≤ P i + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : 𝕎 R<VAR>n : ℕ<GOAL>((map ↑(_root_.frobeniusEquiv R p).symm) (frobenius f)).coeff n = f.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : 𝕎 R<VAR>n : ℕ<GOAL>((map ↑(_root_.frobeniusEquiv R p).symm) ((map (_root_.frobenius R p)) f)).coeff n = f.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : 𝕎 R<VAR>n : ℕ<GOAL>(frobenius ((map ↑(_root_.frobeniusEquiv R p).symm) f)).coeff n = f.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : 𝕎 R<VAR>n : ℕ<GOAL>((map (_root_.frobenius R p)) ((map ↑(_root_.frobeniusEquiv R p).symm) f)).coeff n = f.coeff n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>W.add P Q = addU P Q • ![1, 1, 0]
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom = (singleObjHomologySelfIso c j A).hom ≫ f
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsFiniteMeasure μ<VAR>inst✝² : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hf_int : Integrable f μ<GOAL>μ[f|m ⊓ mΩ] =ᶠ[ae μ] fun ω => ∫ (y : Ω), f y ∂(condexpKernel μ m) ω
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsFiniteMeasure μ<VAR>inst✝² : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hf_int : Integrable f μ<VAR>hX : Measurable id<GOAL>μ[f|m ⊓ mΩ] =ᶠ[ae μ] fun ω => ∫ (y : Ω), f y ∂(condexpKernel μ m) ω
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsFiniteMeasure μ<VAR>inst✝² : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hf_int : Integrable f μ<VAR>hX : Measurable id<GOAL>μ[f|m ⊓ mΩ] =ᶠ[ae μ] fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsFiniteMeasure μ<VAR>inst✝² : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hf_int : Integrable f μ<VAR>hX : Measurable id<VAR>h : μ[f|MeasurableSpace.comap id (m ⊓ mΩ)] =ᶠ[ae μ] fun a => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id a)<GOAL>μ[f|m ⊓ mΩ] =ᶠ[ae μ] fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<GOAL>IsOpen {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<VAR>A : {x} ⊆ s<GOAL>IsOpen {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<VAR>A : {x} ⊆ s<VAR>B : IsClosed (s \ {x})<GOAL>IsOpen {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<VAR>A : {x} ⊆ s<VAR>B : IsClosed (s \ {x})<VAR>C : (s \ {x})ᶜ ∈ 𝓝 x<GOAL>IsOpen {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<VAR>A : {x} ⊆ s<VAR>B : IsClosed (s \ {x})<VAR>C : (s \ {x})ᶜ ∈ 𝓝 x<VAR>D : {x} ∈ 𝓝 x<GOAL>IsOpen {x}
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I✝ J B : Set α<VAR>f x y : α<VAR>M : Matroid α<VAR>X I : Set α<VAR>hI : M.Basis I (X ∩ M.E)<GOAL>∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I✝ J B : Set α<VAR>f x y : α<VAR>M : Matroid α<VAR>X I : Set α<VAR>hI : M.Basis I (X ∩ M.E)<VAR>hI' : M.Basis I (M.closure (X ∩ M.E))<GOAL>∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I✝ J B : Set α<VAR>f x y : α<VAR>M : Matroid α<VAR>X I : Set α<VAR>hI : M.Basis I (X ∩ M.E)<VAR>hI' : M.Basis I (M.closure X)<GOAL>∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>x✝ : X<GOAL>(h.trans h.symm) x✝ = (Homeomorph.refl X) x✝
<VAR>α : Type u_1<VAR>inst✝⁶ : AddCommSemigroup α<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hb : AddLECancellable b<VAR>hca : c ≤ a<VAR>h : a - b < a - c<GOAL>c < b
<VAR>α : Type u_1<VAR>inst✝⁶ : AddCommSemigroup α<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hb : AddLECancellable b<VAR>hca : c ≤ a<VAR>h : a - c + c - b < a - c<GOAL>c < b
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : Semiring R₁<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₂] M₂<VAR>f' : M₂ →ₛₗ[σ₂₃] M₃<VAR>g' : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : Injective ⇑f<VAR>g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂<VAR>h : f.comp g₁ = f.comp g₂<VAR>x : M₁<GOAL>f (g₁ x) = f (g₂ x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<GOAL>z₁.map L ⋯ ≫ z₂.map L ⋯ = (z₁.comp₀ z₂ z₃).map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>this : IsIso (L.map z₂.s)<GOAL>z₁.map L ⋯ ≫ z₂.map L ⋯ = (z₁.comp₀ z₂ z₃).map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>this✝ : IsIso (L.map z₂.s)<VAR>this : IsIso (L.map z₃.s)<GOAL>z₁.map L ⋯ ≫ z₂.map L ⋯ = (z₁.comp₀ z₂ z₃).map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>this✝¹ : IsIso (L.map z₂.s)<VAR>this✝ : IsIso (L.map z₃.s)<VAR>this : IsIso (L.map (z₂.s ≫ z₃.s))<GOAL>z₁.map L ⋯ ≫ z₂.map L ⋯ = (z₁.comp₀ z₂ z₃).map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>this✝¹ : IsIso (L.map z₂.s)<VAR>this✝ : IsIso (L.map z₃.s)<VAR>this : IsIso (L.map (z₂.s ≫ z₃.s))<GOAL>z₁.map L ⋯ ≫ z₂.map L ⋯ = (mk (z₁.f ≫ z₃.f) (z₂.s ≫ z₃.s) ⋯).map L ⋯
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μ_mass : μ.mass = 0<GOAL>μ = 0
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μ_mass : μ.mass = 0<GOAL>↑μ = ↑0
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μ_mass : μ.mass = 0<GOAL>↑μ univ = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝⁵ : IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Nonempty γ<VAR>f✝ : γ → α<VAR>inst✝³ : Finite β<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsDirected α fun x x_1 => x ≥ x_1<VAR>f : β → α<GOAL>BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝⁵ : IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Nonempty γ<VAR>f✝ : γ → α<VAR>inst✝³ : Finite β<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsDirected α fun x x_1 => x ≥ x_1<VAR>f : β → α<VAR>M : α<VAR>hM : ∀ (i : β), M ≤ f i<GOAL>BddBelow (Set.range f)
<VAR>p : ℕ → Prop<VAR>x : ℕ<VAR>h : p x<VAR>a : ℕ<VAR>ha : ∀ j < a, ¬p j<VAR>b : ℕ<VAR>property✝ : ∀ j < b, ¬p j<GOAL>a > b ↔ x - a < x - b
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsLeftRegular (a ^ n) ↔ IsLeftRegular a
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsLeftRegular (a ^ n) → IsLeftRegular a
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>L₀ L₀' : List (TransvectionStruct n 𝕜)<VAR>D₀ : n → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀<GOAL>(List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M * (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod = diagonal (D₀ ∘ ⇑e)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>L₀ L₀' : List (TransvectionStruct n 𝕜)<VAR>D₀ : n → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)<GOAL>(List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M * (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod = diagonal (D₀ ∘ ⇑e)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix p p 𝕜<VAR>e : p ≃ n<VAR>L₀ L₀' : List (TransvectionStruct n 𝕜)<VAR>D₀ : n → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)<GOAL>(List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M) * (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod = diagonal (D₀ ∘ ⇑e)