ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x✝ y x : ℝ<VAR>h : 0 ≤ x<GOAL>arcsin x = arccos √(1 - x ^ 2)
<VAR>x✝ y x : ℝ<VAR>h : 0 ≤ x<GOAL>arccos (cos (arcsin x)) = arcsin x
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : ⊤.Adj v w<GOAL>Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : ⊤.Adj v w<GOAL>v ≠ w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(f =o[l] fun x => -g' x) ↔ f =o[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => -g' x) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
<VAR>m k n : Nat<VAR>H1 : m ∣ k<VAR>H2 : k.Coprime n<GOAL>m.Coprime n
<VAR>m k n : Nat<VAR>H1 : m ∣ k<VAR>H2 : k.Coprime n<GOAL>m.gcd n ∣ 1
<VAR>m k n : Nat<VAR>H1 : m ∣ k<VAR>H2 : k.gcd n = 1<GOAL>m.gcd n ∣ 1
<VAR>m k n : Nat<VAR>H1 : m ∣ k<VAR>H2 : k.gcd n = 1<VAR>this : m.gcd n ∣ k.gcd n<GOAL>m.gcd n ∣ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f g : α → 𝕜<VAR>h : f =o[l] g<GOAL>(fun x => f x / g x) =o[l] fun _x => 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Multiset α<VAR>f : α → Multiset β<VAR>x : β<GOAL>count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Multiset α<VAR>f : α → Multiset β<VAR>x : β<GOAL>(if x ∈ s.dedup.bind f then 1 else 0) = if x ∈ s.bind f then 1 else 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Multiset α<VAR>f : α → Multiset β<VAR>x : β<GOAL>x ∈ s.dedup.bind f ↔ x ∈ s.bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>x : α<VAR>u v : αˣ<GOAL>x * ↑(u * v) = x * ↑u * ↑v
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<VAR>this : 0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}<GOAL>∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)<GOAL>∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)<VAR>x : α<VAR>hx : x ∈ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}<VAR>hxN : x ∉ N<GOAL>∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] E<VAR>hA : (↑A).IsSymmetric<GOAL>IsSelfAdjoint A
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<GOAL>m + n ≤ m + n - 1 + 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨅ i, p i) = ⨅ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>sInf {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨅ i, ↑(p i)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>hn : 0 < n<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<GOAL>(s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<GOAL>image compl (s ⊼ t) = image compl s ⊻ image compl t
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>γ : Type u₃<VAR>δ : Type u₄<VAR>ι : Type u₅<VAR>inst✝¹ : MulZeroClass β<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ β<VAR>a : α<VAR>h : a ∈ (g₁ * g₂).support<GOAL>a ∈ g₁.support ∩ g₂.support
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>γ : Type u₃<VAR>δ : Type u₄<VAR>ι : Type u₅<VAR>inst✝¹ : MulZeroClass β<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ β<VAR>a : α<VAR>h : g₁ a * g₂ a ≠ 0<GOAL>a ∈ g₁.support ∩ g₂.support
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>γ : Type u₃<VAR>δ : Type u₄<VAR>ι : Type u₅<VAR>inst✝¹ : MulZeroClass β<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ β<VAR>a : α<VAR>h : g₁ a * g₂ a ≠ 0<GOAL>¬g₁ a = 0 ∧ ¬g₂ a = 0
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>γ : Type u₃<VAR>δ : Type u₄<VAR>ι : Type u₅<VAR>inst✝¹ : MulZeroClass β<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ β<VAR>a : α<VAR>h : g₁ a * g₂ a ≠ 0<GOAL>¬(g₁ a = 0 ∨ g₂ a = 0)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<VAR>inst✝ : StrongRankCondition R<GOAL>FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<GOAL>LipschitzWith 2 (uncurry dist)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<GOAL>LipschitzWith (1 + 1) (uncurry dist)
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>IsCompl p (ker f)
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>IsCompl p (ker ?m.418830.codRestrict)
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>IsProj ?m.418555 f
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>Submodule R E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hf : Measurable f<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<GOAL>StronglyMeasurable f
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝ y✝ z : X<VAR>r✝ s : ℝ<VAR>x y : X<VAR>r : ℝ<GOAL>y ∈ closedBall x r ↔ x ∈ closedBall y r
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<GOAL>(dOne A) f = 0 ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<GOAL>(∀ (a : G × G), (dOne A) f a = 0 a) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n R<VAR>k : ℕ<GOAL>M ^ k = (aeval M) (X ^ k %ₘ M.charpoly)
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>max a a = a
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>f g : CoprodI M →* N<VAR>h : ∀ (i : ι), f.comp of = g.comp of<VAR>x✝ : (i : ι) × M i<VAR>i : ι<VAR>x : M i<GOAL>(f.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩) = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>f g : CoprodI M →* N<VAR>h : ∀ (i : ι), f.comp of = g.comp of<VAR>x✝ : (i : ι) × M i<VAR>i : ι<VAR>x : M i<GOAL>(g.comp of) x = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X : C<VAR>F : SheafOfTypes J<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.forget X).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : C<VAR>f₁ : W ⟶ (Over.forget X).obj Y₁<VAR>f₂ : W ⟶ (Over.forget X).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂<VAR>W' : Over X := Over.mk (f₁ ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X : C<VAR>F : SheafOfTypes J<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.forget X).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : C<VAR>f₁ : W ⟶ (Over.forget X).obj Y₁<VAR>f₂ : W ⟶ (Over.forget X).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂<VAR>W' : Over X := Over.mk (f₁ ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯<VAR>g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>f : L →ₐ[K] L'<VAR>a₁✝ a₂✝ : IntermediateField K L<VAR>h : map f a₁✝ = map f a₂✝<GOAL>a₁✝ = a₂✝
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra ℚ R<VAR>I : Ideal R<VAR>hI : I ≠ ⊤<VAR>a b : ℕ<VAR>h_ab : ↑a = ↑b<GOAL>a = b
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra ℚ R<VAR>I : Ideal R<VAR>a b : ℕ<VAR>h_ab : ↑a = ↑b<VAR>hI : a ≠ b<GOAL>I = ⊤
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra ℚ R<VAR>I : Ideal R<VAR>a b : ℕ<VAR>h_ab : ↑a = ↑b<VAR>hI : a ≠ b<GOAL>(algebraMap ℚ R) (↑a - ↑b) ∈ I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra ℚ R<VAR>I : Ideal R<VAR>a b : ℕ<VAR>h_ab : ↑a = ↑b<VAR>hI : a ≠ b<GOAL>↑a - ↑b ≠ 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : StandardBorelSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : MeasurableSpace Y<VAR>inst✝¹ : OpensMeasurableSpace Y<VAR>f : X → Y<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>this : UpgradedStandardBorel X := upgradeStandardBorel X<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : StandardBorelSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : MeasurableSpace Y<VAR>inst✝¹ : OpensMeasurableSpace Y<VAR>f : X → Y<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>this : UpgradedStandardBorel X := upgradeStandardBorel X<VAR>τ' : TopologicalSpace X<VAR>hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>hfc : Continuous f<VAR>hτ' : PolishSpace X<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : StandardBorelSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : MeasurableSpace Y<VAR>inst✝¹ : OpensMeasurableSpace Y<VAR>f : X → Y<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>this : UpgradedStandardBorel X := upgradeStandardBorel X<VAR>τ' : TopologicalSpace X<VAR>hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>hfc : Continuous f<VAR>hτ' : PolishSpace X<VAR>m' : MeasurableSpace X := borel X<VAR>b' : BorelSpace X<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : StandardBorelSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : MeasurableSpace Y<VAR>inst✝¹ : OpensMeasurableSpace Y<VAR>f : X → Y<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>this : UpgradedStandardBorel X := upgradeStandardBorel X<VAR>τ' : TopologicalSpace X<VAR>hle✝ : τ' ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>hfc : Continuous f<VAR>hτ' : PolishSpace X<VAR>m' : MeasurableSpace X := borel X<VAR>b' : BorelSpace X<VAR>hle : borel X ≤ borel X<GOAL>AnalyticSet (f '' s)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_5<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h_indep : iCondIndepFun m' hm' m f μ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>CondIndepFun m' hm' (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>this : (List.map Not [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < ker φ, ∃ m, m ≠ 0 ∧ φ m = 0]).TFAE<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>this : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ¬⊥ < ker φ, ∀ (m : M), m ≠ 0 → φ m ≠ 0].TFAE<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>this : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ¬⊥ < ker φ, ∀ (m : M), m ≠ 0 → φ m ≠ 0].TFAE<VAR>aux₁ : ∀ (m : M), m ≠ 0 → φ m ≠ 0 ↔ φ m = 0 → m = 0<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>this : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ¬⊥ < ker φ, ∀ (m : M), m ≠ 0 → φ m ≠ 0].TFAE<VAR>aux₁ : ∀ (m : M), m ≠ 0 → φ m ≠ 0 ↔ φ m = 0 → m = 0<VAR>aux₂ : ker φ = ⊥ ↔ ¬⊥ < ker φ<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE