ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : gcd x y = 0<GOAL>x ∣ 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : ¬gcd x y = 0<VAR>z : R<VAR>hz : y = gcd x y * z<GOAL>x * z * gcd x y = x * y
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasCokernel f<VAR>inst✝² : HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasCokernel g<VAR>inst✝ : HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map f ≫ G.map q = G.map p ≫ G.map g
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasCokernel f<VAR>inst✝² : HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasCokernel g<VAR>inst✝ : HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map f ≫ G.map (coequalizer.π f 0) = 0
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasCokernel f<VAR>inst✝² : HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasCokernel g<VAR>inst✝ : HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map g ≫ G.map (coequalizer.π g 0) = 0
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasCokernel f<VAR>inst✝² : HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasCokernel g<VAR>inst✝ : HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (coequalizer.π f 0) ≫ G.map (cokernel.map f g p q hpq) = G.map q ≫ G.map (coequalizer.π g 0)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasCokernel f<VAR>inst✝² : HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasCokernel g<VAR>inst✝ : HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (coequalizer.π f 0 ≫ cokernel.map f g p q hpq) = G.map (q ≫ coequalizer.π g 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ : α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm x = x ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>hl : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.get ⟨k, hk⟩ ∈ l<GOAL>l.formPerm (l.get ⟨k, hk⟩) = l.get ⟨k, hk⟩ ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>hl : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.get ⟨k, hk⟩ ∈ l<GOAL>(↑⟨k, hk⟩ + 1) % l.length = k ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>hl : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.get ⟨k, hk⟩ ∈ l<GOAL>(k + 1) % l.length = k ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : Mul α<VAR>inst✝² : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : Preorder α<GOAL>PosMulStrictMono α ↔ MulPosStrictMono α
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<GOAL>index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<GOAL>index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<GOAL>index K₁.carrier V + index K₂.carrier V ≤ index (K₁.carrier ∪ K₂.carrier) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<GOAL>index K₁.carrier V + index K₂.carrier V ≤ s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<GOAL>(Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K₁.carrier).Nonempty) s).card + (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K₂.carrier).Nonempty) s).card ≤ s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<GOAL>(Finset.filter (fun x => ((fun h => x * h) ⁻¹' V ∩ K₁.carrier).Nonempty ∨ ((fun h => x * h) ⁻¹' V ∩ K₂.carrier).Nonempty) s).card ≤ s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<GOAL>Disjoint (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K₁.carrier).Nonempty) s) (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K₂.carrier).Nonempty) s)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<GOAL>∀ x ∈ s, ((fun h => x * h) ⁻¹' V ∩ K₁.carrier).Nonempty → ¬((fun h => x * h) ⁻¹' V ∩ K₂.carrier).Nonempty
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<VAR>g₁ : G<VAR>a✝ : g₁ ∈ s<VAR>g₂ : G<VAR>h1g₂ : g₂ ∈ (fun h => g₁ * h) ⁻¹' V<VAR>h2g₂ : g₂ ∈ K₁.carrier<VAR>g₃ : G<VAR>h1g₃ : g₃ ∈ (fun h => g₁ * h) ⁻¹' V<VAR>h2g₃ : g₃ ∈ K₂.carrier<GOAL>False
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<VAR>g₁ : G<VAR>a✝ : g₁ ∈ s<VAR>g₂ : G<VAR>h2g₂ : g₂ ∈ K₁.carrier<VAR>g₃ : G<VAR>h2g₃ : g₃ ∈ K₂.carrier<VAR>h1g₃ : g₁ * g₃ ∈ V<VAR>h1g₂ : g₁ * g₂ ∈ V<GOAL>False
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<VAR>g₁ : G<VAR>a✝ : g₁ ∈ s<VAR>g₂ : G<VAR>h2g₂ : g₂ ∈ K₁.carrier<VAR>g₃ : G<VAR>h2g₃ : g₃ ∈ K₂.carrier<VAR>h1g₃ : g₁ * g₃ ∈ V<VAR>h1g₂ : g₁ * g₂ ∈ V<GOAL>g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<VAR>g₁ : G<VAR>a✝ : g₁ ∈ s<VAR>g₂ : G<VAR>h2g₂ : g₂ ∈ K₁.carrier<VAR>g₃ : G<VAR>h2g₃ : g₃ ∈ K₂.carrier<VAR>h1g₃ : g₁ * g₃ ∈ V<VAR>h1g₂ : g₁ * g₂ ∈ V<GOAL>∃ x ∈ K₁.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)<VAR>s : Finset G<VAR>h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V<VAR>this : ∀ K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V, index K V ≤ (Finset.filter (fun g => ((fun h => g * h) ⁻¹' V ∩ K).Nonempty) s).card<VAR>g₁ : G<VAR>a✝ : g₁ ∈ s<VAR>g₂ : G<VAR>h2g₂ : g₂ ∈ K₁.carrier<VAR>g₃ : G<VAR>h2g₃ : g₃ ∈ K₂.carrier<VAR>h1g₃ : g₁ * g₃ ∈ V<VAR>h1g₂ : g₁ * g₂ ∈ V<GOAL>∃ x ∈ K₂.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>_h : v ≠ w<GOAL>(fun v w => ¬⊥.Adj v w → Fintype.card ↑(⊥.commonNeighbors v w) = 0) v w
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>_h : v ≠ w<GOAL>filter (fun x => x ∈ ⊥.commonNeighbors v w) univ = ∅
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>_h : v ≠ w<VAR>a✝ : V<GOAL>a✝ ∈ filter (fun x => x ∈ ⊥.commonNeighbors v w) univ ↔ a✝ ∈ ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : a = b + c<GOAL>a = c + b
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>(∫ (x : ℝ), cexp (-b * ↑x ^ 2)) ^ 2 = ↑π / b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>cthickening δ E = ⋂ ε ∈ s, thickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<VAR>ε : ℝ<VAR>hε : ε ∈ s<GOAL>cthickening δ E ⊆ thickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>⋂ i ∈ s, thickening i E ⊆ cthickening δ E
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : A.primeSpectrumEquiv a✝ ≤ A.primeSpectrumEquiv b✝<GOAL>a✝ ≤ b✝
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : A.primeSpectrumEquiv a✝ ≤ A.primeSpectrumEquiv b✝<VAR>this : A.idealOfLE ↑(A.primeSpectrumEquiv b✝) ?refine_2 ≤ A.idealOfLE ↑(A.primeSpectrumEquiv a✝) ?refine_1<GOAL>a✝ ≤ b✝
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : A.primeSpectrumEquiv a✝ ≤ A.primeSpectrumEquiv b✝<GOAL>A ≤ ↑(A.primeSpectrumEquiv a✝)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : A.primeSpectrumEquiv a✝ ≤ A.primeSpectrumEquiv b✝<GOAL>A ≤ ↑(A.primeSpectrumEquiv b✝)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : A.primeSpectrumEquiv a✝ ≤ A.primeSpectrumEquiv b✝<VAR>this : b✝.asIdeal ≤ a✝.asIdeal<GOAL>a✝ ≤ b✝
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : a✝ ≤ b✝<GOAL>__src✝ a✝ ≤ __src✝ b✝
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ<VAR>h : a✝ ≤ b✝<GOAL>b✝.asIdeal ≤ a✝.asIdeal
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F L ↥(adjoin L S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>this : ∃ φ, φ.comp (IsScalarTower.toAlgHom F ↥L' ↥(adjoin (↥L') S)) = f'<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F L ↥(adjoin L S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<GOAL>IsIntegral (↥L') s ∧ Splits f'.toRingHom (minpoly (↥L') s)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<VAR>this : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra<GOAL>IsIntegral (↥L') s ∧ Splits f'.toRingHom (minpoly (↥L') s)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<VAR>this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra<VAR>this : IsScalarTower L (↥L') E<GOAL>IsIntegral (↥L') s ∧ Splits f'.toRingHom (minpoly (↥L') s)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<VAR>this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra<VAR>this : IsScalarTower L (↥L') E<GOAL>Splits (f'.comp (algebraMap L ↥L')) (minpoly L s)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<VAR>this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra<VAR>this : IsScalarTower L (↥L') E<GOAL>f'.comp (algebraMap L ↥L') = f.toRingHom
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra L E<VAR>inst✝ : IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)<VAR>L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange<VAR>f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm<VAR>s : E<VAR>hs : s ∈ S<VAR>this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra<VAR>this : IsScalarTower L (↥L') E<VAR>x✝ : L<GOAL>(f'.comp (algebraMap L ↥L')) x✝ = f.toRingHom x✝
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i.succ.succAbove j.succ = (i.succAbove j).succ
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : i < j.succ<GOAL>i.succ.succAbove j.succ = (i.succAbove j).succ
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : j.succ ≤ i<GOAL>i.succ.succAbove j.succ = (i.succAbove j).succ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<GOAL>‖gramSchmidtNormed 𝕜 f n‖ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<GOAL>sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) = (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) + ((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) = (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>hm : MeasurableSet (κ.mutuallySingularSetSlice η a)<GOAL>((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) + ((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) = (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)