ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<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>F : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : Ring E<VAR>inst✝³ : Algebra F E<VAR>inst✝² : StrongRankCondition F<VAR>inst✝¹ : NoZeroSMulDivisors F E<VAR>inst✝ : Nontrivial E<GOAL>LinearIndependent F fun (x : ↑{1}) => ↑x
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<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>F : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : Ring E<VAR>inst✝³ : Algebra F E<VAR>inst✝² : StrongRankCondition F<VAR>inst✝¹ : NoZeroSMulDivisors F E<VAR>inst✝ : Nontrivial E<VAR>this : Nontrivial F := Module.nontrivial F E<GOAL>LinearIndependent F fun (x : ↑{1}) => ↑x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Preorder β<VAR>u : α → β<VAR>h : Tendsto u atTop atTop<VAR>a : α<VAR>b : β<VAR>this : Nonempty α<GOAL>∃ a' ≥ a, b ≤ u a'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Preorder β<VAR>u : α → β<VAR>h : Tendsto u atTop atTop<VAR>a : α<VAR>b : β<VAR>this✝ : Nonempty α<VAR>this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x<GOAL>∃ a' ≥ a, b ≤ u a'
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z : ℍ<VAR>r : ℝ<VAR>w : ℂ<VAR>h : dist w ↑(z.center r) ≤ z.im * Real.sinh r<GOAL>dist (↑(z.center r)) w ≤ z.im * Real.sinh r
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a✝ b a : α<GOAL>(replicate 0 a).Nodup ↔ 0 ≤ 1
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<GOAL>y ∈ cylinder x n ↔ x ∈ cylinder y n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<GOAL>{x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<GOAL>{x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<GOAL>{x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<GOAL>{x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<GOAL>⋂ i ∈ fs, T ↑i ⋯ ⊆ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯<VAR>h₁ : (a₁, a₂).1 ∈ s<GOAL>(f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯<VAR>h₁ : (a₁, a₂).1 ∈ s<VAR>a : ↑s<VAR>ha : a ∈ fs<VAR>haU : (a₁, a₂).1 ∈ U ↑a ⋯<GOAL>(f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯<VAR>h₁ : (a₁, a₂).1 ∈ s<VAR>a : ↑s<VAR>ha : a ∈ fs<VAR>haU : (a₁, a₂).1 ∈ U ↑a ⋯<GOAL>(f (a₁, a₂).1, f (a₁, a₂).2) ∈ t ○ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯<VAR>h₁ : (a₁, a₂).1 ∈ s<VAR>a : ↑s<VAR>ha : a ∈ fs<VAR>haU : (a₁, a₂).1 ∈ U ↑a ⋯<GOAL>(a₁, a₂).1 ∈ ball (a₁, a₂).1 (T ↑a ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : SymmetricRel t<VAR>htr : t ○ t ⊆ r<VAR>U : (a : α) → a ∈ s → Set α<VAR>hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a<VAR>T : (a : α) → a ∈ s → Set (α × α)<VAR>hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α<VAR>hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}<VAR>fs : Finset ↑s<VAR>hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯<VAR>a₁ a₂ : α<VAR>h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯<VAR>h₁ : (a₁, a₂).1 ∈ s<VAR>a : ↑s<VAR>ha : a ∈ fs<VAR>haU : (a₁, a₂).1 ∈ U ↑a ⋯<GOAL>(a₁, a₂).2 ∈ ball (a₁, a₂).1 (T ↑a ⋯)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>x' : Dual 𝕜 E<VAR>c : 𝕜<VAR>hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖<VAR>c_zero : ¬c = 0<GOAL>c⁻¹ • x' ∈ polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>x' : Dual 𝕜 E<VAR>c : 𝕜<VAR>hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖<VAR>c_zero : ¬c = 0<VAR>eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖<GOAL>c⁻¹ • x' ∈ polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>x' : Dual 𝕜 E<VAR>c : 𝕜<VAR>hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖<VAR>c_zero : ¬c = 0<VAR>eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖<VAR>le : ∀ z ∈ s, ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖<GOAL>c⁻¹ • x' ∈ polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>x' : Dual 𝕜 E<VAR>c : 𝕜<VAR>hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖<VAR>c_zero : ¬c = 0<VAR>eq : ∀ (z : E), ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖<VAR>le : ∀ z ∈ s, ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖<VAR>cancel : ‖c⁻¹‖ * ‖c‖ = 1<GOAL>c⁻¹ • x' ∈ polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>(f.extend I).source = f.source
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>h : b ∈ closedBall a r<GOAL>‖b / a‖ ≤ r
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b : R<GOAL>RingQuot.mul r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a * b) }
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b : R<GOAL>(match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x x_1 => x * x_1) ⋯ ⋯ a b }) = { toQuot := Quot.mk (Rel r) (a * b) }
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹² : CommSemiring R₂<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>inst✝¹⁰ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁹ : CommRing R₃<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq o<VAR>M : Matrix n n R₂<VAR>x y : n → R₂<GOAL>∑ i : n, ∑ j : n, x i • y j • M i j = ∑ i : n, ∑ j : n, x i * M i j * y j
<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✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>h : x ^ n.gcd (card G) = 1<GOAL>x ^ n = 1
<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✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>h : x ^ n.gcd (card G) = 1<VAR>m : ℕ<VAR>hm : n = n.gcd (card G) * m<GOAL>x ^ n = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q < padicValRat p r<GOAL>padicValRat p (q + r) = padicValRat p q
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>n : ℕ<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>hx : nilpotencyClass x = 1<GOAL>x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>hx : nilpotencyClass x = 1<VAR>this : IsNilpotent x<GOAL>x = 0
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F : J → C<VAR>B : Bicone F<VAR>j j' : J<VAR>h : j ≠ j'<GOAL>B.ι j ≫ B.π j' = 0
<VAR>X : RingedSpace<VAR>U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<VAR>inst✝ : IsIso i<VAR>f : ↑(X.presheaf.obj U)<GOAL>X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
<VAR>X : RingedSpace<VAR>U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<VAR>inst✝ : IsIso i<VAR>f : ↑(X.presheaf.obj U)<GOAL>X.basicOpen ((X.presheaf.map i) f) ≤ X.basicOpen f
<VAR>X : RingedSpace<VAR>U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<VAR>inst✝ : IsIso i<VAR>f : ↑(X.presheaf.obj U)<GOAL>X.basicOpen f ≤ X.basicOpen ((X.presheaf.map i) f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : SMulPosMono α β<VAR>hab : 0 < a • b<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : SMulPosMono α β<VAR>hab : 0 < a • b<VAR>ha : a < 0<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : SMulPosMono α β<VAR>hab : 0 < 0 • b<GOAL>0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : SMulPosMono α β<VAR>hab : 0 < a • b<VAR>ha : 0 < a<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<VAR>hC : 0 ≤ C<GOAL>‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<VAR>hC : 0 ≤ C<GOAL>‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ C * ‖Integrable.toL1 f hf‖
<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>i : ℕ<GOAL>sMod p i < 2 ^ p - 1
<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>i : ℕ<GOAL>sMod p i % (2 ^ p - 1) < 2 ^ p - 1
<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>i : ℕ<GOAL>|2 ^ p - 1| = 2 ^ p - 1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>f g : MonoOver X<VAR>h : f.obj.left ≅ g.obj.left<VAR>w : autoParam (h.hom ≫ g.arrow = f.arrow) _auto✝<GOAL>h.inv ≫ f.arrow = g.arrow
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : FermatLastTheoremForThreeGen.Solution.X S = 0<GOAL>λ ∣ FermatLastTheoremForThreeGen.Solution.x S
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>(∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<GOAL>Bijective ⇑(Dual.eval R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<GOAL>Bijective ⇑(↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Function.Surjective ⇑(map R S A B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Set.range ⇑(D S B) ⊆ ↑(LinearMap.range (map R S A B))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<VAR>y : A<GOAL>(D S B) ((algebraMap A B) y) ∈ ↑(LinearMap.range (map R S A B))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<VAR>y : A<GOAL>(map R S A B) ((D R A) y) ∈ ↑(LinearMap.range (map R S A B))
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<GOAL>c * a ≤ c * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>c * a ≤ c * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>S✝ : Set α<VAR>hS : IsIrreducible S✝<VAR>hS' : IsClosed S✝<GOAL>∃ x, IsGenericPoint x S✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>S✝ : Set α<VAR>hS : IsIrreducible S✝<VAR>hS' : IsClosed S✝<VAR>hS'' : IsIrreducible (f '' S✝)<GOAL>∃ x, IsGenericPoint x S✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>S✝ : Set α<VAR>hS : IsIrreducible S✝<VAR>hS' : IsClosed S✝<VAR>hS'' : IsIrreducible (f '' S✝)<VAR>x : β<VAR>hx : IsGenericPoint x (closure (f '' S✝))<GOAL>∃ x, IsGenericPoint x S✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>x : β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (f '' (f ⁻¹' T))<VAR>hx : IsGenericPoint x (closure (f '' (f ⁻¹' T)))<GOAL>∃ x, IsGenericPoint x (f ⁻¹' T)