ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)<GOAL>∀ᶠ (i : ι) in l, (support fun y => (φ i).normed μ (x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)<GOAL>∀ᶠ (i : ι) in l, ∀ (x : G), |(φ i).normed μ (x₀ - x)| ≤ K ^ FiniteDimensional.finrank ℝ G / (μ (closedBall x₀ (φ i).rOut)).toReal
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hx : x ≠ 0<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<GOAL>legendreSym p a = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hx : x ≠ 0<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<VAR>hy : y ≠ 0<GOAL>legendreSym p a = 1
<VAR>z τ : ℂ<GOAL>(starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<GOAL>∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>(starRingEnd ℂ) (jacobiTheta₂_term n (-z) τ) = jacobiTheta₂_term n ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
<VAR>α : Type u_1<VAR>inst✝¹ : Add α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x + y) = (equivShrink α) x + (equivShrink α) y
<VAR>α : Type u_1<VAR>inst✝¹ : Add α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x + y) = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) + (equivShrink α).symm ((equivShrink α) y))
<VAR>m✝ n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m : ℕ<VAR>h : m.succ * n = n + m * n<GOAL>repeat m.succ a = append a (repeat m a) ∘ cast h
<VAR>m✝ n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m : ℕ<VAR>h : m.succ * n = n + m * n<GOAL>∀ (x : Fin (m.succ * n)), repeat m.succ a x = (append a (repeat m a) ∘ cast h) x
<VAR>m✝ n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m : ℕ<VAR>h : m.succ * n = n + m * n<GOAL>∀ (x : Fin (n + m * n)), repeat m.succ a (cast ⋯ x) = (append a (repeat m a) ∘ cast h) (cast ⋯ x)
<VAR>α : Type u_1<VAR>inst✝ : HeytingAlgebra α<VAR>a b : α<VAR>hb : IsRegular b<GOAL>Disjoint a bᶜ ↔ a ≤ b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>a b : α<VAR>l : List α<VAR>h : f a = some b<GOAL>lookmap f (a :: l) = b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>a b : α<VAR>l : List α<VAR>h : f a = some b<GOAL>(match f a with | some b => b :: l | none => lookmap.go f l (#[].push a)) = b :: l
<VAR>m n k : ℕ<GOAL>(m + n * k).Coprime n ↔ m.Coprime n
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<GOAL>absNorm ⊥ = 0
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>a✝ : Nontrivial R<GOAL>∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>a✝ : Nontrivial R<GOAL>∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>a✝ : Nontrivial R<VAR>t : R<VAR>ht : dist t 0 < ‖↑x⁻¹‖⁻¹<GOAL>inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>a✝ : Nontrivial R<VAR>t : R<VAR>ht : ‖t‖ < ‖↑x⁻¹‖⁻¹<GOAL>inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>r : R<GOAL>(optionEquivLeft R S₁) (C r) = Polynomial.C (C r)
<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>t u v w : V<VAR>p : G.Walk v w<VAR>he : s(t, u) ∈ p.edges<GOAL>t ∈ p.support
<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>t u v w : V<VAR>p : G.Walk v w<VAR>he✝ : s(t, u) ∈ p.edges<VAR>d : G.Dart<VAR>hd : d ∈ p.darts<VAR>he : d.edge = s(t, u)<GOAL>t ∈ p.support
<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>t u v w : V<VAR>p : G.Walk v w<VAR>he✝ : s(t, u) ∈ p.edges<VAR>d : G.Dart<VAR>hd : d ∈ p.darts<VAR>he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t<GOAL>t ∈ p.support
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<GOAL>Algebra.adjoin R ↑(Submodule.map (monomial 1) I) = reesAlgebra I
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<GOAL>Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<GOAL>reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
<VAR>m n a b c✝ d c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a * c ≡ b * c [MOD n]
<VAR>m n a b c✝ d c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>c * a ≡ c * b [MOD n]
<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<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ ⟪x, y⟫_ℝ = 0
<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<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ InnerProductGeometry.angle x y = π / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
<VAR>d : ℤ<VAR>a : ℤ√d<VAR>hgcd : 0 < a.re.gcd a.im<GOAL>∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im
<VAR>d : ℤ<VAR>a : ℤ√d<VAR>hgcd : 0 < a.re.gcd a.im<VAR>re im : ℤ<VAR>H1 : re.gcd im = 1<VAR>Hre : a.re = re * ↑(a.re.gcd a.im)<VAR>Him : a.im = im * ↑(a.re.gcd a.im)<GOAL>∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im
<VAR>d : ℤ<VAR>a : ℤ√d<VAR>hgcd : 0 < a.re.gcd a.im<VAR>re im : ℤ<VAR>H1 : re.gcd im = 1<VAR>Hre : a.re = ↑(a.re.gcd a.im) * re<VAR>Him : a.im = ↑(a.re.gcd a.im) * im<GOAL>∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : solution p a₁ a₂ = 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : solution p a₁ a₂ = 0<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : solution p a₁ a₂ = 0<VAR>this : 0 = a₂.coeff 0 / a₁.coeff 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : solution p a₁ a₂ = 0<VAR>this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<GOAL>p - 1 ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a b • p + toIocMod hp a b = b
<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>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableAt I' I'' g (f x)<VAR>hf : MDifferentiableAt I I' f x<GOAL>mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
<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>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableAt I' I'' g (f x)<VAR>hf : MDifferentiableAt I I' f x<GOAL>HasMFDerivAt I I'' (g ∘ f) x ((mfderiv I' I'' g (f x)).comp (mfderiv I I' f x))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>↑z = 0 ↔ z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>2 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>x✝ : α<GOAL>x✝ ∈ (f.comp g).Dom ↔ x✝ ∈ g.preimage f.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>x✝ : α<GOAL>(∃ y, ∃ a ∈ g x✝, y ∈ f a) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>x✝ : α<GOAL>(∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝
<VAR>w x✝ y✝ z : ℝ<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>w x✝ y✝ z : ℝ<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a c d : α<VAR>n : ℤ<GOAL>a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : 0 < b<GOAL>a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>this : PreservesColimits G<GOAL>HasCokernel f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>this✝ : PreservesColimits G<VAR>this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f<GOAL>HasCokernel f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>this✝ : PreservesColimits G<VAR>this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f<GOAL>HasCokernel f
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<GOAL>r * x = r * y ↔ x = y
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < φ.order<GOAL>(coeff R n) φ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>n : ℕ<VAR>h : (coeff R n) φ ≠ 0<GOAL>φ.order ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>(s ∪ t).erase a = s.erase a ∪ t.erase a
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ - φ₃).τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂ - φ₄).τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) = S₁.f ≫ h.h₁ - S₁.f ≫ h'.h₁ + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ - φ₃).τ₂ = S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂ - φ₄).τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) = S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - h'.h₁ ≫ S₂.f) + (φ₂.τ₂ - φ₄.τ₂)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ - φ₃).τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.133780, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - h'.h₂ ≫ S₂.g) + (φ₂.τ₃ - φ₄.τ₃)
<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 : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<GOAL>dist p₁ ((reflection s) p₂) = dist p₁ p₂
<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 : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p₁ : P<VAR>hp₁ : (reflection s) p₁ = p₁<VAR>p₂ : P<GOAL>dist p₁ ((reflection s) p₂) = dist p₁ p₂
<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 : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p₁ : P<VAR>hp₁ : (reflection s) p₁ = p₁<VAR>p₂ : P<GOAL>p₁ = (reflection s) p₁
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>h : L (fun n => χ ↑n) s = 0<GOAL>False
<VAR>ι : Type u<VAR>s : Finset ι<VAR>a b : ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>h : a ≠ ⊤ ∧ b ≠ ⊤<GOAL>a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
<VAR>ι : Type u<VAR>s : Finset ι<VAR>a b : ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>h : a ≠ ⊤ ∧ b ≠ ⊤<GOAL>a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>Nat.Prime p
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>Irreducible p
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.rank = (diagonal hA.eigenvalues).rank
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>(↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * ↑(star hA.eigenvectorUnitary)).rank = (diagonal hA.eigenvalues).rank
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>ho : lift.{v, u} o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>lift.{v, u} #(Quotient.out o).α < c
<VAR>x y : ℂ<GOAL>sin (x - y) = sin x * cos y - cos x * sin y
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p = -1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p + 1 = 0
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(-1) ^ p + 1 ^ p = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>↑u * inverse ↑u = 1