ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>x = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f g : α → ℝ<GOAL>∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ
<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>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<GOAL>Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun a => ¬P a) g.support)
<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>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<GOAL>∀ ⦃a : α⦄ (a_1 : α) (b : P a_1), ⟨a_1, b⟩ ∈ f.support ∧ a_1 = a → ¬∃ a_2, ∃ (h : ¬P a_2), ⟨a_2, ⋯⟩ ∈ g.support ∧ a_2 = a
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cone (Discrete.functor f)<VAR>j : Discrete β<GOAL>(fun s => s.π.app default) s ≫ { pt := f default, π := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.π.app j = s.π.app j
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cone (Discrete.functor f)<VAR>j : Discrete β<VAR>h : j = default<GOAL>(fun s => s.π.app default) s ≫ { pt := f default, π := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.π.app j = s.π.app j
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>x ^ y ≤ x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>rexp (log x * y) ≤ rexp (log x * z)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>log x * y ≤ log x * z
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable fun x => rexp (f x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable fun x => rexp (f x)<VAR>this : f = fun x => log (rexp (f x))<GOAL>Measurable f
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable fun x => rexp (f x)<VAR>this : f = fun x => log (rexp (f x))<GOAL>Measurable fun x => log (rexp (f x))
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<GOAL>(fun a => ↑a) '' (closure (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) = intrinsicInterior 𝕜 s
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : Fintype V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<GOAL>p.length < Fintype.card V
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : Fintype V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<GOAL>p.support.length ≤ Fintype.card V
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<GOAL>(X ^ n).leadingCoeff = 1
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>hc : c.IsTrail<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>hc : c.IsTrail<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<VAR>hv : v ∈ c.support<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>hc : c.IsTrail<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<VAR>hv : v ∈ c.support<VAR>puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw<VAR>pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw<VAR>pvu : G.Walk v u := c.dropUntil v hv<VAR>this : c = (puw.append pwv).append pvu<VAR>hbq : s(v, w) ∈ (pvu.append puw).edges<VAR>hpq' : s(v, w) ∈ pwv.reverse.edges<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>hc : c.IsTrail<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<VAR>hv : v ∈ c.support<VAR>puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw<VAR>pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw<VAR>pvu : G.Walk v u := c.dropUntil v hv<VAR>this : c = (puw.append pwv).append pvu<VAR>hbq : s(v, w) ∈ (pvu.append puw).edges<VAR>hpq' : s(v, w) ∈ pwv.edges<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<VAR>hv : v ∈ c.support<VAR>puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw<VAR>pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw<VAR>pvu : G.Walk v u := c.dropUntil v hv<VAR>hc : ((pvu.append puw).edges ++ pwv.edges).Nodup<VAR>this : c = (puw.append pwv).append pvu<VAR>hbq : s(v, w) ∈ (pvu.append puw).edges<VAR>hpq' : s(v, w) ∈ pwv.edges<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → 𝕜<VAR>g₁ g₂ : α → 𝕜'<VAR>h₁ : f₁ =Θ[l] g₁<VAR>h₂ : f₂ =Θ[l] g₂<GOAL>(fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : UniformSpace α<VAR>u₂ : Set (UniformSpace β)<GOAL>Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ u ∈ u₂, Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)
<VAR>c : Char<VAR>cs : List Char<VAR>b e : Pos<GOAL>{ data := c :: cs }.extract (b + c) (e + c) = { data := cs }.extract b e
<VAR>c : Char<VAR>cs : List Char<VAR>b e : Pos<GOAL>(if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ (c :: cs) 0 (b + c) (e + c) }) = if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ cs 0 b e }
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>x : M<GOAL>x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>x : M<GOAL>(∃ y ∈ ↑N, ∃ z ∈ ↑N', y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<VAR>ω : Ω<VAR>hω : Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<GOAL>(fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<VAR>ω : Ω<VAR>hω : Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<GOAL>(fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) = fun n => ∑ i ∈ range n, (truncation (X i) (↑i) ω - X i ω)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<VAR>ω : Ω<VAR>hω : Tendsto (fun n => truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)<VAR>n : ℕ<GOAL>∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω = ∑ i ∈ range n, (truncation (X i) (↑i) ω - X i ω)
<VAR>R✝ : Type u<VAR>inst✝²⁷ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝²⁶ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝²⁵ : CommRing S<VAR>inst✝²⁴ : Algebra R S<VAR>A : Type u<VAR>inst✝²³ : CommRing A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Algebra S A<VAR>inst✝²⁰ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝¹⁹ : CommRing B<VAR>inst✝¹⁸ : Algebra R B<VAR>inst✝¹⁷ : Algebra S B<VAR>inst✝¹⁶ : IsScalarTower R S B<VAR>f✝¹ : A →ₐ[S] B<VAR>F : Type u<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Algebra R F<VAR>inst✝¹³ : Algebra S F<VAR>inst✝¹² : IsScalarTower R S F<VAR>K : Type v<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : Algebra S K<VAR>inst✝⁸ : IsScalarTower R S K<VAR>f✝ : F →ₐ[S] K<VAR>L : Type w<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : IsScalarTower R S L<VAR>g : K →ₐ[S] L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsScalarTower R F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : IsScalarTower R F L<VAR>f : K →ₐ[F] L<VAR>P : W⟮F⟯<VAR>this : Subsingleton (F →ₐ[F] L)<GOAL>(map W f) ((baseChange W F K) P) = (baseChange W F L) P
<VAR>m n : ℕ∞<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>E' : Type u_5<VAR>H' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>e : PartialHomeomorph H H<VAR>e' : PartialHomeomorph H' H'<VAR>he : (contDiffPregroupoid ⊤ I).property (↑e) e.source<VAR>he_symm : (contDiffPregroupoid ⊤ I).property (↑e.symm) e.target<VAR>he' : (contDiffPregroupoid ⊤ I').property (↑e') e'.source<VAR>he'_symm : (contDiffPregroupoid ⊤ I').property (↑e'.symm) e'.target<GOAL>e.prod e' ∈ contDiffGroupoid ⊤ (I.prod I')
<VAR>m n : ℕ∞<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>E' : Type u_5<VAR>H' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>e : PartialHomeomorph H H<VAR>e' : PartialHomeomorph H' H'<VAR>he : (contDiffPregroupoid ⊤ I).property (↑e) e.source<VAR>he_symm : (contDiffPregroupoid ⊤ I).property (↑e.symm) e.target<VAR>he' : (contDiffPregroupoid ⊤ I').property (↑e') e'.source<VAR>he'_symm : (contDiffPregroupoid ⊤ I').property (↑e'.symm) e'.target<GOAL>ContDiffOn 𝕜 ⊤ (↑(I.prod I') ∘ ↑(e.prod e') ∘ ↑(I.prod I').symm) (↑(I.prod I').symm ⁻¹' e.source ×ˢ e'.source ∩ range ↑(I.prod I'))
<VAR>m n : ℕ∞<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>E' : Type u_5<VAR>H' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>e : PartialHomeomorph H H<VAR>e' : PartialHomeomorph H' H'<VAR>he : (contDiffPregroupoid ⊤ I).property (↑e) e.source<VAR>he_symm : (contDiffPregroupoid ⊤ I).property (↑e.symm) e.target<VAR>he' : (contDiffPregroupoid ⊤ I').property (↑e') e'.source<VAR>he'_symm : (contDiffPregroupoid ⊤ I').property (↑e'.symm) e'.target<GOAL>ContDiffOn 𝕜 ⊤ (↑(I.prod I') ∘ ↑(e.prod e').symm ∘ ↑(I.prod I').symm) (↑(I.prod I').symm ⁻¹' (e.prod e'.toPartialEquiv).target ∩ range ↑(I.prod I'))
<VAR>z : ℂ<VAR>hz : z ≠ 0<GOAL>Complex.abs ((starRingEnd ℂ) z / z) = 1
<VAR>z : ℂ<VAR>hz : z ≠ 0<GOAL>Complex.abs z ≠ 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(lineMap a b) r < (lineMap a b) r' ↔ a < b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<GOAL>↑I * (↑I)⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<GOAL>(↑I * (↑I)⁻¹)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<GOAL>x ∈ (fun a => ↑a) 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<GOAL>x ∈ integralClosure A K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<GOAL>∃ M, (Subalgebra.toSubmodule M).FG ∧ x ∈ M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<VAR>x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹<GOAL>∃ M, (Subalgebra.toSubmodule M).FG ∧ x ∈ M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<VAR>x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹<VAR>y : K<VAR>hy : y ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range<GOAL>y ∈ ↑(↑I)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<VAR>x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹<VAR>p : A[X]<VAR>hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range<GOAL>(Polynomial.aeval x) p ∈ ↑(↑I)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<VAR>x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹<VAR>p : A[X]<VAR>hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range<GOAL>∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i ∈ ↑(↑I)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hJ0 : ¬↑I * (↑I)⁻¹ = 0<VAR>x : K<VAR>hx : x ∈ (fun a => ↑a) (↑I * (↑I)⁻¹)⁻¹<VAR>x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹<VAR>p : A[X]<VAR>hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range<VAR>i : ℕ<VAR>hi : i ∈ Finset.range (p.natDegree + 1)<GOAL>x ^ i ∈ ↑(↑I)⁻¹
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<VAR>this : (1 ⍟ fun x => ↑(μ x)) = δ<GOAL>(fun n_1 => χ ↑n_1) ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(μ n)) = δ
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<VAR>this : (1 ⍟ fun x => ↑(μ x)) = δ<GOAL>(fun n_1 => χ ↑n_1) * 1 ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(μ n)) = δ
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁴ : Semifield K<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V₂<VAR>a : K<VAR>h : a ≠ 0<VAR>b : V<GOAL>b ∈ comap (a • f) p ↔ b ∈ comap f p
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : T2Space G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : H →* G<VAR>hf' : DiscreteTopology ↥f.range<VAR>hf : Function.Injective ⇑f.rangeRestrict<GOAL>Tendsto (⇑f) cofinite (cocompact G)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>f i hi (o.derivBFamily f a) = o.derivBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯) (o.derivBFamily f a) = o.derivBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>IsNormal (o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯))
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>IsNormal (f i ?H.hi)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>i < o
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit a<GOAL>a / a = 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s t<GOAL>(G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s t<GOAL>(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)).card + (filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)).card = (s ×ˢ t).card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s t<VAR>this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)<GOAL>(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)).card + (filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)).card = (s ×ˢ t).card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : Disjoint s t<VAR>this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)<GOAL>Disjoint (filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) (filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t))
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : K ⊔ J = ⊤<GOAL>I * K ⊔ J = I ⊔ J