ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<GOAL>𝓝 (x, y) = (𝓝 x).prod (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>∀ {a b : α}, p a ∧ p b → f a b * f b a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>p a ∧ p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>p b ∧ p c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p✝ r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>p a ∧ p c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ ↥⊤.direction = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>(swap 0 1).signAux = ∏ x ∈ {⟨1, 0⟩}, if (swap 0 1) x.fst ≤ (swap 0 1) x.snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a : (_ : Fin (n + 2)) × Fin (n + 2)<VAR>ha₁ : a ∈ finPairsLT (n + 2)<VAR>ha₂ : a ∉ {⟨1, 0⟩}<GOAL>(if (swap 0 1) a.fst ≤ (swap 0 1) a.snd then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ a₂ : Fin (n + 2)<VAR>ha₁ : ⟨a₁, a₂⟩ ∈ finPairsLT (n + 2)<VAR>ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}<GOAL>(if (swap 0 1) ⟨a₁, a₂⟩.fst ≤ (swap 0 1) ⟨a₁, a₂⟩.snd then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ a₂ : Fin (n + 2)<VAR>ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : a₂ < a₁<GOAL>(if (swap 0 1) ⟨a₁, a₂⟩.fst ≤ (swap 0 1) ⟨a₁, a₂⟩.snd then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ a₂ : Fin (n + 2)<VAR>ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : a₂ < a₁<GOAL>(if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₂ : Fin (n + 2)<VAR>ha₂ : ⟨0, a₂⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : a₂ < 0<GOAL>(if (swap 0 1) 0 ≤ (swap 0 1) a₂ then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ a₂ : Fin (n + 2)<VAR>ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : a₂ < a₁<VAR>H : 0 < a₁<GOAL>(if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ : Fin (n + 2)<VAR>H : 0 < a₁<VAR>ha₂ : ⟨a₁, 0⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : 0 < a₁<GOAL>(if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a₁ a₂ : Fin (n + 2)<VAR>ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}<VAR>ha₁ : a₂ < a₁<VAR>H : 0 < a₁<VAR>H' : 0 < a₂<GOAL>(if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsRefl α r<GOAL>(insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r
<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>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G✝ : C ⥤ D<VAR>hG : CompatiblePreserving K G✝<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ.val) T<VAR>h : x✝.Compatible<VAR>hF₁ : CompatiblePreserving K F<VAR>hF₂ : CoverPreserving J K F<VAR>G : SheafOfTypes K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : FamilyOfElements (F.op ⋙ G.val) S.arrows<VAR>hx : x.Compatible<GOAL>∃! t, x.IsAmalgamation 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>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G✝ : C ⥤ D<VAR>hG : CompatiblePreserving K G✝<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ.val) T<VAR>h : x✝.Compatible<VAR>hF₁ : CompatiblePreserving K F<VAR>hF₂ : CoverPreserving J K F<VAR>G : SheafOfTypes K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : FamilyOfElements (F.op ⋙ G.val) S.arrows<VAR>hx : x.Compatible<GOAL>∃ x_1, x.IsAmalgamation x_1
<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>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G✝ : C ⥤ D<VAR>hG : CompatiblePreserving K G✝<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ.val) T<VAR>h : x✝.Compatible<VAR>hF₁ : CompatiblePreserving K F<VAR>hF₂ : CoverPreserving J K F<VAR>G : SheafOfTypes K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : FamilyOfElements (F.op ⋙ G.val) S.arrows<VAR>hx : x.Compatible<GOAL>∀ (y₁ y₂ : (F.op ⋙ G.val).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
<VAR>α : Type u<GOAL>castFreeCommRing = Functor.map fun l => ↑l
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>↑x = (fun l => ↑l) <$> x
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x = (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x = (FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
<VAR>α : Type u<VAR>x : FreeRing α<GOAL>∀ (x : FreeMonoid α), ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) = ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) x
<VAR>α : Type u<VAR>x : FreeRing α<VAR>L : FreeMonoid α<GOAL>↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) = ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) L
<VAR>α : Type u<VAR>x : FreeRing α<VAR>L : FreeMonoid α<GOAL>(FreeMonoid.lift FreeCommRing.of) L = (fun x => FreeAbelianGroup.of ↑x) L
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n n' : M<VAR>g : n ⟶ n'<VAR>X : C<GOAL>(F.map g).app ((F.obj m).obj X) ≫ (F.μ m n').app X = (F.μ m n).app X ≫ (F.map (m ◁ g)).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n n' : M<VAR>g : n ⟶ n'<VAR>X : C<GOAL>(F.map g).app ((F.obj m).obj X) ≫ (F.μ m n').app X = (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (F.μ m n').app X
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₂ : List β<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<VAR>a₁ a₂ : α<VAR>n : a₁ ≠ a₂<VAR>x : α × β<VAR>h₁ : x ∈ map (Prod.mk a₁) l₂<VAR>h₂ : x ∈ map (Prod.mk a₂) l₂<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₂ : List β<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<VAR>a₁ a₂ : α<VAR>n : a₁ ≠ a₂<VAR>b₁ : β<VAR>left✝ : b₁ ∈ l₂<VAR>h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂<VAR>h₂ : (a₁, b₁) ∈ map (Prod.mk a₂) l₂<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₂ : List β<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<VAR>a₁ : α<VAR>b₁ : β<VAR>left✝ : b₁ ∈ l₂<VAR>h₁ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂<VAR>n : a₁ ≠ a₁<VAR>h₂ : (a₁, b₁) ∈ map (Prod.mk a₁) l₂<VAR>mb₂ : b₁ ∈ l₂<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : ℕ →o (Submodule R M)ᵒᵈ<GOAL>EventuallyConst (⇑f) atTop
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : ℕ →o (Submodule R M)ᵒᵈ<GOAL>∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : a ≠ 0<VAR>hab : a ∣ b<GOAL>a ≤ b → b ≠ 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 0 < a<VAR>hab : a ∣ b<GOAL>a ≤ b → 0 < b
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<GOAL>↑p ^ (k + 1 + 1) ∣ a ^ p ^ (k + 1) - b ^ p ^ (k + 1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<GOAL>↑p * ↑p ^ (k + 1) ∣ (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<GOAL>↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<VAR>f : R →+* R ⧸ span {↑p} := mk (span {↑p})<GOAL>↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<VAR>f : R →+* R ⧸ span {↑p} := mk (span {↑p})<VAR>hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0<GOAL>↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<VAR>f : R →+* R ⧸ span {↑p} := mk (span {↑p})<VAR>h : f a = f b<VAR>hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0<GOAL>↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>k : ℕ<VAR>ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k<VAR>f : R →+* R ⧸ span {↑p} := mk (span {↑p})<VAR>h : f a = f b<VAR>hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0<GOAL>↑p = 0
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ l₁ ∩ l₂<GOAL>a ∈ l₂
<VAR>n m : ℕ<VAR>h : Nonempty (Fin n ↪ Fin m)<GOAL>n ≤ m
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>0 < z⁻¹ ↔ 0 < z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>h : 0 < z⁻¹<GOAL>0 < z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>h : 0 < z⁻¹<GOAL>0 < z⁻¹⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : Set (Sym2 α)<VAR>x y : α<GOAL>ToRel s x y → ToRel s y x
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>I : Ideal A<VAR>x y : A<VAR>n : ℕ<VAR>hxy : x ≡ y [SMOD I]<GOAL>x ^ n ≡ y ^ n [SMOD I]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>I : Ideal A<VAR>x y : A<VAR>n : ℕ<VAR>hxy : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y<GOAL>(Ideal.Quotient.mk I) x ^ n = (Ideal.Quotient.mk I) y ^ n
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<GOAL>IsUnramified k (mk φ) ↔ ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<GOAL>IsUnramified k (mk φ)
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬IsUnramified k (mk φ)<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : (mk φ).IsComplex ∧ ((mk φ).comap (algebraMap k K)).IsReal<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))<VAR>this✝ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this : Algebra K ℂ := φ.toAlgebra<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>φ' : K →ₐ[k] ℂ := let __src := star φ; { toRingHom := __src, commutes' := ⋯ }<GOAL>False
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>φ : K →+* ℂ<VAR>H : ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1<VAR>hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))<VAR>this✝² : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝¹ : Algebra K ℂ := φ.toAlgebra<VAR>this✝ : IsScalarTower k K ℂ<VAR>φ' : K →ₐ[k] ℂ := let __src := star φ; { toRingHom := __src, commutes' := ⋯ }<VAR>this : ComplexEmbedding.IsConj φ (φ'.restrictNormal' K)<GOAL>False
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>s : Set M<GOAL>x ∈ span R (insert y s) ↔ ∃ a, x + a • y ∈ span R s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>s : Set M<GOAL>(∃ a, ∃ z ∈ span R s, x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : y ∈ interior s<GOAL>UniqueDiffWithinAt ℝ s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : y ∈ interior s<GOAL>y - x ∈ interior (tangentConeAt ℝ s x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : y ∈ interior s<GOAL>tangentConeAt ℝ s x ∈ 𝓝 (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : interior s ∈ 𝓝 y<GOAL>tangentConeAt ℝ s x ∈ 𝓝 (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : interior s ∈ 𝓝 y<GOAL>(fun x_1 => x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : interior s ∈ 𝓝 y<VAR>z : G<VAR>zs : z ∈ interior s<GOAL>(fun x_1 => x_1 - x) z ∈ tangentConeAt ℝ s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>x : G<VAR>hx : x ∈ closure s<VAR>y : G<VAR>hy : interior s ∈ 𝓝 y<VAR>z : G<VAR>zs : z ∈ interior s<GOAL>openSegment ℝ x z ⊆ interior s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X : Dial C<GOAL>(X.tensorObj tensorUnit).rel = (Subobject.pullback (prod.map (prod.rightUnitor X.src).hom (prod.rightUnitor X.tgt).hom)).obj X.rel
<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>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>n : ℕ<VAR>hn : Even n<GOAL>χ ^ n = 1
<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>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>n : ℕ<VAR>hn : Even (2 * n)<GOAL>χ ^ (2 * n) = 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<GOAL>adjoin F ↑∅ = ⊥