ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>g : S →+* 𝕎 R<VAR>g_compat : ∀ (k : ℕ), (truncate k).comp g = f k<VAR>x : S<GOAL>(lift f f_compat) x = g x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>g : S →+* 𝕎 R<VAR>g_compat : ∀ (k : ℕ), (truncate k).comp g = f k<VAR>x : S<GOAL>∀ (i : ℕ), (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>g : S →+* 𝕎 R<VAR>g_compat : ∀ (k : ℕ), (truncate k).comp g = f k<VAR>x : S<VAR>i : ℕ<GOAL>(lift f f_compat) x - g x ∈ RingHom.ker (truncate i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>BR : RingFilterBasis R<VAR>B : ι → Submodule R M<VAR>hB : BR.SubmodulesBasis B<VAR>x✝ : TopologicalSpace R := BR.topology<VAR>this : TopologicalSpace R := BR.topology<VAR>m : M<VAR>i : ι<GOAL>∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>BR : RingFilterBasis R<VAR>B : ι → Submodule R M<VAR>hB : BR.SubmodulesBasis B<VAR>x✝ : TopologicalSpace R := BR.topology<VAR>this : TopologicalSpace R := BR.topology<VAR>m : M<VAR>i : ι<VAR>V : Set R<VAR>V_in : V ∈ BR<VAR>hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)<GOAL>∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝ : SMul G X<GOAL>IsBlock G ⊥
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.53917, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasLeftResolutions<VAR>X₂ : D₂<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.53917, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasLeftResolutions<VAR>X₂ : D₂<VAR>this : L₂.EssSurj<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.53917, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasLeftResolutions<VAR>X₂ : D₂<VAR>this : L₂.EssSurj<VAR>L : Φ.LeftResolution (L₂.objPreimage X₂)<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g✝ : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)<GOAL>(Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g✝ : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)<VAR>this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f<GOAL>(Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g✝ : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)<VAR>this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f<VAR>h : (Ideal.quotientMap I f ⋯).IsIntegral<GOAL>((Ideal.Quotient.mk I).comp f).IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g✝ : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)<VAR>this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f<VAR>h : (Ideal.quotientMap I f ⋯).IsIntegral<GOAL>g.IsIntegral
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<VAR>hs : IsLowerSet s<VAR>f : α ≃o β<GOAL>IsLowerSet (⇑↑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<VAR>hs : IsLowerSet s<VAR>f : α ≃o β<GOAL>IsLowerSet (⇑(↑f).symm ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>a✝ : α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hf' : AntitoneOn f s<VAR>hs : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>hac : a ≤ c<VAR>hbc : b ≤ c<GOAL>f a = f b
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist (a / b) a = ‖b‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>ha : Absorbent ℝ s<VAR>h : gauge s x ≤ 1<GOAL>x ∈ closure s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>ha : Absorbent ℝ s<VAR>h : gauge s x ≤ 1<VAR>this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s<GOAL>x ∈ closure s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>ha : Absorbent ℝ s<VAR>h : gauge s x ≤ 1<VAR>this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s<GOAL>Tendsto (fun x_1 => x_1 • x) (𝓝[<] 1) (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>this : a ≤ 0 ∨ 0 ≤ a<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>this✝ : a ≤ 0 ∨ 0 ≤ a<VAR>this : b ≤ 0 ∨ 0 ≤ b<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 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 J J' : FractionalIdeal S P<VAR>h : J ≤ J'<GOAL>(fun J => J * I) J ≤ (fun J => J * I) J'
<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 J J' : FractionalIdeal S P<VAR>h : J ≤ J'<GOAL>⟨↑J * ↑I, ⋯⟩ ≤ ⟨↑J' * ↑I, ⋯⟩
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus g = g.neLocus f
<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 p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<GOAL>(p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)
<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 p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<VAR>this : (X - C a).Monic<GOAL>(p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)
<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✝ p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<VAR>this : (X - C a).Monic<VAR>q : R[X] := p /ₘ (X - C a)<GOAL>q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)
<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✝ p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<VAR>this : (X - C a).Monic<VAR>q : R[X] := p /ₘ (X - C a)<GOAL>q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
<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✝ p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<VAR>this✝ : (X - C a).Monic<VAR>q : R[X] := p /ₘ (X - C a)<VAR>this : (p %ₘ (X - C a)).degree < ↑(n + 1)<GOAL>q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsQuasiSeparated s ↔ IsQuasiSeparated Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>s = Subtype.val '' Set.univ
<VAR>x✝ x : ℝ<VAR>hx : x = 0<GOAL>deriv log x = x⁻¹
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>f'' : X'' ⟶ Z''<VAR>g'' : Y'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback f' g'<VAR>inst✝ : HasPullback f'' g''<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>e₃ : f' ≫ j₃ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₂ ≫ g''<GOAL>f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>f'' : X'' ⟶ Z''<VAR>g'' : Y'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback f' g'<VAR>inst✝ : HasPullback f'' g''<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>e₃ : f' ≫ j₃ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₂ ≫ g''<GOAL>g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ (n + 1)).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 q r : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ n * p).Monic
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<GOAL>NumberField.InfinitePlace.NrRealPlaces K = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : w.IsReal<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : NumberField.ComplexEmbedding.IsReal w.embedding<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : NumberField.ComplexEmbedding.IsReal w.embedding<VAR>f : K →+* ℂ := w.embedding<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : NumberField.ComplexEmbedding.IsReal w.embedding<VAR>f : K →+* ℂ := w.embedding<VAR>hζ' : IsPrimitiveRoot (f ζ) k<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : NumberField.ComplexEmbedding.IsReal w.embedding<VAR>f : K →+* ℂ := w.embedding<VAR>hζ' : IsPrimitiveRoot (f ζ) k<VAR>him : (f ζ).im = 0<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : K<VAR>k : ℕ<VAR>hk : 2 < k<VAR>hζ : IsPrimitiveRoot ζ k<VAR>x✝ : { w // w.IsReal }<VAR>w : NumberField.InfinitePlace K<VAR>hwreal : NumberField.ComplexEmbedding.IsReal w.embedding<VAR>f : K →+* ℂ := w.embedding<VAR>hζ' : IsPrimitiveRoot (f ζ) k<VAR>him : (f ζ).im = 0<VAR>hre : (f ζ).re = 1 ∨ (f ζ).re = -1<GOAL>False
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.36857, u_1} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>isomorphisms C f ↔ IsIso f
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<GOAL>x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<VAR>hx : x ∈ I • span R (Set.range f)<GOAL>∀ x ∈ ⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}, ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<VAR>hx : x ∈ I • span R (Set.range f)<GOAL>∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<VAR>hx : x ∈ I • span R (Set.range f)<GOAL>∀ (x y : M), (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) → (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = y) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x + y
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<VAR>hx : x ∈ I • span R (Set.range f)<GOAL>∀ (a : R) (x : M), (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) → ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c => c • f i) = a • x
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n✝ : ?m.31133<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>u : Finset α<VAR>n : ℕ<VAR>hn : n < u.card<GOAL>(powersetCard n.succ u).sup id = u
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n✝ : ?m.31133<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>u : Finset α<VAR>n : ℕ<VAR>hn : n < u.card<GOAL>(powersetCard n.succ u).sup id ≤ u
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n✝ : ?m.31133<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>u : Finset α<VAR>n : ℕ<VAR>hn : n < u.card<GOAL>u ≤ (powersetCard n.succ u).sup id
<VAR>K : Type ?u.600034<VAR>L : Type ?u.600037<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>(aeval (root q)) p = 0
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>closedBall x δ * {y} = closedBall (x * y) δ
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>g : R[X]<VAR>f : C(α, R)<VAR>x : α<GOAL>((aeval f) g) x = eval (f x) g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>g : R[X]<VAR>f : C(α, R)<VAR>x : α<GOAL>∀ (p q : R[X]), ((aeval f) p) x = eval (f x) p → ((aeval f) q) x = eval (f x) q → ((aeval f) (p + q)) x = eval (f x) (p + q)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>g : R[X]<VAR>f : C(α, R)<VAR>x : α<GOAL>∀ (n : ℕ) (a : R), ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)<VAR>a : 𝓞 K<VAR>h_nz : a ≠ 0<VAR>h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)<VAR>a : 𝓞 K<VAR>h_nz : a ≠ 0<VAR>h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)<GOAL>ℚ⟮↑a⟯ = ⊤
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>w₀ : InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : ℝ≥0<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)<VAR>a : 𝓞 K<VAR>h_nz : a ≠ 0<VAR>h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)<VAR>w : InfinitePlace K<GOAL>↑(if w = w₀ then B else 1) ≤ ↑(max B 1)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : Mul α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : DistribMulAction R α<VAR>inst✝ : SMulCommClass R α α<VAR>x : R<VAR>v w : m → α<GOAL>v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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 : ↥(Lp F p μ)<GOAL>f ∈ lpMeas F 𝕜 m p μ ↔ AEStronglyMeasurable' m (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>∅.card ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s<GOAL>(∃ a, s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s<GOAL>(∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}