ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ∪ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>g : SL(2, ℤ)<GOAL>(↑↑↑g).det = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : ℕ → β<GOAL>∏ t ∈ powersetCard n s, f t.card = f n ^ s.card.choose n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : ℕ → β<GOAL>∀ a ∈ powersetCard n s, f a.card = f n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>s : Finset α<VAR>f : ℕ → β<VAR>a : Finset α<VAR>ha : a ∈ powersetCard n s<GOAL>f a.card = f n
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<GOAL>μH[d₂] s = 0 ∨ μH[d₁] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<GOAL>False
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<GOAL>∀ (c : ℝ≥0), c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>μH[d₂] s ≤ ↑c * μH[d₁] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>(fun r => r ^ d₂) ≤ᶠ[𝓝[≥] 0] ↑c • fun r => r ^ d₁
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<GOAL>(fun r => r ^ d₂) ≤ᶠ[𝓝[≥] 0] ↑c • fun r => r ^ d₁
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<GOAL>∀ a ∈ Ico 0 (↑c ^ (d₂ - d₁)⁻¹), a ^ d₂ ≤ (↑c • fun r => r ^ d₁) a
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<VAR>r : ℝ≥0∞<VAR>hr₀ : 0 ≤ r<VAR>hrc : r < ↑c ^ (d₂ - d₁)⁻¹<GOAL>r ^ d₂ ≤ (↑c • fun r => r ^ d₁) r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<VAR>r : ℝ≥0<VAR>hr₀ : 0 ≤ ↑r<VAR>hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹<GOAL>↑r ^ d₂ ≤ (↑c • fun r => r ^ d₁) ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<VAR>r : ℝ≥0<VAR>hr₀ : 0 ≤ ↑r<VAR>hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹<GOAL>↑r ^ d₂ / ↑r ^ d₁ ≤ ↑c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<VAR>hr₀ : 0 ≤ ↑0<VAR>hrc : ↑0 < ↑c ^ (d₂ - d₁)⁻¹<GOAL>↑0 ^ d₂ / ↑0 ^ d₁ ≤ ↑c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<VAR>H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ⊤<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>this : 0 < ↑c ^ (d₂ - d₁)⁻¹<VAR>r : ℝ≥0<VAR>hr₀✝ : 0 ≤ ↑r<VAR>hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹<VAR>hr₀ : r ≠ 0<GOAL>↑r ^ d₂ / ↑r ^ d₁ ≤ ↑c
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>a ∈ l₁ ↔ a ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a : α<GOAL>∃ b, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a b : α<VAR>h : inl a < inl b<GOAL>∃ b, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a : α<VAR>b : β<VAR>h : inl a < inr b<GOAL>∃ b, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a : β<GOAL>∃ b, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a : β<VAR>b : α<VAR>h : inr a < inl b<GOAL>∃ b, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMaxOrder (α ⊕ β)<VAR>a b : β<VAR>h : inr a < inr b<GOAL>∃ b, a < b
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ≅ h<GOAL>f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z✝ : C<VAR>f✝ : Y✝ ⟶ X<VAR>S R✝ : Sieve X<VAR>R : Cᵒᵖ ⥤ Type v₁<VAR>f : R ⟶ yoneda.obj X<VAR>Y Z : C<VAR>t : R.obj (Opposite.op Y)<VAR>g : Z ⟶ Y<GOAL>f.app (Opposite.op Z) (R.map g.op t) = g ≫ f.app (Opposite.op Y) t
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z✝ : C<VAR>f✝ : Y✝ ⟶ X<VAR>S R✝ : Sieve X<VAR>R : Cᵒᵖ ⥤ Type v₁<VAR>f : R ⟶ yoneda.obj X<VAR>Y Z : C<VAR>t : R.obj (Opposite.op Y)<VAR>g : Z ⟶ Y<GOAL>(yoneda.obj X).map g.op (f.app (Opposite.op Y) t) = g ≫ f.app (Opposite.op Y) t
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>r s t w : 𝓞 K<VAR>hr : ¬λ ∣ r<VAR>hs : ¬λ ∣ s<VAR>Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ<VAR>H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t<VAR>H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w<GOAL>IsCoprime r s
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>r s t w : 𝓞 K<VAR>hr : ¬λ ∣ r<VAR>hs : ¬λ ∣ s<VAR>Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ<VAR>H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t<VAR>H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>p_dvd_r : p ∣ r<VAR>p_dvd_s : p ∣ s<GOAL>λ ∣ r
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<GOAL>∑ x : ↥G, ↑↑x ^ k = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<GOAL>∑ x : ↥G, ↑↑x ^ k = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<GOAL>∑ x : ↥G, ↑↑x ^ k = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val).sum<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<VAR>hzero : (↑↑a ^ k - 1) * (Multiset.map (fun i => ↑↑i ^ k) univ.val).sum = 0<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<VAR>hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i => ↑↑i ^ k) univ.val).sum = 0<GOAL>(Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<VAR>hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i => ↑↑i ^ k) univ.val).sum = 0<VAR>h : ↑↑a ^ k - 1 = 0<GOAL>a ^ k = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<VAR>hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i => ↑↑i ^ k) univ.val).sum = 0<VAR>h : ↑↑a ^ k - 1 = 0<GOAL>↑↑(a ^ k) = ↑↑1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card ↥G<VAR>a✝ : Nontrivial K<VAR>this : IsDomain K<VAR>a : ↥G<VAR>ha : a ^ k ≠ 1<VAR>h_multiset_map : Multiset.map (fun x => ↑↑x ^ k) univ.val = Multiset.map (fun x => ↑↑x ^ k * ↑↑a ^ k) univ.val<VAR>h_multiset_map_sum : (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x => ↑↑x ^ k) univ.val).sum * ↑↑a ^ k<VAR>hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i => ↑↑i ^ k) univ.val).sum = 0<VAR>h : ↑↑a ^ k - 1 = 0<GOAL>↑↑(a ^ k) - ↑↑1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>hs : s.SupIndep f<VAR>t : Finset { x // x ∈ s }<VAR>a✝¹ : t ⊆ s.attach<VAR>i : { x // x ∈ s }<VAR>a✝ : i ∈ s.attach<VAR>hi : i ∉ t<GOAL>Disjoint ((fun a => f ↑a) i) (t.sup fun a => f ↑a)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : IsSimpleModule R N<VAR>l : M →ₗ[R] N<GOAL>IsClosed ↑(ker l) ∨ Dense ↑(ker l)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : IsSimpleModule R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<GOAL>IsClosed ↑(ker l) ∨ Dense ↑(ker l)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : IsSimpleModule R N<GOAL>IsClosed ↑(ker 0) ∨ Dense ↑(ker 0)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>inst✝¹ : StrongMono (f ≫ g)<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>inst✝ : Epi z<VAR>u : X ⟶ P<VAR>v : Y ⟶ Q<VAR>sq : CommSq u z f v<GOAL>sq.HasLift
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>inst✝¹ : StrongMono (f ≫ g)<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>inst✝ : Epi z<VAR>u : X ⟶ P<VAR>v : Y ⟶ Q<VAR>sq : CommSq u z f v<VAR>h₀ : u ≫ f ≫ g = z ≫ v ≫ g<GOAL>sq.HasLift
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : OpenEmbedding ⇑g<GOAL>OpenEmbedding ⇑(pullback.fst f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : OpenEmbedding ⇑g<GOAL>⇑(pullback.fst f g) = ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : OpenEmbedding ⇑g<GOAL>⇑(pullback.fst f g) = ⇑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯ ≫ (asIso (pullback.fst f (𝟙 S))).hom)
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>(ι R) x ≠ 1
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>¬(x = 0 ∧ 1 = 0)
<VAR>q a b c : ℚ<GOAL>a + 0 = a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>x✝ : IsFractional S I<GOAL>IsFractional S (0 • I)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>x✝ : IsFractional S I<GOAL>IsFractional S 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>x✝ : IsFractional S I<GOAL>0 = ↑↑0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>n : ℕ<VAR>h : IsFractional S I<GOAL>IsFractional S ((n + 1) • I)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>n : ℕ<VAR>h : IsFractional S I<GOAL>IsFractional S (n • I + I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>P : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>hm : Monotone m<GOAL>(map Subtype.val ∘ₗ comap Subtype.val) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>hm : Monotone m<GOAL>(map Subtype.val) ((comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) = OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>hm : Monotone m<GOAL>(map Subtype.val) (OuterMeasure.ofFunction (fun s_1 => m (Subtype.val '' s_1)) ⋯) = OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f ⊗ g) ≫ (inv f ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>o : Part α<GOAL>map g (map f o) = map (g ∘ f) o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CompactSpace α<VAR>inst✝² : MetricSpace β<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>inst✝ : Nonempty α<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>↑n + a = a
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedRing 𝕜'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormOneClass 𝕜'<VAR>x y : 𝕜<GOAL>dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : HasPullback f g<GOAL>(pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulZeroClass α β<VAR>s✝ : Set α<VAR>t : Set β<VAR>a : α<VAR>s : Set α<GOAL>s • 0 ⊆ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ pullback.snd (𝒰.map j ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Union α<VAR>a b : Part α<VAR>hab : (a ∪ b).Dom<GOAL>(a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Union α<VAR>a b : Part α<VAR>hab : (a ∪ b).Dom<GOAL>(a.bind fun y => map (fun x => y ∪ x) b).get ⋯ = a.get ⋯ ∪ b.get ⋯
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : PartialOrder α<VAR>c : ClosureOperator α<VAR>x✝ y x : α<GOAL>x ∈ {x | c.IsClosed x} ↔ x ∈ range ⇑c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<GOAL>⋃ n, compactCovering X n = univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<GOAL>⋃ x, ⋯.choose x = univ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ = (v.intValuation ↑s)⁻¹ ∨ ↑v.intValuation.toMonoidWithZeroHom r = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ = (v.intValuation ↑s)⁻¹
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s) = v.intValuation ↑s
<VAR>α : Sort u_1<VAR>r p q : α → Prop<VAR>P Q : (x : α) → p x → Prop<VAR>b : Prop<VAR>a : α<GOAL>(∃ x x_1, p x) ↔ p a
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* S<VAR>x✝ : R<GOAL>((map f).comp C) x✝ = (C.comp f) x✝