ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t✝ : Finset β<VAR>a : α<VAR>b c : β<VAR>t : Finset α<VAR>hf : Injective f<GOAL>image f s ⊂ image f t ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t✝ : Finset β<VAR>a : α<VAR>b c : β<VAR>t : Finset α<VAR>hf : Injective f<GOAL>image f s < image f t ↔ s < t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>⊥.direction = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(x.1 ∪ e • x.2).card + (x.2 ∩ e⁻¹ • x.1).card = x.1.card + x.2.card
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>((-z₁).comp z₂ h).v p q hpq = (-z₁.comp z₂ h).v p q hpq
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>s : Stream' α<VAR>x✝ : a ∈ s.odd<VAR>n : ℕ<VAR>h : (fun b => a = b) (s.odd.get n)<GOAL>(fun b => a = b) (s.get (2 * n + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<GOAL>findIdx p xs = i ↔ p (xs.get ⟨i, h⟩) = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>x✝ : p (xs.get ⟨i, h⟩) = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>h1 : p (xs.get ⟨i, h⟩) = true<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>findIdx p xs = i
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>x✝ : p (xs.get ⟨i, h⟩) = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>h1 : p (xs.get ⟨i, h⟩) = true<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>findIdx p xs ≤ i
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>x✝ : p (xs.get ⟨i, h⟩) = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>h1 : i < findIdx p xs<GOAL>p (xs.get ⟨i, h⟩) ≠ true
<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>s : Set X<GOAL>IsClosed s ↔ ∀ (x : X), f x ∈ closure (f '' s) → x ∈ s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<VAR>y : E<VAR>hy : y ∈ closure s<GOAL>y ∈ ⇑(homothety x t) '' interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<VAR>y : E<VAR>hy : y ∈ closure s<VAR>hne : t ≠ 0<GOAL>y ∈ ⇑(homothety x t) '' interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<VAR>y : E<VAR>hy : y ∈ closure s<VAR>hne : t ≠ 0<GOAL>(homothety x t⁻¹) y ∈ openSegment ℝ x y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<VAR>y : E<VAR>hy : y ∈ closure s<VAR>hne : t ≠ 0<GOAL>(lineMap x y) t⁻¹ ∈ (fun x_1 => (lineMap x y) x_1⁻¹) '' Ioi 1
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ x : P<GOAL>intrinsicInterior 𝕜 {x} = {x}
<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>inst✝ : FunLike 𝓕 E F<GOAL>‖1‖₊ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<GOAL>(s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂
<VAR>α β : Type u<GOAL>lift.{u, v} 2 = 2
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hvs : Set.InjOn v ↑s<VAR>hx : ∀ i ∈ s, x ≠ v i<VAR>hs : s.Nonempty<GOAL>eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ = 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle x (x - y) = ↑(Real.arccos (‖x‖ / ‖x - y‖))
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<GOAL>qrSign m n = (-1) ^ (m / 2 * (n / 2))
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<GOAL>J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<VAR>h : m % 4 = 1<GOAL>J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<VAR>h : m % 4 = 3<GOAL>J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<GOAL>(coord R M x h) ⟨x, ⋯⟩ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>g : S →+* T<VAR>hmap : ∀ (a : R), g ((algebraMap R S) a) = i a<VAR>hroot : g h.root = x<VAR>a : S<GOAL>g a = (lift i x hx h) a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>g : S →+* T<VAR>hmap : ∀ (a : R), g ((algebraMap R S) a) = i a<VAR>hroot : g h.root = x<VAR>a : S<GOAL>g (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i)) = (lift i x hx h) (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i))
<VAR>z : ℤ<GOAL>sqrt ↑z = ↑(Int.sqrt z)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>(X ^ n).eraseLead = 0
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l✝ : Subspace η α ι<VAR>x✝ : η → α<VAR>i✝ : ι<VAR>a : α<VAR>e : η<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>l : Subspace η α ι<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>x : η' → α'<VAR>i : ι'<GOAL>↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f₁ f₂ : Π₀ (i : ι), β i<VAR>x✝ : ι<GOAL>(erase i (f₁ + f₂)) x✝ = (erase i f₁ + erase i f₂) x✝
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : insert f (B \ {e}) ⊆ B'<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : insert f (B \ {e}) ⊆ B'<VAR>hcard : (B' \ B).encard = (B \ B').encard<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})<VAR>hcard : (B' \ B).encard = (B \ B').encard<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hcard : (B' \ B).encard = (B \ B').encard<VAR>hfB : f ∈ B'<VAR>h : B \ B' = {e}<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hcard : ∃ x, B' \ B = {x}<VAR>hfB : f ∈ B'<VAR>h : B \ B' = {e}<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hfB : f ∈ B'<VAR>h : B \ B' = {e}<VAR>x : α<VAR>hx : B' \ B = {x}<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hfB : f ∈ B'<VAR>h : B \ B' = {e}<VAR>hx : B' \ B = {f}<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hfB : f ∈ B'<VAR>h : B \ B' = {e}<VAR>hx : B' \ B = {f}<GOAL>M.Base B'
<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>r : α → α → Prop<VAR>f : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) f<VAR>h : ∀ (x : ι), DirectedOn r (f x)<GOAL>DirectedOn r (⋃ x, f x)
<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>r : α → α → Prop<VAR>f : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) f<VAR>h : ∀ (x : ι), DirectedOn r (f x)<GOAL>∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x < z \ y<VAR>hyz : y ≤ z<GOAL>x ⊔ y < z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x < z \ y<VAR>hyz : y ≤ z<GOAL>x ⊔ y < z \ y ⊔ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x < z \ y<VAR>hyz : y ≤ z<VAR>h' : z \ y ⊔ y ≤ x ⊔ y<GOAL>z \ y ≤ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x < z \ y<VAR>hyz : y ≤ z<VAR>h' : z \ y ⊔ y ≤ x ⊔ y<GOAL>(z \ y) \ y ≤ x
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<GOAL>s.FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝² : DecidableEq R<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>this : ∀ y ∈ t1, ∃ x ∈ s, f x = y<GOAL>s.FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<GOAL>span R ↑(Finset.image g t1 ∪ t2) = s
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<GOAL>span R (g '' ↑t1) ⊔ span R ↑t2 = s
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<GOAL>span R (g '' ↑t1) ⊔ span R ↑t2 ≤ s
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<GOAL>s ≤ span R (g '' ↑t1) ⊔ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝² : DecidableEq R<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>this : f x ∈ map f s<GOAL>x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝² : DecidableEq R<VAR>this✝¹ : DecidableEq M<VAR>this✝ : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>this : ∃ l ∈ Finsupp.supported R R ↑t1, (Finsupp.total P P R id) l = f x<GOAL>x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>l : P →₀ R<VAR>hl1 : l ∈ Finsupp.supported R R ↑t1<VAR>hl2 : (Finsupp.total P P R id) l = f x<GOAL>x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>l : P →₀ R<VAR>hl1 : l ∈ Finsupp.supported R R ↑t1<VAR>hl2 : (Finsupp.total P P R id) l = f x<GOAL>(Finsupp.total M M R id).toFun ((Finsupp.lmapDomain R R g) l) ∈ span R (g '' ↑t1)
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>l : P →₀ R<VAR>hl1 : l ∈ Finsupp.supported R R ↑t1<VAR>hl2 : (Finsupp.total P P R id) l = f x<GOAL>x - (Finsupp.total M M R id) ((Finsupp.lmapDomain R R g) l) ∈ span R ↑t2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>P : Type u_6<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>s : Submodule R M<VAR>this✝¹ : DecidableEq R<VAR>this✝ : DecidableEq M<VAR>this : DecidableEq P<VAR>t1 : Finset P<VAR>ht1 : span R ↑t1 = map f s<VAR>t2 : Finset M<VAR>ht2 : span R ↑t2 = s ⊓ LinearMap.ker f<VAR>g : P → M<VAR>hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y<VAR>x : M<VAR>hx : x ∈ s<VAR>l : P →₀ R<VAR>hl1 : l ∈ Finsupp.supported R R ↑t1<VAR>hl2 : (Finsupp.total P P R id) l = f x<GOAL>x - (Finsupp.total M M R id) ((Finsupp.lmapDomain R R g) l) ∈ s ∧ x - (Finsupp.total M M R id) ((Finsupp.lmapDomain R R g) l) ∈ LinearMap.ker f
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>∅.centerMass w z = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>x✝ : ↑(range f)<GOAL>(f ∘ rangeSplitting f) x✝ = ↑x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>x✝ : ↑(range f)<GOAL>f (rangeSplitting f x✝) = ↑x✝
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (a * b⁻¹) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<VAR>this : f a * (f b)⁻¹ = 1<GOAL>f (a * b⁻¹) = 1
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>n : ℕ<GOAL>IsOpen {f | ↑n ≤ (↑f).rank}