ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a₂ : P.mp.A<VAR>f₂ : P.mp.B a₂ ⟹ α<VAR>r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩<VAR>this : a₁ = a₂<GOAL>⟨a₁, f₁⟩ = ⟨a₂, f₂⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>a₁ : P.mp.A<VAR>f₁ f₂ : P.mp.B a₁ ⟹ α<VAR>r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩<VAR>i : Fin2 n<VAR>p : P.mp.B a₁ i<GOAL>f₁ i p = f₂ i p
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>a₁ : P.mp.A<VAR>i✝ : Fin2 n<VAR>x : P.last.M<VAR>a : P.A<VAR>f : P.last.B a → P.last.M<VAR>h' : x.dest = ⟨a, f⟩<VAR>i : Fin2 n<VAR>c : P.drop.B a i<VAR>f₁ f₂ : P.mp.B x ⟹ α<VAR>r : R ⟨x, f₁⟩ ⟨x, f₂⟩<VAR>e₁' : x.dest = ⟨a, f⟩<VAR>e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩<VAR>e₂' : x.dest = ⟨a, f⟩<VAR>e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂<VAR>e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩<VAR>h'' : ∀ (i : (P.B a).last), R ((fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)<GOAL>f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>a₁ : P.mp.A<VAR>i✝ : Fin2 n<VAR>x : P.last.M<VAR>a : P.A<VAR>f : P.last.B a → P.last.M<VAR>h' : x.dest = ⟨a, f⟩<VAR>i : P.last.B a<VAR>c : Fin2 n<VAR>p : Path P (f i) c<VAR>IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p<VAR>f₁ f₂ : P.mp.B x ⟹ α<VAR>r : R ⟨x, f₁⟩ ⟨x, f₂⟩<VAR>e₁' : x.dest = ⟨a, f⟩<VAR>e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩<VAR>e₂' : x.dest = ⟨a, f⟩<VAR>e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂<VAR>e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩<VAR>h'' : ∀ (i : (P.B a).last), R ((fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)<GOAL>f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁴ : Countable ι✝<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>StronglyMeasurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁴ : Countable ι✝<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁴ : Countable ι✝<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>IsSeparable (range g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t✝ u v : Finset α<VAR>a b x : α<VAR>h : x ∉ s<VAR>t : Finset α<GOAL>s \ insert x t = s \ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t✝ u v : Finset α<VAR>a b x : α<VAR>h : x ∉ s<VAR>t : Finset α<VAR>y : α<VAR>hy : y ∈ s \ t<GOAL>y ∈ s \ insert x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t✝ u v : Finset α<VAR>a b x : α<VAR>h : x ∉ s<VAR>t : Finset α<VAR>y : α<VAR>hy : y ∈ s ∧ y ∉ t<GOAL>y ∈ s ∧ ¬y = x ∧ y ∉ t
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M₁<VAR>h : 0 < finrank R M<GOAL>Finite R M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M₁<VAR>h : ¬Finite R M<GOAL>¬0 < finrank R M
<VAR>α : Type u<VAR>inst✝ : CommRing α<VAR>x y : α<VAR>n : ℕ<VAR>h : Odd n<GOAL>x + y ∣ x ^ n + y ^ n
<VAR>α : Type u<VAR>inst✝ : CommRing α<VAR>x y : α<VAR>n : ℕ<VAR>h : Odd n<VAR>h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n<GOAL>x + y ∣ x ^ n + y ^ n
<VAR>α : Type u<VAR>inst✝ : CommRing α<VAR>x y : α<VAR>n : ℕ<VAR>h : Odd n<VAR>h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n<GOAL>x + y ∣ x ^ n + y ^ n
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>g : G<VAR>x : k[G]<GOAL>of' k G g * x %ᵒᶠ g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>g : G<VAR>x : k[G]<VAR>g' : G<GOAL>(of' k G g * x %ᵒᶠ g) g' = 0 g'
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>g : G<VAR>x : k[G]<VAR>g' : G<GOAL>(of' k G g * x %ᵒᶠ g) g' = 0
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>p : α<VAR>this : DecidableEq α := Classical.decEq α<VAR>hpi : Irreducible p<VAR>a b : α<VAR>x✝ : p ∣ a * b<VAR>x : α<VAR>hx : a * b = p * x<VAR>hab0 : ¬a * b = 0<VAR>hx0 : x ≠ 0<GOAL>p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>p : α<VAR>this : DecidableEq α := Classical.decEq α<VAR>hpi : Irreducible p<VAR>a b : α<VAR>x✝ : p ∣ a * b<VAR>x : α<VAR>hx : a * b = p * x<VAR>hab0 : ¬a * b = 0<VAR>hx0 : x ≠ 0<VAR>ha0 : a ≠ 0<GOAL>p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>p : α<VAR>this : DecidableEq α := Classical.decEq α<VAR>hpi : Irreducible p<VAR>a b : α<VAR>x✝ : p ∣ a * b<VAR>x : α<VAR>hx : a * b = p * x<VAR>hab0 : ¬a * b = 0<VAR>hx0 : x ≠ 0<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>p : α<VAR>this : DecidableEq α := Classical.decEq α<VAR>hpi : Irreducible p<VAR>a b : α<VAR>x✝ : p ∣ a * b<VAR>x : α<VAR>hx : a * b = p * x<VAR>hab0 : ¬a * b = 0<VAR>hx0 : x ≠ 0<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>fx : Multiset α<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x<VAR>fa : Multiset α<VAR>hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a<VAR>fb : Multiset α<VAR>hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b<VAR>h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)<GOAL>p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn₁ : n ≠ 1<GOAL>minOrder (ZMod n) = ↑n.minFac
<VAR>α : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn₁ : n ≠ 1<VAR>this : Fact (1 < n)<GOAL>minOrder (ZMod n) = ↑n.minFac
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>0 < clog b n
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>0 < clog b ((n + b - 1) / b) + 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l.prod ≠ 1<GOAL>∃ x ∈ l, x ≠ 1
<GOAL>√3 / 2 / (1 / 2) = √3
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = 0 ↔ angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>π / 2 ∈ Icc 0 π
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm_not : ¬SigmaFinite (μ.trim hm)<GOAL>μ[f|m] = 0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm_not : ¬SigmaFinite (μ.trim hm)<GOAL>¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<GOAL>∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ = φ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>t✝ : Finset κ<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>a : α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>J : Ideal R<VAR>hJ : J ≠ 0<GOAL>count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>J : Ideal R<VAR>hJ : J ≠ 0<GOAL>↑J ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>J : Ideal R<VAR>hJ : J ≠ 0<GOAL>↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a b x : α<VAR>l : List α<VAR>h : Chain' R (x :: l)<VAR>y : α<VAR>hy : y ∈ l.head?<GOAL>R x y
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a b x : α<VAR>l : List α<VAR>y : α<VAR>h : Chain' R (x :: y :: l.tail)<VAR>hy : y ∈ l.head?<GOAL>R x y
<VAR>o : Ordinal.{u_1}<GOAL>o < ω ↔ ∃ n, o = ↑n
<VAR>E : Type u_1<VAR>inst✝ : SeminormedGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>IsBounded s → IsBounded s⁻¹
<VAR>E : Type u_1<VAR>inst✝ : SeminormedGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>(∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ ⦃x : E⦄, x ∈ s → ‖x‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>s₁.mongePoint = s₂.mongePoint
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<GOAL>Function.Bijective ⇑(gelfandTransform ℂ A)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<GOAL>Function.Surjective ⇑(gelfandTransform ℂ A)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }<GOAL>Function.Surjective ⇑(gelfandTransform ℂ A)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }<GOAL>rng = ⊤
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }<VAR>h : rng.topologicalClosure = rng<GOAL>rng = ⊤
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }<VAR>h : rng.topologicalClosure = rng<VAR>x✝¹ x✝ : ↑(characterSpace ℂ A)<GOAL>x✝¹ ≠ x✝ → ∃ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ ≠ f x✝
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }<VAR>h : rng.topologicalClosure = rng<VAR>x✝¹ x✝ : ↑(characterSpace ℂ A)<GOAL>(∀ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ = f x✝) → x✝¹ = x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>F : Realizer α<VAR>s : Set α<VAR>a : α<VAR>this : (a : Prop) → Decidable a<GOAL>(a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>F : Realizer α<VAR>s : Set α<VAR>a : α<VAR>this : (a : Prop) → Decidable a<GOAL>(¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis' I X<VAR>hIJ : I ⊆ J<VAR>hJ : M.Indep J<GOAL>J ∩ X = I
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁵ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝⁴ : LinearOrderedAddCommGroup G<VAR>inst✝³ : Archimedean G<VAR>inst✝² : AddGroup H<VAR>inst✝¹ : AddConstMapClass F G H a b<VAR>f : F<VAR>R : H → H → Prop<VAR>inst✝ : IsTrans H R<VAR>hR : CovariantClass H H (fun x y => y + x) R<VAR>ha : 0 < a<VAR>l : G<VAR>hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)<VAR>x y : G<VAR>hxy : (fun x x_1 => x < x_1) x y<GOAL>R (f x) (f y)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁵ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝⁴ : LinearOrderedAddCommGroup G<VAR>inst✝³ : Archimedean G<VAR>inst✝² : AddGroup H<VAR>inst✝¹ : AddConstMapClass F G H a b<VAR>f : F<VAR>R : H → H → Prop<VAR>inst✝ : IsTrans H R<VAR>ha : 0 < a<VAR>l : G<VAR>hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)<VAR>x y : G<VAR>hxy : (fun x x_1 => x < x_1) x y<VAR>hR : Covariant H H (fun x y => y + x) R<GOAL>R (f x) (f y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝ : HasTerminal C<VAR>X : MonoOver (⊤_ C)<VAR>Z : C<VAR>f g : Z ⟶ X.obj.left<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝ : HasTerminal C<VAR>X : MonoOver (⊤_ C)<VAR>Z : C<VAR>f g : Z ⟶ X.obj.left<GOAL>f ≫ X.arrow = g ≫ X.arrow
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : n ≠ 0<GOAL>minimalPeriod (fun x_1 => x ^ n * x_1) 1 = minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝¹ : CommSemiring R<VAR>p✝ m : ℕ<VAR>inst✝ : DecidableEq σ<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>p ∈ restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i p.degrees ≤ n
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝¹ : CommSemiring R<VAR>p✝ m : ℕ<VAR>inst✝ : DecidableEq σ<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>(∀ s ∈ p.support, ∀ (i : σ), s i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, b i ≤ n
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>n : M₂<GOAL>(0, n) ∈ snd R M M₂
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>∀ (x y : ↥(snd R M M₂)), (fun x => (↑x).2) (x + y) = (fun x => (↑x).2) x + (fun x => (↑x).2) y
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>∀ (m : R) (x : ↥(snd R M M₂)), { toFun := fun x => (↑x).2, map_add' := ⋯ }.toFun (m • x) = (RingHom.id R) m • { toFun := fun x => (↑x).2, map_add' := ⋯ }.toFun x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<VAR>hx : (x, y) ∈ snd R M M₂<GOAL>(fun n => ⟨(0, n), ⋯⟩) ({ toFun := fun x => (↑x).2, map_add' := ⋯, map_smul' := ⋯ }.toFun ⟨(x, y), hx⟩) = ⟨(x, y), hx⟩
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<VAR>hx✝ : (x, y) ∈ snd R M M₂<VAR>hx : x = 0<GOAL>(fun n => ⟨(0, n), ⋯⟩) ({ toFun := fun x => (↑x).2, map_add' := ⋯, map_smul' := ⋯ }.toFun ⟨(x, y), hx✝⟩) = ⟨(x, y), hx✝⟩
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<GOAL>(x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.trailingCoeff = f.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>p.trailingDegree = ↑n ↔ p.natTrailingDegree = n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝² : TopologicalSpace X<VAR>Z B : C<VAR>π : Z ⟶ B<VAR>inst✝¹ : HasPullback π π<VAR>inst✝ : PreservesLimit (cospan π π) G<VAR>a : C(↑(G.obj Z), X)<VAR>ha : ⇑a ∘ ⇑(G.map (pullback.fst π π)) = ⇑a ∘ ⇑(G.map (pullback.snd π π))<VAR>x y : ↑(G.obj Z)<VAR>hxy : (G.map π) x = (G.map π) y<VAR>xy : ↑(G.obj (pullback π π)) := (PreservesPullback.iso G π π).inv ((TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩)<VAR>ha' : a ((G.map (pullback.fst π π)) xy) = a ((G.map (pullback.snd π π)) xy)<GOAL>a x = a y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝² : TopologicalSpace X<VAR>Z B : C<VAR>π : Z ⟶ B<VAR>inst✝¹ : HasPullback π π<VAR>inst✝ : PreservesLimit (cospan π π) G<VAR>a : C(↑(G.obj Z), X)<VAR>ha : ⇑a ∘ ⇑(G.map (pullback.fst π π)) = ⇑a ∘ ⇑(G.map (pullback.snd π π))<VAR>x y : ↑(G.obj Z)<VAR>hxy : (G.map π) x = (G.map π) y<VAR>xy : ↑(G.obj (pullback π π)) := (PreservesPullback.iso G π π).inv ((TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩)<VAR>ha' : a ((G.map (pullback.fst π π)) xy) = a ((G.map (pullback.snd π π)) xy)<VAR>h₁ : ∀ (y : ↑(pullback (G.map π) (G.map π))), (G.map (pullback.fst π π)) ((PreservesPullback.iso G π π).inv y) = (pullback.fst (G.map π) (G.map π)) y<GOAL>a x = a y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝² : TopologicalSpace X<VAR>Z B : C<VAR>π : Z ⟶ B<VAR>inst✝¹ : HasPullback π π<VAR>inst✝ : PreservesLimit (cospan π π) G<VAR>a : C(↑(G.obj Z), X)<VAR>ha : ⇑a ∘ ⇑(G.map (pullback.fst π π)) = ⇑a ∘ ⇑(G.map (pullback.snd π π))<VAR>x y : ↑(G.obj Z)<VAR>hxy : (G.map π) x = (G.map π) y<VAR>xy : ↑(G.obj (pullback π π)) := (PreservesPullback.iso G π π).inv ((TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩)<VAR>ha' : a ((G.map (pullback.fst π π)) xy) = a ((G.map (pullback.snd π π)) xy)<VAR>h₁ : ∀ (y : ↑(pullback (G.map π) (G.map π))), (G.map (pullback.fst π π)) ((PreservesPullback.iso G π π).inv y) = (pullback.fst (G.map π) (G.map π)) y<VAR>h₂ : ∀ (y : ↑(pullback (G.map π) (G.map π))), (G.map (pullback.snd π π)) ((PreservesPullback.iso G π π).inv y) = (pullback.snd (G.map π) (G.map π)) y<GOAL>a x = a y