ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>inst✝ : Nontrivial M<VAR>s t : Set α<VAR>h : Disjoint (supported M R s) (supported M R t)<VAR>x : α<VAR>hx1 : x ∈ s<VAR>hx2 : x ∈ t<VAR>y : M<VAR>hy : y ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>inst✝ : Nontrivial M<VAR>s t : Set α<VAR>h : Disjoint (supported M R s) (supported M R t)<VAR>x : α<VAR>hx1 : x ∈ s<VAR>hx2 : x ∈ t<VAR>y : M<VAR>hy : y ≠ 0<VAR>this : single x y ∈ ⊥<GOAL>False
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>inst✝ : Nontrivial M<VAR>s t : Set α<VAR>h : Disjoint (supported M R s) (supported M R t)<VAR>x : α<VAR>hx1 : x ∈ s<VAR>hx2 : x ∈ t<VAR>y : M<VAR>hy : y ≠ 0<VAR>this : y = 0<GOAL>False
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : T2Space β<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<GOAL>∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : T2Space β<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>u : Set τ<VAR>hu_mem : u ∈ f<VAR>hu : closure (image2 ϕ u s) ⊆ n<GOAL>∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : T2Space β<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>u : Set τ<VAR>hu_mem : u ∈ f<VAR>hu : closure (image2 ϕ u s) ⊆ n<VAR>t : τ<VAR>ht : t ∈ u<VAR>x : α<VAR>hx : x ∈ s<GOAL>ϕ t x ∈ n
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<GOAL>cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<VAR>h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length<GOAL>cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<VAR>h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length<VAR>h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length<GOAL>cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<VAR>h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length<VAR>h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length<VAR>h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))<GOAL>cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x✝ y✝ z : α<VAR>h : ∀ (x : α), p x ↔ p (f x)<VAR>x y : { x // p x }<VAR>n : ℤ<GOAL>(f.subtypePerm h ^ n) x = y ↔ (f ^ n) ↑x = ↑y
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>k : ℕ<VAR>h : ∀ a ∈ s, k ∣ count a s<GOAL>∃ u, s = k • u
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>k : ℕ<VAR>h : ∀ a ∈ s, k ∣ count a s<GOAL>s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>k : ℕ<VAR>h : ∀ a ∈ s, k ∣ count a s<VAR>h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}<GOAL>s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>n : ℕ∞<VAR>x : M<VAR>hf : MDifferentiableAt I I' f x<VAR>hg : MDifferentiableAt I' I'' g (f x)<GOAL>mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f✝ : M →ₗ[R] N →ₗ[R] P<VAR>f : M ⊗[R] N →ₗ[R] P<GOAL>lift ((mk R M N).compr₂ f) = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • (f • g) x + b • (f • g) y ≤ (f • g) (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x • g x + b • f y • g y ≤ f (a * x + b * y) • g (a * x + b * y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x • g x + b • f y • g y ≤ (a • f x + b • f y) • (a • g x + b • g y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x) = (a • f x + b • f y) • (a • g x + b • g y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x) = (a • f x) • a • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>∀ (x : α), x ∈ Ico a b ∩ Iio c ↔ x ∈ Ico a (min b c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c : α<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>(Ioc a b).erase b = Ioo a b
<VAR>a b m n✝ p n : ℕ<VAR>hn : n ≠ 0<GOAL>(n.factorization.prod fun x x_1 => x ^ x_1) = n
<VAR>a b m n✝ p n : ℕ<VAR>hn : n ≠ 0<GOAL>((Multiset.toFinsupp ↑n.primeFactorsList).prod fun x x_1 => x ^ x_1) = n
<VAR>a b m n✝ p n : ℕ<VAR>hn : n ≠ 0<GOAL>n.primeFactorsList.prod = n
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → LightProfinite<VAR>B : LightProfinite<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (forget LightProfinite).obj (X a)<GOAL>(ι X a ≫ desc X π) x = (π a) x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>x✝ y z : R<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>1 < v x ↔ v x⁻¹ < 1
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i : ι<VAR>hi : i < i0<GOAL>pred^[(-toZ i0 i).toNat] i0 = i
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i : ι<VAR>hi : i < i0<GOAL>pred^[Nat.find ⋯] i0 = i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>hqn : n < q<GOAL>(homotopyPToId X (q + 1)).hom n (n + 1) = (homotopyPToId X q).hom n (n + 1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeInf δ<VAR>g : γ → δ<VAR>a : δ<VAR>h : (image₂ f s t).Nonempty<GOAL>a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : Field 𝕂<VAR>inst✝³ : DivisionRing 𝔸<VAR>inst✝² : Algebra 𝕂 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>((expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n !
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>a : α<VAR>s t : Set α<GOAL>doset a s t = Set.image2 (fun x x_1 => x * a * x_1) s t
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>IsCompactlyGenerated α
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : ∀ (k : α), IsCompactElement k<GOAL>IsCompactlyGenerated α
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → β → α<GOAL>(∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β, (F y x_2.1, F y x_2.2) ∈ x) ↔ ∀ (i : ι), UniformContinuous (F i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Odd n ↔ ¬Even n
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then true else let_fun this := ⋯; { data := l ++ c :: m ++ r }.anyAux { byteIdx := utf8Len l + utf8Len (c :: m) } p ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) else false) = (c :: m).any p
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then true else let_fun this := ⋯; { data := l ++ c :: m ++ r }.anyAux { byteIdx := utf8Len l + utf8Len (c :: m) } p ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })) = (c :: m).any p
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(p c || { data := l ++ c :: (m ++ r) }.anyAux { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p { byteIdx := utf8Len l + c.utf8Size }) = (p c || m.any p)
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>{ data := l ++ c :: (m ++ r) }.anyAux { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p { byteIdx := utf8Len l + c.utf8Size } = m.any p
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>h : f.natDegree ≠ 0<GOAL>f.natSepDegree ≠ 0
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>h : f.natDegree ≠ 0<GOAL>(f.aroots f.SplittingField).toFinset.Nonempty
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>h : f.natDegree ≠ 0<GOAL>rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯ ∈ (f.aroots f.SplittingField).toFinset
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>h : f.natDegree ≠ 0<GOAL>f ≠ 0 ∧ (aeval (rootOfSplits (algebraMap F f.SplittingField) ⋯ ⋯)) f = 0
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>a s : R<VAR>h : s ∈ v.supp<GOAL>v (a + s) = v a
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>a s : R<VAR>h : s ∈ v.supp<VAR>aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a<GOAL>v (a + s) = v a
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>a s : R<VAR>h : s ∈ v.supp<VAR>aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a<GOAL>v a ≤ v (a + s)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<VAR>z : ℤ_[p]<VAR>hz : ih_gen n z<GOAL>‖↑(Polynomial.eval z F)‖ / ‖↑(Polynomial.eval z (Polynomial.derivative F))‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<VAR>z : ℤ_[p]<VAR>hz : ih_gen n z<GOAL>‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s • 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Semiring R₂<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>σ₂₁ : R₂ →+* R<VAR>inst✝ : RingHomSurjective σ₂₁<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[σ₂₁] M<VAR>h : ∀ (c : M₂), f c ∈ p<VAR>p' : Submodule R₂ M₂<VAR>x✝ : ↥p<VAR>x : M<VAR>hx : x ∈ p<GOAL>⟨x, hx⟩ ∈ map (codRestrict p f h) p' ↔ ⟨x, hx⟩ ∈ comap p.subtype (map f p')
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>A ↓∩ ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, A ↓∩ B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>A ↓∩ ⋃₀ S = ⋃ x ∈ S, A ↓∩ x
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX : Orthonormal 𝕜 Subtype.val<GOAL>∃ b, ∀ i ∈ s, b i = v i