ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>ha : a < 0<VAR>k : ℤ<GOAL>a ^ (2 * k + 1) < 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>ha : a < 0<VAR>k : ℤ<GOAL>a ^ (2 * k) * a < 0
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>L : List (List α)<VAR>hL : ¬[] ∈ l₁ :: l₂ :: L<GOAL>Chain' R (l₁ :: l₂ :: L).join ↔ (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>L : List (List α)<VAR>hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L<GOAL>Chain' R (l₁ :: l₂ :: L).join ↔ (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>L : List (List α)<VAR>hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L<GOAL>(Chain' R l₁ ∧ ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).join.head? → R x y) ↔ (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧ (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>L : List (List α)<VAR>hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L<GOAL>(Chain' R l₁ ∧ ((Chain' R l₂ ∧ ∀ (x : List α), x ∈ L → Chain' R x) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).join.head? → R x y) ↔ (∀ (l : List α), l ∈ l₁ :: l₂ :: L → Chain' R l) ∧ (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>L : List (List α)<VAR>hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L<GOAL>(Chain' R l₁ ∧ Chain' R l₂ ∧ (∀ (x : List α), x ∈ L → Chain' R x) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ (∀ (x : List α), x ∈ L → Chain' R x) ∧ (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧ Chain' (fun l₁ l₂ => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>a : α<VAR>x✝ : a ∈ minimals (fun x x_1 => x ≤ x_1) ↑(upperClosure s)<VAR>b : α<VAR>hb : b ∈ s<VAR>hba : b ≤ a<VAR>right✝ : ∀ ⦃b : α⦄, b ∈ ↑(upperClosure s) → (fun x x_1 => x ≤ x_1) b a → (fun x x_1 => x ≤ x_1) a b<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>x✝ : b ∈ ↑(upperClosure s)<VAR>hba : (fun x x_1 => x ≤ x_1) b a<VAR>c : α<VAR>hc : c ∈ s<VAR>hcb : c ≤ b<GOAL>(fun x x_1 => x ≤ x_1) a b
<VAR>d n : ℤ<GOAL>ofInt n = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>f : Filter α<VAR>F : f.Realizer<GOAL>f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>f : Filter α<VAR>F : f.Realizer<GOAL>(∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>f : Filter α<VAR>F : f.Realizer<GOAL>(∃ x, F.F.f x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ≤ Realizer.bot.F.f b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>(∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>S.Exact ↔ IsIso (imageToKernel S.f S.g ⋯)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>Epi (imageToKernel S.f S.g ⋯) ↔ IsIso (imageToKernel S.f S.g ⋯)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → Option β<VAR>s : Multiset α<VAR>l : List α<GOAL>List.filterMap f (List.filter (fun b => decide (p b)) l) = List.filterMap (fun x => if p x then f x else none) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Irreducible p<VAR>u : αˣ<VAR>hu : p * ↑u = q<VAR>a b : α<VAR>hab : q = a * b<GOAL>q * ↑u⁻¹ = a * (b * ↑u⁻¹)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} 𝒮<VAR>inst✝³ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝² : p.IsStronglyCartesian f φ<VAR>R' R'' : 𝒮<VAR>a' a'' : 𝒳<VAR>f' : R' ⟶ S<VAR>f'' : R'' ⟶ S<VAR>g : R' ⟶ R<VAR>g' : R'' ⟶ R'<VAR>H : f' = g ≫ f<VAR>H' : f'' = g' ≫ f'<VAR>φ' : a' ⟶ b<VAR>φ'' : a'' ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian f' φ'<VAR>inst✝ : p.IsHomLift f'' φ''<GOAL>f'' = (g' ≫ g) ≫ f
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} 𝒮<VAR>inst✝³ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝² : p.IsStronglyCartesian f φ<VAR>R' R'' : 𝒮<VAR>a' a'' : 𝒳<VAR>f' : R' ⟶ S<VAR>f'' : R'' ⟶ S<VAR>g : R' ⟶ R<VAR>g' : R'' ⟶ R'<VAR>H : f' = g ≫ f<VAR>H' : f'' = g' ≫ f'<VAR>φ' : a' ⟶ b<VAR>φ'' : a'' ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian f' φ'<VAR>inst✝ : p.IsHomLift f'' φ''<GOAL>map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ ⋯ φ''
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} 𝒮<VAR>inst✝³ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝² : p.IsStronglyCartesian f φ<VAR>R' R'' : 𝒮<VAR>a' a'' : 𝒳<VAR>f' : R' ⟶ S<VAR>f'' : R'' ⟶ S<VAR>g : R' ⟶ R<VAR>g' : R'' ⟶ R'<VAR>H : f' = g ≫ f<VAR>H' : f'' = g' ≫ f'<VAR>φ' : a' ⟶ b<VAR>φ'' : a'' ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian f' φ'<VAR>inst✝ : p.IsHomLift f'' φ''<GOAL>(map p f' φ' H' φ'' ≫ map p f φ H φ') ≫ φ = φ''
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : IsPullback fst snd f g<VAR>inst✝ : HasPullback f g<GOAL>h.isoPullback.inv ≫ fst = pullback.fst f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ : ι →₀ α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a b : α<VAR>f1 f2 : ι →₀ α<GOAL>(f1 - f2).support ⊆ f1.support
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : NonUnitalNonAssocSemiring A<VAR>inst✝¹⁰ : Module R A<VAR>inst✝⁹ : Star A<VAR>inst✝⁸ : NonUnitalNonAssocSemiring B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : Star B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : Module R C<VAR>inst✝³ : Star C<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>IsClosed ↑s.innerDualCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>IsClosed (⋂ i, ↑{↑i}.innerDualCone)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>∀ (i : ↑s), IsClosed ↑{↑i}.innerDualCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>x : ↑s<GOAL>IsClosed ↑{↑x}.innerDualCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>x : ↑s<VAR>h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0<GOAL>IsClosed ↑{↑x}.innerDualCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>x : ↑s<VAR>h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0<GOAL>IsClosed (inner ↑x ⁻¹' Ici 0)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝ : Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>x : P<VAR>j : ι<GOAL>(b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) x
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝ : Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>x : P<VAR>j : ι<GOAL>(b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) ((Finset.affineCombination k Finset.univ ⇑b₂) fun i => (b₂.coord i) x)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝ : Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>x : P<VAR>j : ι<GOAL>(b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ ⇑b₂)) fun i => (b₂.coord i) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<GOAL>min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p r ≤ padicValRat p q<GOAL>min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p r ≤ padicValRat p q<GOAL>padicValRat p r ≤ padicValRat p (r + q)
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : LinearOrder α<VAR>a✝ b✝ c d a b : α<VAR>p : α → Prop<VAR>ha : p a<VAR>hb : p b<VAR>h : a ≤ b<GOAL>p (a ⊔ b)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : LinearOrder α<VAR>a✝ b✝ c d a b : α<VAR>p : α → Prop<VAR>ha : p a<VAR>hb : p b<VAR>h : b ≤ a<GOAL>p (a ⊔ b)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>u v : F<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>u v : F<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>(v ^ 3 * Q y * (u * P z) ^ 3 - u ^ 3 * P y * (v * Q z) ^ 3) * (P z * Q z) = (u * v) ^ 2 * (Q y * P z ^ 3 - P y * Q z ^ 3) * (u * P z * (v * Q z))
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ : ℝ<VAR>s✝ t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ : ℝ<VAR>s✝ t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ : ℝ<VAR>s✝ t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ : ℝ<VAR>s✝ t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>(EMetric.diam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>inst✝ : LocallyCompactSpace α<VAR>hs : IsCompact s<GOAL>∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>inst✝ : LocallyCompactSpace α<VAR>hs : IsCompact s<VAR>K : Set α<VAR>K_compact : IsCompact K<VAR>hK : s ⊆ interior K<GOAL>∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>inst✝ : LocallyCompactSpace α<VAR>hs : IsCompact s<VAR>K : Set α<VAR>K_compact : IsCompact K<VAR>hK : s ⊆ interior K<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : cthickening δ s ⊆ interior K<GOAL>∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>inst✝ : LocallyCompactSpace α<VAR>hs : IsCompact s<VAR>K : Set α<VAR>K_compact : IsCompact K<VAR>hK : s ⊆ interior K<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : cthickening δ s ⊆ interior K<GOAL>IsCompact (cthickening δ s)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>f : α → β<GOAL>map (fun x => (f x, x)) l = (map f l).zip l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>f : α → β<GOAL>(map f l).zip (map (fun x => x) l) = (map f l).zip l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>f : α → β<GOAL>map (fun x => x) l = l
<VAR>α : Type u_1<VAR>p✝ : α → Prop<VAR>inst✝ : DecidablePred p✝<VAR>l✝ : List α<VAR>a✝ : α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>ih : l.any p = true ↔ ∃ a, a ∈ l ∧ p a = true<GOAL>(a :: l).any p = true ↔ ∃ a_1, a_1 ∈ a :: l ∧ p a_1 = true
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : MulPosMono α<VAR>inst✝ : MulPosReflectLE α<VAR>a0 : 0 < a<GOAL>a ≤ b * a ↔ 1 * a ≤ b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>val✝ : Fintype ι<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>val✝ : Fintype ι<GOAL>∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>num (-g) z / denom (-g) z = num g z / denom g z
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>num (-g) z * denom g z = num g z * denom (-g) z
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(-(↑(↑↑g 0 0) * ↑z) + -↑(↑↑g 0 1)) * (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) = (↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)) * (-(↑(↑↑g 1 0) * ↑z) + -↑(↑↑g 1 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 E<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = adjoint B ↔ ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 E<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜<VAR>i : ι<GOAL>A (b i) = (adjoint B) (b i)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>(∃ u, u.card = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : ↥A<VAR>p : K[X]<VAR>ne_zero : p ≠ 0<VAR>aeval_eq : (aeval ↑x) p = 0<GOAL>(↑x)⁻¹ ∈ A
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : ↥A<VAR>p : K[X]<VAR>ne_zero : p ≠ 0<VAR>aeval_eq : (aeval x) p = 0<GOAL>(↑x)⁻¹ ∈ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommMonoid α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>∏ i : { x // x ∈ range n }, f ↑i = ∏ i ∈ range n, f i
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>i : SetLike A B<VAR>p q : A<GOAL>p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m✝ : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>f y = p.partialSum m (y - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m✝ : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : y - x ∈ EMetric.ball 0 r<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>f y = p.partialSum m (y - x)
<VAR>x : ℝ<VAR>hx : x < 0<GOAL>x < sin x
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>1 = lift.{v, u} a ↔ 1 = a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>DiffContOnCl ℂ (fun z => invInterpStrip f z ε) (verticalStrip 0 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>Differentiable ℂ fun z => invInterpStrip f z ε
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 0)) ^ (y - 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>Differentiable ℂ fun y => (↑ε + ↑(sSupNormIm f 1)) ^ (-y)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>(LinearIndependent K fun o => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>LinearIndependent K (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧ (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ≠ 0 ∧ ((((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ∈ span K (range (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) → (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default = 0) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>LinearIndependent K (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧ ¬x = 0 ∧ (x ∈ span K (range (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) → x = 0) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>h : LinearIndependent K v ∧ x ∉ span K (range v)<GOAL>¬x = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>y z : V<VAR>h : LinearIndependent K v ∧ 0 ∉ span K (range v)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<VAR>h : s ⊆ e.source<GOAL>↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>s t : Set β<VAR>hs : IsCompl s t<VAR>ha : HasProd (f ∘ Subtype.val) a<VAR>hb : HasProd (f ∘ Subtype.val) b<GOAL>HasProd f (a * b)
<GOAL>arctan 2⁻¹ + arctan 3⁻¹ = π / 4