ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>g : ↥A<VAR>w : NormalWord d<GOAL>(if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h else let g' := unitsSMulGroup φ d 1 (↑g • w).head; cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) = ↑(φ g) • if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h else let g' := unitsSMulGroup φ d 1 w.head; cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>g : ↥A<VAR>w : NormalWord d<VAR>this : Cancels 1 (↑g • w) ↔ Cancels 1 w<GOAL>(if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h else let g' := unitsSMulGroup φ d 1 (↑g • w).head; cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) = ↑(φ g) • if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h else let g' := unitsSMulGroup φ d 1 w.head; cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>f : Fin n → G<VAR>i : ℕ<VAR>hn : i < n<GOAL>(partialProd f ⟨i, hn⟩.castSucc)⁻¹ * partialProd f ⟨i, hn⟩.succ = f ⟨i, hn⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : SubNegZeroMonoid G<VAR>inst✝ : SubNegZeroMonoid H<VAR>f : G → H<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x y : G), f (x - y) = f x - f y<VAR>v₁ v₂ : α →₀ G<VAR>x✝ : α<GOAL>(mapRange f hf (v₁ - v₂)) x✝ = (mapRange f hf v₁ - mapRange f hf v₂) x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompletelyNormalSpace Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<VAR>s t : Set X<VAR>hd₁ : Disjoint (closure s) t<VAR>hd₂ : Disjoint s (closure t)<GOAL>Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompletelyNormalSpace Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<VAR>s t : Set X<VAR>hd₁ : Disjoint (closure s) t<VAR>hd₂ : Disjoint s (closure t)<GOAL>Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompletelyNormalSpace Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<VAR>s t : Set X<VAR>hd₁ : Disjoint (closure s) t<VAR>hd₂ : Disjoint s (closure t)<GOAL>Disjoint (closure (e '' s)) (e '' t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : CompletelyNormalSpace Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<VAR>s t : Set X<VAR>hd₁ : Disjoint (closure s) t<VAR>hd₂ : Disjoint s (closure t)<GOAL>Disjoint (e '' s) (closure (e '' t))
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.30188<VAR>s✝ t s : Finset α<GOAL>s.powerset = (range (s.card + 1)).disjiUnion (fun i => powersetCard i s) ⋯
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.30188<VAR>s✝ t s a : Finset α<VAR>ha : a ∈ s.powerset<GOAL>a ∈ (range (s.card + 1)).disjiUnion (fun i => powersetCard i s) ⋯
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.30188<VAR>s✝ t s a : Finset α<VAR>ha : a ∈ (range (s.card + 1)).disjiUnion (fun i => powersetCard i s) ⋯<GOAL>a ∈ s.powerset
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(ψ ⇔ φ).Realize v xs
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⇔ ψ).Realize v xs
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁸ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>G : Type u_9<VAR>inst✝³ : Group G<VAR>inst✝² : SMul G R<VAR>inst✝¹ : MulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>g : G<VAR>x : M<GOAL>span R {g • x} = span R {x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁸ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>G : Type u_9<VAR>inst✝³ : Group G<VAR>inst✝² : SMul G R<VAR>inst✝¹ : MulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>g : G<VAR>x : M<GOAL>span R {x} ≤ span R {g • x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁸ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>G : Type u_9<VAR>inst✝³ : Group G<VAR>inst✝² : SMul G R<VAR>inst✝¹ : MulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>g : G<VAR>x : M<GOAL>x = g⁻¹ • g • x
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>x : α<VAR>y : β<VAR>hd : α<VAR>tl : List α<VAR>ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (indexOf x tl) y else map f tl<VAR>hl : (hd :: tl).Nodup<GOAL>map (update f x y) (hd :: tl) = if x ∈ hd :: tl then (map f (hd :: tl)).set (indexOf x (hd :: tl)) y else map f (hd :: tl)
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>x : α<VAR>y : β<VAR>hd : α<VAR>tl : List α<VAR>ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (indexOf x tl) y else map f tl<VAR>hl : hd ∉ tl ∧ tl.Nodup<GOAL>map (update f x y) (hd :: tl) = if x ∈ hd :: tl then (map f (hd :: tl)).set (indexOf x (hd :: tl)) y else map f (hd :: tl)
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>x : α<VAR>y : β<VAR>hd : α<VAR>tl : List α<VAR>ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (indexOf x tl) y else map f tl<VAR>hl : hd ∉ tl ∧ tl.Nodup<GOAL>(update f x y hd :: if x ∈ tl then (map f tl).set (indexOf x tl) y else map f tl) = if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (indexOf x (hd :: tl)) y else f hd :: map f tl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a✝ a : α<VAR>hs : MeasurableSet s<GOAL>s ∈ ae (dirac a) ↔ a ∈ s
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this : ExpChar E q<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<VAR>h : (minpoly F x).natSepDegree = 1<GOAL>∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<VAR>x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n<VAR>n : ℕ<VAR>h : Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<VAR>x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n<VAR>n : ℕ<VAR>h : constantCoeff (Polynomial.map (algebraMap F E) (minpoly F x)) = constantCoeff ((X - C x) ^ q ^ n)<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<VAR>x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n<VAR>n : ℕ<VAR>h : (algebraMap F E) ((minpoly F x).coeff 0) = (0 - x) ^ q ^ n<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>this✝ : ExpChar E q<VAR>this : ExpChar E[X] q<VAR>x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n<VAR>n : ℕ<VAR>h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Add α<VAR>inst✝⁵ : Sub α<VAR>inst✝⁴ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Add β<VAR>inst✝¹ : Sub β<VAR>inst✝ : OrderedSub β<VAR>f : AddHom α β<VAR>hf : Monotone ⇑f<VAR>a b : α<GOAL>f a - f b ≤ f (a - b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Add α<VAR>inst✝⁵ : Sub α<VAR>inst✝⁴ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Add β<VAR>inst✝¹ : Sub β<VAR>inst✝ : OrderedSub β<VAR>f : AddHom α β<VAR>hf : Monotone ⇑f<VAR>a b : α<GOAL>f a ≤ f (a - b + b)
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<GOAL>χ ^ 2 = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>i : ℕ<GOAL>(truncateFun n x).out.coeff i = (init n x).coeff i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>i : ℕ<GOAL>(if h : i < n then TruncatedWittVector.coeff ⟨i, h⟩ (truncateFun n x) else 0) = if i < n then x.coeff i else 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>i : ℕ<VAR>hi : i < n<GOAL>TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b✝ c : β<VAR>a b : ℕ<GOAL>range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b✝ c : β<VAR>a b : ℕ<GOAL>(range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a b : α<GOAL>sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s s' t : Set α<VAR>hs : IsOpen s<VAR>hs' : IsOpen s'<VAR>ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'<GOAL>IsOpen (t.ite s s')
<VAR>c : ℝ<VAR>f✝ g✝ : ℕ → Bool<VAR>n✝ : ℕ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>h3 : c < 1<VAR>n : ℕ<VAR>ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n + 1, f k = g k<VAR>fn : f (n + 1) = false<VAR>gn : g (n + 1) = true<GOAL>cantorFunction c f < cantorFunction c g
<VAR>c : ℝ<VAR>f✝ g✝ : ℕ → Bool<VAR>n✝ : ℕ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>h3 : c < 1<VAR>n : ℕ<VAR>ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n + 1, f k = g k<VAR>fn : f (n + 1) = false<VAR>gn : g (n + 1) = true<GOAL>((bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) < (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
<VAR>c : ℝ<VAR>f✝ g✝ : ℕ → Bool<VAR>n✝ : ℕ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>h3 : c < 1<VAR>n : ℕ<VAR>ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n + 1, f k = g k<VAR>fn : f (n + 1) = false<VAR>gn : g (n + 1) = true<GOAL>((bif g 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) < (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
<VAR>c : ℝ<VAR>f✝ g✝ : ℕ → Bool<VAR>n✝ : ℕ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>h3 : c < 1<VAR>n : ℕ<VAR>ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n + 1, f k = g k<VAR>fn : f (n + 1) = false<VAR>gn : g (n + 1) = true<GOAL>(c * cantorFunction c fun n => f (n + 1)) < c * cantorFunction c fun n => g (n + 1)
<VAR>c : ℝ<VAR>f✝ g✝ : ℕ → Bool<VAR>n✝ : ℕ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>h3 : c < 1<VAR>n : ℕ<VAR>ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n + 1, f k = g k<VAR>fn : f (n + 1) = false<VAR>gn : g (n + 1) = true<GOAL>(cantorFunction c fun n => f (n + 1)) < cantorFunction c fun n => g (n + 1)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hs : Convex R s<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hz : ∀ i ∈ t, z i ∈ s<GOAL>∑ i ∈ t, w i • z i ∈ s
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>J(a ^ 2 | b) = 1
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasStrictDerivAt h₂ h₂' (h x)<VAR>hh : HasStrictDerivAt h h' x<GOAL>HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasStrictDerivAt h₂ h₂' (h x)<VAR>hh : HasStrictDerivAt h h' x<GOAL>HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
<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 : γ<GOAL>(image₂ f s t).card = s.card * t.card ↔ InjOn (fun x => f x.1 x.2) (↑s ×ˢ ↑t)
<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 : γ<GOAL>(image₂ f s t).card = (s ×ˢ t).card ↔ InjOn (fun x => f x.1 x.2) ↑(s ×ˢ t)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<GOAL>∀ (x : Ideal R), x ∉ nonPrincipals R
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<GOAL>x ∈ I
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<GOAL>x ∈ I
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<GOAL>¬IsPrincipal (colon I (Ideal.span {y}))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<VAR>b : R<VAR>hb : colon I (Ideal.span {y}) = Submodule.span R {b}<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<VAR>b : R<VAR>hb : colon I (Ideal.span {y}) = Submodule.span R {b}<GOAL>I = Submodule.span R {a * b}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<VAR>b : R<VAR>hb : colon I (Ideal.span {y}) = Submodule.span R {b}<VAR>i : R<VAR>hi : i ∈ I<GOAL>i ∈ Submodule.span R {a * b}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → IsPrincipal P<VAR>J : Ideal R<VAR>hJ : J ∈ nonPrincipals R<VAR>I : Ideal R<VAR>Ibad : I ∈ nonPrincipals R<VAR>Imax : ∀ z ∈ nonPrincipals R, I ≤ z → z = I<VAR>Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J<VAR>hI1 : ¬I = ⊤<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>hy : y ∉ I<VAR>a : R<VAR>ha : I ⊔ Ideal.span {y} = Submodule.span R {a}<VAR>b : R<VAR>hb : colon I (Ideal.span {y}) = Submodule.span R {b}<GOAL>Ideal.span {a} * Ideal.span {b} ≤ I
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ico (-(π / 2)) (π / 2)<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ico (-(π / 2)) (π / 2)<VAR>hx₁ : x ≤ -1<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ico (-(π / 2)) (π / 2)<VAR>hx₁ : -1 ≤ x<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ico (-(π / 2)) (π / 2)<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : 1 < x<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>x✝ y✝ x y : ℝ<VAR>hy : y ∈ Ico (-(π / 2)) (π / 2)<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1.direction ⊔ s2.direction ≤ (s1 ⊔ s2).direction