ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : AddCommMonoid N'<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid P'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N'<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R P'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>e : N ≃ₗ[R] N'<GOAL>Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Exact ⇑f ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : AddCommMonoid N'<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid P'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N'<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R P'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>e : N ≃ₗ[R] N'<GOAL>Submodule.map (↑e) (LinearMap.ker g) = Submodule.map (↑e) (LinearMap.range f) ↔ LinearMap.ker g = LinearMap.range f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : NormOneClass A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ < ‖k‖<GOAL>‖a‖ * ‖1‖ < ‖k‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>σ : ι ≃ ι'<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => G) G'<GOAL>‖domDomCongr σ f‖ = ‖f‖
<VAR>a : Ordinal.{u_1}<VAR>H : ∀ ⦃b c : Ordinal.{u_1}⦄, b < a → c < a → b + c ≠ a<GOAL>Principal (fun x x_1 => x + x_1) a
<VAR>a : Ordinal.{u_1}<VAR>H : ∀ ⦃b c : Ordinal.{u_1}⦄, b < a → c < a → b + c ≠ a<VAR>ha : ¬Principal (fun x x_1 => x + x_1) a<GOAL>False
<VAR>b c : Ordinal.{u_1}<VAR>H : ∀ ⦃b_1 c_1 : Ordinal.{u_1}⦄, b_1 < b + c → c_1 < b + c → b_1 + c_1 ≠ b + c<VAR>ha : ¬Principal (fun x x_1 => x + x_1) (b + c)<VAR>hb : b < b + c<VAR>hc : c < b + c<GOAL>False
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>C₁ : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : MonoidalCategory C₁<VAR>C₂ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} C₂<VAR>inst✝ : MonoidalCategory C₂<GOAL>∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ g = f ▷ X₂ ≫ Y₁ ◁ g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = h₃ + h₂ ≫ S₂.g + Hom.τ₃ 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.193906, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<GOAL>⊤.smallSets = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>(Multiset.map (fun a => X - C a) s).prod.natDegree = Multiset.card s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>(Multiset.map (natDegree ∘ fun a => X - C a) s).sum = Multiset.card s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>s : Multiset R<GOAL>∀ f ∈ Multiset.map (fun a => X - C a) s, f.Monic
<VAR>z : ℂ<VAR>n : ℤ<GOAL>(z / ↑n).re = z.re / ↑n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>S : Set α := {x | f x < 0}<GOAL>(μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun x => ENNReal.ofReal (-f x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>S : Set α := {x | f x < 0}<VAR>hS : MeasurableSet S<GOAL>(μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun x => ENNReal.ofReal (-f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>h : f =ᶠ[ae μ] g<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((mapₗ f) μ) s = ((mapₗ g) μ) s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<GOAL>a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<GOAL>∀ (y : 𝕎 k × ↥(nonZeroDivisors (𝕎 k))), Localization.mk y.1 y.2 ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk y.1 y.2 = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>r q : 𝕎 k<VAR>hq : q ∈ nonZeroDivisors (𝕎 k)<VAR>hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>r q : 𝕎 k<VAR>hq : q ∈ nonZeroDivisors (𝕎 k)<VAR>hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0<VAR>hq0 : q ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>r q : 𝕎 k<VAR>hq : q ∈ nonZeroDivisors (𝕎 k)<VAR>hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0<VAR>hq0 : q ≠ 0<VAR>hr0 : r ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>q : 𝕎 k<VAR>hq : q ∈ nonZeroDivisors (𝕎 k)<VAR>hq0 : q ≠ 0<VAR>m : ℕ<VAR>r' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hrq : Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 ≠ 0<VAR>hr0 : ↑p ^ m * r' ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m_1, φ b * Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 = ↑p ^ m_1 * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>m : ℕ<VAR>r' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hr0 : ↑p ^ m * r' ≠ 0<VAR>n : ℕ<VAR>q' : 𝕎 k<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>hq0 : ↑p ^ n * q' ≠ 0<VAR>hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m_1, φ b * Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 = ↑p ^ m_1 * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a : FractionRing (𝕎 k)<VAR>m : ℕ<VAR>r' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hr0 : ↑p ^ m * r' ≠ 0<VAR>n : ℕ<VAR>q' : 𝕎 k<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>hq0 : ↑p ^ n * q' ≠ 0<VAR>hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 = ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<GOAL>c * b = d * a ↔ a * d = c * b
<VAR>p n✝ k n : ℕ<VAR>hn : n < p → n !.factorization p = 0<VAR>h : n + 1 < p<GOAL>(n + 1)!.factorization p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a = b⁻¹<GOAL>a * b = 1
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>hp : nil.IsCycle<GOAL>G ≠ ⊥
<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 a : α → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : α), a i ≠ ⊤<VAR>j : α<GOAL>a j < ⊤
<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 a : α → ℝ≥0∞<VAR>j : α<VAR>h : ⊤ ≤ a j<GOAL>∑' (i : α), a i = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<GOAL>CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<GOAL>HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<GOAL>Pairwise (Disjoint on fun r => frontier (thickening r A))
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<VAR>r₁ r₂ : ℝ<VAR>hr : r₁ < r₂<GOAL>Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<VAR>r₁ r₂ : ℝ<VAR>hr : r₁ < r₂<VAR>h₁ : r₁ ≤ 0<GOAL>Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<VAR>r₁ r₂ : ℝ<VAR>hr : r₁ < r₂<VAR>h₁ : 0 ≤ r₁<GOAL>Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<VAR>r₁ r₂ : ℝ<VAR>hr : r₁ < r₂<VAR>h₁ : 0 ≤ r₁<VAR>h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂<GOAL>r₁ = r₂
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<VAR>A : Set α<VAR>r₁ r₂ : ℝ<VAR>hr : r₁ < r₂<VAR>h₁ : 0 ≤ r₁<VAR>h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal<GOAL>r₁ = r₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<GOAL>∏ i : Fin (a + b), f i = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<GOAL>∏ x : Fin a ⊕ Fin b, f (finSumFinEquiv.toFun x) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<GOAL>∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))
<VAR>z : ℍ<VAR>c d : ℝ<VAR>hd : 1 ≤ d ^ 2<GOAL>r z ≤ Complex.abs (↑c * ↑z + ↑d)
<VAR>z : ℍ<VAR>c d : ℝ<VAR>hd : 1 ≤ d ^ 2<VAR>H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)<GOAL>r z ≤ Complex.abs (↑c * ↑z + ↑d)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>inst✝ : (i : ι) → SMul K (R i)<VAR>r : K<VAR>s : Set ι<VAR>t : (i : ι) → Set (R i)<VAR>y : (i : ι) → R i<VAR>h : y ∈ s.pi t<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(fun x => r • x) y i ∈ (r • t) i
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>hw : w.IsComplex<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : OneHom N P<VAR>x✝ : M<GOAL>(f.comp 1) x✝ = 1 x✝
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.toMap (x₁ * x₂) = f.toMap ↑(y₁ * y₂) * (f.toMap x₁ * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y₁)⁻¹ * (f.toMap x₂ * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y₂)⁻¹))
<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₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f.toMap x₁ * f.toMap x₂ * f.toMap ↑y₂ * f.toMap ↑y₁ = f.toMap ↑y₁ * f.toMap ↑y₂ * f.toMap x₁ * f.toMap x₂
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e✝ : Basis ι R M<VAR>e : M ≃ₗ[R] M<VAR>f f' : M →ₗ[R] M<VAR>h : ∀ (x : M), f x = f' (e x)<GOAL>Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e✝ : Basis ι R M<VAR>e : M ≃ₗ[R] M<VAR>f f' : M →ₗ[R] M<VAR>h : ∀ (x : M), f x = f' (e x)<GOAL>Associated (LinearMap.det f' * LinearMap.det ↑e) (LinearMap.det f' * 1)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : CliffordAlgebra Q →ₐ[R] A<GOAL>(lift Q) ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i₁ i₁' : I₁<VAR>h : ¬c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>(K.d i₁ i₁').f i₂ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>⨆ n, aeSeq hf p n =ᶠ[ae μ] ⨆ n, f n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>μ {a | ¬⨆ i, aeSeq hf p i a = ⨆ i, f i a} = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<VAR>h_ss : aeSeqSet hf p ⊆ {a | ⨆ i, aeSeq hf p i a = ⨆ i, f i a}<GOAL>μ {a | ¬⨆ i, aeSeq hf p i a = ⨆ i, f i a} = 0
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m✝ m : M<VAR>p : Polynomial ↥(subfield M F)<VAR>x : ↥(subfield M F)<GOAL>m • Polynomial.C x = Polynomial.C x
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m✝ m : M<VAR>p✝ p q : Polynomial ↥(subfield M F)<VAR>ihp : m • p = p<VAR>ihq : m • q = q<GOAL>m • (p + q) = p + q
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m✝ m : M<VAR>p : Polynomial ↥(subfield M F)<VAR>n : ℕ<VAR>x : ↥(subfield M F)<VAR>x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n<GOAL>m • (Polynomial.C x * Polynomial.X ^ (n + 1)) = Polynomial.C x * Polynomial.X ^ (n + 1)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit a m).land (bit b n) = bit (a && b) (m.land n)
<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hxr : x ^ n = ↑m<VAR>hv : (multiplicity (↑p) m).get ⋯ % n ≠ 0<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hxr : x ^ 0 = ↑m<VAR>hv : (multiplicity (↑p) m).get ⋯ % 0 ≠ 0<GOAL>Irrational x
<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hxr : x ^ n = ↑m<VAR>hv : (multiplicity (↑p) m).get ⋯ % n ≠ 0<VAR>hnpos : n > 0<GOAL>Irrational x
<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hxr : x ^ n = ↑m<VAR>hv : (multiplicity (↑p) m).get ⋯ % n ≠ 0<VAR>hnpos : n > 0<GOAL>¬∃ y, x = ↑y
<VAR>n : ℕ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hv : (multiplicity (↑p) m).get ⋯ % n ≠ 0<VAR>hnpos : n > 0<VAR>y : ℤ<VAR>hxr : ↑y ^ n = ↑m<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hm : m ≠ 0<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hv : (multiplicity (↑p) m).get ⋯ % n ≠ 0<VAR>hnpos : n > 0<VAR>y : ℤ<VAR>hxr : y ^ n = m<GOAL>False
<VAR>n p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnpos : n > 0<VAR>y : ℤ<VAR>hm : y ^ n ≠ 0<VAR>hv : (multiplicity (↑p) (y ^ n)).get ⋯ % n ≠ 0<GOAL>False
<VAR>n p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnpos : n > 0<VAR>y : ℤ<VAR>hm : y ^ n ≠ 0<VAR>hv : (multiplicity (↑p) (y ^ n)).get ⋯ % n ≠ 0<VAR>this : y ≠ 0<GOAL>False
<VAR>n p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnpos : n > 0<VAR>y : ℤ<VAR>hm : y ^ n ≠ 0<VAR>this : y ≠ 0<VAR>hv : 0 ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a b : α<GOAL>b ∈ {a} ↔ b = a
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<GOAL>‖U‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<GOAL>∀ (i i_1 : n), ‖U i i_1‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i✝¹ i✝ : n<GOAL>‖U i✝¹ i✝‖ ≤ 1
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>hb : b ≠ ⊥<VAR>hab : Disjoint a b<VAR>hc : a ⊔ b = c<GOAL>(insert b P.parts).SupIndep id
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>hb : b ≠ ⊥<VAR>hab : Disjoint a b<VAR>hc : a ⊔ b = c<GOAL>(insert b ↑P.parts).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>hb : b ≠ ⊥<VAR>hab : Disjoint a b<VAR>hc : a ⊔ b = c<GOAL>(insert b P.parts).sup id = c
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>dist x y = √(dist x.1 y.1 ^ 2 + dist x.2 y.2 ^ 2)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>√(‖(x - y).1‖ ^ 2 + ‖(x - y).2‖ ^ 2) = √(‖x.1 - y.1‖ ^ 2 + ‖x.2 - y.2‖ ^ 2)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>W : Subspace K V<GOAL>W ⊔ span S = span (↑W ∪ S)
<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<GOAL>W.addY P Q / addZ P Q ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<GOAL>T2Space (Quotient (MulAction.orbitRel G X))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<GOAL>IsClosed (diagonal (Quotient (MulAction.orbitRel G X)))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : ProperSMul G X<VAR>R : Setoid X := MulAction.orbitRel G X<VAR>π : X → Quotient R := Quotient.mk'<GOAL>IsClosed (diagonal (Quotient R))