ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>a ^ n • b = b ↔ ↑(minimalPeriod (fun x => a • x) b) ∣ n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>h : IsUnit p.leadingCoeff<GOAL>(h.unit⁻¹ • p).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>h : IsUnit p.leadingCoeff<GOAL>↑h.unit⁻¹ • p.leadingCoeff = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>k : Rˣ<VAR>hk : ↑k = p.leadingCoeff<GOAL>↑(IsUnit.unit ⋯)⁻¹ • p.leadingCoeff = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>k : Rˣ<VAR>hk : ↑k = p.leadingCoeff<GOAL>k = ⋯.unit * 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : Epi 0<GOAL>IsZero Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α → E⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), Disjoint (support f) (support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P f}<GOAL>∀ (f : ↥(Lp E p μ)), P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α → E⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), Disjoint (support f) (support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P f}<VAR>f : ↥(Lp E p μ)<GOAL>∀ (a : { x // x ∈ ↑(simpleFunc E p μ) }), P ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α → E⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), Disjoint (support f) (support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P f}<VAR>f : ↥(Lp E p μ)<GOAL>∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p hs ⋯ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α → E⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), Disjoint (support f) (support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P f}<VAR>f : ↥(Lp E p μ)<GOAL>∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P ↑(simpleFunc.toLp f hf) → P ↑(simpleFunc.toLp g hg) → P ↑(simpleFunc.toLp f hf + simpleFunc.toLp g hg)
<VAR>x : ℝ<GOAL>sin (π / 6) = 1 / 2
<VAR>x : ℝ<GOAL>cos (π / 2 - π / 6) = cos (π / 3)
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (x : Y), (f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>x : Y<GOAL>(f.comp (f.inverse' g k₂ h₁ h₂)) x = (MulActionHom.id N) x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>x : Y<GOAL>f ((f.inverse' g k₂ h₁ h₂) x) = x
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<GOAL>orderOf x = n
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<GOAL>orderOf x = n
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<GOAL>a = 1
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<VAR>h : ¬a = 1<GOAL>False
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<VAR>h : ¬a = 1<VAR>a_min_fac_dvd_p_sub_one : a.minFac ∣ n<GOAL>False
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<VAR>h : ¬a = 1<VAR>a_min_fac_dvd_p_sub_one : a.minFac ∣ n<GOAL>x ^ (n / a.minFac) = 1
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<VAR>h : ¬a = 1<VAR>a_min_fac_dvd_p_sub_one : a.minFac ∣ n<GOAL>a.minFac ∣ a
<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>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<VAR>a : ℕ<VAR>ha : n = orderOf x * a<VAR>h : ¬a = 1<VAR>a_min_fac_dvd_p_sub_one : a.minFac ∣ n<GOAL>IsOfFinOrder x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h's : r < μ s<GOAL>∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h's : ∃ i, r < (μ.restrict (spanningSets μ i)) s<GOAL>∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>n : ℕ<VAR>hn : r < (μ.restrict (spanningSets μ n)) s<GOAL>∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>n : ℕ<VAR>hn : r < μ (s ∩ spanningSets μ n)<GOAL>∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>n : ℕ<VAR>hn : r < μ (s ∩ spanningSets μ n)<GOAL>μ (s ∩ spanningSets μ n) < ⊤
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K✝ : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Fintype I<VAR>inst✝³ : Fintype J<VAR>inst✝² : Algebra K R<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : DecidableEq J<VAR>c : K<VAR>i✝ j✝ : I × J<GOAL>__spread✝⁻⁰.toFun ((algebraMap K (Matrix I I (Matrix J J R))) c) i✝ j✝ = (algebraMap K (Matrix (I × J) (I × J) R)) c i✝ j✝
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K✝ : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Fintype I<VAR>inst✝³ : Fintype J<VAR>inst✝² : Algebra K R<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : DecidableEq J<VAR>c : K<VAR>i✝ j✝ : I × J<GOAL>diagonal ((algebraMap K (I → Matrix J J R)) c) i✝.1 j✝.1 i✝.2 j✝.2 = diagonal ((algebraMap K (I × J → R)) c) i✝ j✝
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K✝ : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Fintype I<VAR>inst✝³ : Fintype J<VAR>inst✝² : Algebra K R<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : DecidableEq J<VAR>c : K<VAR>i✝ j✝ : I × J<GOAL>(if i✝.1 = j✝.1 then (fun r => r • diagonal fun x => 1) c else 0) i✝.2 j✝.2 = if i✝ = j✝ then (fun r => r • 1) c else 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<VAR>f : R[X]<GOAL>(C a).natDegree + f.natDegree = 0 + f.natDegree
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0<VAR>p q : k[X]<VAR>hq : Irreducible q<VAR>a✝ : q ∣ map (RingHom.id k) p<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0<VAR>p q : k[X]<VAR>hq : Irreducible q<VAR>a✝ : q ∣ map (RingHom.id k) p<VAR>this : Irreducible (q * C q.leadingCoeff⁻¹)<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0<VAR>p q : k[X]<VAR>hq : Irreducible q<VAR>a✝ : q ∣ map (RingHom.id k) p<VAR>this : Irreducible (q * C q.leadingCoeff⁻¹)<VAR>x : k<VAR>hx : eval x (q * C q.leadingCoeff⁻¹) = 0<GOAL>q.degree = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>Multiset.map f univ.val = ↑(List.ofFn f)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : DecidableEq (Associates α)<VAR>m p : Associates α<VAR>h₁ : m ≠ 0<VAR>h₂ : Irreducible p<VAR>k : ℕ<GOAL>p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : DecidableEq (Associates α)<VAR>p : Associates α<VAR>h₂ : Irreducible p<VAR>k : ℕ<VAR>m : α<VAR>hm : m ≠ 0<VAR>h₁ : Associates.mk m ≠ 0<GOAL>p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : DecidableEq (Associates α)<VAR>p : Associates α<VAR>h₂ : Irreducible p<VAR>k : ℕ<VAR>m : α<VAR>hm : m ≠ 0<VAR>h₁ : Associates.mk m ≠ 0<VAR>this : Nontrivial α<GOAL>p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<GOAL>ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>z.proj ∈ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>IsOpen ((s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>↑e z ∈ (s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>(↑e z).1 ∈ s ∩ (a.pretrivializationAt z.proj).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>z.proj ∈ s ∩ (a.pretrivializationAt z.proj).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X✝ : Type u_4<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : TotalSpace F E → X<VAR>s : Set B<VAR>hs : IsOpen s<VAR>hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>z : TotalSpace F E<VAR>hz : z ∈ TotalSpace.proj ⁻¹' s<VAR>e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯<GOAL>z ∈ e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (Set α)<GOAL>⋂₀ s = ⋂ i, ↑i
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>hA : A ∈ center (SpecialLinearGroup n R)<VAR>i : n<GOAL>(scalar n) (↑A i i) = ↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>hA : A ∈ center (SpecialLinearGroup n R)<VAR>i : n<VAR>r : R<VAR>hr : (scalar n) r = ↑A<GOAL>(scalar n) (↑A i i) = ↑A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>hc : Multiset.card m = n + 1<VAR>a : α<VAR>h : a ∈ m<GOAL>Multiset.card (m.erase a) = n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<GOAL>(CoordinateRing.basis W) 0 = 1
<VAR>α : Type u<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>s : Set (Set α)<VAR>hfin : s.Finite<GOAL>⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K✝ : Multifork I<VAR>inst✝¹ : HasProduct I.left<VAR>inst✝ : HasProduct I.right<VAR>K : Multifork I<GOAL>∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y), ((Functor.const WalkingParallelPair).obj K.pt).map f ≫ (fun x => match x with | WalkingParallelPair.zero => Pi.lift K.ι | WalkingParallelPair.one => Pi.lift K.ι ≫ I.fstPiMap) Y = (fun x => match x with | WalkingParallelPair.zero => Pi.lift K.ι | WalkingParallelPair.one => Pi.lift K.ι ≫ I.fstPiMap) X ≫ (parallelPair I.fstPiMap I.sndPiMap).map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = 2<GOAL>∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = 2<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>x : α<VAR>h : ∃ x_1, s \ {x} = {x_1}<VAR>hx : x ∈ s<GOAL>∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>h : s \ {x} = {y}<GOAL>∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>h : s \ {x} = {y}<GOAL>s = {x, y}
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>l : ℕ<VAR>r : α<VAR>tl : ℕ<VAR>zl : ℤ<VAR>tr t : α<VAR>prl₁ : l = tl<VAR>prl₂ : ↑tl = zl<VAR>prr : r = tr<VAR>prt : smulg zl tr = t<GOAL>smul l r = t
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x : M<VAR>hx : x ∈ s<GOAL>∃ i, 0 < (f i) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x : M<VAR>hx : x ∈ s<VAR>h : ∀ (i : ι), (f i) x ≤ 0<GOAL>False
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H✝ : Type uH<VAR>inst✝³ : TopologicalSpace H✝<VAR>I : ModelWithCorners ℝ E H✝<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H✝ M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x : M<VAR>hx : x ∈ s<VAR>h : ∀ (i : ι), (f i) x ≤ 0<VAR>H : ∀ (i : ι), (f i) x = 0<GOAL>False