ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < p.natDegree<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < p.natDegree<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < p.natDegree<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>map f (erase + lead) = p ∧ (erase + lead).degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>(erase + lead).degree = p.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>(erase + lead).degree = lead.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>erase.degree < lead.degree
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ {p : S[X]}, p ∈ lifts f → p.natDegree = m → ∃ q, map f q = p ∧ q.degree = p.degree<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hdeg : p.natDegree = n<VAR>erase_zero : ¬p.eraseLead = 0<VAR>deg_erase : p.eraseLead.natDegree < n<VAR>pzero : p ≠ 0<VAR>lead_zero : p.coeff p.natDegree ≠ 0<VAR>lead : R[X]<VAR>hlead : map f lead = (monomial p.natDegree) (p.coeff p.natDegree) ∧ lead.degree = ((monomial p.natDegree) (p.coeff p.natDegree)).degree<VAR>deg_lead : lead.degree = ↑p.natDegree<VAR>erase : R[X]<VAR>herase : map f erase = Polynomial.erase p.natDegree p ∧ erase.degree = (Polynomial.erase p.natDegree p).degree<GOAL>(Polynomial.erase p.natDegree p).degree < p.degree
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.reverse.Subsingleton ↔ s.Subsingleton
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s✝ t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>s : Set α<GOAL>𝓟 (exterior s) = 𝓝ˢ s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<GOAL>matPolyEquiv (diagonal fun x => X) = X
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>h : a * b = c<GOAL>b = c / a
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>y₁ * (x₂ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) + y₂ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) + ((y₁ - y₂) / (x₁ - x₂) * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) + y₁) * (x₁ - x₂) = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>(y₁ * (x₂ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) - ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂)) + y₂ * ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁)) * ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂))) + ((y₁ - y₂) * ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ - (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁) + y₁ * ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂)))) * (x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>t : Set β<VAR>x : β<VAR>x✝ : x ∈ range f ∩ t<VAR>y : α<VAR>h_eq : f y = x<VAR>hx : x ∈ t<GOAL>y ∈ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>t : Set β<VAR>x : β<VAR>x✝ : x ∈ range f ∩ t<VAR>y : α<VAR>h_eq : f y = x<VAR>hx : x ∈ t<GOAL>x ∈ t
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Star α<GOAL>Mᴴ.updateColumn i (star b) = (M.updateRow i b)ᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Star α<GOAL>((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))<GOAL>μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ (n + 1) • μ (s ∆ (f ⁻¹' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))<GOAL>μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>n : ℕ<VAR>ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))<GOAL>μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>hf : MeasurePreserving f μ μ<VAR>n : ℕ<VAR>ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))<VAR>hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ<GOAL>μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>h : e ∈ M.E \ B<GOAL>M.Dep (insert e B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>h : e ∈ M.E \ B<GOAL>¬M.Indep (insert e B)
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<VAR>hb : ℵ₀ ≤ b<GOAL>a ≤ a * b
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<VAR>hb : ℵ₀ ≤ b<GOAL>b ≤ a * b
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommMonoid R✝<VAR>R' : Type u_2<VAR>inst✝² : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝¹ : CommRing R''<VAR>R : Type u_4<VAR>inst✝ : CommRing R<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>a✝ : Rˣ<GOAL>(χ.ringHomComp f)⁻¹ ↑a✝ = (χ⁻¹.ringHomComp f) ↑a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>∑ i : Fin n, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>(2 * d + 1) ^ n - 1 = (∑ i : Fin n, d * (2 * d + 1) ^ ↑i) * 2
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>ha : IsUnit a<VAR>hb : IsUnit b<GOAL>IsUnit (a / b)
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>ha : IsUnit a<VAR>hb : IsUnit b<GOAL>IsUnit (a * b⁻¹)
<VAR>f g : StieltjesFunction<VAR>h : ∀ (x : ℝ), ↑f x = ↑g x<GOAL>f = g
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>l : List α<VAR>hl : l.length = n<GOAL>insertNth b j.succ (insertNth a i ⟨l, hl⟩) = insertNth a i.castSucc (insertNth b j ⟨l, hl⟩)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>l : List α<VAR>hl : l.length = n<GOAL>↑(insertNth b j.succ (insertNth a i ⟨l, hl⟩)) = ↑(insertNth a i.castSucc (insertNth b j ⟨l, hl⟩))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>l : List α<VAR>hl : l.length = n<GOAL>List.insertNth (↑j + 1) b (List.insertNth (↑i) a l) = List.insertNth (↑i) a (List.insertNth (↑j) b l)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>l : List α<VAR>hl : l.length = n<GOAL>↑i ≤ ↑j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>l : List α<VAR>hl : l.length = n<GOAL>↑j ≤ l.length
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(X ^ n).rootSet S = {0}
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 ≠ 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>(pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op = (pushout.inl f g).op
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op).unop = (pushout.inl f g).op.unop
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>(pullback.fst f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inl f g
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥A<GOAL>of ↑a * t⁻¹ = t⁻¹ * of ↑(φ a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥A<GOAL>of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>f g : Π₀ (i : ι), β i<VAR>i✝ : κ<GOAL>(comapDomain h hh (f + g)) i✝ = (comapDomain h hh f + comapDomain h hh g) i✝
<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✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V →ₗ[K] V →ₛₗ[J] V₂<VAR>x y : V<GOAL>y ∈ (Submodule.span K {x}).orthogonalBilin B ↔ y ∈ ker (B x)
<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✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V →ₗ[K] V →ₛₗ[J] V₂<VAR>x y : V<GOAL>(∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B x) y = 0
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<GOAL>↑h.unit⁻¹ ∈ S
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<GOAL>↑h.unit⁻¹ ∈ S
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<GOAL>↑hx.unit⁻¹ ∈ S
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<GOAL>↑hx.unit⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<VAR>this : IsStarNormal (star x * x)<GOAL>↑hx.unit⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<VAR>this : IsStarNormal (star x * x)<VAR>hx' : IsUnit ⟨star x * x, ⋯⟩<GOAL>↑hx.unit⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<VAR>this : IsStarNormal (star x * x)<VAR>hx' : IsUnit ⟨star x * x, ⋯⟩<GOAL>↑hx.unit⁻¹ = ↑↑hx'.unit⁻¹
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<VAR>hx : IsUnit (star x * x)<VAR>this : IsStarNormal (star x * x)<VAR>hx' : IsUnit ⟨star x * x, ⋯⟩<GOAL>↑hx.unit * ↑↑hx'.unit⁻¹ = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j✝ j : ι<GOAL>(P.reflection i) (P.root j) ∈ range ⇑P.root
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : InfSet α<VAR>inst✝² : InfSet β<VAR>inst✝¹ : InfSet γ<VAR>inst✝ : InfSet δ<VAR>g : sInfHom β γ<VAR>f₁ f₂ : sInfHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg hgf : ¬f /ₘ g = 0<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg : ¬f /ₘ g = 0<VAR>hgf : ¬f.degree < g.degree<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg : ¬f /ₘ g = 0<VAR>hgf : g.degree ≤ f.degree<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg : ¬f /ₘ g = 0<VAR>hgf : g.degree ≤ f.degree<VAR>this : g.degree + (f /ₘ g).degree = f.degree<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg : ¬f /ₘ g = 0<VAR>hgf : g.degree ≤ f.degree<VAR>this : g.degree + (f /ₘ g).degree = f.degree<VAR>hf : f ≠ 0<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q f g : R[X]<VAR>hg : g.Monic<VAR>a✝ : Nontrivial R<VAR>hfg : ¬f /ₘ g = 0<VAR>hgf : g.degree ≤ f.degree<VAR>this : g.natDegree + (f /ₘ g).natDegree = f.natDegree<VAR>hf : f ≠ 0<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Group G<VAR>x : G<GOAL>x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)