ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card G = p<VAR>g g' : G<VAR>hg : g ≠ 1<GOAL>g' ∈ zpowers g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ∀ i ∈ s, i < a<GOAL>ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ∀ i ∈ s, i < a<GOAL>(ThreeGPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ∀ i ∈ s, i < a<GOAL>((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>h : TendstoUniformly F f p<VAR>h' : TendstoUniformly F' f' p'<GOAL>TendstoUniformly (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>h : TendstoUniformlyOn F f p univ<VAR>h' : TendstoUniformlyOn F' f' p' univ<GOAL>TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>hK : IsPGroup p ↥K<VAR>hHK : H ≤ K<VAR>a b : ↥H<VAR>h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b<GOAL>↑((Subgroup.inclusion hHK) a) = ↑((Subgroup.inclusion hHK) b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : T3Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasProd g a<VAR>hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)<VAR>hf' : Multipliable f<GOAL>HasProd f a
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ (c • s) = μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s<VAR>s : Set X<VAR>hs : T0Space ↑s<VAR>x y : { x // x ∈ s }<VAR>hxy : Inseparable ↑x ↑y<GOAL>↑x = ↑y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s<VAR>s : Set X<VAR>hs : T0Space ↑s<VAR>x y : { x // x ∈ s }<VAR>hxy : Inseparable x y<GOAL>↑x = ↑y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>c ∈ s ○ t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>s : Multiset α<VAR>x y z : α<GOAL>(fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) x y) z = (fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) x z) y
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>s : Multiset α<GOAL>foldl (fun x y => y * x) ⋯ 1 s = foldl (fun x x_1 => x * x_1) ⋯ 1 s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : ContractibleSpace X<VAR>inst✝ : ContractibleSpace Y<GOAL>Nonempty (X ≃ₕ Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : ContractibleSpace X<VAR>inst✝ : ContractibleSpace Y<VAR>h : X ≃ₕ Unit<GOAL>Nonempty (X ≃ₕ Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : ContractibleSpace X<VAR>inst✝ : ContractibleSpace Y<VAR>h : X ≃ₕ Unit<VAR>h' : Y ≃ₕ Unit<GOAL>Nonempty (X ≃ₕ Y)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p q : α → Prop<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<GOAL>Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>G : Type u_4<VAR>x : E<GOAL>⟪x, I • x⟫_ℝ = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝² : Group N<VAR>P : Type u_6<VAR>inst✝¹ : Group P<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>inst✝ : (i : η) → Group (f i)<VAR>I : Set η<VAR>x : (i : η) → f i<GOAL>(x ∈ pi I fun i => ⊤) ↔ x ∈ ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>n : M<VAR>h : ∀ x ∈ l, x ≤ n<GOAL>l.prod ≤ n ^ l.length
<VAR>X : Type u_3<VAR>Y : ?m.22013<VAR>A✝ : Type ?u.22022<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace A✝<VAR>E : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g g₁ g₂ : A → E<VAR>h₁ : ContinuousOn g₁ s<VAR>h₂ : ContinuousOn g₂ s<VAR>he : Set.EqOn (p ∘ g₁) (p ∘ g₂) s<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>Set.EqOn g₁ g₂ s
<VAR>X : Type u_3<VAR>Y : ?m.22013<VAR>A✝ : Type ?u.22022<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace A✝<VAR>E : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g g₁ g₂ : A → E<VAR>h₁ : ContinuousOn g₁ s<VAR>h₂ : ContinuousOn g₂ s<VAR>he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>s.restrict g₁ = s.restrict g₂
<VAR>X : Type u_3<VAR>Y : ?m.22013<VAR>A✝ : Type ?u.22022<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace A✝<VAR>E : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g g₁ g₂ : A → E<VAR>h₁ : Continuous (s.restrict g₁)<VAR>h₂ : Continuous (s.restrict g₂)<VAR>he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>s.restrict g₁ = s.restrict g₂
<VAR>X : Type u_3<VAR>Y : ?m.22013<VAR>A✝ : Type ?u.22022<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace A✝<VAR>E : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : PreconnectedSpace ↑s<VAR>g g₁ g₂ : A → E<VAR>h₁ : Continuous (s.restrict g₁)<VAR>h₂ : Continuous (s.restrict g₂)<VAR>he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)<VAR>a : A<VAR>has : a ∈ s<VAR>ha : g₁ a = g₂ a<GOAL>s.restrict g₁ = s.restrict g₂
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<GOAL>∀ (t : Set α), (OuterMeasure.ofFunction m h₀) (t ∩ s) + (OuterMeasure.ofFunction m h₀) (t \ s) ≤ (OuterMeasure.ofFunction m h₀) t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>f : ℕ → Set α<VAR>hf : t ⊆ ⋃ i, f i<GOAL>(OuterMeasure.ofFunction m h₀) (t ∩ s) + (OuterMeasure.ofFunction m h₀) (t \ s) ≤ ∑' (i : ℕ), m (f i)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>f : ℕ → Set α<VAR>hf : t ⊆ ⋃ i, f i<GOAL>t ∩ s ⊆ ⋃ i, (fun i => f i ∩ s) i
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>f : ℕ → Set α<VAR>hf : t ⊆ ⋃ i, f i<GOAL>t \ s ⊆ ⋃ i, (fun i => f i \ s) i
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>h₀ : m ∅ = 0<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>f : ℕ → Set α<VAR>hf : t ⊆ ⋃ i, f i<GOAL>∑' (i : ℕ), m ((fun i => f i ∩ s) i) + ∑' (i : ℕ), m ((fun i => f i \ s) i) ≤ ∑' (i : ℕ), m (f i)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf : Integrable f μ<GOAL>(ν.withDensityᵥ fun x => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ : α<VAR>f : α → β<VAR>ha : ∀ x < a, f x = f a<VAR>hb : ∀ (x : α), b < x → f x = f b<VAR>x : α<GOAL>IccExtend h (f ∘ Subtype.val) x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ : α<VAR>f : α → β<VAR>ha : ∀ x < a, f x = f a<VAR>hb : ∀ (x : α), b < x → f x = f b<VAR>x : α<VAR>hxa : x < a<GOAL>IccExtend h (f ∘ Subtype.val) x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ : α<VAR>f : α → β<VAR>ha : ∀ x < a, f x = f a<VAR>hb : ∀ (x : α), b < x → f x = f b<VAR>x : α<VAR>hax : a ≤ x<GOAL>IccExtend h (f ∘ Subtype.val) x = f x
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : K<VAR>e : α ^ n = a<GOAL>Splits (RingHom.id K) (X ^ n - C a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : LT α<VAR>s : Finset ι<VAR>f : ι → WithBot α<GOAL>∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : LinearOrder m<VAR>M : Matrix m m R<VAR>h : M.BlockTriangular ⇑toDual<GOAL>M.det = ∏ i : m, M i i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : LinearOrder m<VAR>M : Matrix m m R<VAR>h : M.BlockTriangular ⇑toDual<GOAL>Mᵀ.det = ∏ i : m, M i i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>maximalIdeal ℤ_[p] = Ideal.span {↑p}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv = (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).inv ≫ 𝟙 (𝟙_ C) ▷ 𝟙_ C = (λ_ (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ 𝟙 (𝟙_ C) = (ρ_ (𝟙_ C)).inv
<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>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p : TangentBundle I M<VAR>q : TangentBundle I H<VAR>h : q.proj ∈ (chartAt H p.proj).target<GOAL>{ proj := ↑(chartAt H p.proj).symm q.proj, snd := (mfderiv I I (↑(chartAt H p.proj).symm) q.proj) q.snd } = ↑(chartAt (ModelProd H E) p).symm ((TotalSpace.toProd H E) q)
<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>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p : TangentBundle I M<VAR>q : TangentBundle I H<VAR>h : q.proj ∈ (chartAt H p.proj).target<GOAL>{ proj := ↑(chartAt H p.proj).symm q.proj, snd := (fderivWithin 𝕜 (writtenInExtChartAt I I q.proj ↑(chartAt H p.proj).symm) (range ↑I) (↑(extChartAt I q.proj) q.proj)) q.snd } = ↑(chartAt (ModelProd H E) p).symm ((TotalSpace.toProd H E) q)
<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>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p : TangentBundle I M<VAR>q : TangentBundle I H<VAR>h : q.proj ∈ (chartAt H p.proj).target<GOAL>q.proj = ↑↑(achart H p.proj) (↑((chartAt H p.proj).prod (PartialHomeomorph.refl E)).symm (q.proj, q.snd)).1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : ¬Integrable (fun x => rexp (f x)) μ<GOAL>μ.tilted f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : ¬Integrable (fun x => rexp (f x)) μ<GOAL>(μ.withDensity fun x => ENNReal.ofReal (rexp (f x) / 0)) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h : σ ≠ 1<GOAL>(filter (fun x => σ x = x) univ).card < Fintype.card α - 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h : σ ≠ 1<GOAL>1 < (filter (fun x => ¬σ x = x) univ).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hd : d ≠ 0<VAR>hn : 2 ≤ n<GOAL>↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hd : d ≠ 0<VAR>hn : 2 ≤ n<GOAL>↑d ^ (n - 2) / ↑n = ↑(d ^ n) / ↑(n * d ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hd : d ≠ 0<VAR>hn : 2 ≤ n<GOAL>↑d ≠ 0
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.CliqueFree (r + 1) ∧ ∀ (H : SimpleGraph V) [inst : DecidableRel H.Adj], H.CliqueFree (r + 1) → H.edgeFinset.card ≤ G.edgeFinset.card<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<GOAL>G.CliqueFree (r + 1) → ∃ H inst, H.CliqueFree (r + 1) ∧ G.edgeFinset.card < H.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<GOAL>∃ H inst, H.CliqueFree (r + 1) ∧ G.edgeFinset.card < H.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<GOAL>G.edgeFinset.card < ((G.replaceVertex s t).replaceVertex s u).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<GOAL>G.edgeFinset.card < ((G.replaceVertex s t).replaceVertex s u).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<GOAL>G.edgeFinset.card < ((G.replaceVertex s t).replaceVertex s u).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<VAR>this : ¬(G.replaceVertex s t).Adj s u<GOAL>G.edgeFinset.card < ((G.replaceVertex s t).replaceVertex s u).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<VAR>this : ¬(G.replaceVertex s t).Adj s u<GOAL>G.edgeFinset.card < G.edgeFinset.card + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<VAR>this : ¬(G.replaceVertex s t).Adj s u<VAR>l1 : (G.replaceVertex s t).degree s = G.degree s<GOAL>G.edgeFinset.card < G.edgeFinset.card + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<VAR>this : ¬(G.replaceVertex s t).Adj s u<VAR>l1 : (G.replaceVertex s t).degree s = G.degree s<VAR>l2 : (G.replaceVertex s t).degree u = G.degree u - 1<GOAL>G.edgeFinset.card < G.edgeFinset.card + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<VAR>hst : ¬G.Adj s t<VAR>dst : G.degree s = G.degree t<VAR>dsu : G.degree s = G.degree u<VAR>h : G.Adj t u<VAR>cf : G.CliqueFree (r + 1)<VAR>nst : s ≠ t<VAR>ntu : t ≠ u<VAR>this : ¬(G.replaceVertex s t).Adj s u<VAR>l1 : (G.replaceVertex s t).degree s = G.degree s<VAR>l2 : (G.replaceVertex s t).degree u = G.degree u - 1<VAR>l3 : 0 < G.degree u<GOAL>G.edgeFinset.card < G.edgeFinset.card + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u