ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' x✝ : List α<GOAL>(permutationsAux2 t (is ++ ts) [] x✝ id).2 = (permutationsAux2 t is [] x✝ fun x => x ++ ts).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' x✝ : List α<GOAL>(permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).2 = (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).2
<VAR>p : ℕ+<VAR>pp : p.Prime<VAR>contra : p = 1<GOAL>False
<VAR>p : ℕ+<VAR>pp : p.Prime<VAR>contra : p = 1<GOAL>↑p = 1
<VAR>p : ℕ+<VAR>pp : p.Prime<VAR>contra : p = 1<GOAL>p = 1
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.75509, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>n : ℕ<GOAL>((Γ₀.splitting K).ι n ≫ (Γ₀.splitting K).desc (op [n]) fun A => f.f (unop A.fst).len ≫ ((Γ₀.splitting K').cofan (op [n])).inj A) = f.f n ≫ (Γ₀.splitting K').ι n
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.75509, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K'✝ : ChainComplex C ℕ<VAR>f✝ : K✝ ⟶ K'✝<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>n : ℕ<GOAL>f.f (unop (Splitting.IndexSet.id (op [n])).fst).len ≫ ((Γ₀.splitting K').cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) = f.f n ≫ ((Γ₀.splitting K').cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : Semiring R<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>B₁ : Matrix n₁ n R<VAR>B₂ : Matrix n₂ n R<VAR>i✝ : m<VAR>j✝ : n<GOAL>(A₁.fromColumns A₂ * B₁.fromRows B₂) i✝ j✝ = (A₁ * B₁ + A₂ * B₂) i✝ j✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → Opens ↑X<VAR>F : Presheaf C X<VAR>F' : Sheaf C X<VAR>h : Opens.IsBasis (Set.range B)<VAR>α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val<VAR>i : ι<GOAL>((restrictHomEquivHom F F' h) α).app (op (B i)) = α.app (op i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → Opens ↑X<VAR>F : Presheaf C X<VAR>F' : Sheaf C X<VAR>h : Opens.IsBasis (Set.range B)<VAR>α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val<VAR>i : ι<GOAL>((restrictHomEquivHom F F' h) α).app (op (B i)) = ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<VAR>rx : IsRightRegular x<GOAL>(f * single x r).support = image (fun x_1 => x_1 * x) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<VAR>rx : IsRightRegular x<VAR>y : G<VAR>hy : y ∈ image (fun x_1 => x_1 * x) f.support<GOAL>y ∈ (f * single x r).support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<VAR>rx : IsRightRegular x<VAR>y : G<VAR>yf : y ∈ f.support<VAR>hy : y * x ∈ image (fun x_1 => x_1 * x) f.support<GOAL>y * x ∈ (f * single x r).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<GOAL>m0 ≤ ⊤.caratheodory
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<GOAL>m0 ≤ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h : a ⋖ b<GOAL>Ioi a = Ici b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : 0 < l.length<GOAL>maximum_of_length_pos h ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : 0 < l.length<GOAL>l.maximum = ↑(maximum_of_length_pos h)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<GOAL>μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>R : ℝ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hf' : ∀ x ∈ ∅, HasFDerivWithinAt f (f' x) ∅ x<VAR>hs : ∅ ⊆ closedBall 0 R<VAR>h'f' : ∀ x ∈ ∅, (f' x).det = 0<GOAL>μ (f '' ∅) ≤ ↑ε * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>h's : s.Nonempty<GOAL>μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>h's : s.Nonempty<VAR>this : ∀ (A : E →L[ℝ] E), ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t<GOAL>μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>h's : s.Nonempty<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t<GOAL>μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<VAR>h's : s.Nonempty<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))<VAR>Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<GOAL>μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)
<VAR>x y : ℝ<VAR>f : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)<GOAL>x ≤ mk f
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<GOAL>mk x ≤ mk f
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<GOAL>¬mk f < mk x
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<GOAL>¬f < x
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<GOAL>False
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<VAR>i : ℕ<VAR>H : ∀ j ≥ i, mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2<GOAL>False
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<VAR>i : ℕ<VAR>H : ∀ j ≥ i, mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2<GOAL>↑(↑f i) < mk x
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<VAR>i : ℕ<VAR>H : ∀ j ≥ i, mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2<GOAL>const abs ↑(↑f i) < x
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<VAR>i : ℕ<VAR>H : ∀ j ≥ i, mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>K / 2 ≤ ↑(x - const abs ↑(↑f i)) j
<VAR>x✝ y : ℝ<VAR>f x : CauSeq ℚ abs<VAR>h : ∃ i, ∀ j ≥ i, mk x ≤ ↑(↑f j)<VAR>K : ℚ<VAR>K0 : K > 0<VAR>hK : ∃ i, ∀ j ≥ i, K ≤ ↑(x - f) j<VAR>i : ℕ<VAR>H : ∀ j ≥ i, mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>this : K + -(K / 2) ≤ ↑(x - f) j + (↑f j - ↑f i)<GOAL>K / 2 ≤ ↑(x - const abs ↑(↑f i)) j
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>σ : Perm n<VAR>inst✝ : CommRing R<GOAL>(Perm.permMatrix R σ).det = ↑↑(Perm.sign σ)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : o → Matrix m n α<VAR>i✝ : n × o<VAR>j✝ : m × o<GOAL>(blockDiagonal M)ᵀ i✝ j✝ = blockDiagonal (fun k => (M k)ᵀ) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : o → Matrix m n α<VAR>i✝ : n × o<VAR>j✝ : m × o<GOAL>(if i✝.2 = j✝.2 then M i✝.2 j✝.1 i✝.1 else 0) = if i✝.2 = j✝.2 then M j✝.2 j✝.1 i✝.1 else 0
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>r : R<VAR>u : U<VAR>x✝¹ : Γ'<VAR>x✝ : Γ<GOAL>((A.compHahnSeries B (r • u)).coeff x✝¹).coeff x✝ = ((r • A.compHahnSeries B u).coeff x✝¹).coeff x✝
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>r : R<VAR>u : U<VAR>x✝¹ : Γ'<VAR>x✝ : Γ<GOAL>(r • A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ = r • (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>p.content = gcd p.leadingCoeff p.eraseLead.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : p.natDegree ∈ p.support<GOAL>p.content = gcd p.leadingCoeff p.eraseLead.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : p.natDegree ∈ p.support<GOAL>gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) = gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : p.natDegree ∈ p.support<VAR>i : ℕ<VAR>hi : i ∈ p.support.erase p.natDegree<GOAL>p.coeff i = p.eraseLead.coeff i
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : p.natDegree ∈ p.support<VAR>i : ℕ<VAR>hi : i ≠ p.natDegree ∧ i ∈ p.support<GOAL>p.coeff i = p.eraseLead.coeff i
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝²⁶ : CommRing A<VAR>inst✝²⁵ : CommRing B<VAR>inst✝²⁴ : Algebra A B<VAR>inst✝²³ : Field K<VAR>inst✝²² : Field L<VAR>inst✝²¹ : Algebra A K<VAR>inst✝²⁰ : IsFractionRing A K<VAR>inst✝¹⁹ : Algebra B L<VAR>inst✝¹⁸ : Algebra K L<VAR>inst✝¹⁷ : Algebra A L<VAR>inst✝¹⁶ : IsScalarTower A B L<VAR>inst✝¹⁵ : IsScalarTower A K L<VAR>inst✝¹⁴ : IsIntegralClosure B A L<VAR>inst✝¹³ : FiniteDimensional K L<VAR>Aₘ : Type ?u.446485<VAR>Bₘ : Type ?u.446488<VAR>inst✝¹² : CommRing Aₘ<VAR>inst✝¹¹ : CommRing Bₘ<VAR>inst✝¹⁰ : Algebra Aₘ Bₘ<VAR>inst✝⁹ : Algebra A Aₘ<VAR>inst✝⁸ : Algebra B Bₘ<VAR>inst✝⁷ : Algebra A Bₘ<VAR>inst✝⁶ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁵ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁴ : IsLocalization M Aₘ<VAR>inst✝³ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝² inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : B<GOAL>(algebraMap A K) (IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x)) ⋯) = (norm K) ((algebraMap B L) x)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝¹⁰ : NontriviallyNormedField R<VAR>inst✝⁹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁸ : (x : B) → Module R (E x)<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace R F<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (x : B) → TopologicalSpace (E x)<VAR>inst✝² : FiberBundle F E<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>((continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯)) v = (coordChangeL R e e' b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝¹⁰ : NontriviallyNormedField R<VAR>inst✝⁹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁸ : (x : B) → Module R (E x)<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace R F<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (x : B) → TopologicalSpace (E x)<VAR>inst✝² : FiberBundle F E<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>((continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯)) v = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<GOAL>Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>aux : {0}ᶜ ∈ 𝓝 μ.mass<GOAL>Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>aux : {0}ᶜ ∈ 𝓝 μ.mass<VAR>eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0<GOAL>Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>aux : {0}ᶜ ∈ 𝓝 μ.mass<VAR>eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0<VAR>eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f<GOAL>Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>aux : {0}ᶜ ∈ 𝓝 μ.mass<VAR>eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0<VAR>eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f<GOAL>Tendsto (fun x => (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<VAR>lim_mass : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>aux : {0}ᶜ ∈ 𝓝 μ.mass<VAR>eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0<VAR>eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f<VAR>lim_pair : Tendsto (fun i => ((μs i).mass⁻¹, (μs i).testAgainstNN f)) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f))<GOAL>Tendsto (fun x => (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.mass⁻¹ * μ.testAgainstNN f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>fold (fun x x_1 => x ∪ x_1) ∅ singleton ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s<GOAL>fold (fun x x_1 => x ∪ x_1) ∅ singleton (insert a s) = insert a s
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖ = univ.sup' ⋯ fun w => (normAtPlace w) x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>univ.sup' ⋯ (Subtype.val ∘ fun w => ⟨(normAtPlace w) x, ⋯⟩) = univ.sup' ⋯ fun w => (normAtPlace w) x
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<VAR>h : a • x ∈ a • S<GOAL>x ∈ S
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs₁ : BddAbove s<VAR>hs₂ : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs₁ : BddAbove s<VAR>hs₂ : s.Nonempty<VAR>p : Seminorm 𝕜 E<VAR>hp : p ∈ s<VAR>x : E<VAR>this : Nonempty ↑s<GOAL>p x ≤ ⨆ i, ↑i x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs₁ : BddAbove s<VAR>hs₂ : s.Nonempty<VAR>p : Seminorm 𝕜 E<VAR>hp : p ∈ upperBounds s<VAR>x : E<VAR>this : Nonempty ↑s<GOAL>⨆ i, ↑i x ≤ p x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>x y : α<VAR>l : List α<VAR>xl : ¬x ∈ l<VAR>yl : ¬y ∈ l<GOAL>List.insert x (y :: l) ~ List.insert y (x :: l)