ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Fix F α<GOAL>(mk ∘ dest) x = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Fix F α<GOAL>∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → (mk ∘ dest) (mk x) = mk x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ : Fix F α<VAR>x : F (α ::: Fix F α)<GOAL>(TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → mk (mk x).dest = mk x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ : Fix F α<VAR>x : F (α ::: Fix F α)<GOAL>(TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ : Fix F α<VAR>x : F (α ::: Fix F α)<VAR>h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x<GOAL>mk ((TypeVec.id ::: _root_.id) <$$> x) = mk x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>A.det = A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>(-1) ^ 0 * A 0 0 * ((-1) ^ 0 * A 1 1 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 1) + ((-1) ^ (0 + 1) * A 0 1 * ((-1) ^ 0 * A 1 0 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 0) + (-1) ^ (0 + 1 + 1) * A 0 2 * ((-1) ^ 0 * A 1 0 * A 2 1 + (-1) ^ (0 + 1) * A 1 1 * A 2 0)) = A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>pprime : Nat.Prime p<GOAL>∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>pprime : Nat.Prime p<GOAL>f ↑p = ↑p ^ (- -logb (↑p) (f ↑p))
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>pprime : Nat.Prime p<GOAL>f ↑p = ↑p ^ logb (↑p) (f ↑p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>pprime : Nat.Prime p<GOAL>↑p ≠ 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R (n + 1) = 2 * X * T R n - T R (n - 1)
<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₁'' : I₁<VAR>i₂ : I₂<GOAL>(K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Lattice (α i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hn : 0 < n<VAR>c : F<GOAL>iteratedDerivWithin n (fun z => c + f z) s x = iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>iteratedDerivWithin n (derivWithin (fun z => c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>Set.EqOn (derivWithin (fun z => c + f z) s) (derivWithin f s) s
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<VAR>y : 𝕜<VAR>hy : y ∈ s<GOAL>derivWithin (fun z => c + f z) s y = derivWithin f s y
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>b✝ b : α<VAR>l : List α<VAR>hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l<VAR>a : α<VAR>h : Chain R a (b :: l)<GOAL>destutter' R a (b :: l) = a :: b :: l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>b✝ b : α<VAR>l : List α<VAR>hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l<VAR>a : α<VAR>h✝ : Chain R a (b :: l)<VAR>h : R a b<VAR>hc : Chain R b l<GOAL>destutter' R a (b :: l) = a :: b :: l
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b✝ : ↑B<VAR>hb : b✝ ∈ MonoidHom.range f<VAR>b : ↑B := b✝<GOAL>b • ↑(MonoidHom.range f) = ↑(MonoidHom.range f)
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b✝ : ↑B<VAR>hb : b✝ ∈ MonoidHom.range f<VAR>b : ↑B := b✝<GOAL>b • ↑(MonoidHom.range f) = 1 • ↑(MonoidHom.range f)
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b✝ : ↑B<VAR>hb : b✝ ∈ MonoidHom.range f<VAR>b : ↑B := b✝<GOAL>b⁻¹ ∈ MonoidHom.range f
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime x (y ^ n)
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime x (∏ _x ∈ range n, y)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<GOAL>𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>b : OrthonormalBasis (Fin (n + 1)) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<GOAL>o.volumeForm = -b.toBasis.det
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>b : OrthonormalBasis (Fin (n + 1)) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>o.volumeForm = -b.toBasis.det
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>b : OrthonormalBasis (Fin (n + 1)) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>Nat.casesAuxOn (motive := fun a => n + 1 = a → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ) (n + 1) (fun h => Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ) (fun [Fact (finrank ℝ E = 0)] o => ⋯.by_cases (fun x => AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x => -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) ⋯ o) (fun n_1 h => Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ) (fun [Fact (finrank ℝ E = n_1 + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o) ⋯ = -b.toBasis.det
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>b : OrthonormalBasis (Fin (n + 1)) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>e.toBasis.orientation ≠ b.toBasis.orientation
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>b : OrthonormalBasis (Fin (n + 1)) ℝ E<VAR>hb : b.toBasis.orientation ≠ o<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>e.toBasis.orientation = o
<VAR>x : ℝ<VAR>h₁ : -π < x<VAR>h₂ : x ≤ π<GOAL>(↑(expMapCircle x)).arg = x
<VAR>f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)<GOAL>∃ C, Tendsto f (𝓝[≠] 1) (𝓝 C)
<VAR>f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)<GOAL>∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z
<VAR>f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)<GOAL>(fun z => f z - f 1) =o[𝓝[≠] 1] fun z => (z - 1)⁻¹
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-x ‖ 0 ↔ x ‖ 0
<VAR>α : Type u_1<VAR>l m r : List Char<VAR>f : α → Char → α<VAR>init : α<GOAL>Substring.foldl f init { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } } = List.foldl f init m
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (M.mul ⊗ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M.X).hom = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (𝟙 (M.X ⊗ M.X) ⊗ (λ_ (𝟙_ C)).hom) ≫ (M.mul ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ M.mul ▷ 𝟙_ C) ≫ (ρ_ M.X).hom = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (M.X ⊗ M.X) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (M.X ⊗ M.X)).hom ≫ M.mul = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<GOAL>∫ (x : X) in ∅, f x ∂μ = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → ℕ → M<VAR>p : ℕ × ℕ<VAR>hp : p ∈ antidiagonal n<GOAL>f p n = f p (p.1 + p.2)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<GOAL>infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>r : ℝ≥0∞<VAR>h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r<GOAL>infEdist x s < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>r : ℝ≥0∞<VAR>h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ<GOAL>infEdist x s < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>r : ℝ≥0∞<VAR>y : α<VAR>hy : infEdist y s ≤ ENNReal.ofReal δ<VAR>hxy : edist x y < r - ENNReal.ofReal δ<GOAL>infEdist x s < r
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : 1 < finrank R M<GOAL>1 < Module.rank R M
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>L'' : Language<VAR>e'✝ : L' ≃ᴸ L''<VAR>e✝ e : L ≃ᴸ L'<VAR>e' : L' ≃ᴸ L''<GOAL>(e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>L'' : Language<VAR>e'✝ : L' ≃ᴸ L''<VAR>e✝ e : L ≃ᴸ L'<VAR>e' : L' ≃ᴸ L''<GOAL>(e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>b : B<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>h : φ.order.Dom<GOAL>(coeff R (φ.order.get h)) φ ≠ 0
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.lcm b).factorization = a.factorization ⊔ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
<VAR>a✝¹ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : ℕ<GOAL>(a.factorization + b.factorization) a✝ = (a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization) a✝
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a b✝ c✝ b c x : α<VAR>h : x * x - b * x + c = 0<GOAL>∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a b✝ c✝ b c x : α<VAR>h : x * x - b * x + c = 0<VAR>this : c = x * (b - x)<GOAL>∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a b✝ c✝ b c x : α<VAR>h : x * x - b * x + c = 0<VAR>this : c = x * (b - x)<GOAL>(b - x) * (b - x) - b * (b - x) + c = 0
<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>inst✝ : Nontrivial L<GOAL>chainLength α 0 = 2
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → m ≤ n + 1 → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯<VAR>self : motive (n + 1) ⋯<GOAL>leRec (motive := fun {n_1} mn => {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} → ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn) (fun {motive} of_succ self => self) (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self = of_succ n ⋯ self
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h : f ≫ sndX φ i = g ≫ sndX φ i<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : A ⟶ X φ i<VAR>h : f ≫ sndX φ i = g ≫ sndX φ i<GOAL>f ≫ (XIso φ i hi).hom = g ≫ (XIso φ i hi).hom
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : PseudoMetricSpace X<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>inst✝ : IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a b : α<VAR>h : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[<] b, s ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<GOAL>(condexpL1CLM F' hm μ) ↑f = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<VAR>hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g<GOAL>(condexpL1CLM F' hm μ) ↑f = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<VAR>hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g<GOAL>(condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<VAR>hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g<GOAL>∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ⊤), (fun g => (condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<VAR>hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g<GOAL>∀ ⦃f g : α → F'⦄ (hf : Memℒp f 1 (μ.trim hm)) (hg : Memℒp g 1 (μ.trim hm)), Disjoint (Function.support f) (Function.support g) → (fun g => (condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) (Memℒp.toLp f hf) → (fun g => (condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) (Memℒp.toLp g hg) → (fun g => (condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) (Memℒp.toLp f hf + Memℒp.toLp g hg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>f : ↥(lpMeas F' ℝ m 1 μ)<VAR>g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f<VAR>hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g<GOAL>IsClosed {f | (fun g => (condexpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g) = ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) f}