ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<VAR>a' : α<VAR>x' : E<VAR>ha'x' : a' ∈ u ∧ dist x' x < t - t'<VAR>y : E<VAR>hy : dist y (a', x').2 < t'<VAR>z : E<VAR>hz : dist z (a', x').2 < t'<VAR>dyx : dist y x ≤ t<GOAL>‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r s : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>L : E →L[𝕜] F<VAR>this✝ : ProperSpace E<VAR>a : α<VAR>x : E<VAR>r' : ℝ<VAR>hr : ∀ (y : E), dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r<VAR>Irr' : r / 2 < r'<VAR>Ir'r : r' ≤ r<VAR>ha : Continuous (f a)<VAR>t : ℝ<VAR>hrt : r / 2 < t<VAR>htr' : t < r'<VAR>t' : ℝ<VAR>hrt' : r / 2 < t'<VAR>ht't : t' < t<VAR>b : ℝ<VAR>b_lt : b < s * r<VAR>hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : b + 2 * ε < s * r<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>au : a ∈ u<VAR>hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε<VAR>this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)<VAR>a' : α<VAR>x' : E<VAR>ha'x' : a' ∈ u ∧ dist x' x < t - t'<VAR>y : E<VAR>hy : dist y (a', x').2 < t'<VAR>z : E<VAR>hz : dist z (a', x').2 < t'<VAR>dyx : dist y x ≤ t<VAR>dzx : dist z x ≤ t<GOAL>‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α✝<VAR>a✝ b✝ c : α✝<VAR>α : Type u_3<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(Icc a b).Subsingleton ↔ b ≤ a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α✝<VAR>a✝ b✝ c : α✝<VAR>α : Type u_3<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : (Icc a b).Subsingleton<GOAL>b ≤ a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α✝<VAR>a✝ b✝ c : α✝<VAR>α : Type u_3<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>¬(Icc a b).Subsingleton
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α✝<VAR>a✝ b✝ c : α✝<VAR>α : Type u_3<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>(Icc a b).Nontrivial
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>d : G.Dart<GOAL>d ∈ filter (fun d => d.toProd.1 = v) univ ↔ d ∈ image (G.dartOfNeighborSet v) univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>d : G.Dart<GOAL>d.toProd.1 = v ↔ ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d
<VAR>α : Type u_1<VAR>l : List α<VAR>this : DecidableEq α<GOAL>(powersetAux l).revzip ~ (powersetAux' l).revzip
<VAR>α : Type u_1<VAR>l : List α<VAR>this : DecidableEq α<GOAL>List.map (fun x => (x, ↑l - x)) (powersetAux l) ~ List.map (fun x => (x, ↑l - x)) (powersetAux' l)
<VAR>a s : ℝ<GOAL>(Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s
<VAR>a s : ℝ<GOAL>∀ (b c : ℝ), (Summable fun n => 1 / |↑n + b| ^ s) → Summable fun n => 1 / |↑n + c| ^ s
<VAR>a s b c : ℝ<VAR>h : Summable fun n => 1 / |↑n + b| ^ s<GOAL>∀ᶠ (x : ℕ) in atTop, 1 / |↑x + b| ^ s = 0 → 1 / |↑x + c| ^ s = 0
<VAR>a s b c : ℝ<VAR>h : Summable fun n => 1 / |↑n + b| ^ s<GOAL>Tendsto ((fun n => 1 / |↑n + c| ^ s) / fun n => 1 / |↑n + b| ^ s) atTop (𝓝 1)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<GOAL>gcd (b * a) (c * a) = gcd b c * normalize a
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>this✝ : Module.Finite R (n → R)<VAR>this : Module.Free R (n → R)<GOAL>A.rank ≤ Fintype.card n
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝⁴ : Fintype ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>u : (i : ι) → M i<VAR>m : E<GOAL>(fderivWithin 𝕜 (fun y => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<GOAL>μ s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<GOAL>∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<VAR>R : ℝ<GOAL>μ (s ∩ closedBall 0 R) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<VAR>R : ℝ<GOAL>Pairwise (Disjoint on fun n => {u n} + s ∩ closedBall 0 R)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<VAR>R : ℝ<VAR>n : ℕ<GOAL>{u n} + s ∩ closedBall 0 R ≤ {u n} + s
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c : ℂ<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<GOAL>fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongMono f<GOAL>Mono g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongMono f<GOAL>Mono (e.inv.left ≫ f ≫ e.hom.right)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongMono f<VAR>this : Mono (f ≫ e.hom.right)<GOAL>Mono (e.inv.left ≫ f ≫ e.hom.right)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongMono f<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>inst✝ : Epi z<GOAL>HasLiftingProperty z g
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : Set.Unbounded (fun x x_1 => x < x_1) s<GOAL>IsNormal (enumOrd s) ↔ IsClosed s
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : Set.Unbounded (fun x x_1 => x < x_1) s<VAR>Hs : StrictMono (enumOrd s)<GOAL>IsNormal (enumOrd s) ↔ IsClosed s
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : Set.Unbounded (fun x x_1 => x < x_1) s<VAR>Hs : StrictMono (enumOrd s)<VAR>h : IsNormal (enumOrd s)<VAR>ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Ordinal.{u}<VAR>hf : ∀ (i : ι), f i ∈ s<GOAL>sup f ∈ s
<VAR>s : Set Ordinal.{u}<VAR>a✝ : Ordinal.{u}<VAR>hs : Set.Unbounded (fun x x_1 => x < x_1) s<VAR>Hs : StrictMono (enumOrd s)<VAR>h : IsClosed s<VAR>a : Ordinal.{u}<VAR>ha : a.IsLimit<VAR>o : Ordinal.{u}<VAR>H : ∀ b < a, enumOrd s b ≤ o<GOAL>enumOrd s a ≤ o
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>⟪lp.single 2 i a, f⟫_𝕜 = ⟪a, ↑f i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>HasSum (fun i_1 => ⟪↑(lp.single 2 i a) i_1, ↑f i_1⟫_𝕜) ⟪a, ↑f i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>(fun i_1 => ⟪↑(lp.single 2 i a) i_1, ↑f i_1⟫_𝕜) = fun b' => if b' = i then ⟪a, ↑f i⟫_𝕜 else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<VAR>j : ι<GOAL>⟪↑(lp.single 2 i a) j, ↑f j⟫_𝕜 = if j = i then ⟪a, ↑f i⟫_𝕜 else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<VAR>j : ι<GOAL>⟪if h : j = i then ⋯ ▸ a else 0, ↑f j⟫_𝕜 = if j = i then ⟪a, ↑f i⟫_𝕜 else 0
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<GOAL>orderOf (xa i) = 2 ^ 2
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<VAR>this : Fact (Nat.Prime 2)<GOAL>orderOf (xa i) = 2 ^ 2
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<VAR>this : Fact (Nat.Prime 2)<GOAL>¬xa i ^ 2 ^ 1 = 1
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod (2 * n)<VAR>this : Fact (Nat.Prime 2)<GOAL>xa i ^ 2 ^ (1 + 1) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>v w : F<GOAL>((innerₗ F).flip v) w = ((innerₗ F) v) w
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderTop α<VAR>a b c : α<GOAL>Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>T : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<GOAL>lift f g = f ≫ inl + g ≫ inr
<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>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : DivisionSemiring α<VAR>inst✝⁴ : NeZero 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊓ y = 2⁻¹ • (x + y - |y - 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>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : DivisionSemiring α<VAR>inst✝⁴ : NeZero 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<VAR>this : Invertible 2 := invertibleOfNonzero ⋯<GOAL>x ⊓ y = 2⁻¹ • (x + y - |y - x|)
<VAR>x : ℤ[i]<GOAL>toComplex x = 0 ↔ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Fintype α<VAR>inst : optParam (Fintype (Sym2 α)) Sym2.instFintype<VAR>a✝ : Sym2 α<GOAL>a✝ ∈ univ.sym2 ↔ a✝ ∈ univ
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>f : Perm α<VAR>g : Perm β<VAR>i : (x : α) → f x ≠ x → β<VAR>h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)<VAR>hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂<VAR>hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y<VAR>x : { x // f x ≠ x }<GOAL>g (i ↑x ⋯) ≠ i ↑x ⋯
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>f : Perm α<VAR>g : Perm β<VAR>i : (x : α) → f x ≠ x → β<VAR>h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)<VAR>hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂<VAR>hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y<VAR>x : { x // f x ≠ x }<VAR>this : f (f ↑x) ≠ f ↑x<GOAL>g (i ↑x ⋯) ≠ i ↑x ⋯
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>f : Perm α<VAR>g : Perm β<VAR>i : (x : α) → f x ≠ x → β<VAR>h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)<VAR>hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂<VAR>hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y<VAR>x : { x // f x ≠ x }<VAR>this : f (f ↑x) ≠ f ↑x<GOAL>i (f ↑x) this ≠ i ↑x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>s' s t : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<VAR>h : s ⊆ t<GOAL>filterMap f s f_inj ⊆ filterMap f t f_inj
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>s' s t : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<VAR>h : s.val ≤ t.val<GOAL>(filterMap f s f_inj).val ≤ (filterMap f t f_inj).val
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>hs : IsOpen s<GOAL>s ∩ frontier s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Countable α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.toPMF.toMeasure s = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Countable α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x => μ {x}) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S✝ : Subsemigroup M<VAR>ι : Sort u_4<VAR>S : ι → Subsemigroup M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }<VAR>a✝ : P.obj (op X)<GOAL>(((Pi.lift fun f => P.map (↑f.snd).op) ≫ Pi.lift fun fg => Pi.π (fun f => P.obj (op f.fst)) fg.1 ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op) ≫ Pi.π (fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) fg) a✝ = (((Pi.lift fun f => P.map (↑f.snd).op) ≫ Pi.lift fun fg => Pi.π (fun f => P.obj (op f.fst)) fg.2 ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op) ≫ Pi.π (fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) fg) a✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }<VAR>a✝ : P.obj (op X)<GOAL>(P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op) a✝ = (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op) a✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }<VAR>a✝ : P.obj (op X)<VAR>this : HasPullback ↑fg.1.snd ↑fg.2.snd<GOAL>(P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op) a✝ = (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op) a✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>inst✝ : R.hasPullbacks<VAR>fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }<VAR>a✝ : P.obj (op X)<VAR>this : HasPullback ↑fg.1.snd ↑fg.2.snd<GOAL>P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.2.snd).op a✝ = (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op) a✝
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ~ l₂ ↔ ∀ (a : α), count a l₁ = count a l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>H : ∀ (a : α), count a l₁ = count a l₂<GOAL>l₁ ~ l₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i✝ j✝ : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → MulOneClass (f i)<VAR>x : (i : I) → f i<VAR>i j : I<GOAL>Commute (mulSingle i (x i)) (mulSingle j (x j))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i✝ j : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → MulOneClass (f i)<VAR>x : (i : I) → f i<VAR>i : I<GOAL>Commute (mulSingle i (x i)) (mulSingle i (x i))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i✝ j✝ : I<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : (i : I) → MulOneClass (f i)<VAR>x : (i : I) → f i<VAR>i j : I<VAR>hij : i ≠ j<GOAL>Commute (mulSingle i (x i)) (mulSingle j (x j))
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<GOAL>A.det = ∑ j : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<GOAL>A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<GOAL>A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<GOAL>(-1) ^ ↑i * (↑↑(sign i.cycleRange⁻¹) * A.det) = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<GOAL>↑↑(sign i.cycleRange⁻¹) * A.det = ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<GOAL>∑ j : Fin n.succ, (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j * ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det = ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<VAR>j : Fin n.succ<VAR>x✝ : j ∈ univ<GOAL>(-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j * ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det = (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det<VAR>j : Fin n.succ<VAR>x✝ : j ∈ univ<GOAL>(-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) j * (A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove).det) = (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)