ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → δ<VAR>h : μ ≤ ν<VAR>hf : AEMeasurable f ν<VAR>s : Set δ<VAR>hs : MeasurableSet s<GOAL>(map f μ) s ≤ (map f ν) s
<VAR>β : Type v<VAR>inst✝¹ : NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>inst✝ : IsComplete β norm<VAR>s : Set β<VAR>os : IsOpen s<VAR>lfs : f.lim ∈ s<GOAL>∃ a, ∀ b ≥ a, ↑f b ∈ s
<VAR>β : Type v<VAR>inst✝¹ : NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>inst✝ : IsComplete β norm<VAR>s : Set β<VAR>os : IsOpen s<VAR>lfs : f.lim ∈ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : Metric.ball f.lim ε ⊆ s<GOAL>∃ a, ∀ b ≥ a, ↑f b ∈ s
<VAR>β : Type v<VAR>inst✝¹ : NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>inst✝ : IsComplete β norm<VAR>s : Set β<VAR>os : IsOpen s<VAR>lfs : f.lim ∈ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : Metric.ball f.lim ε ⊆ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < ε<GOAL>∃ a, ∀ b ≥ a, ↑f b ∈ s
<VAR>β : Type v<VAR>inst✝¹ : NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>inst✝ : IsComplete β norm<VAR>s : Set β<VAR>os : IsOpen s<VAR>lfs : f.lim ∈ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : Metric.ball f.lim ε ⊆ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < ε<VAR>b : ℕ<VAR>hb : b ≥ N<GOAL>dist (↑f b) f.lim < ε
<VAR>β : Type v<VAR>inst✝¹ : NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>inst✝ : IsComplete β norm<VAR>s : Set β<VAR>os : IsOpen s<VAR>lfs : f.lim ∈ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : Metric.ball f.lim ε ⊆ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < ε<VAR>b : ℕ<VAR>hb : b ≥ N<GOAL>‖f.lim - ↑f b‖ < ε
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<GOAL>Nat.card (G ⧸ H) * Nat.card ↥H = s * p * Nat.card ↥H
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<GOAL>Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p = 0
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<GOAL>Nat.card ↑(Subtype.val '' ↑(comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))) = p ^ (n + 1)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<GOAL>Nat.card ↑↑(comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)) = Nat.card (↥(H.subgroupOf H.normalizer) × ↥(zpowers x))
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<VAR>y : G<VAR>hy : y ∈ H<GOAL>y ∈ Subgroup.map H.normalizer.subtype (comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<VAR>y : G<VAR>hy : y ∈ H<GOAL>∃ x_1, ↑x_1 ∈ zpowers x ∧ ↑x_1 = y
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<VAR>y : G<VAR>hy : y ∈ H<GOAL>(fun x_1 => x ^ x_1) 0 = ↑⟨y, ⋯⟩
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<VAR>y : G<VAR>hy : y ∈ H<GOAL>x ^ 0 = ↑⟨y, ⋯⟩
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<VAR>s : ℕ<VAR>hs : Nat.card G = s * p ^ (n + 1)<VAR>hcard : Nat.card (G ⧸ H) = s * p<VAR>hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p<VAR>hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)<VAR>x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer<VAR>hx : orderOf x = p<VAR>hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)<VAR>y : G<VAR>hy : y ∈ H<GOAL>⟨y, ⋯⟩ ∈ H.subgroupOf H.normalizer
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<GOAL>K' = K
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<GOAL>K' = K
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<VAR>dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯<GOAL>K' = K
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<VAR>dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯<VAR>finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree<GOAL>K' = K
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<VAR>dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯<VAR>finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree<GOAL>finrank (↥K') E ≤ finrank (↥K) E
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<VAR>dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯<VAR>finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree<GOAL>(minpoly (↥K') α).natDegree ≤ (minpoly (↥K) α).natDegree
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K✝ : Type u<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K✝ L<VAR>inst✝ : FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<VAR>g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)<VAR>K' : IntermediateField F E := adjoin F ↑g.coeffs<VAR>hsub : K' ≤ K<VAR>dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯<VAR>finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree<GOAL>(minpoly (↥K) α).natDegree = (g.toSubring K'.toSubring ⋯).natDegree
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<GOAL>IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : (fun x => ↑x * (⅟↑da * ⅟↑db)) (na * ↑db + nb * ↑da) = (fun x => ↑x * (⅟↑da * ⅟↑db)) (↑k * nc)<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db<VAR>h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da<VAR>h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc<GOAL>↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * ↑db + nb * ↑da = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da<VAR>h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc<GOAL>↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<GOAL>↑(g • z) = ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<GOAL>↑(g • z) = ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<GOAL>↑(g • z) = ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<VAR>nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0<GOAL>↑(g • z) = ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<VAR>nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0<GOAL>(↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) = ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) + (↑(p 1) * ↑z - ↑(p 0)) * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) * denom (↑g) z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<VAR>nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0<GOAL>(↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))) = ((↑(p 0) * ↑(↑g 0 0) + ↑(p 1) * ↑(↑g 0 1)) * ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1))) + (↑(p 1) * ↑z - ↑(p 0)) * ↑(↑g).det * (↑(p 0) ^ 2 + ↑(p 1) ^ 2)) * denom (↑g) z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<VAR>nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0<GOAL>(↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))) = ((↑(↑g 1 0) * ↑(↑g 0 0) + ↑(↑g 1 1) * ↑(↑g 0 1)) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))) + (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) * ↑(↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) * (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2)) * denom (↑g) z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<VAR>nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0<VAR>this : Int.cast ∘ p ≠ 0<VAR>nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0<GOAL>(↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))) = ((↑(↑g 1 0) * ↑(↑g 0 0) + ↑(↑g 1 1) * ↑(↑g 0 1)) * ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))) + (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) * (↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0)) * (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2)) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : β → γ → ℝ≥0∞ := Function.curry f<GOAL>∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g b c ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : β → γ → ℝ≥0∞ := Function.curry f<GOAL>∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : β → γ → ℝ≥0∞ := Function.curry f<GOAL>Measurable (Function.uncurry g)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : MulZeroOneClass M₀<VAR>s t : Set ι<VAR>i : ι<VAR>inst✝ : Nontrivial M₀<GOAL>s.indicator 1 i = 1 ↔ i ∈ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>n : Type u_8<VAR>inst✝ : Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : EuclideanSpace ℝ n<GOAL>x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>n : Type u_8<VAR>inst✝ : Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : EuclideanSpace ℝ n<VAR>this : 0 ≤ ∑ i : n, x i ^ 2<GOAL>x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>x : L<VAR>n : Module.End R ↥↑(weightSpace M χ) := (toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id<GOAL>(LinearMap.trace R ↥↑(weightSpace M χ) ∘ₗ ↑(toEnd R L ↥↑(weightSpace M χ))) x = (finrank R ↥↑(weightSpace M χ) • χ) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>x : L<VAR>n : Module.End R ↥↑(weightSpace M χ) := (toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id<VAR>h₁ : (toEnd R L ↥↑(weightSpace M χ)) x = n + χ x • LinearMap.id<GOAL>(LinearMap.trace R ↥↑(weightSpace M χ) ∘ₗ ↑(toEnd R L ↥↑(weightSpace M χ))) x = (finrank R ↥↑(weightSpace M χ) • χ) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>x : L<VAR>n : Module.End R ↥↑(weightSpace M χ) := (toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id<VAR>h₁ : (toEnd R L ↥↑(weightSpace M χ)) x = n + χ x • LinearMap.id<VAR>h₂ : (LinearMap.trace R ↥↑(weightSpace M χ)) n = 0<GOAL>(LinearMap.trace R ↥↑(weightSpace M χ) ∘ₗ ↑(toEnd R L ↥↑(weightSpace M χ))) x = (finrank R ↥↑(weightSpace M χ) • χ) x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ : L → R<VAR>x : L<VAR>n : Module.End R ↥↑(weightSpace M χ) := (toEnd R L ↥↑(weightSpace M χ)) x - χ x • LinearMap.id<VAR>h₁ : (toEnd R L ↥↑(weightSpace M χ)) x = n + χ x • LinearMap.id<VAR>h₂ : (LinearMap.trace R ↥↑(weightSpace M χ)) n = 0<GOAL>0 + (LinearMap.trace R ↥↑(weightSpace M χ)) (χ x • LinearMap.id) = (finrank R ↥↑(weightSpace M χ) • χ) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b<VAR>a : α<GOAL>(Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b<VAR>a : α<GOAL>(Set.range fun l => foldr (fun z w => f w z) a l.reverse) ⊆ Set.range fun l => foldr (fun z w => g w z) a l.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b<VAR>a : α<GOAL>Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)