ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<VAR>R : Finpartition (s \ t)<VAR>hR₁ : ∀ x ∈ R.parts, x.card = m ∨ x.card = m + 1<VAR>hR₂ : ∀ x ∈ (P.avoid t).parts, (x \ (filter (fun y => y ⊆ x) R.parts).biUnion id).card ≤ m<VAR>hR₃ : (filter (fun i => i.card = m + 1) R.parts).card = if 0 < a then b else b - 1<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<VAR>R : Finpartition (s \ t)<VAR>hR₁ : ∀ x ∈ R.parts, x.card = m ∨ x.card = m + 1<VAR>hR₂ : ∀ x ∈ (P.avoid t).parts, (x \ (filter (fun y => y ⊆ x) R.parts).biUnion id).card ≤ m<VAR>hR₃ : (filter (fun i => i.card = m + 1) R.parts).card = if 0 < a then b else b - 1<GOAL>∀ x ∈ (R.extend ⋯ ⋯ ⋯).parts, x.card = m ∨ x.card = m + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<VAR>R : Finpartition (s \ t)<VAR>hR₁ : ∀ x ∈ R.parts, x.card = m ∨ x.card = m + 1<VAR>hR₂ : ∀ x ∈ (P.avoid t).parts, (x \ (filter (fun y => y ⊆ x) R.parts).biUnion id).card ≤ m<VAR>hR₃ : (filter (fun i => i.card = m + 1) R.parts).card = if 0 < a then b else b - 1<GOAL>∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) (R.extend ⋯ ⋯ ⋯).parts).biUnion id).card ≤ m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<VAR>R : Finpartition (s \ t)<VAR>hR₁ : ∀ x ∈ R.parts, x.card = m ∨ x.card = m + 1<VAR>hR₂ : ∀ x ∈ (P.avoid t).parts, (x \ (filter (fun y => y ⊆ x) R.parts).biUnion id).card ≤ m<VAR>hR₃ : (filter (fun i => i.card = m + 1) R.parts).card = if 0 < a then b else b - 1<GOAL>(filter (fun i => i.card = m + 1) (R.extend ⋯ ⋯ ⋯).parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<VAR>ht : t.Nonempty<VAR>hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = (s \ t).card<VAR>R : Finpartition (s \ t)<VAR>hR₁ : ∀ x ∈ R.parts, x.card = m ∨ x.card = m + 1<VAR>hR₂ : ∀ x ∈ (P.avoid t).parts, (x \ (filter (fun y => y ⊆ x) R.parts).biUnion id).card ≤ m<VAR>hR₃ : (filter (fun i => i.card = m + 1) R.parts).card = if 0 < a then b else b - 1<GOAL>(if ¬0 < a then insert t (filter (fun i => i.card = m + 1) R.parts) else filter (fun i => i.card = m + 1) R.parts).card = b
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<VAR>t : Finset G<VAR>ht : K ⊆ ⋃ x ∈ t, interior ((fun x_1 => x * x_1) ⁻¹' V)<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1<GOAL>(map f m).prod = f i ^ count i m
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>l : List ι<VAR>hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦l⟧ → f i' = 1<GOAL>(map f ⟦l⟧).prod = f i ^ count i ⟦l⟧
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R✝ : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>R : WSeq α → WSeq β → Prop<VAR>h1 : R s t<VAR>h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct<GOAL>Computation.LiftRel (LiftRelO R✝ (LiftRel R✝)) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R✝ : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>R : WSeq α → WSeq β → Prop<VAR>h1 : R s t<VAR>h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R✝ R a b → LiftRelO R✝ (LiftRel R✝) a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R✝ : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>R : WSeq α → WSeq β → Prop<VAR>h1 : R s t<VAR>h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct<GOAL>∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R✝ s t
<VAR>d : Nat<VAR>n : Int<VAR>a : Nat<VAR>d0 : d ≠ 0<VAR>a0 : a ≠ 0<GOAL>normalize (n * ↑a) (d * a) ⋯ = normalize n d d0
<VAR>d : Nat<VAR>n : Int<VAR>a : Nat<VAR>d0 : d ≠ 0<VAR>a0 : a ≠ 0<GOAL>normalize (n * ↑a) (d * a) ⋯ = normalize (↑a * n) (a * d) ⋯
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂<GOAL>c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>lift.{max u w, w} #↥((closure L).toFun s) ≤ #(L.Term ↑s)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ lift.{w, max u w} #(L.Term ↑s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.82138, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.82138, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>ShortComplex.mk ((F.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯ ≅ ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>t : Cardinal.{max u w}<VAR>hf : BddAbove (range f)<VAR>w : ∀ (i : ι), lift.{u, w} (f i) ≤ t<GOAL>lift.{u, w} (iSup f) ≤ t
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>t : Cardinal.{max u w}<VAR>hf : BddAbove (range f)<VAR>w : ∀ (i : ι), lift.{u, w} (f i) ≤ t<GOAL>⨆ i, lift.{u, w} (f i) ≤ t
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<GOAL>Submartingale (-f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>(-f) i ≤ᶠ[ae μ] μ[(-f) j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>(-f) i ≤ᶠ[ae μ] -μ[f j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝¹ : Ω<VAR>a✝ : (μ[f j|↑ℱ i]) a✝¹ ≤ f i a✝¹<GOAL>(-f) i a✝¹ ≤ (-μ[f j|↑ℱ i]) a✝¹
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : upcrossings a b f ω ≠ ⊤<GOAL>¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k<GOAL>¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k<GOAL>¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k<VAR>h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a<VAR>h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω<GOAL>False
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k<VAR>h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a<VAR>h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω<GOAL>False
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>hab : a < b<VAR>hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k<VAR>h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a<VAR>h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω<GOAL>¬∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B X X' Y Y' Z : C<VAR>inst✝ : Closed A<GOAL>uncurry (𝟙 ((ihom A).obj X)) = (ihom.ev A).app X
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>↑⁅I, N⁆ = Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>↑⁅I, N⁆ ≤ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ ↑⁅I, N⁆
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>max a b ≠ c
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>(if a ≤ b then b else a) ≠ c
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>(haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>this : IsCompact (haarProduct ↑K₀)<GOAL>(haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>this : IsCompact (haarProduct ↑K₀)<VAR>t : Finset (OpenNhdsOf 1)<GOAL>(haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>this : IsCompact (haarProduct ↑K₀)<VAR>t : Finset (OpenNhdsOf 1)<VAR>V₀ : Set G := ⋂ V ∈ t, V.carrier<GOAL>(haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>this : IsCompact (haarProduct ↑K₀)<VAR>t : Finset (OpenNhdsOf 1)<VAR>V₀ : Set G := ⋂ V ∈ t, V.carrier<VAR>h1V₀ : IsOpen V₀<GOAL>(haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>this : IsCompact (haarProduct ↑K₀)<VAR>t : Finset (OpenNhdsOf 1)<VAR>V₀ : Set G := ⋂ V ∈ t, V.carrier<VAR>h1V₀ : IsOpen V₀<VAR>h2V₀ : 1 ∈ V₀<GOAL>(haarProduct ↑K₀ ∩ ⋂ i ∈ t, clPrehaar (↑K₀) i).Nonempty
<VAR>A : Type u_1<VAR>inst✝ : SeminormedGroup A<VAR>n : ℕ<VAR>δ : ℝ<VAR>a : A<GOAL>a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ ball b δ
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange P<VAR>hP' : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : R ⟶ T<VAR>H : P g<VAR>this✝ : Algebra ↑R ↑S := toAlgebra f<VAR>this : Algebra ↑R ↑T := toAlgebra g<GOAL>P (pushout.inl f g)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange P<VAR>hP' : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : R ⟶ T<VAR>H : P g<VAR>this✝ : Algebra ↑R ↑S := toAlgebra f<VAR>this : Algebra ↑R ↑T := toAlgebra g<GOAL>P ({ cocone := CommRingCat.pushoutCocone ↑R ↑S ↑T, isColimit := CommRingCat.pushoutCoconeIsColimit ↑R ↑S ↑T }.cocone.ι.app WalkingSpan.left)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : StableUnderBaseChange P<VAR>hP' : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : R ⟶ T<VAR>H : P g<VAR>this✝ : Algebra ↑R ↑S := toAlgebra f<VAR>this : Algebra ↑R ↑T := toAlgebra g<GOAL>P Algebra.TensorProduct.includeLeftRingHom
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R✝ R : Presieve X<GOAL>IsSheafFor P R ↔ IsSheafFor P (generate R).arrows
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R✝ R : Presieve X<GOAL>(IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P (generate R).arrows
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R✝ R : Presieve X<GOAL>(IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSeparatedFor P (generate R).arrows ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t