ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>inst✝ : Nonempty ι<VAR>f : ι → G.Subgraph<GOAL>(⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>inst✝ : Nonempty ι<VAR>f : ι → G.Subgraph<GOAL>(∀ G' ∈ Set.range fun i => f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ i : ι, ‖x i‖ ^ (ENNReal.ofReal p).toReal) ^ (1 / (ENNReal.ofReal p).toReal)<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖<VAR>nm_add : ∀ (x y : ι → ℝ), ‖x + y‖ ≤ ‖x‖ + ‖y‖<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), ‖r • x‖ ≤ ‖r‖ * ‖x‖<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>x✝ : ι → ℝ<GOAL>∑ i : ι, |x✝ i| ^ p < 1 ↔ (∑ i : ι, |x✝ i| ^ p) ^ (1 / p) < 1
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>(2 * Gamma (1 / p + 1)) ^ card ι = ∫ (x : ι → ℝ), rexp (-((∑ i : ι, |x i| ^ p) ^ (1 / p)) ^ p)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h₁ : 0 < p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℝ)) / p + 1
<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>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h_indep : iIndepFun m f μ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>(∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y✝ : E<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CharZero 𝕜<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y✝ : E<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CharZero 𝕜<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<VAR>n : ℕ<GOAL>((↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) = (p n) fun x => y
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(factors a).prod ~ᵤ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(Classical.choose ⋯).prod ~ᵤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Monoid α<VAR>inst✝⁴ : Monoid β<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>a b : α<VAR>n : ℕ<GOAL>a ^ n ∣ b → f a ^ n ∣ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Monoid α<VAR>inst✝⁴ : Monoid β<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>a b : α<VAR>n : ℕ<GOAL>a ^ n ∣ b → f (a ^ n) ∣ f b
<VAR>α : Type u<VAR>a : α<VAR>m : Multiset α<GOAL>FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>hμp : Disjoint (f.eigenspace μ) p<GOAL>eigenspace (LinearMap.restrict f hfp) μ = ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>hμp : Disjoint (f.eigenspace μ) p<GOAL>eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>hμp : Disjoint (f.eigenspace μ) p<VAR>x : ↥p<VAR>hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ<GOAL>x ∈ ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s1 s2 : Computation α<VAR>f : α → β<VAR>h1 : s1 ~ s2<GOAL>map f s1 ~ map f s2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s1 s2 : Computation α<VAR>f : α → β<VAR>h1 : s1 ~ s2<GOAL>LiftRel (fun x x_1 => x = x_1) (map f s1) (map f s2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<VAR>g : β ≃ₜ γ<GOAL>f.toContinuousMap.comp f.symm.toContinuousMap = ContinuousMap.id β
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x + y, x + y⟫_𝕜 + re ⟪x - y, x - y⟫_𝕜 = 2 * (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)) = re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜 + (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>a : α<VAR>f : α →₀ M<GOAL>single a (f a) + erase a f = f
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>k : K<VAR>S : List (Γ k)<VAR>n : ℕ<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<GOAL>L.nth n k = S.reverse.get? n
<VAR>K : Type u_1<VAR>Γ : K → Type u_2<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>k : K<VAR>S : List (Γ k)<VAR>n : ℕ<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<GOAL>(Option.map some (S.reverse.get? n)).iget = S.reverse.get? n
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group α<VAR>inst✝ : HasDistribNeg α<VAR>a : α<GOAL>(-a)⁻¹ = -a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f g : α → β<GOAL>(InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∈ sᶜ, s.piecewise f g x ≠ s.piecewise f g y) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f g : α → β<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ sᶜ<GOAL>s.piecewise f g x ≠ s.piecewise f g y ↔ f x ≠ g y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p q : TM<GOAL>p ∈ (chartAt (ModelProd H E) q).source ↔ p.proj ∈ (chartAt H q.proj).source
<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>inst✝ : DecidableEq α<VAR>a : α<VAR>h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1<GOAL>s.prod = a ^ count a s
<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>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : ∀ (a' : α), a' ≠ a → a' ∈ ⟦l⟧ → a' = 1<GOAL>prod ⟦l⟧ = a ^ count a ⟦l⟧
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this : DecidableEq L<GOAL>IsNoetherian A C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<GOAL>IsNoetherian A C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<VAR>b' : Basis { x // x ∈ s } K L := (traceForm K L).dualBasis ⋯ b<GOAL>IsNoetherian A C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this✝ : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<VAR>b' : Basis { x // x ∈ s } K L := (traceForm K L).dualBasis ⋯ b<VAR>this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')<GOAL>IsNoetherian A C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this✝ : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<VAR>b' : Basis { x // x ∈ s } K L := (traceForm K L).dualBasis ⋯ b<VAR>this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')<VAR>f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict<GOAL>IsNoetherian A C
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this✝ : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<VAR>b' : Basis { x // x ∈ s } K L := (traceForm K L).dualBasis ⋯ b<VAR>this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')<VAR>f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict<GOAL>LinearMap.ker f = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsNoetherianRing A<VAR>this✝ : DecidableEq L<VAR>s : Finset L<VAR>b : Basis { x // x ∈ s } K L<VAR>hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (b x)<VAR>b' : Basis { x // x ∈ s } K L := (traceForm K L).dualBasis ⋯ b<VAR>this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')<VAR>f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict<GOAL>LinearMap.ker (↑A (Algebra.linearMap C L)) = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>q : ℚ<GOAL>inducedMap α β ↑q = ↑q