ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>z w : E<VAR>hd : DiffContOnCl ℂ f s<VAR>hz : IsMaxOn (norm ∘ f) s z<VAR>hsub : ball z (dist w z) ⊆ s<VAR>H₁ : ‖f w‖ = ‖f z‖<VAR>H₂ : ‖f w + f z‖ = ‖f z + f z‖<GOAL>‖f w + f z‖ = ‖f w‖ + ‖f z‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>v w : V<GOAL>G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>v w : V<GOAL>(v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e) → G.Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>v w : V<VAR>hne : v ≠ w<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>hv : v ∈ e ∧ w ∈ e<GOAL>G.Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>v w : V<VAR>hne : v ≠ w<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>hv : e = s(v, w)<GOAL>G.Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>v w : V<VAR>hne : v ≠ w<VAR>he : s(v, w) ∈ G.edgeSet<GOAL>G.Adj v w
<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>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H✝ K✝ : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>H K : S<VAR>h : H ≤ K<VAR>val✝ : G<VAR>property✝ : val✝ ∈ H<GOAL>↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Mono (f ≫ g)<VAR>Z : C<VAR>a b : Z ⟶ X<VAR>w : (a ≫ f) ≫ g = (b ≫ f) ≫ g<GOAL>a = b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Mono (f ≫ g)<VAR>Z : C<VAR>a b : Z ⟶ X<VAR>w : a ≫ f ≫ g = b ≫ f ≫ g<GOAL>a = b
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<GOAL>map₂ f (span R {m}) = map (f m)
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>s : Submodule R N<GOAL>map₂ f (span R {m}) s = map (f m) s
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<VAR>h : y - z ≠ 0<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<VAR>h : y + -z ≠ 0<GOAL>x ^ (y + -z) = x ^ y / x ^ z
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>edist (Memℒp.toLp f hf) (Memℒp.toLp g hg) = eLpNorm (f - g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : α → E<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<GOAL>eLpNorm (↑↑(Memℒp.toLp f hf) - ↑↑(Memℒp.toLp g hg)) p μ = eLpNorm (f - g) p μ
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b<VAR>h₂ : (e₂.oadd n₂ a₂).NF<GOAL>(e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>h' : (a₁ - a₂).NFBelow e₁.repr<GOAL>(e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>h' : (a₁.sub a₂).NFBelow e₁.repr<GOAL>(match e₁.cmp e₂ with | Ordering.lt => 0 | Ordering.gt => e₁.oadd n₁ a₁ | Ordering.eq => match (↑n₁).sub ↑n₂ with | 0 => if n₁ = n₂ then a₁.sub a₂ else 0 | k.succ => e₁.oadd k.succPNat a₁).NFBelow b
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>h' : (a₁.sub a₂).NFBelow e₁.repr<VAR>this : (e₁.cmp e₂).Compares e₁ e₂<GOAL>(match e₁.cmp e₂ with | Ordering.lt => 0 | Ordering.gt => e₁.oadd n₁ a₁ | Ordering.eq => match (↑n₁).sub ↑n₂ with | 0 => if n₁ = n₂ then a₁.sub a₂ else 0 | k.succ => e₁.oadd k.succPNat a₁).NFBelow b
<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>inst✝³¹ : SmoothManifoldWithCorners I 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>inst✝²⁵ : SmoothManifoldWithCorners I' 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 : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>hf : ContMDiff I I' n f<VAR>hg : ContMDiff J J' n g<VAR>p : M × N<GOAL>ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>m n : ℕ<GOAL>take m (iterate f a n) = iterate f a (min m n)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>r : R<GOAL>(expand R p) f = C r ↔ f = C r
<VAR>P : Type u_1<VAR>inst✝¹ : LE P<VAR>I✝ J✝ s t : Ideal P<VAR>x y : P<VAR>inst✝ : IsDirected P fun x x_1 => x ≥ x_1<VAR>I J : Ideal P<GOAL>(↑I ∩ ↑J).Nonempty
<VAR>P : Type u_1<VAR>inst✝¹ : LE P<VAR>I✝ J✝ s t : Ideal P<VAR>x y : P<VAR>inst✝ : IsDirected P fun x x_1 => x ≥ x_1<VAR>I J : Ideal P<VAR>a : P<VAR>ha : a ∈ ↑I<GOAL>(↑I ∩ ↑J).Nonempty
<VAR>P : Type u_1<VAR>inst✝¹ : LE P<VAR>I✝ J✝ s t : Ideal P<VAR>x y : P<VAR>inst✝ : IsDirected P fun x x_1 => x ≥ x_1<VAR>I J : Ideal P<VAR>a : P<VAR>ha : a ∈ ↑I<VAR>b : P<VAR>hb : b ∈ ↑J<GOAL>(↑I ∩ ↑J).Nonempty
<VAR>P : Type u_1<VAR>inst✝¹ : LE P<VAR>I✝ J✝ s t : Ideal P<VAR>x y : P<VAR>inst✝ : IsDirected P fun x x_1 => x ≥ x_1<VAR>I J : Ideal P<VAR>a : P<VAR>ha : a ∈ ↑I<VAR>b : P<VAR>hb : b ∈ ↑J<VAR>c : P<VAR>hac : c ≤ a<VAR>hbc : c ≤ b<GOAL>(↑I ∩ ↑J).Nonempty
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>k : ℤ<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hc₁ : ChainClosure r c₁<VAR>hc₂ : ChainClosure r c₂<VAR>hc : SuccChain r c₂ = c₂<GOAL>c₁ ⊆ c₂
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>q : Stmt₂<VAR>v : σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<VAR>IH : Reaches₀ (TM1.step (tr M)) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }<GOAL>Reaches₀ (TM1.step (tr M)) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) } { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>q : Stmt₂<VAR>v : σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<VAR>IH : Reaches₀ (TM1.step (tr M)) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }<GOAL>{ l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } ∈ TM1.step (tr M) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>q : Stmt₂<VAR>v : σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<VAR>IH : Reaches₀ (TM1.step (tr M)) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }<GOAL>some (TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) = some { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>q : Stmt₂<VAR>v : σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<VAR>IH : Reaches₀ (TM1.step (tr M)) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }<GOAL>(bif false then TM1.stepAux (trNormal q) v (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))) else TM1.stepAux (goto fun x x => ret q) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))) = { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a✝ b a : α<VAR>l : List α<GOAL>(a :: l).Nodup ↔ a ∉ l ∧ l.Nodup
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j : Fin m<GOAL>↑j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j : Fin m<GOAL>∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ↑k✝ < Fintype.card { i // f i ≤ a }<GOAL>f k✝ ≤ a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ¬f k✝ ≤ a<GOAL>Fintype.card { i // f i ≤ a } ≤ ↑k✝
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ¬f k✝ ≤ a<GOAL>(Finset.filter (fun i => f i ≤ a) Finset.univ).card ≤ (Finset.Iio k✝).card
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ¬f k✝ ≤ a<VAR>i : Fin m<GOAL>i ∉ Finset.Iio k✝ → i ∉ Finset.filter (fun i => f i ≤ a) Finset.univ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ¬f k✝ ≤ a<VAR>i : Fin m<GOAL>¬i < k✝ → ¬f i ≤ a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : DecidableRel LE.le<VAR>m : ℕ<VAR>f : Fin m → α<VAR>a : α<VAR>h_sorted : Monotone f<VAR>j k✝ : Fin m<VAR>h : ¬f k✝ ≤ a<VAR>i : Fin m<VAR>hij : ¬i < k✝<VAR>hia : f i ≤ a<GOAL>f k✝ ≤ a
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l : List α✝<VAR>h : l₁ ++ l <+ l₂ ++ l<GOAL>l₁ <+ l₂
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l : List α✝<VAR>h : l₁ ++ l <+ l₂ ++ l<VAR>this : (l₁ ++ l).reverse <+ (l₂ ++ l).reverse<GOAL>l₁ <+ l₂
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l : List α✝<VAR>h : l₁ ++ l <+ l₂ ++ l<VAR>this : l₁ <+ l₂<GOAL>l₁ <+ l₂
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>h_nhd : ↑H ∈ 𝓝 1<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>h_nhd : ∃ t ⊆ ↑H, IsOpen t ∧ 1 ∈ t<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<GOAL>Disjoint (f • W) (g • W)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<GOAL>∀ ⦃a : L ≃ₐ[K] L⦄, a ∈ f • W → a ∉ g • W
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : f * w1 = g * w2<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<VAR>h_in_H : w1 * w2⁻¹ ∈ H<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<VAR>h_in_H : φ ∈ E.fixingSubgroup<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<VAR>h_in_H : ∀ x ∈ E, φ x = x<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : f ≠ g<VAR>φ : L ≃ₐ[K] L := f⁻¹ * g<VAR>x : L<VAR>hx : f x ≠ g x<VAR>hφx : φ x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)<VAR>H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup<VAR>h_basis : ↑H ∈ galGroupBasis K L<VAR>W : Set (L ≃ₐ[K] L)<VAR>hWH : W ⊆ ↑H<VAR>hW_open : IsOpen W<VAR>hW_1 : 1 ∈ W<VAR>w1 : L ≃ₐ[K] L<VAR>hw1 : w1 ∈ W<VAR>w2 : L ≃ₐ[K] L<VAR>hw2 : w2 ∈ W<VAR>h : w1 * w2⁻¹ = f⁻¹ * g<VAR>h_in_H : x ∈ E → φ x = x<GOAL>False