ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>𝕜✝ : Type u_2<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜✝<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜✝ F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ G<VAR>inst✝⁹ : NormedAddCommGroup H<VAR>inst✝⁸ : NormedSpace 𝕜✝ H<VAR>𝕝 : Type u_7<VAR>inst✝⁷ : NontriviallyNormedField 𝕝<VAR>inst✝⁶ : NormedAlgebra 𝕜✝ 𝕝<VAR>A✝ : Type u_8<VAR>inst✝⁵ : NormedRing A✝<VAR>inst✝⁴ : NormedAlgebra 𝕜✝ A✝<VAR>𝕜 : Type u_10<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>A : Type u_9<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormOneClass A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>(formalMultilinearSeries_geometric 𝕜 A).radius ≤ 1
<VAR>α : Type u_1<VAR>𝕜✝ : Type u_2<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜✝<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜✝ F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ G<VAR>inst✝⁹ : NormedAddCommGroup H<VAR>inst✝⁸ : NormedSpace 𝕜✝ H<VAR>𝕝 : Type u_7<VAR>inst✝⁷ : NontriviallyNormedField 𝕝<VAR>inst✝⁶ : NormedAlgebra 𝕜✝ 𝕝<VAR>A✝ : Type u_8<VAR>inst✝⁵ : NormedRing A✝<VAR>inst✝⁴ : NormedAlgebra 𝕜✝ A✝<VAR>𝕜 : Type u_10<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>A : Type u_9<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormOneClass A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>h : f ≠ 0<VAR>h₀ : ∀ {α : Type ?u.167292} {β : Type ?u.167295} (f : α → β), (fun x => x) ∘ f = f<VAR>h₁ : ∀ {α : Type ?u.167360} {β : Type ?u.167363} (f : α → β), (f ∘ fun x => x) = f<VAR>h₂ : WithBot.some = Nat.cast<GOAL>((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>h : f ≠ 0<VAR>h₀ : ∀ {α β : Type} (f : α → β), (fun x => x) ∘ f = f<VAR>h₁ : ∀ {α : Type ?u.167360} {β : Type ?u.167363} (f : α → β), (f ∘ fun x => x) = f<VAR>h₂ : WithBot.some = Nat.cast<VAR>h' : (((finSuccEquiv R n) f).support.sup fun x => x) = degreeOf 0 f<GOAL>((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Odd (m - n) ↔ (Odd m ↔ Even n)
<VAR>a x z x✝ : ℂ<GOAL>x✝ ∈ (fun θ => cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(¬∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(∃ s, IsOpen s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(withDensity 0 f) s = 0 s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, f a ∂0 = 0 s
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>x y : ℝ<GOAL>sin x ^ 2 ≤ 1
<VAR>x y : ℝ<GOAL>sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : ¬p₁ = p₂<VAR>hp₃p₂ : ¬p₃ = p₂<GOAL>∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : ¬p₁ = p₂<VAR>hp₃p₂ : ¬p₃ = p₂<GOAL>p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<GOAL>R ∈ J.sieves X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<GOAL>∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ J.sieves Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y✝ : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>Sieve.pullback f R ∈ J.sieves Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y✝ : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>Sieve.pullback f R = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y✝ : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>Sieve.pullback f S ≤ Sieve.pullback f R
<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>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : γ → β → δ<VAR>n : α → γ<GOAL>map₂ m (map n f) g = map₂ (fun a b => m (n a) b) f g
<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>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : γ → β → δ<VAR>n : α → γ<GOAL>map ((fun p => m p.1 p.2) ∘ fun p => (n p.1, id p.2)) (f ×ˢ g) = map (fun p => m (n p.1) p.2) (f ×ˢ g)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<GOAL>(erase n p).coeff n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>hn : 1 < n<VAR>t : Finset β<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>hn : 1 < n<VAR>t : Finset β<VAR>f : α ↪ β<GOAL>(∃ s, G.IsClique ↑s ∧ map f s = t) ∧ t.card = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s✝ : Finset α<VAR>a b c : α<VAR>hn : 1 < n<VAR>f : α ↪ β<VAR>s : Finset α<VAR>hs : G.IsNClique n s<GOAL>(∃ s_1, G.IsClique ↑s_1 ∧ map f s_1 = map f s) ∧ (map f s).card = n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>h₁.f' ≫ cyclesMap' φ h₁ h₂ = φ.τ₁ ≫ h₂.f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>x : ℝ≥0<GOAL>‖↑x‖ = ↑x
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>a : Fin n<GOAL>0 < a ↔ a ≠ 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e e' : Pretrivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<VAR>hx : x = inclusion ⋯ ⟨↑x, ⋯⟩<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<VAR>hx : x = inclusion ⋯ ⟨↑x, ⋯⟩<VAR>hy : y = inclusion ⋯ ⟨↑y, ⋯⟩<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<VAR>hx : x = inclusion ⋯ ⟨↑x, ⋯⟩<VAR>hy : y = inclusion ⋯ ⟨↑y, ⋯⟩<VAR>hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k<GOAL>iUnionLift S f hf (iUnion S) ⋯ (op x y) = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)<VAR>x y : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>j : ι<VAR>hj : ↑y ∈ S j<VAR>k : ι<VAR>hik : S i ≤ S k<VAR>hjk : S j ≤ S k<VAR>hx : x = inclusion ⋯ ⟨↑x, ⋯⟩<VAR>hy : y = inclusion ⋯ ⟨↑y, ⋯⟩<VAR>hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k<GOAL>f k ⟨↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)), hxy⟩ = f k (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)
<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>f✝ g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>f : α → ℝ≥0∞<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
<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>f✝ g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>f : α → ℝ≥0∞<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : E ≃ₐ[F] E<VAR>x : ↑(p.rootSet E)<VAR>ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)<GOAL>↑(ψ (ψ.symm (↑((↑ϕ).restrictNormalAux p.SplittingField) (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) ↑((rootsEquivRoots p E).symm x))))) = ϕ ↑x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : E ≃ₐ[F] E<VAR>x : ↑(p.rootSet E)<VAR>ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)<GOAL>↑(↑((↑ϕ).restrictNormalAux p.SplittingField) (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) ↑((rootsEquivRoots p E).symm x))) = ϕ ↑x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : E ≃ₐ[F] E<VAR>x : ↑(p.rootSet E)<VAR>ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)<GOAL>ϕ ↑((rootsEquivRoots p E) ((rootsEquivRoots p E).symm x)) = ϕ ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<GOAL>∃ M, IsMaxChain r M ∧ c ⊆ M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>H : ∃ m ∈ {s | c ⊆ s ∧ IsChain r s}, c ⊆ m ∧ ∀ a ∈ {s | c ⊆ s ∧ IsChain r s}, m ⊆ a → a = m<GOAL>∃ M, IsMaxChain r M ∧ c ⊆ M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<GOAL>∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s}, IsChain (fun x x_1 => x ⊆ x_1) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>cs : Set (Set α)<VAR>hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}<VAR>hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs<VAR>s : Set α<VAR>hs : s ∈ cs<GOAL>∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ cs, s ⊆ ub
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>cs : Set (Set α)<VAR>hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}<VAR>hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs<VAR>s : Set α<VAR>hs : s ∈ cs<GOAL>IsChain r (⋃₀ cs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>cs : Set (Set α)<VAR>hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}<VAR>hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs<VAR>s : Set α<VAR>hs : s ∈ cs<VAR>y : α<VAR>sy : Set α<VAR>hsy : sy ∈ cs<VAR>hysy : y ∈ sy<VAR>z : α<VAR>sz : Set α<VAR>hsz : sz ∈ cs<VAR>hzsz : z ∈ sz<VAR>hyz : y ≠ z<GOAL>r y z ∨ r z y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>cs : Set (Set α)<VAR>hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}<VAR>hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs<VAR>s : Set α<VAR>hs : s ∈ cs<VAR>y : α<VAR>sy : Set α<VAR>hsy : sy ∈ cs<VAR>hysy : y ∈ sy<VAR>z : α<VAR>hyz : y ≠ z<VAR>hsz : sy ∈ cs<VAR>hzsz : z ∈ sy<GOAL>r y z ∨ r z y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<VAR>cs : Set (Set α)<VAR>hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}<VAR>hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs<VAR>s : Set α<VAR>hs : s ∈ cs<VAR>y : α<VAR>sy : Set α<VAR>hsy : sy ∈ cs<VAR>hysy : y ∈ sy<VAR>z : α<VAR>sz : Set α<VAR>hsz : sz ∈ cs<VAR>hzsz : z ∈ sz<VAR>hyz : y ≠ z<VAR>hsseq : sy ≠ sz<GOAL>r y z ∨ r z y
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : Semiring R<VAR>s : AddSubmonoid R<VAR>n : ℕ<GOAL>s ^ n = closure (↑s ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : E'' → F''<VAR>s : Set E''<VAR>x₀ : E''<VAR>n : ℕ<VAR>h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hx₀ : x₀ ∈ s<VAR>hn : n ≠ 0<GOAL>‖x₀ - x₀‖ ^ n = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : Center C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<VAR>U : C<GOAL>(f.f ⊗ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd.β U).hom = ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ⊗ g.f)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<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>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>m : M₁<GOAL>((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁) m = ((AlgHom.id R (CliffordAlgebra Q₁)).toLinearMap ∘ₗ ι Q₁) m
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M₁<VAR>n : ℕ<VAR>hn : finrank R M = n.succ<GOAL>0 < n.succ
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Subsingleton A<VAR>a : A<GOAL>σ a = ∅
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<GOAL>multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<VAR>hx_odd : Odd x<GOAL>multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<GOAL>multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<GOAL>multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<GOAL>2 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<GOAL>¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>i : ℕ<GOAL>¬2 ^ (1 + 1) ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)