ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ }<GOAL>f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<GOAL>f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } (c /. d) = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }<GOAL>f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>hc : c /. d = n₂ /. ↑d₂<GOAL>f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>hc : c /. d = n₂ /. ↑d₂<GOAL>f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>hc : c /. d = n₂ /. ↑d₂<VAR>d₁0 : ↑d₁ ≠ 0<GOAL>f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
<VAR>q : ℚ<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>c₁ : n₁.natAbs.Coprime d₁<VAR>ha : a /. b = n₁ /. ↑d₁<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>c₂ : n₂.natAbs.Coprime d₂<VAR>hc : c /. d = n₂ /. ↑d₂<VAR>d₁0 : ↑d₁ ≠ 0<VAR>d₂0 : ↑d₂ ≠ 0<GOAL>f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>(s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : (s ∩ Icc x y).OrdConnected<VAR>z : α<VAR>hz : z ∈ Icc x y<GOAL>z ∈ s
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : (s ∩ Icc x y).OrdConnected<VAR>z : α<VAR>hz : z ∈ Icc x y<VAR>hxy : x ≤ y<GOAL>z ∈ s
<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 = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>H : Set ι<VAR>x : M<VAR>hmem : x ∈ Submodule.span R (e '' H)<VAR>i : ι<VAR>hi : (ε i) x ≠ 0<GOAL>i ∈ H
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>H : Set ι<VAR>i : ι<VAR>l : ι →₀ R<VAR>supp_l : l ∈ Finsupp.supported R R H<VAR>hmem : (Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)<VAR>hi : (ε i) ((Finsupp.total ι M R e) l) ≠ 0<GOAL>i ∈ H
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>H : Set ι<VAR>i : ι<VAR>l : ι →₀ R<VAR>supp_l : l ∈ Finsupp.supported R R H<VAR>hmem : (Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)<VAR>hi : (ε i) ((Finsupp.total ι M R e) l) ≠ 0<GOAL>¬l i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm = StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : NonAssocSemiring R<VAR>f : ℕ → ℕ → R<VAR>n : ℕ<GOAL>∑ ij ∈ antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 = ∑ ij ∈ antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) + ∑ ij ∈ antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Integrable (fun x => y₀) μ<VAR>n : ℕ<GOAL>Integrable (↑(approxOn f fmeas s y₀ h₀ n)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f 1 μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) 1 μ<VAR>n : ℕ<GOAL>Memℒp (↑(approxOn f fmeas s y₀ h₀ n)) 1 μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝¹ y z✝ x z : E<VAR>x✝ : z ∈ [x-[𝕜]x]<VAR>a b : 𝕜<VAR>left✝¹ : 0 ≤ a<VAR>left✝ : 0 ≤ b<VAR>hab : a + b = 1<VAR>hz : a • x + b • x = z<GOAL>z ∈ {x}
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>takeD n [] a = replicate n a
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>g.Separable
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (g * f).Separable<GOAL>g.Separable
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>φ : ι → Type u_4<VAR>f : (ι : ι) → φ ι → M<VAR>hf : ∀ (i : ι), LinearIndependent R (f i)<GOAL>LinearIndependent R fun ix => single ix.fst (f ix.fst ix.snd)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>φ : ι → Type u_4<VAR>f : (ι : ι) → φ ι → M<VAR>hf : ∀ (i : ι), LinearIndependent R (f i)<GOAL>∀ (j : ι), LinearIndependent R fun x => single j (f j x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>φ : ι → Type u_4<VAR>f : (ι : ι) → φ ι → M<VAR>hf : ∀ (i : ι), LinearIndependent R (f i)<GOAL>∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (Set.range fun x => single i (f i x))) (⨆ i ∈ t, span R (Set.range fun x => single i (f i x)))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝ : CommRing A<VAR>a : A<VAR>n✝ : ℕ<GOAL>(coeff A n✝) ((rescale a) X) = (coeff A n✝) ((C A) a * X)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝ : CommRing A<VAR>a : A<VAR>n✝ : ℕ<GOAL>(a ^ n✝ * if n✝ = 1 then 1 else 0) = a * if n✝ = 1 then 1 else 0
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Nontrivial R<VAR>ι : Type w<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Nontrivial R<VAR>ι : Type w<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>lift.{v, w} #ι ≤ lift.{w, v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Nontrivial R<VAR>ι : Type w<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>lift.{v, w} #ι ≤ lift.{w, v} #↑↑⟨range v, ⋯⟩
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (y - x) y).sign = -(o.oangle x y).sign
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<GOAL>log b r = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<GOAL>∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<VAR>s : Set α<VAR>hms : MeasurableSet s<GOAL>∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<VAR>s : Set α<VAR>hms : MeasurableSet s<GOAL>∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<VAR>s : Set α<VAR>hms : MeasurableSet s<GOAL>∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hmg : Measurable g<VAR>hgf : g ≤ f<VAR>hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ<VAR>s : Set α<VAR>hms : MeasurableSet s<GOAL>∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ⊤
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_5<VAR>β : α → Type u_4<VAR>ne : ∀ (a : α), Nonempty (β a)<VAR>p : α → Prop<VAR>this : DecidablePred p := Classical.decPred p<GOAL>Surjective fun f => restrict p f
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_5<VAR>β : α → Type u_4<VAR>ne : ∀ (a : α), Nonempty (β a)<VAR>p : α → Prop<VAR>this : DecidablePred p := Classical.decPred p<VAR>f : (x : Subtype p) → β ↑x<GOAL>∀ (x : Subtype p), (fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) x = f x
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_5<VAR>β : α → Type u_4<VAR>ne : ∀ (a : α), Nonempty (β a)<VAR>p : α → Prop<VAR>this : DecidablePred p := Classical.decPred p<VAR>f : (x : Subtype p) → β ↑x<VAR>x : α<VAR>hx : p x<GOAL>(fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) ⟨x, hx⟩ = f ⟨x, hx⟩
<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>n : ℕ<VAR>hn : 0 < n<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 F E<VAR>v : Fin n → F<VAR>A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}<GOAL>(p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v
<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>n : ℕ<VAR>hn : 0 < n<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 F E<VAR>v : Fin n → F<VAR>A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}<VAR>B : Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}<GOAL>(p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v
<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>n : ℕ<VAR>hn : 0 < n<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 F E<VAR>v : Fin n → F<VAR>A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}<VAR>B : Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}<VAR>C : (p (Composition.single n hn).length) (q.applyComposition (Composition.single n hn) v) = (p 1) fun x => (q n) v<GOAL>(p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<GOAL>μ.withDensity f ≪ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs₁ : MeasurableSet s<VAR>hs₂ : μ s = 0<GOAL>(μ.withDensity f) s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs₁ : MeasurableSet s<VAR>hs₂ : μ s = 0<GOAL>∫⁻ (a : α) in s, f a ∂μ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝ : DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : (image f s).Nonempty<VAR>g : β → α<GOAL>(image f s).sup' hs g = s.sup' ⋯ (g ∘ f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝ : DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : (image f s).Nonempty<VAR>g : β → α<GOAL>↑((image f s).sup' hs g) = ↑(s.sup' ⋯ (g ∘ f))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝ : DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>hs : (image f s).Nonempty<VAR>g : β → α<GOAL>s.sup ((WithBot.some ∘ g) ∘ f) = s.sup (WithBot.some ∘ g ∘ f)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>s : κ → HomogeneousIdeal 𝒜<GOAL>(⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>x : PowerSeries R<GOAL>∀ {a b : ℕ}, { toFun := Nat.cast, inj' := ⋯ } a ≤ { toFun := Nat.cast, inj' := ⋯ } b ↔ a ≤ b
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>x : PowerSeries R<GOAL>∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin (l.rotate n).length<GOAL>(l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩
<VAR>a✝ b✝ : ℤ<VAR>n✝ a b n : ℕ<VAR>a_le_n : a ≤ n<VAR>b_le_n : b ≤ n<GOAL>(↑a - ↑b).natAbs ≤ n
<VAR>a✝ b✝ : ℤ<VAR>n✝ a b n : ℕ<VAR>a_le_n : a ≤ n<VAR>b_le_n : b ≤ n<GOAL>|↑a - ↑b| ≤ ↑n
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>(a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c
<VAR>n m a : ℕ<VAR>h : n ≤ m<VAR>ha : m - n ∣ a<VAR>p : ℕ<VAR>pp : Prime p<VAR>hn : p ∣ n * a + 1<VAR>hm : p ∣ m * a + 1<GOAL>False
<VAR>n m a : ℕ<VAR>h : n ≤ m<VAR>ha : m - n ∣ a<VAR>p : ℕ<VAR>pp : Prime p<VAR>hn : p ∣ n * a + 1<VAR>hm : p ∣ m * a + 1<VAR>this : p ∣ (m - n) * a<GOAL>False
<VAR>n m a : ℕ<VAR>h : n ≤ m<VAR>ha : m - n ∣ a<VAR>p : ℕ<VAR>pp : Prime p<VAR>hn : p ∣ n * a + 1<VAR>hm : p ∣ m * a + 1<VAR>this✝ : p ∣ (m - n) * a<VAR>this : p ∣ a<GOAL>False
<VAR>n m a : ℕ<VAR>h : n ≤ m<VAR>ha : m - n ∣ a<VAR>p : ℕ<VAR>pp : Prime p<VAR>hn : p ∣ n * a + 1<VAR>hm : p ∣ m * a + 1<VAR>this✝ : p ∣ (m - n) * a<VAR>this : p ∣ a<GOAL>p = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁✝ w₂✝ : ι → k<VAR>p✝ : ι → V<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 0<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>(s.weightedVSub p) w ∈ vectorSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂} ↔ ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁✝ w₂✝ : ι → k<VAR>p✝ : ι → V<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 0<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>(∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w) ↔ ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a ⊗ₜ[R] m ∈ baseChange A p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a • 1 ⊗ₜ[R] m ∈ baseChange A p
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>s : ↥M<GOAL>mk' S 0 s = 0