ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : SemilatticeSup γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsLUB s b<GOAL>IsLUB (insert a s) (a ⊔ b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : SemilatticeSup γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsLUB s b<GOAL>IsLUB ({a} ∪ s) (a ⊔ b)
<VAR>r x : ℝ<VAR>hx : 0 ≤ x<GOAL>exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x)))
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<GOAL>mapIdx f l = [] ↔ l = []
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_5<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>iCondIndepFun m' hm' m f μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_5<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>(∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']) ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_5<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>∀ (i : ι), Measurable (f i)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise fun x y => Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise fun x y => Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : a * b ^ m < a * b ^ (n + 1)<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : a * b ^ m < a * b ^ (n + 1)<VAR>i2 : a * b ^ n < a * b ^ (m + 1)<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : m ≤ n<VAR>i2 : n ≤ m<GOAL>m = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : RegularSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasProd f a<VAR>hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)<GOAL>HasProd g a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<GOAL>upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<VAR>α : W.LeftFraction φ.Y' φ'.Y'<VAR>hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<VAR>α : W.LeftFraction φ.Y' φ'.Y'<VAR>hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f<VAR>ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<VAR>α : W.LeftFraction φ.Y' φ'.Y'<VAR>hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f<VAR>ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯<VAR>this : IsIso (L.map φ'.s)<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<VAR>α : W.LeftFraction φ.Y' φ'.Y'<VAR>hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f<VAR>ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯<VAR>this✝ : IsIso (L.map φ'.s)<VAR>this : IsIso (L.map α.s)<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f f' : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<VAR>φ' : W.LeftFraction X Y<VAR>hφ' : f' = φ'.map L ⋯<VAR>α : W.LeftFraction φ.Y' φ'.Y'<VAR>hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f<VAR>ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯<VAR>this✝¹ : IsIso (L.map φ'.s)<VAR>this✝ : IsIso (L.map α.s)<VAR>this : IsIso (L.map (φ'.s ≫ α.s))<GOAL>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>IsCompl a b ↔ IsCompl ↑a ↑b
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n<GOAL>(p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n<GOAL>n = n - k + k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ᵐ ⊓ a⁻ᵐ = 1
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>M : Type u_2<VAR>inst✝ : AddCommMonoid M<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → Prepartition J<VAR>f : Box ι → M<GOAL>∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>M : Type u_2<VAR>inst✝ : AddCommMonoid M<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → Prepartition J<VAR>f : Box ι → M<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ ↑π.boxes<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ ↑π.boxes<VAR>hne : J₁ ≠ J₂<VAR>J' : Box ι<VAR>h₁' : J' ∈ (fun J => (πi J).boxes) J₁<VAR>h₂' : J' ∈ (fun J => (πi J).boxes) J₂<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>(x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>(x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>y = (x ◃ x) ◃ x ◃⁻¹ y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>y = x ◃ x ◃⁻¹ y
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>LipschitzWith 1 ⇑equivRealProd
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (Iic a) = ⊤
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (Iio a) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>map (Quotient.mk J) I = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>I ≤ J
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n✝ n : ℕ<VAR>ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s<VAR>m : Sym α (n + 1)<GOAL>m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n✝ n : ℕ<VAR>ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s<VAR>m : Sym α (n + 1)<GOAL>(∃ v ∈ s, m ∈ image (Sym.cons v) (s.sym n)) → ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n✝ n : ℕ<VAR>ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s<VAR>m : Sym α (n + 1)<VAR>h : ∀ a ∈ m, a ∈ s<GOAL>∃ v ∈ s, m ∈ image (Sym.cons v) (s.sym n)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>hd : s ⊆ interior t<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>hd : s ⊆ interior t<VAR>f : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, f x = 0<VAR>h1 : ∀ᶠ (x : M) in 𝓝ˢ s, f x = 1<VAR>hf : ∀ (x : M), f x ∈ Icc 0 1<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>hd : s ⊆ interior t<VAR>f : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, f x = 0<VAR>h1 : ∀ᶠ (x : M) in 𝓝ˢ s, f x = 1<VAR>hf : ∀ (x : M), f x ∈ Icc 0 1<VAR>x : M<VAR>hx : x ∉ t<GOAL>f x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>hfp : map f p = 0<VAR>x : R<GOAL>f x = f x * f p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>hfp : map f p = 0<VAR>x : R<GOAL>f x * (map f p).coeff p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hp : p.Monic<VAR>h : ∀ (x : R), f x = 0<VAR>n : ℕ<GOAL>(map f p).coeff n = coeff 0 n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>h : cfc f a = cfc g a<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>Set.EqOn f g (spectrum R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>h : (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } = (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }<GOAL>Set.EqOn f g (spectrum R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>h : (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } = (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }<VAR>this : { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } = { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }<GOAL>Set.EqOn f g (spectrum R a)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x y : M<GOAL>ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<GOAL>(β_ (𝟙_ C) (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom = (λ_ (𝟙_ C)).hom
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarRing A<VAR>inst✝² : ContinuousStar A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : StarModule ℂ A<VAR>a b : ↥(selfAdjoint A)<VAR>h : Commute ↑a ↑b<GOAL>↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarRing A<VAR>inst✝² : ContinuousStar A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : StarModule ℂ A<VAR>a b : ↥(selfAdjoint A)<VAR>h : Commute ↑a ↑b<VAR>hcomm : Commute (I • ↑a) (I • ↑b)<GOAL>↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : IsCyclotomicExtension ∅ A B<GOAL>⊥ = ⊤
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>b - a + a = b ↔ a ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a + (b - a) = b ↔ a ≤ b
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤
<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>chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β = chainLength α β
<VAR>x y : ℤ<GOAL>toComplex { re := x, im := y } = ↑x + ↑y * I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Finite<VAR>h : s ⊆ t<VAR>hst : t.encard = s.encard + 1<GOAL>∃ a, t = insert a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Finite<VAR>h : s ⊆ t<VAR>hst : ∃ x, t \ s = {x}<GOAL>∃ a, t = insert a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Finite<VAR>h : s ⊆ t<VAR>x : α<VAR>hx : t \ s = {x}<GOAL>∃ a, t = insert a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Finite<VAR>h : s ⊆ t<VAR>x : α<VAR>hx : t \ s = {x}<GOAL>t = insert x s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>y : N ⊗[R] Q<GOAL>(inverse Q hfg hg) ((rTensor Q g) y) = Submodule.Quotient.mk y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : LT α<VAR>s : Finset ι<VAR>f : ι → WithBot α<GOAL>⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a / mabs a = (a⁻ᵐ ^ 2)⁻¹
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>S : Set G<VAR>hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap<VAR>hS2 : closure S = ⊤<VAR>h : IsPretransitive G α<GOAL>Function.Surjective ⇑(toPermHom G α)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>S : Set G<VAR>hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap<VAR>hS2 : closure S = ⊤<VAR>h : IsPretransitive G α<GOAL>(toPermHom G α).range = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>S : Set G<VAR>hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap<VAR>hS2 : closure S = ⊤<VAR>h : IsPretransitive G α<VAR>this : IsPretransitive (↥(toPermHom G α).range) α<GOAL>(toPermHom G α).range = ⊤