ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>x : X<VAR>h : range f ∈ 𝓝 (f x)<GOAL>ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>c d : ℕ → ℝ<VAR>ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>c d : ℕ → ℝ<VAR>ss : Icc a b ⊆ ⋃ i, Ioo (c i) (d i)<GOAL>∀ (s : Finset ℕ) (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<VAR>ab : b ≤ a<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<VAR>ab : a ≤ b<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<VAR>ab : a ≤ b<VAR>this : b ∈ ⋃ i ∈ ↑s, Ioo (c i) (d i)<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<VAR>ab : a ≤ b<VAR>this : ∃ i, c i < b ∧ i ∈ s ∧ b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>cv : Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (c i) (d i)<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cv : Icc a b ⊆ ⋃ i_1 ∈ ↑(insert i (s.erase i)), Ioo (c i_1) (d i_1)<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ insert i (s.erase i), ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ∑ i ∈ insert i (s.erase i), ofReal (↑f (d i) - ↑f (c i))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ofReal (↑f (c i) - ↑f a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>c d : ℕ → ℝ<VAR>s✝ s : Finset ℕ<VAR>IH : ∀ t ⊂ s, ∀ (b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))<VAR>b : ℝ<VAR>ab : a ≤ b<VAR>i : ℕ<VAR>cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (c x) (d x)<VAR>cb : c i < b<VAR>is : i ∈ s<VAR>bd : b < d i<GOAL>Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Ioo (c i_1) (d i_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ∃ u, Monotone u ∧ Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>g : ℕ → ℝ≥0∞<VAR>h✝ : Monotone g<VAR>hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ<VAR>hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n<VAR>ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>g : ℕ → ℝ≥0∞<VAR>h✝ : Monotone g<VAR>hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ<VAR>hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n<VAR>ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν<VAR>hξm : Measurable ξ<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>g : ℕ → ℝ≥0∞<VAR>h✝ : Monotone g<VAR>hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ<VAR>hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n<VAR>ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν<VAR>hξm : Measurable ξ<VAR>μ₁ : Measure α := μ - ν.withDensity ξ<VAR>hμ₁ : μ₁ = μ - ν.withDensity ξ<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>g : ℕ → ℝ≥0∞<VAR>h✝ : Monotone g<VAR>hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ<VAR>hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n<VAR>ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν<VAR>hξm : Measurable ξ<VAR>μ₁ : Measure α := μ - ν.withDensity ξ<VAR>hμ₁ : μ₁ = μ - ν.withDensity ξ<VAR>hle : ν.withDensity ξ ≤ μ<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>g : ℕ → ℝ≥0∞<VAR>h✝ : Monotone g<VAR>hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ<VAR>hf₂ : ∀ (n : ℕ), (fun f => ∫⁻ (x : α), f x ∂ν) (f n) = g n<VAR>ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k<VAR>hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν<VAR>hξm : Measurable ξ<VAR>μ₁ : Measure α := μ - ν.withDensity ξ<VAR>hμ₁ : μ₁ = μ - ν.withDensity ξ<VAR>hle : ν.withDensity ξ ≤ μ<VAR>this : IsFiniteMeasure (ν.withDensity ξ)<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l✝ : Filter α<VAR>f : α → β<VAR>l : Filter β<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : Tendsto f cofinite l<GOAL>(f ⁻¹' l.ker)ᶜ.Countable
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l✝ : Filter α<VAR>f : α → β<VAR>l : Filter β<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : Tendsto f cofinite l<GOAL>(comap f l).kerᶜ.Countable
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<GOAL>∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<VAR>N : ℕ<VAR>hN : N ≥ N₀<VAR>p : ℕ<VAR>hp : p ∈ N₀.primesBelow<GOAL>p ∈ range N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a : α<VAR>has : a ∉ s<GOAL>(insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>(llcomp R M N M).compr₂ (trace R M) = (llcomp R N M N).flip.compr₂ (trace R N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N) = ((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>g : Module.Dual R N<VAR>m : M<VAR>f : Module.Dual R M<VAR>n : N<GOAL>((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N))) g) m)) f) n = ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N))) g) m)) f) n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>disj : b ∉ map f K<GOAL>∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>disj : ∀ (y : F), (adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ<GOAL>b ∈ map f K
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<GOAL>(algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<GOAL>mk' K (num A x) (den A x) = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : WellFounded (rι on f)<VAR>hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<GOAL>WellFounded (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : WellFounded (rι on f)<VAR>hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<VAR>c c' : γ<VAR>h : (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩) c c'<GOAL>((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : WellFounded (rι on f)<VAR>hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<VAR>c c' : γ<VAR>h : (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩) c c'<VAR>h' : rι ((fun c => ⟨f c, g (f c) c⟩) c).fst ((fun c => ⟨f c, g (f c) c⟩) c').fst<GOAL>((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : WellFounded (rι on f)<VAR>hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<VAR>c c' : γ<VAR>h : (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩) c c'<VAR>h' : ((fun c => ⟨f c, g (f c) c⟩) c).fst = ((fun c => ⟨f c, g (f c) c⟩) c').fst<VAR>h'' : rπ ((fun c => ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c => ⟨f c, g (f c) c⟩) c).snd) ((fun c => ⟨f c, g (f c) c⟩) c').snd<GOAL>((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c => ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩) c c'
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommMonoid R✝<VAR>R' : Type u_2<VAR>inst✝² : CommMonoidWithZero R'<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>χ : MulChar R R'<GOAL>χ ↑(ringChar R) = 0
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<GOAL>∃ h, Continuous h ∧ f ∘ h = φ