ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ slitPlane<VAR>A : p.1 ≠ 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => cexp (log x.1 * x.2)<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) (p.1 ^ p.2 • (p.2 / p.1) • ContinuousLinearMap.fst ℂ ℂ ℂ + p.1 ^ p.2 • log p.1 • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ slitPlane<VAR>A : p.1 ≠ 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => cexp (log x.1 * x.2)<GOAL>HasStrictFDerivAt (fun x => cexp (log x.1 * x.2)) (p.1 ^ p.2 • (p.2 / p.1) • ContinuousLinearMap.fst ℂ ℂ ℂ + p.1 ^ p.2 • log p.1 • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>n m : ℕ<VAR>a : Fin n<GOAL>↑↑↑a = ↑a.castSucc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<VAR>hdivb : p ^ (multiplicity p b).get ⋯ ∣ b<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<VAR>hdivb : p ^ (multiplicity p b).get ⋯ ∣ b<VAR>hpoweq : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) = p ^ (multiplicity p a).get ⋯ * p ^ (multiplicity p b).get ⋯<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<VAR>hdivb : p ^ (multiplicity p b).get ⋯ ∣ b<VAR>hpoweq : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) = p ^ (multiplicity p a).get ⋯ * p ^ (multiplicity p b).get ⋯<VAR>hdiv : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) ∣ a * b<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<VAR>hdivb : p ^ (multiplicity p b).get ⋯ ∣ b<VAR>hpoweq : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) = p ^ (multiplicity p a).get ⋯ * p ^ (multiplicity p b).get ⋯<VAR>hdiv : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) ∣ a * b<VAR>hsucc : ¬p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯ + 1) ∣ a * b<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<VAR>hdiva : p ^ (multiplicity p a).get ⋯ ∣ a<VAR>hdivb : p ^ (multiplicity p b).get ⋯ ∣ b<VAR>hpoweq : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) = p ^ (multiplicity p a).get ⋯ * p ^ (multiplicity p b).get ⋯<VAR>hdiv : p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) ∣ a * b<VAR>hsucc : ¬p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯ + 1) ∣ a * b<GOAL>p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯) ∣ a * b ∧ ¬p ^ ((multiplicity p a).get ⋯ + (multiplicity p b).get ⋯ + 1) ∣ a * b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>y : Y<GOAL>comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)
<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>ι : Type u_1<VAR>N : ι → LieSubmodule R L M<GOAL>CompleteLattice.Independent N ↔ CompleteLattice.Independent fun i => ↑(N i)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<GOAL>l.concat a = (a :: l.reverse).reverse
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : a + b = 1<GOAL>a < a + b
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : a + b = 1<GOAL>a⁻¹⁻¹ + b⁻¹⁻¹ = 1
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<GOAL>multiplicity p ((p ^ n).choose k) + multiplicity p k ≤ ↑n
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<VAR>hdisj : Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 n.succ)) (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))<GOAL>multiplicity p ((p ^ n).choose k) + multiplicity p k ≤ ↑n
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<VAR>hdisj : Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 n.succ)) (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))<GOAL>(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ)).card ≤ n
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<VAR>hdisj : Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 n.succ)) (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))<VAR>filter_le_Ico : (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ)).card ≤ (Ico 1 n.succ).card<GOAL>(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ)).card ≤ n
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<GOAL>↑n ≤ multiplicity p ((p ^ n).choose k) + multiplicity p k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<GOAL>multiplicity p (p ^ n) ≤ multiplicity p ((p ^ n).choose k) + multiplicity p k
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ<VAR>a✝¹ : α<VAR>a✝ : Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))<VAR>h'x : ρ.rnDeriv μ a✝¹ = v.limRatioMeas hρ a✝¹<GOAL>Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (ρ.rnDeriv μ a✝¹))
<VAR>K : Type u_1<VAR>hK : NormedField K<VAR>h : IsNonarchimedean (sorryAx (K → ℝ) true)<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>Γ₀ : Type u_3<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : v.RankOne<VAR>x : L<GOAL>0 ≤ norm x
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<GOAL>(contractRight 1) d = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : AddCommGroup M₂<VAR>f g : M →+ M₂<VAR>h : f.toIntLinearMap = g.toIntLinearMap<VAR>x : M<GOAL>f x = g x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>d : σ →₀ ℕ<GOAL>(bind₂ f) ((monomial d) 1) = (monomial d) 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<GOAL>IsRadical (minpoly K f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<GOAL>(annihilator K[X] (AEval' f)).IsRadical
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<GOAL>Epi f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<GOAL>Epi f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<VAR>this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧<GOAL>Epi f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<VAR>this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧<VAR>R : C<VAR>x : R ⟶ (Over.mk (p.hom ≫ f)).left<VAR>y : R ⟶ (Over.mk (𝟙 Q)).left<VAR>w✝ : Epi x<VAR>ey : Epi y<VAR>comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom<GOAL>Epi f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<VAR>this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧<VAR>R : C<VAR>x : R ⟶ (Over.mk (p.hom ≫ f)).left<VAR>y : R ⟶ (Over.mk (𝟙 Q)).left<VAR>w✝ : Epi x<VAR>ey : Epi y<VAR>comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom<GOAL>(x ≫ p.hom) ≫ f = y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<VAR>this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧<VAR>R : C<VAR>x : R ⟶ (Over.mk (p.hom ≫ f)).left<VAR>y : R ⟶ (Over.mk (𝟙 Q)).left<VAR>w✝ : Epi x<VAR>ey : Epi y<VAR>comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q<GOAL>(x ≫ p.hom) ≫ f = y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Surjective (pseudoApply f)<VAR>pbar : Pseudoelement P<VAR>hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))<VAR>p : Over P<VAR>hp : ⟦p⟧ = pbar<VAR>this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧<VAR>R : C<VAR>x : R ⟶ (Over.mk (p.hom ≫ f)).left<VAR>y : R ⟶ (Over.mk (𝟙 Q)).left<VAR>w✝ : Epi x<VAR>ey : Epi y<VAR>comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q<GOAL>y ≫ 𝟙 Q = y
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(x * y).arg = ↑x.arg + ↑y.arg
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x * y = ↑(abs x * abs y) * (↑(↑x.arg + ↑y.arg).cos + ↑(↑x.arg + ↑y.arg).sin * I)
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x * y = ↑(abs x) * ↑(abs y) * (cexp (↑x.arg * I) * cexp (↑y.arg * I))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>p a b c d x y : R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : GCDMonoid R<VAR>h1 : p ∣ a * x + b * y<VAR>h2 : p ∣ c * x + d * y<GOAL>p ∣ (a * d - b * c) * gcd x y
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>p a b c d x y : R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : GCDMonoid R<VAR>h1 : p ∣ a * x + b * y<VAR>h2 : p ∣ c * x + d * y<GOAL>p ∣ gcd ((a * d - b * c) * x) ((a * d - b * c) * y)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 1 < t<GOAL>Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 1 < t<GOAL>t ^ (-r⁻¹) < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal
<VAR>p q : ℚ<VAR>hp : 0 ≤ p<GOAL>(p * q).toNNRat = p.toNNRat * q.toNNRat
<VAR>p q : ℚ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>(p * q).toNNRat = p.toNNRat * q.toNNRat
<VAR>p q : ℚ<VAR>hp : 0 ≤ p<VAR>hq : q ≤ 0<GOAL>(p * q).toNNRat = p.toNNRat * q.toNNRat
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>midpoint R x y = midpoint R y x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H : Subgroup G<VAR>a : G<VAR>h : a ∈ H.normalCore<GOAL>a ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H : Subgroup G<VAR>a : G<VAR>h : a ∈ H.normalCore<GOAL>1 * a * 1⁻¹ ∈ H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<GOAL>IsBlock G (orbit (↥H) a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<GOAL>∀ (g : G), (∃ x ∈ g • orbit (↥H) a, x ∈ orbit (↥H) a) → g • orbit (↥H) a = orbit (↥H) a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<VAR>g : G<VAR>h₁ h₂ : ↥H<VAR>h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂<GOAL>g • orbit (↥H) a = orbit (↥H) a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<VAR>g : G<VAR>h₁ h₂ : ↥H<VAR>h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂<GOAL>g ∈ H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<VAR>g : G<VAR>h₁ h₂ : ↥H<VAR>h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂<GOAL>↑h₂⁻¹ * g * ↑h₁ ∈ H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<VAR>g : G<VAR>h₁ h₂ : ↥H<VAR>h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂<GOAL>↑h₂⁻¹ * g * ↑h₁ ∈ stabilizer G a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : stabilizer G a ≤ H<VAR>g : G<VAR>h₁ h₂ : ↥H<VAR>h : (fun x => g • x) ((fun m => m • a) h₁) = (fun m => m • a) h₂<GOAL>g • ↑h₁ • a = ↑h₂ • a
<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✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype m<VAR>v : m → α<VAR>A : Matrix m n α<GOAL>-v ᵥ* -A = v ᵥ* A
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Semiring α<VAR>inst✝¹ : AddCommMonoid β<VAR>inst✝ : Module α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>hσ : σ.IsCycleOn ↑s<VAR>f : ι → α<VAR>g : ι → β<GOAL>(∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range s.card, ∑ i ∈ s, f i • g ((σ ^ k) i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Semiring α<VAR>inst✝¹ : AddCommMonoid β<VAR>inst✝ : Module α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>hσ : σ.IsCycleOn ↑s<VAR>f : ι → α<VAR>g : ι → β<GOAL>∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range s.card, ∑ i ∈ s, f i • g ((σ ^ k) i)
<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✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : FiniteDimensional 𝕜 V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure s
<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✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : FiniteDimensional 𝕜 V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>(∃ y, (∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧ ↑y = x) ↔ ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
<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✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : FiniteDimensional 𝕜 V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>(∃ y, (∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧ ↑y = x) → ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
<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✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : FiniteDimensional 𝕜 V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>x : P<VAR>h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty<GOAL>∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → ⟨x, ?h.refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty
<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✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : FiniteDimensional 𝕜 V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>x : P<VAR>h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty<GOAL>x ∈ ↑(affineSpan 𝕜 s)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Monoid M<VAR>a b : M<VAR>h : Commute a b<GOAL>(a * b) ^ 0 = a ^ 0 * b ^ 0
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Monoid M<VAR>a b : M<VAR>h : Commute a b<VAR>n : ℕ<GOAL>(a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivWithinAt c c' s x<VAR>hu : HasDerivWithinAt u u' s x<GOAL>HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s 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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivWithinAt c c' s x<VAR>hu : HasDerivWithinAt u u' s x<VAR>this : HasDerivWithinAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) s x<GOAL>HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>l : List α<VAR>a : α<VAR>h : a ∈ ⟦l⟧<GOAL>a ∣ prod ⟦l⟧
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>Monotone (upperCentralSeries G)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ upperCentralSeries G n<VAR>y : G<GOAL>x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G n).fst
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ upperCentralSeries G n<VAR>y : G<GOAL>x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G n).fst
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l✝ l : Filter α<GOAL>∀ (S : Set (Set α)), #↑S < ℵ₀ → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : ℕ<VAR>E : Fin n → Type u_2<VAR>inst✝¹ : (i : Fin n) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : Fin n), SigmaFinite volume<VAR>f : (i : Fin n) → E i → 𝕜<GOAL>∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∉ upperClosure ↑s<VAR>ht : a ∉ upperClosure ↑t<GOAL>a ∉ upperClosure ↑(s ∪ t)