ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = S.g ≫ x<GOAL>(S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯ = 0
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.83401, u_1} C<VAR>inst✝⁵ : Category.{?u.83405, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>X Y : C<VAR>m : M<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>inst✝⁵ : Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>X Y : C<VAR>m : M<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>(F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' = (F.shift a).map ((shiftFunctor C n).map f) ≫ (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫ (F.shiftIso mn a a'' ⋯).hom.app Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(pullback (D.f i j) (D.f i k))<GOAL>invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) = (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(unop (op U)), is_open' := ⋯ })) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(pullback (D.f i j) (D.f i k))<VAR>e : invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯) = (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(unop (op U)), is_open' := ⋯ }))<GOAL>invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) = (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(unop (op U)), is_open' := ⋯ })) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>U : Opens ↑↑(pullback (D.f i j) (D.f i k))<VAR>e : ∀ {Z : C} (h : (D.V (k, i)).presheaf.obj (op ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj { carrier := ⇑(D.t' k i j).base ⁻¹' ↑U, is_open' := ⋯ })) ⟶ Z), invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯) ≫ h = (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) { carrier := ⇑(D.t' k i j).base ⁻¹' ↑U, is_open' := ⋯ } ≫ h<GOAL>invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) = invApp (pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯)
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o a b : Ordinal.{u}<VAR>ha : a < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o<VAR>hb : b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o<GOAL>op a b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o a b : Ordinal.{u}<VAR>ha : ∃ n, a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<VAR>hb : ∃ n, b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<GOAL>∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o a b : Ordinal.{u}<VAR>m : ℕ<VAR>hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o<VAR>n : ℕ<VAR>hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<GOAL>∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o a b : Ordinal.{u}<VAR>m : ℕ<VAR>hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o<VAR>n : ℕ<VAR>hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<VAR>h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<GOAL>∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>o a b : Ordinal.{u}<VAR>m : ℕ<VAR>hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o<VAR>n : ℕ<VAR>hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o<VAR>h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o<GOAL>∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
<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>h₁ : IsOpen s₁<VAR>h₂ : IsOpen s₂<GOAL>IsOpen (s₁ ∪ s₂)
<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>h₁ : IsOpen s₁<VAR>h₂ : IsOpen s₂<GOAL>IsOpen (⋃ b, bif b then s₁ else s₂)
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>l✝ l : List α<GOAL>l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>l✝ l : List α<GOAL>l✝ ∈ ↑l.cyclicPermutations ↔ ↑l✝ = Quotient.mk'' l
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<GOAL>(increment hP G ε).IsEquipartition
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<GOAL>∃ b, ∀ a ∈ ↑(increment hP G ε).parts, a.card = b ∨ a.card = b + 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>A : Finset α<VAR>hA : A ∈ ↑(increment hP G ε).parts<GOAL>A.card = m ∨ A.card = m + 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>A : Finset α<VAR>hA : ∃ A_1, ∃ (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts<GOAL>A.card = m ∨ A.card = m + 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>A U : Finset α<VAR>hU : U ∈ P.parts<VAR>hA : A ∈ (chunk hP G ε hU).parts<GOAL>A.card = m ∨ A.card = m + 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g<VAR>a b : G<VAR>hab : (a, b) ∈ A ×ˢ B<VAR>h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2<GOAL>∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g<VAR>a b : G<VAR>hab : (a, b) ∈ A ×ˢ B<VAR>h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2<VAR>ha : (a, b).1 ∈ A<VAR>hb : (a, b).2 ∈ B<GOAL>∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
<VAR>α β : LinOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget LinOrd).obj α<GOAL>(↑e ≫ ↑e.symm) x = (𝟙 α) x
<VAR>α β : LinOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget LinOrd).obj β<GOAL>(↑e.symm ≫ ↑e) x = (𝟙 β) x
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x y : R<VAR>I J : Ideal R<GOAL>span {x} * I = span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>S : Subgroupoid D<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>𝟙 c ∈ (comap φ S).arrows c c
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>S : Subgroupoid D<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>𝟙 (φ.obj c) ∈ S.arrows (φ.obj c) (φ.obj c)
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>S : Subgroupoid D<VAR>Sn : S.IsNormal<VAR>c✝ d✝ : C<VAR>f : c✝ ⟶ d✝<VAR>γ : c✝ ⟶ c✝<VAR>hγ : γ ∈ (comap φ S).arrows c✝ c✝<GOAL>Groupoid.inv f ≫ γ ≫ f ∈ (comap φ S).arrows d✝ d✝
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>S : Subgroupoid D<VAR>Sn : S.IsNormal<VAR>c✝ d✝ : C<VAR>f : c✝ ⟶ d✝<VAR>γ : c✝ ⟶ c✝<VAR>hγ : γ ∈ (comap φ S).arrows c✝ c✝<GOAL>Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj d✝)
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>e : f ≅ g<GOAL>e.inv.right ≫ e.hom.right = 𝟙 g.right
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i : ℤ<VAR>h : y ∈ zpowers x<GOAL>orderOf y ∣ orderOf x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x : G<VAR>i k : ℤ<VAR>h : x ^ k ∈ zpowers x<GOAL>orderOf (x ^ k) ∣ orderOf x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x : G<VAR>i k : ℤ<VAR>h : x ^ k ∈ zpowers x<GOAL>(x ^ k) ^ orderOf x = 1
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>t : ℂ<GOAL>∫ (x : ℝ), cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>t : ℂ<GOAL>∫ (x : ℝ), cexp (-b * ↑x ^ 2 + I * t * ↑x + 0) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>a : α<VAR>inst✝¹ : Countable β<VAR>inst✝ : MeasurableSingletonClass β<VAR>μ : Measure α<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>a✝ : MeasurableSet s<GOAL>(map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>a : α<VAR>inst✝¹ : Countable β<VAR>inst✝ : MeasurableSingletonClass β<VAR>μ : Measure α<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>a✝ : MeasurableSet s<VAR>this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})<GOAL>(map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>m : (i : ι) → E i<VAR>i : ι<VAR>hi : ‖m i‖ = 0<GOAL>‖f m‖ = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r<VAR>I : Ideal S<VAR>hI : I ≠ ⊤<VAR>x : S<VAR>r s : R<VAR>hr : IsUnit (f s)<VAR>hr' : f s * x = f r<GOAL>1 ∉ I
<VAR>k m n : Nat<VAR>H : k.Coprime m<GOAL>m.gcd (n * k) = m.gcd n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℤ<VAR>x : G<GOAL>f (n • a + x) = f x + n • b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>(sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>(if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
<VAR>R : Type u_1<VAR>n : ℕ<VAR>w✝ : ℤ<GOAL>(1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>w✝ : ℤ<GOAL>1 % 4 = 1
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → SeminormedGroup (π i)<VAR>inst✝ : SeminormedGroup E<VAR>f x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<GOAL>M.support = M.verts
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w : V<VAR>h : M.IsMatching<VAR>v : V<VAR>hv : v ∈ M.verts<GOAL>v ∈ M.support
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>↑a ≤ max ↑b ↑c ↔ a ≤ max b c
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>x : S<VAR>h : x ∈ I<GOAL>↑(absNorm I) ∣ (Algebra.norm ℤ) x
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>x : S<VAR>h : x ∈ I<GOAL>absNorm I ∣ absNorm (span {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>σ : Perm n<VAR>M : Matrix n n R<GOAL>sign σ • detRowAlternating M = ↑↑(sign σ) * M.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint (mulSupport f) s ↔ EqOn f 1 s
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : TopologicalSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSemiring R<VAR>B : Type u_3<VAR>inst✝³ : Semiring B<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>toAlgHom✝¹ : A →ₐ[R] B<VAR>cont✝¹ : Continuous (↑↑toAlgHom✝¹.toRingHom).toFun<VAR>toAlgHom✝ : A →ₐ[R] B<VAR>cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun<GOAL>↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔ toAlgHom✝¹ = toAlgHom✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>s : Set Y<GOAL>closure (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure s \ f ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>s : Set Y<GOAL>closure (f ⁻¹' s) ⊆ f ⁻¹' closure 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 : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.negAddY (P x / P z ^ 2) (P x / P z ^ 2) (P y / P z ^ 3) (-n / (P z * d)) = (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) / (P z * d) ^ 3
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>hs : s ⊆ f.source<GOAL>MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>hs : s ⊆ f.source<GOAL>↑I '' (f.target ∩ ↑f.symm ⁻¹' s) ⊆ ↑I '' (↑f.symm ⁻¹' s)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<GOAL>M.Base (M.E \ B) ↔ B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<GOAL>M.Base (M.E \ B) ↔ (∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<VAR>h : M.Base (M.E \ B)<VAR>I : Set α<VAR>hI : I ⊆ M.E<VAR>B' : Set α<VAR>x✝ : M.Base B' ∧ Disjoint I B'<VAR>hBI : B ⊆ I<VAR>hB' : M.Base B'<VAR>hIB' : Disjoint I B'<GOAL>I ⊆ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<VAR>x✝ : (∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hBB' : Disjoint B B'<VAR>h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<GOAL>M.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<VAR>x✝ : (∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hBB' : Disjoint B B'<VAR>h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<GOAL>M.Base (M.E \ (M.E \ B'))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<VAR>x✝ : (∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hBB' : Disjoint B B'<VAR>h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.Base x ∧ Disjoint y x → B ⊆ y → B = y<GOAL>B ⊆ M.E \ B'
<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 x : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<VAR>q : G.Walk w x<GOAL>(p.concat h).append q = p.append (cons h q)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommGroup G<VAR>g : G ⧸ torsion G<VAR>hne : g ≠ 1<VAR>hfin : IsOfFinOrder g<GOAL>g = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommGroup G<VAR>g : G<VAR>hne : ↑g ≠ 1<VAR>hfin : IsOfFinOrder ↑g<GOAL>↑g = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommGroup G<VAR>g : G<VAR>hne : ↑g ≠ 1<VAR>hfin : IsOfFinOrder ↑g<VAR>m : ℕ<VAR>mpos : 0 < m<VAR>hm : ↑g ^ m = 1<GOAL>↑g = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommGroup G<VAR>g : G<VAR>hne : ↑g ≠ 1<VAR>hfin : IsOfFinOrder ↑g<VAR>m : ℕ<VAR>mpos : 0 < m<VAR>hm : ↑g ^ m = 1<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : (fun x => x ^ m) g ^ n = 1<GOAL>↑g = 1
<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>a b : G<GOAL>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>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => f x / r) l atBot ↔ r < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>(s \ t).ncard + t.ncard = (s ∪ t).ncard
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i j : Fin n✝<VAR>n : ℕ<GOAL>succAbove 1 1 = 2
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>LieIdeal.map f I ≤ f.idealRange
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>LieIdeal.map f I ≤ LieIdeal.map f ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>h : x ∈ closure s<GOAL>infEdist x s = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>h : x ∈ closure s<GOAL>infEdist x (closure s) = 0
<VAR>α : Sort u_1<VAR>inst✝ : Unique α<VAR>p : α → Prop<VAR>h : p default<VAR>x : α<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>t : Finset β<VAR>s : Finset α<VAR>f : α → Finset β<GOAL>t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>t : Finset β<VAR>s : Finset α<VAR>f : α → Finset β<GOAL>(s.biUnion fun x => f x ∩ t) = s.biUnion fun x => t ∩ f x