ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<VAR>y : K<VAR>mem_J : y ∈ J<VAR>not_mem_zero : y ∉ 0<VAR>y' : R₁<VAR>hy' : (algebraMap R₁ K) y' = aJ • y<GOAL>IsFractional R₁⁰ (I / J)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<VAR>y : K<VAR>mem_J : y ∈ J<VAR>not_mem_zero : y ∉ 0<VAR>y' : R₁<VAR>hy' : (algebraMap R₁ K) y' = aJ • y<GOAL>aI * y' ∈ R₁⁰ ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<VAR>y : K<VAR>mem_J : y ∈ J<VAR>not_mem_zero : y ∉ 0<VAR>y' : R₁<VAR>hy' : (algebraMap R₁ K) y' = aJ • y<VAR>b : K<VAR>hb : b ∈ I / J<GOAL>IsInteger R₁ ((aI * y') • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<VAR>y : K<VAR>mem_J : y ∈ J<VAR>not_mem_zero : y ∉ 0<VAR>y' : R₁<VAR>hy' : (algebraMap R₁ K) y' = aJ • y<VAR>b : K<VAR>hb : b ∈ I / J<GOAL>(aI * y') • b = aI • (b * aJ • y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a b : M₂<GOAL>(fun v => m fun i => v (σ i)) (update v i (a + b)) = (fun v => m fun i => v (σ i)) (update v i a) + (fun v => m fun i => v (σ i)) (update v i b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a b : M₂<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(fun v => m fun i => v (σ i)) (update v i (a + b)) = (fun v => m fun i => v (σ i)) (update v i a) + (fun v => m fun i => v (σ i)) (update v i b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a b : M₂<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(m fun i_1 => update (v ∘ ⇑σ) (σ.symm i) (a + b) i_1) = (m fun i_1 => update (v ∘ ⇑σ) (σ.symm i) a i_1) + m fun i_1 => update (v ∘ ⇑σ) (σ.symm i) b i_1
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a : R<VAR>b : M₂<GOAL>(fun v => m fun i => v (σ i)) (update v i (a • b)) = a • (fun v => m fun i => v (σ i)) (update v i b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a : R<VAR>b : M₂<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(fun v => m fun i => v (σ i)) (update v i (a • b)) = a • (fun v => m fun i => v (σ i)) (update v i b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>inst✝ : DecidableEq ι₂<VAR>v : ι₂ → M₂<VAR>i : ι₂<VAR>a : R<VAR>b : M₂<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(m fun i_1 => update (v ∘ ⇑σ) (σ.symm i) (a • b) i_1) = a • m fun i_1 => update (v ∘ ⇑σ) (σ.symm i) b i_1
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<GOAL>stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : SigmaFinite (μ.trim ⋯)<GOAL>stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this✝ : SigmaFinite (μ.trim ⋯)<VAR>this : μ[stoppedValue f τ|hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n|hτ.measurableSpace]|hσ.measurableSpace]<GOAL>stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this✝ : SigmaFinite (μ.trim ⋯)<VAR>this : μ[stoppedValue f τ|hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n|hτ.measurableSpace]|hσ.measurableSpace]<GOAL>stoppedValue f σ =ᶠ[ae μ] μ[f n|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this✝ : SigmaFinite (μ.trim ⋯)<VAR>this : μ[stoppedValue f τ|hσ.measurableSpace] =ᶠ[ae μ] μ[μ[f n|hτ.measurableSpace]|hσ.measurableSpace]<GOAL>hσ.measurableSpace ≤ hτ.measurableSpace
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>‖a / b‖ ≤ ‖a‖ + ‖b‖
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a.natAbs = b.natAbs ↔ a = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p q : A[X]<GOAL>invFun R A (p + q) = invFun R A p + invFun R A q
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F.leftOp<VAR>hc : IsLimit c<VAR>s : Cocone F<VAR>j : J<GOAL>((coconeOfConeLeftOp c).ι.app j ≫ (fun s => (hc.lift (coneLeftOpOfCocone s)).op) s).unop = (s.ι.app j).unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F.leftOp<VAR>hc : IsLimit c<VAR>s : Cocone F<VAR>m : (coconeOfConeLeftOp c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => (hc.lift (coneLeftOpOfCocone s)).op) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cone F.leftOp<VAR>hc : IsLimit c<VAR>s : Cocone F<VAR>m : (coconeOfConeLeftOp c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j<VAR>j : Jᵒᵖ<GOAL>(m.unop ≫ c.π.app j).op = (((fun s => (hc.lift (coneLeftOpOfCocone s)).op) s).unop ≫ c.π.app j).op
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : MapsTo g s f'.source<GOAL>ContinuousOn (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) ↔ ContinuousOn g s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : MapsTo g s f'.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) (↑(f.extend I) x) ↔ ContinuousWithinAt g s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : MapsTo g s f'.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>𝓝[↑(f.extend I) '' s] ↑(f.extend I) x = 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : MapsTo g s f'.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ f.source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : MapsTo g s f'.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>s ⊆ f.source
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>e.functor.map (e.unit.app X) = e.counitInv.app (e.functor.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : NonUnitalNonAssocSemiring A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R A A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : Module R B<VAR>inst✝² : IsScalarTower R B B<VAR>inst✝¹ : SMulCommClass R B B<VAR>S : NonUnitalSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ iSup K<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ ((inclusion h) x) = (f i) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : NonUnitalNonAssocSemiring A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R A A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : Module R B<VAR>inst✝² : IsScalarTower R B B<VAR>inst✝¹ : SMulCommClass R B B<VAR>S : NonUnitalSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ iSup K<GOAL>↑(K i) ⊆ ↑(iSup K)
<VAR>M : Type u_1<VAR>inst✝ : CommGroup M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : L<VAR>φ₁ φ₂ : R<VAR>h : φ₁ ≠ φ₂<GOAL>Disjoint (weightSpaceOf M φ₁ x) (weightSpaceOf M φ₂ x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : L<VAR>φ₁ φ₂ : R<VAR>h : φ₁ ≠ φ₂<GOAL>Disjoint ↑(weightSpaceOf M φ₁ x) ↑(weightSpaceOf M φ₂ x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>SigmaFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal<GOAL>SigmaFinite (μ.withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0∞<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal<GOAL>SigmaFinite (μ.withDensity fun x => ↑(f x).toNNReal)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<GOAL>Injective ⇑(base φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>d : Transversal φ<GOAL>Injective ⇑(base φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>d : Transversal φ<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)<VAR>a₁✝ a₂✝ : H<VAR>h : ((fun x x_1 => x • x_1) ∘ ⇑(base φ)) a₁✝ = ((fun x x_1 => x • x_1) ∘ ⇑(base φ)) a₂✝<GOAL>a₁✝ = a₂✝
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasLimit F<VAR>x y : limit F<VAR>w : ∀ (j : J), limit.π F j x = limit.π F j y<GOAL>x = y
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasLimit F<VAR>x y : limit F<VAR>w : ∀ (j : J), limit.π F j x = limit.π F j y<GOAL>(limitEquivSections F) x = (limitEquivSections F) y
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ p₅ p₆ : P<VAR>h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}<VAR>h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ 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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ p₅ p₆ : P<VAR>h₁₂₄₅ : Submodule.span ℝ {p₁ -ᵥ p₂} = Submodule.span ℝ {p₄ -ᵥ p₅}<VAR>h₃₂₆₅ : Submodule.span ℝ {p₃ -ᵥ p₂} = Submodule.span ℝ {p₆ -ᵥ p₅}<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>G.map (F.map (f✝ ≫ g✝)) = G.map (F.map f✝) ≫ G.map (F.map g✝)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f✝ : ι →₀ α<VAR>f : ι →₀ Finset α<GOAL>f.pi.card = f.prod fun i => ↑(f i).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f✝ : ι →₀ α<VAR>f : ι →₀ Finset α<GOAL>∏ i ∈ f.support, (f i).card = f.prod fun i => ↑(f i).card
<VAR>R : Type uR<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>x✝ : Dual R M₂<GOAL>x✝ ∈ ker f.dualMap ↔ x✝ ∈ (range f).dualAnnihilator