ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>w : ι → Rˣ<GOAL>e.det ⇑(e.unitsSMul w) = ∏ i : ι, ↑(w i)
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<GOAL>Dependent f ↔ ¬Independent f
<VAR>n : Type u<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α : Type v<VAR>inst✝² : CommRing α<VAR>inst✝¹ : StarRing α<VAR>A✝ : Matrix n n α<VAR>β : Type v<VAR>inst✝ : CommRing β<VAR>A : Matrix n n β<GOAL>A ∈ orthogonalGroup n β ↔ star A * A = 1
<VAR>n : Type u<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α : Type v<VAR>inst✝² : CommRing α<VAR>inst✝¹ : StarRing α<VAR>A✝ : Matrix n n α<VAR>β : Type v<VAR>inst✝ : CommRing β<VAR>A : Matrix n n β<VAR>hA : star A * A = 1<GOAL>A * star A = 1
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<GOAL>¬IsSquare d
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<VAR>hp : a.x ^ 2 - d * a.y ^ 2 = 1<GOAL>¬IsSquare d
<VAR>b : ℤ<VAR>a : Solution₁ (b * b)<VAR>ha : 1 < a.x<VAR>hp : a.x ^ 2 - b * b * a.y ^ 2 = 1<GOAL>False
<VAR>b : ℤ<VAR>a : Solution₁ (b * b)<VAR>ha : 1 < a.x<VAR>hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1<GOAL>False
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℤ<VAR>c w : ℂ<VAR>R : ℝ<VAR>hn : n < 0<VAR>hw : w ∈ sphere c |R|<GOAL>(∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℤ<VAR>c w : ℂ<VAR>hn : n < 0<VAR>hw : w ∈ sphere c |0|<GOAL>(∮ (z : ℂ) in C(c, 0), (z - w) ^ n) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℤ<VAR>c w : ℂ<VAR>R : ℝ<VAR>hn : n < 0<VAR>hw : w ∈ sphere c |R|<VAR>h0 : R ≠ 0<GOAL>(∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<GOAL>x ∈ map f.toMonoidHom H.normalizer ↔ x ∈ (map f.toMonoidHom H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<GOAL>(∀ (h : G), h ∈ H ↔ f.symm x * h * (f.symm x)⁻¹ ∈ H) ↔ ∀ (h : N), f.symm h ∈ H ↔ f.symm (x * h * x⁻¹) ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<GOAL>∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a) ∈ H ↔ f.symm (x * f.toEquiv a * x⁻¹) ∈ H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<VAR>a✝ : G<GOAL>(a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a✝) ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<VAR>a✝ : G<GOAL>(a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (a✝ ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : G ≃* N<VAR>x : N<VAR>a✝ : G<GOAL>(a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (a✝ ∈ H ↔ f.symm x * f.symm (f.toEquiv a✝) * (f.symm x)⁻¹ ∈ H)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Monotone 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>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>r : R<GOAL>constantCoeff (C r) = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β → σ<VAR>ho : Primrec o<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>a : α<GOAL>(Nat.casesOn (encode (o a)) (encode (f a)) fun b => (encode ((decode (encode (a, b).1)).bind fun a => Option.map (g a) (decode b))).pred) = encode (Option.casesOn (o a) (f a) (g a))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>z : S<VAR>x : R<VAR>y : ↥M<VAR>h : z * (algebraMap R S) ↑y = (algebraMap R S) x<VAR>hx : x = 0<GOAL>z = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>z : S<VAR>x : R<VAR>y : ↥M<VAR>h : z * (algebraMap R S) ↑y = 0<VAR>hx : x = 0<GOAL>z = 0
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l f✝ f₁ f₂ : Filter α✝<VAR>g g₁ g₂ : Filter β<VAR>m : α✝ → β<VAR>m' : β → γ<VAR>s : Set α✝<VAR>t : Set β<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : ∀ (j : ι), Nonempty (α j)<VAR>i : ι<VAR>f : Filter (α i)<GOAL>(comap (eval i) f).NeBot ↔ f.NeBot
<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>n : ℕ<VAR>fs : Finset (Fin (n + 1))<VAR>h : fs.Nonempty<GOAL>∑ i : PointsWithCircumcenterIndex n, centroidWeightsWithCircumcenter fs i = 1
<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>n : ℕ<VAR>fs : Finset (Fin (n + 1))<VAR>h : fs.Nonempty<GOAL>(∑ x : Fin (n + 1), if x ∈ fs then (↑fs.card)⁻¹ else 0) = ∑ i : Fin (n + 1), (↑fs).indicator (centroidWeights ℝ fs) i
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<GOAL>s ∈ fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<GOAL>s ∈ fixedBy (Set α) g⁻¹
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<VAR>a : α<GOAL>a ∈ g⁻¹ • s ↔ a ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<VAR>a : α<GOAL>g • a ∈ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<VAR>a : α<VAR>h✝ : a ∈ fixedBy α g<GOAL>g • a ∈ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (fixedBy α g)ᶜ ⊆ s<VAR>a : α<VAR>h✝ : a ∉ fixedBy α g<GOAL>g • a ∈ s ↔ a ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hs₂ : IsOpen s<VAR>hx : x ∈ ε • s<GOAL>gauge s x < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hs₂ : IsOpen s<VAR>hx : x ∈ ε • s<VAR>this : ε⁻¹ • x ∈ s<GOAL>gauge s x < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hs₂ : IsOpen s<VAR>hx : x ∈ ε • s<VAR>this : ε⁻¹ • x ∈ s<VAR>h_gauge_lt : gauge s (ε⁻¹ • x) < 1<GOAL>gauge s x < ε
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.factors.prod = FactorSet.prod ↑{⟨p, hp⟩}
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p = match ↑{⟨p, hp⟩} with | none => 0 | some s => (Multiset.map Subtype.val s).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p = {p}.prod
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F.op ⟶ G.op<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(G.map f ≫ (fun X => (α.app (op X)).unop) Y).op = ((fun X => (α.app (op X)).unop) X ≫ F.map f).op
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>x : C(↑s, 𝕜)<GOAL>x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔ x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>x : C(↑s, 𝕜)<GOAL>(∃ y ∈ span 𝕜 {1}, ∃ z ∈ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule, y + z = x) ↔ x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
<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>point✝ : PointClass F<VAR>a✝ : Fin 3 → F<VAR>hP : W.NonsingularLift (Quot.mk Setoid.r a✝)<GOAL>(-mk hP).toAffineLift = -(mk hP).toAffineLift
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : b ≠ 0<VAR>ha : 2 ≤ a<VAR>h : a ^ n ∣ b<GOAL>n < b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : b ≠ 0<VAR>ha : 2 ≤ a<VAR>h : a ^ n ∣ b<GOAL>a ^ n < a ^ b
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<GOAL>∃ l, Chain r a l ∧ (a :: l).getLast ⋯ = b
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<GOAL>∃ l, Chain r b l ∧ (b :: l).getLast ⋯ = b
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<GOAL>∀ {a c : α}, r a c → Relation.ReflTransGen r c b → (∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b) → ∃ l, Chain r a l ∧ (a :: l).getLast ⋯ = b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>H = ⊥ ∨ Nontrivial ↥H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<VAR>this : Nontrivial ↥H ↔ H ≠ ⊥<GOAL>H = ⊥ ∨ Nontrivial ↥H
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Iio a * Iic b ⊆ Iio (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.10523) (N : Type ?u.10522) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Iio a * Iic b ⊆ Iio (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.10523) (N : Type ?u.10522) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : y ∈ Iio a<VAR>z : α<VAR>hzb : z ∈ Iic b<GOAL>(fun x x_1 => x * x_1) y z ∈ Iio (a * b)
<VAR>p : ℕ<VAR>z : ℤ<VAR>hp : p ≠ 1<VAR>hz : z ≠ 0<GOAL>padicValRat p ↑z = ↑((multiplicity (↑p) z).get ⋯)
<VAR>ι✝ : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n : A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>M : ι → Set A<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)
<VAR>ι✝ : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n : A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>M : ι → Set A<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∏ i ∈ ∅, span R (M i) = span R (∏ i ∈ ∅, M i)
<VAR>ι✝ : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M✝ N : Submodule R A<VAR>m n : A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>M : ι → Set A<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i) → ∏ i ∈ insert a s, span R (M i) = span R (∏ i ∈ insert a s, M i)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : (x : M) → x ∈ span R s → Prop<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯<VAR>x : M<VAR>hx : x ∈ span R s<GOAL>p x hx
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : (x : M) → x ∈ span R s → Prop<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯<VAR>x : M<VAR>hx : x ∈ span R s<GOAL>∃ (x_1 : x ∈ span R s), p x x_1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>T : Monad C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>{ obj := fun X => X, map := fun {X Y} f => f ≫ T.η.app Y }.map (f ≫ g) = (f ≫ T.η.app Y) ≫ T.map (g ≫ T.η.app Z) ≫ T.μ.app Z
<VAR>M : Type u<VAR>inst✝² : Monoid M<VAR>α : Type v<VAR>inst✝¹ : MulAction M α<VAR>β : Type u_1<VAR>inst✝ : MulAction M β<VAR>S : Submonoid M<VAR>a : α<VAR>g : ↥S<GOAL>(fun m => m • a) g ∈ orbit M a
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝¹ : StandardBorelSpace Ω<VAR>inst✝ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>hμ : IsFiniteMeasure μ<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>h_indep : CondIndepSet m hm t t μ<VAR>this : ∀ (a : Ω), IsFiniteMeasure ((condexpKernel μ m) a)<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝¹ : StandardBorelSpace Ω<VAR>inst✝ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>hμ : IsFiniteMeasure μ<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>h_indep : CondIndepSet m hm t t μ<VAR>this : ∀ (a : Ω), IsFiniteMeasure ((condexpKernel μ m) a)<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝¹ : StandardBorelSpace Ω<VAR>inst✝ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>hμ : IsFiniteMeasure μ<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>h_indep : CondIndepSet m hm t t μ<VAR>this : ∀ (a : Ω), IsFiniteMeasure ((condexpKernel μ m) a)<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<VAR>ω : Ω<VAR>hω_eq : (((condexpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω<VAR>hω : ((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = 1<GOAL>(μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝¹ : StandardBorelSpace Ω<VAR>inst✝ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>hμ : IsFiniteMeasure μ<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>h_indep : CondIndepSet m hm t t μ<VAR>this : ∀ (a : Ω), IsFiniteMeasure ((condexpKernel μ m) a)<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<VAR>ω : Ω<VAR>hω_eq : (((condexpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω<VAR>hω : ((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = 1<GOAL>(((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = ⊤) ∨ ((condexpKernel μ m) ω) t = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>s : ℤ<GOAL>Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>s : ℤ<VAR>this : Valued.v 1 = 1<GOAL>Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>s : ℤ<VAR>this : Valued.v ((single s) 1) = (Valued.v ((single (-s)) 1))⁻¹<GOAL>Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>s : ℤ<VAR>this : Valued.v ((single s) 1) * Valued.v ((single (-s)) 1) = 1<GOAL>Valued.v ((single (-s)) 1) ≠ 0
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (g_nat 0 a t) (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>g_nat 0 a t = fun i => rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>(↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>(↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t + ↑n * (-π * t))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c : RingCon R<GOAL>ringConGen ⇑c ≤ c
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c : RingCon R<GOAL>sInf {s | ∀ (x y : R), c x y → s x y} ≤ c
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m n : ℕ<GOAL>(Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n✝ : ℕ<VAR>h : ¬IsOfFinOrder x<VAR>n m : ℕ<VAR>hnm : (fun n => x ^ n) n = (fun n => x ^ n) m<GOAL>n = m
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>s : Set α<VAR>m : ι → OuterMeasure α<GOAL>(restrict s) (⨅ i, (restrict s) (m i)) = (restrict (range Subtype.val)) (⨅ i, (restrict s) (m i))
<VAR>a : ℤ<GOAL>|a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>(pderiv 2) (X 1 ^ 2 * X 2 + C W.a₁ * X 0 * X 1 * X 2 + C W.a₃ * X 1 * X 2 ^ 2 - (X 0 ^ 3 + C W.a₂ * X 0 ^ 2 * X 2 + C W.a₄ * X 0 * X 2 ^ 2 + C W.a₆ * X 2 ^ 3)) = X 1 ^ 2 + C W.a₁ * X 0 * X 1 + C (2 * W.a₃) * X 1 * X 2 - (C W.a₂ * X 0 ^ 2 + C (2 * W.a₄) * X 0 * X 2 + C (3 * W.a₆) * X 2 ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>↑2 * X 1 ^ (2 - 1) * 0 * X 2 + X 1 ^ 2 * 1 + (((0 * X 0 + C W.a₁ * 0) * X 1 + C W.a₁ * X 0 * 0) * X 2 + C W.a₁ * X 0 * X 1 * 1) + ((0 * X 1 + C W.a₃ * 0) * X 2 ^ 2 + C W.a₃ * X 1 * (↑2 * X 2 ^ (2 - 1) * 1)) - (↑3 * X 0 ^ (3 - 1) * 0 + ((0 * X 0 ^ 2 + C W.a₂ * (↑2 * X 0 ^ (2 - 1) * 0)) * X 2 + C W.a₂ * X 0 ^ 2 * 1) + ((0 * X 0 + C W.a₄ * 0) * X 2 ^ 2 + C W.a₄ * X 0 * (↑2 * X 2 ^ (2 - 1) * 1)) + (0 * X 2 ^ 3 + C W.a₆ * (↑3 * X 2 ^ (3 - 1) * 1))) = X 1 ^ 2 + C W.a₁ * X 0 * X 1 + 2 * C W.a₃ * X 1 * X 2 - (C W.a₂ * X 0 ^ 2 + 2 * C W.a₄ * X 0 * X 2 + 3 * C W.a₆ * X 2 ^ 2)
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>c ≠ 0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>c ^ 2 ≠ 0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>0 < c ^ 2
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>0 < (a ^ 2) ^ 2 + (b ^ 2) ^ 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>hn : Nonempty α<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<VAR>hb : ∀ (i : ι), (f i).NeBot<GOAL>(iInf f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>hn : Nonempty α<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<VAR>hb : ∀ (i : ι), (f i).NeBot<VAR>h✝ : IsEmpty ι<GOAL>(iInf f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>hn : Nonempty α<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<VAR>hb : ∀ (i : ι), (f i).NeBot<VAR>h✝ : Nonempty ι<GOAL>(iInf f).NeBot
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : PreservesFilteredColimits (forget C)<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (forget C)<VAR>inst✝¹ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<GOAL>IsIso (f.val.app (op U))