ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<GOAL>A.det = ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).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<GOAL>∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding (univ ×ˢ univ), sign σ • ∏ i : Fin n.succ, A (σ i) i = ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).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<GOAL>∑ x : Fin n.succ, ∑ y : Perm (Fin n), sign (decomposeFin.symm (x, y)) • ∏ x_1 : Fin n.succ, A ((decomposeFin.symm (x, y)) x_1) x_1 = ∑ x : Fin n.succ, (-1) ^ ↑x * A x 0 * (of fun i j => A (x.succAbove i) j.succ).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>x✝ : i ∈ univ<GOAL>∑ y : Perm (Fin n), sign (decomposeFin.symm (0, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (0, y)) x) x = (-1) ^ ↑0 * A 0 0 * (of fun i j => A (Fin.succAbove 0 i) j.succ).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>x✝ : i✝ ∈ univ<VAR>i : Fin n<GOAL>∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x = (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).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>x✝ : i✝ ∈ univ<VAR>i : Fin n<VAR>this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)<GOAL>∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x = (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).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>x✝ : i✝ ∈ univ<VAR>i : Fin n<VAR>this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)<GOAL>∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x = ∑ i_1 : Perm (Fin n), -1 * (A i.succ 0 * sign i_1 • ∏ i_2 : Fin n, (of fun i_3 j => A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2)
<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>x✝¹ : i✝ ∈ univ<VAR>i : Fin n<VAR>this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)<VAR>σ : Perm (Fin n)<VAR>x✝ : σ ∈ univ<GOAL>sign (decomposeFin.symm (i.succ, σ)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x = -1 * (A i.succ 0 * sign σ • ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)
<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>x✝¹ : i✝ ∈ univ<VAR>i : Fin n<VAR>this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)<VAR>σ : Perm (Fin n)<VAR>x✝ : σ ∈ univ<GOAL>(-1 * sign σ) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x = -1 * (A i.succ 0 * sign σ • ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)
<VAR>x y : ℂ<GOAL>x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>x y : ℂ<GOAL>(if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>p : List α → Prop<VAR>base : p []<VAR>ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])<VAR>q : List α → Prop := fun l => p l.reverse<GOAL>∀ (l : List α), p l
<VAR>α : Type u<VAR>β : Type v<VAR>p : List α → Prop<VAR>base : p []<VAR>ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])<VAR>q : List α → Prop := fun l => p l.reverse<VAR>pq : ∀ (l : List α), p l.reverse → q l<GOAL>∀ (l : List α), p l
<VAR>α : Type u<VAR>β : Type v<VAR>p : List α → Prop<VAR>base : p []<VAR>ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])<VAR>q : List α → Prop := fun l => p l.reverse<VAR>pq : ∀ (l : List α), p l.reverse → q l<VAR>qp : ∀ (l : List α), q l.reverse → p l<GOAL>∀ (l : List α), p l
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>((toLinearMap₂ b₁ b₁) J).IsAdjointPair ((toLinearMap₂ b₂ b₂) J') ((toLin b₁ b₂) A) ((toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>(toLinearMap₂ b₂ b₂) J' ∘ₗ (toLin b₁ b₂) A = ((toLinearMap₂ b₁ b₁) J).compl₂ ((toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'<GOAL>(toLinearMap₂ b₂ b₂) J' ∘ₗ (toLin b₁ b₂) A = ((toLinearMap₂ b₁ b₁) J).compl₂ ((toLin b₂ b₁) A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'<GOAL>Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'
<VAR>α : Type<VAR>n : ℕ<VAR>xs : Vector α n<VAR>β σ₁ γ σ₂ : Type<VAR>f₁ : α → β → σ₁ → σ₁ × γ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<VAR>R : σ₁ → σ₂ → Prop<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2<VAR>n✝ : ℕ<VAR>xs✝ : Vector α n✝<VAR>ys✝ : Vector β n✝<VAR>x✝ : α<VAR>y✝ : β<VAR>a✝ : ∀ {s₁ : σ₁} {s₂ : σ₂}, R s₁ s₂ → R (mapAccumr₂ f₁ xs✝ ys✝ s₁).1 (mapAccumr₂ f₂ xs✝ ys✝ s₂).1 ∧ (mapAccumr₂ f₁ xs✝ ys✝ s₁).2 = (mapAccumr₂ f₂ xs✝ ys✝ s₂).2<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>h₀ : R s₁ s₂<GOAL>R (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).1 (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).1 ∧ (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).2 = (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h : m < n<GOAL>(if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h : m < n<VAR>h_not : ¬∃ j, ∃ (_ : j ∈ Set.Icc n m), u j ω ∈ s<GOAL>(if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h : m < n<VAR>h_not : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>(if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) = m
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : IsPushout f g inl inr<VAR>h' : IsPushout f g inl' inr'<GOAL>inr' ≫ (isoIsPushout X Y h h').inv = inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f a ∂c • μ = c * ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this : Memℒp f ⊤ μ<GOAL>Memℒp f p μ
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>S₁ S₂ : Split C<VAR>F₁ : S₁.X ⟶ S₂.X<VAR>f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n<VAR>c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>F₂ : S₁.X ⟶ S₂.X<VAR>c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n<GOAL>{ F := F₁, f := f₁, comm := c₁ } = { F := F₂, f := f₁, comm := c₂ }
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>S₁ S₂ : Split C<VAR>F₁ : S₁.X ⟶ S₂.X<VAR>f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n<VAR>c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>F₂ : S₁.X ⟶ S₂.X<VAR>c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n<GOAL>F₁ = F₂
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>S₁ S₂ : Split C<VAR>F₁ : S₁.X ⟶ S₂.X<VAR>f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n<VAR>c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>F₂ : S₁.X ⟶ S₂.X<VAR>c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op [n]) = f₁ n ≫ S₂.s.ι n<VAR>h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n<GOAL>∀ (n : ℕ), S₁.s.φ F₁ n = S₁.s.φ F₂ n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>L : Set X<VAR>L_compact : IsCompact L<VAR>L_closed : IsClosed L<VAR>KL : K ⊆ interior L<VAR>LU : L ⊆ U<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>L : Set X<VAR>L_compact : IsCompact L<VAR>L_closed : IsClosed L<VAR>KL : K ⊆ interior L<VAR>LU : L ⊆ U<VAR>A : closure (interior L) ⊆ L<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>L : Set X<VAR>L_compact : IsCompact L<VAR>L_closed : IsClosed L<VAR>KL : K ⊆ interior L<VAR>LU : L ⊆ U<VAR>A : closure (interior L) ⊆ L<GOAL>IsCompact (closure (interior L))
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n => χ ↑n) s))
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y Z : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C<VAR>inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C<VAR>inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)<VAR>x : FunctorObjIndex f πX<GOAL>f x.i ≫ Sigma.ι (functorObjTgtFamily f πX) x ≫ ρFunctorObj f πX = x.t ≫ ιFunctorObj f πX
<VAR>a b : Cardinal.{u_1}<GOAL>a + b ≤ max (max a b) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<GOAL>a + b ≤ max (max a b) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha : a < ℵ₀<GOAL>a + b ≤ max (max a b) ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0<VAR>h0 : a = 0 → Nonempty ι<GOAL>⨅ i, f i * a = (⨅ i, f i) * a
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CharP R p<VAR>P : Type u₃<VAR>inst✝³ : CommSemiring P<VAR>inst✝² : CharP P p<VAR>inst✝¹ : PerfectRing P p<VAR>inst✝ : PerfectRing R p<VAR>f : ℕ → R<VAR>hf : ∀ (n : ℕ), f (n + 1) ^ p = f n<VAR>n✝ n : ℕ<VAR>ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n<GOAL>(⇑(frobeniusEquiv R p).symm)^[n.succ] (f 0) ^ p = f n.succ ^ p
<VAR>α : Type u_1<VAR>I✝ B X : Set α<VAR>inst✝ : DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<VAR>I : Set α<GOAL>(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔ ∀ (J : Finset α), ↑J ⊆ I → Indep J
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>l : E →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>hs₁ : IsOpen s<VAR>hs₂ : s.Nonempty<VAR>hs₃ : ∀ x ∈ s, l x ≠ 0<GOAL>Continuous ⇑l
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>l : E →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>hs₁ : IsOpen s<VAR>hs₂ : s.Nonempty<VAR>hs₃ : ∀ x ∈ s, l x ≠ 0<VAR>hl : Dense ↑(ker l)<GOAL>False
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>l : E →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>hs₁ : IsOpen s<VAR>hs₃ : ∀ x ∈ s, l x ≠ 0<VAR>hl : Dense ↑(ker l)<VAR>x : E<VAR>hx : x ∈ s<GOAL>False
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>l : E →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>hs₁ : IsOpen s<VAR>hs₃ : ∀ x ∈ s, l x ≠ 0<VAR>hl : Dense ↑(ker l)<VAR>x : E<VAR>hx : x ∈ s<VAR>this : x ∈ interior (↑(ker l))ᶜ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<GOAL>f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<GOAL>(∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>h : ¬q = 0<GOAL>(p * q).natDegree = (q * p).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>h : ¬q = 0<GOAL>q.leadingCoeff * p.leadingCoeff ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, s.min = ↑b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h✝ : a ∈ s<VAR>b : α<VAR>h : s.inf WithTop.some = ↑b<VAR>right✝ : b ≤ a<GOAL>∃ b, s.min = ↑b
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>f 0 ((ComplexShape.up ℕ).prev 0) ≫ Q.d ((ComplexShape.up ℕ).prev 0) 0 = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>¬(ComplexShape.up ℕ).Rel 0 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>#ι < ℵ₀
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>lift.{?u.168006, w} #ι < lift.{?u.168006, w} ℵ₀
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>lift.{?u.168006, w} #ι ≤ ?b
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>?b < lift.{?u.168006, w} ℵ₀
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type w<VAR>inst✝ : Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>Cardinal.{max w ?u.168006}
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>1 ≤ star x ↔ 1 ≤ x