ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>hA : IsLeftRegular A.det<VAR>hB : IsLeftRegular B.det<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>hA : IsLeftRegular A.det<VAR>hB : IsLeftRegular B.det<VAR>hAB : IsLeftRegular (A * B).det<GOAL>(A * B).adjugate = B.adjugate * A.adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>hA : IsLeftRegular A.det<VAR>hB : IsLeftRegular B.det<VAR>hAB : IsLeftRegular (A * B).det<GOAL>(fun x => A * B * x) (A * B).adjugate = (fun x => A * B * x) (B.adjugate * A.adjugate)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>hA : IsLeftRegular A.det<VAR>hB : IsLeftRegular B.det<VAR>hAB : IsLeftRegular (A * B).det<GOAL>A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℝ<GOAL>ρ.IicSnd r ≤ ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ρ.IicSnd r) s ≤ ρ.fst s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>ρ (s ×ˢ Iic r) ≤ ρ (Prod.fst ⁻¹' s)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Zero α<VAR>inst✝² : One α<VAR>inst✝¹ : Zero β<VAR>inst✝ : One β<VAR>f : α → β<VAR>h₀ : f 0 = 0<VAR>h₁ : f 1 = 1<VAR>i✝ j✝ : n<GOAL>map 1 f i✝ j✝ = 1 i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Zero α<VAR>inst✝² : One α<VAR>inst✝¹ : Zero β<VAR>inst✝ : One β<VAR>f : α → β<VAR>h₀ : f 0 = 0<VAR>h₁ : f 1 = 1<VAR>i✝ j✝ : n<GOAL>f (if i✝ = j✝ then 1 else 0) = if i✝ = j✝ then 1 else 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>δ K ε a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r<VAR>ha : f a ≤ δ<VAR>bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε<VAR>H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)<VAR>x : ℝ<VAR>hx : x ∈ Icc a b<GOAL>f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>δ K ε a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r<VAR>ha : f a ≤ δ<VAR>bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε<VAR>H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)<VAR>x : ℝ<VAR>hx : x ∈ Icc a b<GOAL>ε ∈ closure (Ioi ε)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>δ K ε a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r<VAR>ha : f a ≤ δ<VAR>bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε<VAR>H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)<VAR>x : ℝ<VAR>hx : x ∈ Icc a b<GOAL>ContinuousWithinAt (fun y => gronwallBound δ K y (x - a)) (Ioi ε) ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulReflectLT α β<VAR>h : 0 < a • b<VAR>ha : 0 ≤ a<GOAL>a • 0 < a • b
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<GOAL>0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ<GOAL>0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₁ s.center ≤ s.radius<GOAL>0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫_ℝ
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Fintype F<VAR>inst✝³ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>F' : Type u_2<VAR>inst✝² : Field F'<VAR>inst✝¹ : Fintype F'<VAR>inst✝ : DecidableEq F'<VAR>hF' : ringChar F' ≠ 2<VAR>h : ringChar F' ≠ ringChar F<VAR>χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')<GOAL>(quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Fintype F<VAR>inst✝³ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>F' : Type u_2<VAR>inst✝² : Field F'<VAR>inst✝¹ : Fintype F'<VAR>inst✝ : DecidableEq F'<VAR>hF' : ringChar F' ≠ 2<VAR>h : ringChar F' ≠ ringChar F<VAR>χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')<VAR>hχ₁ : χ ≠ 1<GOAL>(quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Fintype F<VAR>inst✝³ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>F' : Type u_2<VAR>inst✝² : Field F'<VAR>inst✝¹ : Fintype F'<VAR>inst✝ : DecidableEq F'<VAR>hF' : ringChar F' ≠ 2<VAR>h✝ : ringChar F' ≠ ringChar F<VAR>χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')<VAR>hχ₁ : χ ≠ 1<VAR>h : (χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')<GOAL>(quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Fintype F<VAR>inst✝³ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>F' : Type u_2<VAR>inst✝² : Field F'<VAR>inst✝¹ : Fintype F'<VAR>inst✝ : DecidableEq F'<VAR>hF' : ringChar F' ≠ 2<VAR>h✝ : ringChar F' ≠ ringChar F<VAR>χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')<VAR>hχ₁ : χ ≠ 1<VAR>h : ↑((quadraticChar F') (χ (-1) * ↑(Fintype.card F))) = χ ↑(Fintype.card F')<GOAL>(quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : x ∈ periodicPts f<GOAL>y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : x ∈ periodicPts f<GOAL>(∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ n, f^[n] x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : x ∈ periodicPts f<GOAL>(∃ n, f^[n] x = y) → ∃ a < minimalPeriod f x, f^[a] x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>∃ a < minimalPeriod f x, f^[a] x = f^[n] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>f^[n % minimalPeriod f x] x = f^[n] x
<VAR>a b k m n✝ p n : ℕ<GOAL>n.primeFactors.Nonempty ↔ 1 < n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.83140, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.s = s'.s<GOAL>s = s'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.83140, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.s = s'.s<VAR>this : Mono S.f<GOAL>s = s'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.83140, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.s = s'.s<VAR>this : Mono S.f<VAR>eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂<GOAL>s = s'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.83140, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.s = s'.s<VAR>this : Mono S.f<VAR>eq : s.r = s'.r<GOAL>s = s'
<VAR>x y : ℝ<GOAL>Real.zero.cauchy = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b✝ b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i => (i, b), inj' := ⋯ } s
<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>h : TendstoUniformlyOn F f p s<VAR>g : γ → α<GOAL>TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)
<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>h : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>g : γ → α<GOAL>TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsGalois X<VAR>x y : ↑(F.obj X)<GOAL>∃ g, g • x = y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsGalois X<VAR>x y : ↑(F.obj X)<VAR>φ : Aut X<VAR>h : φ • x = y<GOAL>∃ g, g • x = y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsGalois X<VAR>x y : ↑(F.obj X)<VAR>φ : Aut X<VAR>h : φ • x = y<VAR>a : AutGalois F<VAR>ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ<GOAL>∃ g, g • x = y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsGalois X<VAR>x y : ↑(F.obj X)<VAR>φ : Aut X<VAR>h : φ • x = y<VAR>a : AutGalois F<VAR>ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ<GOAL>(autMulEquivAutGalois F).symm { unop' := a } • x = y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p x y : α<VAR>h : Prime p<VAR>i : ℕ<VAR>hxy : p ^ (i + 1) ∣ x * y<GOAL>p ^ (i + 1) ∣ x ∨ p ∣ y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p x y : α<VAR>h : Prime p<VAR>i : ℕ<VAR>hxy : p ^ (i + 1) ∣ x * y<GOAL>¬p ∣ y → p ^ (i + 1) ∣ x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p y : α<VAR>h : Prime p<VAR>hy : ¬p ∣ y<VAR>i : ℕ<VAR>ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x<VAR>x : α<VAR>hxy : p ^ (i + 1 + 1) ∣ x * y<GOAL>p ^ (i + 1 + 1) ∣ x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p y : α<VAR>h : Prime p<VAR>hy : ¬p ∣ y<VAR>i : ℕ<VAR>ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x<VAR>x : α<VAR>hxy : p * p ^ (i + 1) ∣ x * y<GOAL>p * p ^ (i + 1) ∣ x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p y : α<VAR>h : Prime p<VAR>hy : ¬p ∣ y<VAR>i : ℕ<VAR>ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x<VAR>x' : α<VAR>hxy : p * p ^ (i + 1) ∣ p * x' * y<GOAL>p * p ^ (i + 1) ∣ p * x'
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p y : α<VAR>h : Prime p<VAR>hy : ¬p ∣ y<VAR>i : ℕ<VAR>ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x<VAR>x' : α<VAR>hxy : p * p ^ (i + 1) ∣ p * (x' * y)<GOAL>p * p ^ (i + 1) ∣ p * x'
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>x : M<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>IsLocalHomeomorph f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>x : M<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>IsLocalHomeomorphOn f univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>x : M<VAR>hf : IsLocalDiffeomorphOn I J n f univ<GOAL>IsLocalHomeomorphOn f univ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : BoundedOrder β<VAR>f : α ≃o β<GOAL>IsSimpleOrder α ↔ IsSimpleOrder β
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f : σ → S₁<VAR>s : Set S₁<GOAL>Algebra.adjoin R s = (aeval Subtype.val).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<GOAL>xs.sym2.length = (xs.length + 1).choose 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>inst✝ : NormedAddCommGroup β<VAR>hp_top : p ≠ ⊤<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp_top : 0 ≠ ⊤<VAR>hf : Memℒp f 0 μ<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>inst✝ : NormedAddCommGroup β<VAR>hp_top : p ≠ ⊤<VAR>f : α → β<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hp₀ : p ≠ 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : PseudoMetricSpace X<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>inst✝ : IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<GOAL>univ.inf' ⋯ f = ⨅ i, f i
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>X✝ Y✝ : StructuredArrow F (const J)<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>((fun c => { pt := c.right, ι := c.hom }) X✝).ι.app j ≫ f.right = ((fun c => { pt := c.right, ι := c.hom }) Y✝).ι.app j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>X✝ Y✝ : StructuredArrow F (const J)<VAR>f : X✝ ⟶ Y✝<VAR>j : J<VAR>e_1✝ : (F.obj j ⟶ ((fun c => { pt := c.right, ι := c.hom }) Y✝).pt) = (((fromPUnit F).obj X✝.left).obj j ⟶ ((const J).obj Y✝.right).obj j)<VAR>e_5✝ : F = (fromPUnit F).obj X✝.left<GOAL>((fun c => { pt := c.right, ι := c.hom }) Y✝).ι = (fromPUnit F).map f.left ≫ Y✝.hom
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M : Type x<VAR>inst✝³ : Monoid M<VAR>φ : G →* H<VAR>A B C : Type u<VAR>inst✝² : CommGroup A<VAR>inst✝¹ : CommGroup B<VAR>inst✝ : CommGroup C<VAR>f : A →* B<VAR>g : B →* A<VAR>e : A ≃* B<VAR>d : B ≃* C<VAR>n : ℤ<VAR>x : A ⧸ (zpowGroupHom n).range<GOAL>((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) x = (equivQuotientZPowOfEquiv (e.trans d) n) x
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M : Type x<VAR>inst✝³ : Monoid M<VAR>φ : G →* H<VAR>A B C : Type u<VAR>inst✝² : CommGroup A<VAR>inst✝¹ : CommGroup B<VAR>inst✝ : CommGroup C<VAR>f : A →* B<VAR>g : B →* A<VAR>e : A ≃* B<VAR>d : B ≃* C<VAR>n : ℤ<VAR>x : A ⧸ (zpowGroupHom n).range<GOAL>((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out' x)) = (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out' x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hf : Function.Injective ⇑f<VAR>hfg : LinearMap.range f = LinearMap.ker g<VAR>h1 : IsSMulRegular M r<VAR>h2 : IsSMulRegular M'' r<GOAL>IsSMulRegular M' r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hf : Function.Injective ⇑f<VAR>hfg : LinearMap.range f = LinearMap.ker g<VAR>h1 : IsSMulRegular M r<VAR>h2 : IsSMulRegular M'' r<GOAL>∀ (x : M'), r • x = 0 → x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hf : Function.Injective ⇑f<VAR>hfg : LinearMap.range f = LinearMap.ker g<VAR>h1 : IsSMulRegular M r<VAR>h2 : IsSMulRegular M'' r<VAR>y : M<VAR>hx : r • f y = 0<GOAL>f y = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hf : Function.Injective ⇑f<VAR>hfg : LinearMap.range f = LinearMap.ker g<VAR>h1 : IsSMulRegular M r<VAR>h2 : IsSMulRegular M'' r<VAR>y : M<VAR>hx : r • f y = 0<GOAL>r • y = 0
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>(l₁.diff l₂).erase a = (l₁.erase a).diff l₂
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter β<VAR>f : β → α<GOAL>Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℕ<GOAL>im ↑n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Group α<VAR>a✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ᵐ / a⁻ᵐ = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s : Set E<VAR>y : E<VAR>a b : 𝕜<VAR>a✝¹ : 0 ≤ a<VAR>a✝ : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • y + b • y ∈ {y}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<GOAL>x ∈ S'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<GOAL>x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<GOAL>x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<GOAL>x ∈ toSubmodule (ofId (↥S') S).range