ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>w✝¹ : Submodule R M<VAR>N' : Submodule R N<VAR>w✝ : w✝¹ ≤ M₁<VAR>hN : N' ≤ N₁<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (map (inclusion w✝) (inclusion hN)))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>w✝¹ : Submodule R M<VAR>N' : Submodule R N<VAR>w✝ : w✝¹ ≤ M₁<VAR>hN : N' ≤ N₁<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w✝)))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN)))
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x : R<VAR>I J : Ideal R<GOAL>span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x : R<VAR>I J : Ideal R<GOAL>(∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J) ↔ ∀ z ∈ I, x * z ∈ J
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G), g • B = B ∨ Disjoint (g • B) B) → IsBlock G B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G), g • B = B ∨ Disjoint (g • B) B) → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B<VAR>g g' : G<GOAL>g • B = g' • B ∨ Disjoint (g • B) (g' • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B<VAR>g g' : G<GOAL>(g'⁻¹ * g) • B = B → g • B = g' • B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B<VAR>g g' : G<GOAL>Disjoint ((g'⁻¹ * g) • B) B → Disjoint (g • B) (g' • B)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>l₁ l₂ : List α<VAR>this : ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y<GOAL>Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>l₁ l₂ : List α<VAR>this : ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y<GOAL>(Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>f✝ : X✝ ⟶ Y<VAR>inst✝¹ : HasImage f✝<VAR>A B : C<VAR>X : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : HasImage f<VAR>h : A ⟶ underlying.obj X<VAR>w : h ≫ X.arrow = f<GOAL>((imageSubobjectIso f).hom ≫ image.lift (MonoFactorisation.mk (underlying.obj X) X.arrow h ⋯)) ≫ X.arrow = (imageSubobject f).arrow
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp ppred pred : Pair K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_conts_eq : g.conts n = ppred<VAR>succ_nth_conts_eq : g.conts (n + 1) = pred<GOAL>g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp ppred pred : Pair K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_conts_eq : g.contsAux (n + 1) = ppred<VAR>succ_nth_conts_eq : g.contsAux (n + 1 + 1) = pred<GOAL>g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D
<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>ι : Type u_4<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>X : Type u_1<VAR>k : ℤ<VAR>h : k ≠ 0<VAR>a : FreeAbelianGroup X<VAR>x : X<GOAL>x ∈ (k • a).support ↔ x ∈ a.support
<VAR>X : Type u_1<VAR>k : ℤ<VAR>h : k ≠ 0<VAR>a : FreeAbelianGroup X<VAR>x : X<GOAL>k • (coeff x) a ≠ 0 ↔ (coeff x) a ≠ 0
<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✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I J : Ideal A<VAR>x✝ : DvdNotUnit I J<VAR>hI : I ≠ 0<VAR>H : Ideal A<VAR>hunit : ¬IsUnit H<VAR>hmul : J = I * H<VAR>h : J = I<GOAL>I * H = I * 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>eq : cs.length (w * cs.simple i) = cs.length w<GOAL>False
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>eq : cs.length (w * cs.simple i) = cs.length w<VAR>length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2<GOAL>False
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>eq : cs.length (w * cs.simple i) = cs.length w<VAR>length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2<GOAL>False
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>eq : cs.length (w * cs.simple i) = cs.length w<VAR>length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2<VAR>even : cs.length w % 2 = 0<GOAL>False
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>eq : cs.length (w * cs.simple i) = cs.length w<VAR>length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2<VAR>odd : cs.length w % 2 = 1<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictAntiOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictAntiOn f s
<VAR>x x' y y' : ZFSet<VAR>H : x.pair y = x'.pair y'<GOAL>x = x' ∧ y = y'
<VAR>x x' y y' : ZFSet<VAR>H : x.pair y = x'.pair y'<VAR>ae : ∀ (z : ZFSet), z ∈ x.pair y ↔ z ∈ x'.pair y'<GOAL>x = x' ∧ y = y'
<VAR>x x' y y' : ZFSet<VAR>H : x.pair y = x'.pair y'<VAR>ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}<GOAL>x = x' ∧ y = y'
<VAR>x y y' : ZFSet<VAR>H : x.pair y = x.pair y'<VAR>ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}<VAR>he : x = y → y = y'<GOAL>x = x ∧ y = y'
<VAR>x y y' : ZFSet<VAR>H : x.pair y = x.pair y'<VAR>ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}<VAR>he : x = y → y = y'<VAR>xyx : {x, y} = {x}<GOAL>x = x ∧ y = y'
<VAR>x y y' : ZFSet<VAR>H : x.pair y = x.pair y'<VAR>ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}<VAR>he : x = y → y = y'<VAR>xyy' : {x, y} = {x, y'}<GOAL>x = x ∧ y = y'
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<GOAL>p x fun n => aeSeq hf p n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<GOAL>p x fun n => AEMeasurable.mk (f n) ⋯ x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<GOAL>p x fun n => f n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}<GOAL>p x fun n => f n x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}<VAR>hx' : x ∈ {x | p x fun n => f n x}<GOAL>p x fun n => f n x
<VAR>p x ε : ℝ<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε
<VAR>x ε : ℝ<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • 0) ε
<VAR>p x ε : ℝ<VAR>hp : p ≠ 0<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε
<VAR>p x ε : ℝ<VAR>hp : p ≠ 0<VAR>y : ℝ<GOAL>y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ z, closedBall (x + z • p) ε
<VAR>p x ε : ℝ<VAR>hp : p ≠ 0<VAR>y : ℝ<GOAL>|y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε ↔ ∃ i, |y - x - ↑i * p| ≤ ε
<VAR>p x ε : ℝ<VAR>hp : p ≠ 0<VAR>y : ℝ<VAR>n : ℤ<VAR>hn : |y - x - ↑n * p| ≤ ε<GOAL>|y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε
<VAR>p x ε : ℝ<VAR>hp : p ≠ 0<VAR>y : ℝ<VAR>n : ℤ<VAR>hn : |p⁻¹ * (y - x) - ↑n| ≤ |p⁻¹| * ε<GOAL>|p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))| ≤ |p⁻¹| * ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : β → γ<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>f '' s.seq t = ((fun x => f ∘ x) '' s).seq t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : Multiset α<VAR>xs : List α<GOAL>(map f ⟦xs⟧).sym2 = map (Sym2.map f) (Multiset.sym2 ⟦xs⟧)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k✝ n✝ k n : ℕ<VAR>hkn : k ≤ n<GOAL>addRothNumber (Iio ↑k) ≤ rothNumberNat k
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k✝ n✝ k n : ℕ<VAR>hkn : k ≤ n<GOAL>Set.BijOn Nat.cast ↑(range k) ↑(Iio ↑k)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k✝ n✝ k n : ℕ<VAR>hkn : k ≤ n<GOAL>Set.MapsTo Nat.cast ↑(range k) ↑(Iio ↑k)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k✝ n✝ k n : ℕ<VAR>hkn : k ≤ n<GOAL>Set.SurjOn Nat.cast ↑(range k) ↑(Iio ↑k)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k✝ n✝ k n : ℕ<VAR>hkn : k ≤ n<GOAL>∀ (x : Fin n.succ), ↑x < k → ∃ x_1 < k, ↑x_1 = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x y : M × R<VAR>f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q := ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂ (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)<GOAL>((even.lift (Q' Q)) { bilin := f, contract := ⋯, contract_mid := ⋯ }) (((even.ι (Q' Q)).bilin x) y) = ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>x : α<VAR>hxB' : x ∈ B'<VAR>hx : x ∉ I<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>x : α<VAR>hxB' : x ∈ B'<VAR>hx : x ∉ I<VAR>hxB : x ∉ B<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e✝ f : α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>x : α<VAR>hxB' : x ∈ B'<VAR>hx : x ∉ I<VAR>hxB : x ∉ B<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hBase : M.Base (insert e (B' \ {x}))<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<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>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2 = s.radius
<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>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) = ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • (o.rotation ↑(π / 2)) (midpoint ℝ 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>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>p_monic : p.Monic<VAR>p_1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>p_monic : p.Monic<VAR>p_1 : p ≠ 1<GOAL>(∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>Hnext : ∀ (n : ℕ), Injective next<GOAL>Injective (leRecOn hnm fun {k} => next)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>x : G × N<GOAL>x ∈ K.prod ⊤ ↔ x ∈ comap (MonoidHom.fst G N) K
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.extend (min 0 0) = a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.truncate 0 0 = (refl a).cast ⋯ ⋯
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>map (fun x => x.1 * x.2) (μ.prod (dirac 1)) = μ
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>map ((fun x => x.1 * x.2) ∘ fun x => (x, 1)) μ = μ
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>Measurable fun x => (x, 1)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>n : ℕ<GOAL>n • {a} = replicate n a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>inhabited_h : Inhabited α<GOAL>∃ f, StrictMono f
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → α<VAR>hf : StrictMono f<VAR>hf₀ : f 0 = default<GOAL>∃ f, StrictMono f
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → α<VAR>hf : StrictMono f<VAR>hf₀ : f 0 = default<VAR>g : ℕ → α<VAR>hg : StrictAnti g<VAR>hg₀ : g 0 = default<GOAL>∃ f, StrictMono f
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → α<VAR>hf : StrictMono f<VAR>hf₀ : f 0 = default<VAR>g : ℕ → α<VAR>hg : StrictAnti g<VAR>hg₀ : g 0 = default<GOAL>∀ (n : ℤ), (Int.casesOn n f fun n => g (n + 1)) < Int.casesOn (n + 1) f fun n => g (n + 1)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 (‖Polynomial.eval a (Polynomial.derivative F)‖ * 0))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>(taylor r) 1 = C 1
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>m : M<GOAL>‖inr m‖ = ‖m‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>h : MDifferentiableAt I I' f p.proj<GOAL>tangentMapWithin I I' f s p = tangentMap I I' f p
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>h : MDifferentiableWithinAt I I' f univ p.proj<GOAL>tangentMapWithin I I' f s p = tangentMap I I' f p
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>h : MDifferentiableWithinAt I I' f univ p.proj<GOAL>tangentMapWithin I I' f s p = tangentMapWithin I I' f univ p
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>z : E<VAR>hs : Convex ℝ s<GOAL>ConvexOn ℝ s fun z' => dist z' z
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>0 ≤ log ↑n