ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>2 ∣ x ^ 2 ^ (multiplicity 2 (n + 1)).get h - y ^ 2 ^ (multiplicity 2 (n + 1)).get h
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>¬2 ∣ x ^ 2 ^ (multiplicity 2 (n + 1)).get h
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>¬2 ∣ ↑k
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>¬2 ∣ k
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<VAR>hpn : 2 ∣ k<GOAL>2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<VAR>hpn : 2 ∣ k<GOAL>2 ^ (multiplicity 2 (n + 1)).get h * 2 ∣ n + 1
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<VAR>hpn : 2 ∣ k<GOAL>2 ^ (multiplicity 2 (n + 1)).get h * 2 ∣ 2 ^ (multiplicity 2 (n + 1)).get h * k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>MapsTo.restrict f (f ⁻¹' t) t ⋯ '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y Z : C<VAR>f : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M✝ : Type u_4<VAR>M : Type u<VAR>inst✝ : RightCancelMonoid M<VAR>a b : M<GOAL>a * b = b ↔ a * b = 1 * b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>LinearMap.range ↑b.repr = Finsupp.supported R R univ
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>firstDiff x y = firstDiff y x
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>γ : Type u_3<VAR>inst✝ : Monoid γ<VAR>f : M → γ<VAR>hf : IsMonoidHom f<GOAL>IsSubmonoid (Set.range f)
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>γ : Type u_3<VAR>inst✝ : Monoid γ<VAR>f : M → γ<VAR>hf : IsMonoidHom f<GOAL>IsSubmonoid (f '' Set.univ)
<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>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>(⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f i<VAR>i✝ : I<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : One γ<VAR>i : α<VAR>c : γ<GOAL>Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<GOAL>f.inverse.domain = LinearMap.range f.toFun
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<GOAL>Submodule.map (LinearMap.fst R F E) (Submodule.map (LinearEquiv.prodComm R E F) f.graph) = Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph)
<VAR>G : Type u<VAR>F : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝³ : Monoid M₁<VAR>inst✝² : Monoid M₂<VAR>inst✝¹ : FunLike F M₁ M₂<VAR>inst✝ : MonoidHomClass F M₁ M₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>m₁ : M₁<GOAL>f m₁ ^ exponent M₁ = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m✝ m : (i : ι) → OuterMeasure (α i)<VAR>n : OuterMeasure ((i : ι) → α i)<GOAL>n ≤ OuterMeasure.pi m ↔ ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m✝ m : (i : ι) → OuterMeasure (α i)<VAR>n : OuterMeasure ((i : ι) → α i)<GOAL>(∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) ↔ ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : Generators R S<VAR>x y : S<VAR>e : P.σ x = P.σ y<GOAL>x = y
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : PresheafedSpace C<VAR>base : ↑X ⟶ ↑Y<VAR>c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf<VAR>h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'<GOAL>{ base := base, c := c } = { base := base, c := c' }
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : PresheafedSpace C<VAR>base : ↑X ⟶ ↑Y<VAR>c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf<VAR>h : c = c'<GOAL>{ base := base, c := c } = { base := base, c := c' }
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝² : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(lift G f P g Hg)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝² : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<GOAL>∀ (a : DirectLimit G f), (lift G f P g Hg) a = 0 → a = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝² : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0<VAR>z : DirectLimit G f<VAR>hz : (lift G f P g Hg) z = 0<GOAL>z = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝² : CommRing P<VAR>g✝ : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (lift G f P g✝ Hg) ((of G f i✝) g) = 0<GOAL>(of G f i✝) g = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝² : CommRing P<VAR>g✝ : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0<VAR>i✝ : ι<VAR>g : G i✝<VAR>hz : (g✝ i✝) g = 0<GOAL>(of G f i✝) g = 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>h : a ∉ l₁.keys<GOAL>dlookup a (l₁.kunion l₂) = dlookup a l₂
<VAR>l r : List Char<GOAL>ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α✝<VAR>α : Type u_4<VAR>a b : α<VAR>inst✝ : Preorder α<GOAL>IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℤ<VAR>x : α<GOAL>f (x + (↑n * (2 * c) + c)) = -f x
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)<VAR>m : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (last n)<GOAL>(f.uncurryRight.curryRight m) x = (f m) x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>b : Basis ι R M<VAR>inst✝ : Nontrivial M<GOAL>Nonempty ι
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>b : Basis ι R M<VAR>inst✝ : Nontrivial M<VAR>x y : M<VAR>ne : x ≠ y<GOAL>Nonempty ι
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>b : Basis ι R M<VAR>inst✝ : Nontrivial M<VAR>x y : M<VAR>ne : x ≠ y<VAR>i : ι<VAR>h✝ : ¬(b.repr x) i = (b.repr y) i<GOAL>Nonempty ι
<VAR>n✝ m n : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<VAR>h : k ≤ 0<GOAL>↑k = ↑0
<VAR>n✝ m n : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<VAR>h : k ≤ 0<GOAL>0 = ↑0
<VAR>n✝ m n : ℕ<VAR>inst✝ : NeZero n<GOAL>0 ≤ 0
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond : f ≫ g = 0<VAR>cond2 : g ≫ h = 0<GOAL>explicitCokernelDesc cond ≫ h = 0
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond : f ≫ g = 0<VAR>cond2 : g ≫ h = 0<GOAL>g ≫ h = explicitCokernelπ f ≫ 0
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Basis (B ∩ X) X ↔ M✶.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : M.Base B<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>h : M✶.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)<GOAL>M.Basis (B ∩ X) X
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<GOAL>Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<GOAL>Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<GOAL>(f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l = ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<GOAL>p = ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : ¬p = ⊥<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<VAR>f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<VAR>f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯<VAR>f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this✝ : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<VAR>f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯<VAR>f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯<VAR>this : IsNilpotent (f₂ - f₁)<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this✝ : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<VAR>f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯<VAR>f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯<VAR>this : IsNilpotent (f₂ - f₁)<VAR>hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<VAR>a✝ : Nontrivial M<VAR>this✝ : IsReduced R<VAR>p : Submodule R M := (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) l<VAR>hp : Nontrivial ↥p<VAR>f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯<VAR>f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯<VAR>this : μ₁ = μ₂<VAR>hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<GOAL>∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<GOAL>∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<GOAL>∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<GOAL>(∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<GOAL>(∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<GOAL>(f a).Dom ∨ (g a).Dom → (k' a).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<VAR>h : (f a).Dom ∨ (g a).Dom<GOAL>(k' a).Dom