ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>x✝ : Finset (α ⊕ β ⊕ γ)<GOAL>∀ (x : α) (x_1 : β) (x_2 : γ), (x, x_1, x_2) ∈ t → toTriangle (x, x_1, x_2) = x✝ → ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄ (x : α) (x_3 : β) (x_4 : γ), (x, x_3, x_4) ∈ t → toTriangle (x, x_3, x_4) = y → ¬x✝ = y → (↑x✝ ∩ ↑y).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c✝ c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>habc : (a, b, c) ∈ t<VAR>x : α<VAR>y : β<VAR>z : γ<VAR>hxyz : (x, y, z) ∈ t<VAR>h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)<GOAL>(↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c✝ c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>habc : (a, b, c) ∈ t<VAR>x : α<VAR>y : β<VAR>z : γ<VAR>hxyz : (x, y, z) ∈ t<VAR>h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)<VAR>this : (a, b, c) ≠ (x, y, z)<GOAL>(↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c✝ c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>habc : (a, b, c) ∈ t<VAR>x : α<VAR>y : β<VAR>z : γ<VAR>hxyz : (x, y, z) ∈ t<VAR>h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)<VAR>this : a = x → b = y → ¬c = z<GOAL>(↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a✝ a' : α<VAR>b✝ b' : β<VAR>c✝ c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>habc : (a, b, c) ∈ t<VAR>x : α<VAR>y : β<VAR>z : γ<VAR>hxyz : (x, y, z) ∈ t<VAR>h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)<VAR>this : a = x → b = y → ¬c = z<GOAL>(∀ (a_1 : α), Sum.inl a_1 = Sum.inl a → Sum.inl a_1 = Sum.inl x → (∀ (a_4 : α), Sum.inl a_4 = Sum.inl a → Sum.inl a_4 = Sum.inl x → Sum.inl a_1 = Sum.inl a_4) ∧ (∀ (a : β), Sum.inr (Sum.inl a) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inl a) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr z) → False) ∧ ∀ (b_1 : γ), Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) → False) ∧ (∀ (a_1 : β), Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr z) → (∀ (a_4 : α), Sum.inl a_4 = Sum.inl a → Sum.inl a_4 = Sum.inl x → False) ∧ (∀ (a : β), Sum.inr (Sum.inl a) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inl a) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr z) → Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl a)) ∧ ∀ (b_1 : γ), Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) → Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr b_1)) ∧ ∀ (b_1 : γ), Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) → (∀ (a_3 : α), Sum.inl a_3 = Sum.inl a → Sum.inl a_3 = Sum.inl x → False) ∧ (∀ (a : β), Sum.inr (Sum.inl a) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inl a) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a) = Sum.inr (Sum.inr z) → Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl a)) ∧ ∀ (b_2 : γ), Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inr c) → Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inr z) → Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr b_2)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<GOAL>Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : NonUnitalNonAssocSemiring R<VAR>inst✝ : NonUnitalNonAssocSemiring S<VAR>b : S<VAR>s : α →₀ R<VAR>f : α → R → S<GOAL>b * s.sum f = s.sum fun a c => b * f a c
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>↑f x ∈ Icc 0 1
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>this : ↑f x = 0 ∨ ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x<GOAL>↑f x ∈ Icc 0 1
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>h : ↑f x = 0<GOAL>0 ∈ Icc 0 1
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>h : ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x<GOAL>(↑f.toContDiffBump ∘ ↑(extChartAt I c)) x ∈ Icc 0 1
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : MonoCoprod C<VAR>I : Type u_2<VAR>X : I → C<VAR>c : Cofan X<VAR>h : IsColimit c<VAR>i : I<VAR>inst✝ : HasCoproduct fun k => X ↑k<VAR>ι : Unit → I := fun x => i<VAR>hι : Function.Injective ι<GOAL>Mono (c.inj i)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>b : β<VAR>v : Vector α n<VAR>f : α → β<GOAL>b ∈ (map f v).toList ↔ ∃ a ∈ v.toList, f a = b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F) (-1) = χ₄ ↑(Fintype.card F)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1<GOAL>(quadraticChar F) (-1) = χ₄ ↑(Fintype.card F)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1<GOAL>(if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1<VAR>n : ℕ<GOAL>(if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1<VAR>n : ℕ<VAR>h₂ : Even n<GOAL>(if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1<VAR>n : ℕ<VAR>h₂ : Odd n<GOAL>(if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : G →L[𝕜] E<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>x : G<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun x => g
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : G →L[𝕜] E<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>x : G<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x = (iteratedFDerivWithin 𝕜 i f univ (g x)).compContinuousLinearMap fun x => g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>(fun n => ε (b i * ↑n) - ε ↑n) =Θ[atTop] fun n => 1 / log ↑n ^ 2
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U : R<VAR>hU : ∀ᶠ (x : R) in map u f, (fun x x_1 => x ≥ x_1) x U<VAR>V : R<VAR>hV : ∀ᶠ (x : R) in map v f, (fun x x_1 => x ≥ x_1) x V<GOAL>IsBoundedUnder (fun x x_1 => x ≥ x_1) f (u + v)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U : R<VAR>hU : ∀ᶠ (x : R) in map u f, (fun x x_1 => x ≥ x_1) x U<VAR>V : R<VAR>hV : ∀ᶠ (x : R) in map v f, (fun x x_1 => x ≥ x_1) x V<GOAL>∀ᶠ (x : R) in map (u + v) f, (fun x x_1 => x ≥ x_1) x (U + V)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U V : R<VAR>hU : ∀ᶠ (a : α) in f, u a ≥ U<VAR>hV : ∀ᶠ (a : α) in f, v a ≥ V<GOAL>∀ᶠ (a : α) in f, u a + v a ≥ U + V
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0<GOAL>P.toPoly ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h0 : P.toPoly = 0<GOAL>P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h0 : P.toPoly = 0<GOAL>Cubic.a 0 = 0 ∧ Cubic.b 0 = 0 ∧ Cubic.c 0 = 0 ∧ Cubic.d 0 = 0
<VAR>i j : ℤ<GOAL>i.gcd j * i.lcm j = (i * j).natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b d : α<VAR>x y : WithBot α<GOAL>unbot' d x = unbot' d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>a x b c : E<GOAL>a + x ∈ [a + b-[𝕜]a + c] ↔ x ∈ [b-[𝕜]c]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : GroupWithZero G₀<VAR>inst✝ : ContinuousMul G₀<VAR>a : G₀<VAR>h : Tendsto Inv.inv (𝓝 1) (𝓝 1)<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>ContinuousAt Inv.inv x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : GroupWithZero G₀<VAR>inst✝ : ContinuousMul G₀<VAR>a : G₀<VAR>h : Tendsto Inv.inv (𝓝 1) (𝓝 1)<VAR>x : G₀<VAR>hx : x ≠ 0<VAR>hx' : x⁻¹ ≠ 0<GOAL>ContinuousAt Inv.inv x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : GroupWithZero G₀<VAR>inst✝ : ContinuousMul G₀<VAR>a : G₀<VAR>h : Tendsto Inv.inv (𝓝 1) (𝓝 1)<VAR>x : G₀<VAR>hx : x ≠ 0<VAR>hx' : x⁻¹ ≠ 0<GOAL>Tendsto ((fun x_1 => x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun x_1 => x * x_1) (𝓝 1) (𝓝 1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_neg : ∀ (x : R), f (-x) = f x<VAR>x y : R<GOAL>f (-x * y) / f y = f (x * y) / f y
<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>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f : α → β<VAR>s : Set α<VAR>e : α ≃ α<VAR>he : QuasiMeasurePreserving (⇑e) μ μ<VAR>he' : QuasiMeasurePreserving (⇑e.symm) μ μ<VAR>k : ℤ<VAR>hs : ⇑e '' s =ᵐ[μ] s<GOAL>⇑(e ^ k) '' s =ᵐ[μ] s
<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>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f : α → β<VAR>s : Set α<VAR>e : α ≃ α<VAR>he : QuasiMeasurePreserving (⇑e) μ μ<VAR>he' : QuasiMeasurePreserving (⇑e.symm) μ μ<VAR>k : ℤ<VAR>hs : ⇑e '' s =ᵐ[μ] s<GOAL>⇑(e ^ k).symm ⁻¹' s =ᵐ[μ] s
<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>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f : α → β<VAR>s : Set α<VAR>e : α ≃ α<VAR>he : QuasiMeasurePreserving (⇑e) μ μ<VAR>he' : QuasiMeasurePreserving (⇑e.symm) μ μ<VAR>hs : ⇑e '' s =ᵐ[μ] s<VAR>k : ℕ<GOAL>⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
<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>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f : α → β<VAR>s : Set α<VAR>e : α ≃ α<VAR>he : QuasiMeasurePreserving (⇑e) μ μ<VAR>he' : QuasiMeasurePreserving (⇑e.symm) μ μ<VAR>hs : ⇑e '' s =ᵐ[μ] s<VAR>k : ℕ<GOAL>⇑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a' : (quotient C (ComplexShape.up ℤ)).obj K₁ ⟶ (quotient C (ComplexShape.up ℤ)).obj K₂<VAR>ha' : a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b' : (quotient C (ComplexShape.up ℤ)).obj L₁ ⟶ (quotient C (ComplexShape.up ℤ)).obj L₂<VAR>hb' : b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>b' : (quotient C (ComplexShape.up ℤ)).obj L₁ ⟶ (quotient C (ComplexShape.up ℤ)).obj L₂<VAR>hb' : b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b'' : L₁ ⟶ L₂<VAR>hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b'' : L₁ ⟶ L₂<VAR>hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b'' : L₁ ⟶ L₂<VAR>hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)<VAR>γ : T₁ ⟶ T₂ := e₁.hom ≫ CochainComplex.mappingCone.trianglehMapOfHomotopy H ≫ e₂.inv<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b'' : L₁ ⟶ L₂<VAR>hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)<VAR>γ : T₁ ⟶ T₂ := e₁.hom ≫ CochainComplex.mappingCone.trianglehMapOfHomotopy H ≫ e₂.inv<VAR>comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃