ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p : ℕ<VAR>inst✝¹ : NeZero p<VAR>inst✝ : CharP R p<VAR>x : ℤ<GOAL>∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
<VAR>K : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p : ℕ<VAR>inst✝¹ : NeZero p<VAR>inst✝ : CharP R p<VAR>x : ℤ<VAR>this : Fact (Nat.Prime p)<GOAL>∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
<VAR>K : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p : ℕ<VAR>inst✝¹ : NeZero p<VAR>inst✝ : CharP R p<VAR>x : ℤ<VAR>this : Fact (Nat.Prime p)<VAR>a b : ZMod p<VAR>hab : a ^ 2 + b ^ 2 = ↑x<GOAL>∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
<VAR>K : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p : ℕ<VAR>inst✝¹ : NeZero p<VAR>inst✝ : CharP R p<VAR>x : ℤ<VAR>this : Fact (Nat.Prime p)<VAR>a b : ZMod p<VAR>hab : a ^ 2 + b ^ 2 = ↑x<GOAL>↑a.val ^ 2 + ↑b.val ^ 2 = ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable ((fun x => ∫⁻ (y : γ), (fun u => f (u.1.2, u.2)) (x, y) ∂η x) ∘ Prod.mk a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun u => f (u.1.2, u.2)
<VAR>α : Sort u_1<VAR>n m : Nat<VAR>f : α → Fin n → α<VAR>x : α<VAR>h : m < n<GOAL>foldl.loop n f x m = foldl.loop n f (f x ⟨m, h⟩) (m + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a✝ a : α<VAR>ha : a ≠ 0<VAR>x y : α<GOAL>edist ((Equiv.mulRight₀ a ha).toFun x) ((Equiv.mulRight₀ a ha).toFun y) = ↑‖a‖₊ * edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>i j : α<VAR>σ : Perm α<GOAL>σ * swap i j * swap i j = σ
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.F n).obj X = (h.F (n + 0)).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>inst✝ : HasKernel f<VAR>W : C<VAR>h : W ⟶ X<VAR>w : (kernelSubobject f).Factors h<GOAL>h ≫ f = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<GOAL>‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<VAR>aux : ∀ (n : ℤ), 0 < ↑p ^ n<GOAL>‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<VAR>aux : ∀ (n : ℤ), 0 < ↑p ^ n<VAR>hx0 : ¬x = 0<GOAL>‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<VAR>aux : ∀ (n : ℤ), 0 < ↑p ^ n<VAR>hx0 : ¬x = 0<GOAL>↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<VAR>aux : ∀ (n : ℤ), 0 < ↑p ^ n<VAR>hx0 : ¬x = 0<VAR>h1p : 1 < ↑p<GOAL>↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<VAR>aux : ∀ (n : ℤ), 0 < ↑p ^ n<VAR>hx0 : ¬x = 0<VAR>h1p : 1 < ↑p<VAR>H : StrictMono fun x => ↑p ^ x<GOAL>↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>he : x₁ ≈ x₃<VAR>h₁ : P2 x₁ x₃ y₁<VAR>h₃ : P2 x₁ x₃ y₃<VAR>h3 : P3 x₁ x₂ y₂ y₃<GOAL>P1 x₁ x₂ x₃ y₁ y₂ y₃
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>he : x₁ ≈ x₃<VAR>h₁ : P2 x₁ x₃ y₁<VAR>h₃ : P2 x₁ x₃ y₃<VAR>h3 : P3 x₁ x₂ y₂ y₃<GOAL>⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₁ * y₃⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ map (algebraMap R K) f<GOAL>g ∈ lifts (algebraMap (↥(integralClosure R K)) K)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ map (algebraMap R K) f<VAR>this : map (algebraMap K g.SplittingField) g ∈ lifts (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField)<GOAL>g ∈ lifts (algebraMap (↥(integralClosure R K)) K)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ map (algebraMap R K) f<VAR>a : g.SplittingField<VAR>ha : a ∈ (map (algebraMap K g.SplittingField) g).roots<GOAL>a ∈ f.aroots g.SplittingField
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ map (algebraMap R K) f<VAR>a : g.SplittingField<VAR>ha : a ∈ (map (algebraMap K g.SplittingField) g).roots<GOAL>a ∈ (map (algebraMap K g.SplittingField) (map (algebraMap R K) f)).roots
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g.Monic<VAR>hd : g ∣ map (algebraMap R K) f<VAR>a : g.SplittingField<VAR>ha : a ∈ (map (algebraMap K g.SplittingField) g).roots<GOAL>map (algebraMap K g.SplittingField) g ∣ map (algebraMap K g.SplittingField) (map (algebraMap R K) f)
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddAbove (range f)<VAR>h_mon : Monotone f<GOAL>∃ r, Tendsto f atTop (𝓝 r)
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddAbove (range f)<VAR>h_mon : Monotone f<VAR>B : ℝ<VAR>hB : IsLUB (range f) B<GOAL>∃ r, Tendsto f atTop (𝓝 r)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<VAR>C : Set X<GOAL>AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>k : ℕ<VAR>x✝ : autoParam (k + 2 ≤ 4) _auto✝<GOAL>((AdicCompletion.firstRow I M f).sc ⋯ k ⋯).Exact
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>k : ℕ<VAR>x✝ : autoParam (k + 2 ≤ 4) _auto✝<GOAL>∀ (x₂ : ↑((AdicCompletion.firstRow I M f).sc ⋯ k ⋯).X₂), ((AdicCompletion.firstRow I M f).sc ⋯ k ⋯).g x₂ = 0 → ∃ x₁, ((AdicCompletion.firstRow I M f).sc ⋯ k ⋯).f x₁ = x₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>nim o₁ ≈ nim o₂ ↔ o₁ = o₂
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Free R S<GOAL>(relNorm R) ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ✝ : α → Sort u_6<VAR>s✝ : Set α<VAR>f g : (i : α) → δ✝ i<VAR>inst✝² : (j : α) → Decidable (j ∈ s✝)<VAR>δ : α → Type u_7<VAR>inst✝¹ : (i : α) → Preorder (δ i)<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : α) → δ i<VAR>h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i<VAR>h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i<GOAL>s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), HasFDerivWithinAt (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ((proj i).comp ((↑(EuclideanSpace.equiv ι 𝕜)).comp f')) t y) ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') t y
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>X✝ Y✝ : LeftLift f g<VAR>η : X✝ ⟶ Y✝<GOAL>((fun t => t.whisker h) X✝).unit ≫ (h ◁ η.right) ▷ f = ((fun t => t.whisker h) Y✝).unit
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>X✝ Y✝ : LeftLift f g<VAR>η : X✝ ⟶ Y✝<GOAL>(h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ η.right) ▷ f = h ◁ Y✝.unit ≫ (α_ h Y✝.lift f).inv
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>X✝ Y✝ : LeftLift f g<VAR>η : X✝ ⟶ Y✝<GOAL>(h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ η.right) ▷ f = h ◁ (X✝.unit ≫ η.right ▷ f) ≫ (α_ h Y✝.lift f).inv
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : Nontrivial α<GOAL>xᶜ < x ↔ x = ⊤
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℤ → M<VAR>hf₁ : HasProd (fun n => f ↑n) m<VAR>hf₂ : HasProd (fun n => f (-(↑n + 1))) m'<VAR>hi₂ : Injective Int.negSucc<VAR>this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)<GOAL>HasProd f (m * m')
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>k : ℕ<GOAL>(bind₁ (xInTermsOfW p R)) (W_ R k) = X k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>k : ℕ<GOAL>∑ x ∈ range (k + 1), (bind₁ (xInTermsOfW p R)) (C (↑p ^ x) * X x ^ p ^ (k - x)) = X k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>k : ℕ<GOAL>∑ x ∈ range (k + 1), C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>k : ℕ<GOAL>X k - ∑ i ∈ range k, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) + ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_mem : x ∈ closure E<GOAL>(thickenedIndicator δ_pos E) x = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : LE α<VAR>inst✝² : LE β<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>EquivLike.inv f b ≤ a ↔ b ≤ f a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>M' : Type u_11<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>x : M'<GOAL>x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>M' : Type u_11<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>x : M'<GOAL>(∃ y, O.subtype y ∈ N ∧ ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>M' : Type u_11<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>x : M'<GOAL>(∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y, O.subtype y ∈ N ∧ ϕ y = x
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Finite n<VAR>A : Matrix m n R<GOAL>(Function.Surjective fun v => v ᵥ* A) ↔ ∃ B, B * A = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Finite n<VAR>A : Matrix m n R<VAR>val✝ : Fintype n<GOAL>(Function.Surjective fun v => v ᵥ* A) ↔ ∃ B, B * A = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Finite n<VAR>A : Matrix m n R<VAR>val✝ : Fintype n<VAR>h : Function.Surjective fun v => v ᵥ* A<VAR>rows : n → m → R<VAR>hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1<GOAL>∃ B, B * A = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Finite n<VAR>A : Matrix m n R<VAR>val✝ : Fintype n<VAR>h : Function.Surjective fun v => v ᵥ* A<VAR>rows : n → m → R<VAR>hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1<VAR>i j : n<GOAL>(of rows * A) i j = 1 i j
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Finite n<VAR>A : Matrix m n R<VAR>val✝ : Fintype n<VAR>h : Function.Surjective fun v => v ᵥ* A<VAR>rows : n → m → R<VAR>hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1<VAR>i j : n<GOAL>(of rows i ᵥ* A) j = (fun v => v ᵥ* A) (rows i) j
<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>H : Subgroup N<VAR>x : G × N<GOAL>x ∈ ⊤.prod H ↔ x ∈ comap (MonoidHom.snd G N) H
<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>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>image₂ f s t ⊆ image₂ f s' t'
<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>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>image2 f ↑s ↑t ⊆ image2 f ↑s' ↑t'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<GOAL>False
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>m : M<GOAL>(B (v i)) m = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>(B (v i)) (v.repr.symm vi) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>∑ x ∈ vi.support, (B (v i)) (vi x • v x) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>∀ x ∈ vi.support, (B (v i)) (vi x • v x) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>(B (v i)) (vi j • v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>I' (vi j) • (B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>(B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>(B (v i)) (v i) = 0