ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<VAR>hspan0 : span {x} ≠ ⊥<VAR>span_le : span {x} ≤ P<GOAL>P = span {x}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<VAR>hspan0 : span {x} ≠ ⊥<VAR>span_le : span {x} ≤ P<GOAL>P ∣ span {x}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<VAR>hspan0 : span {x} ≠ ⊥<VAR>span_le : span {x} ≤ P<GOAL>normalizedFactors (span {x}) ≤ normalizedFactors P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<VAR>hspan0 : span {x} ≠ ⊥<VAR>span_le : span {x} ≤ P<GOAL>∀ (a : Ideal R), Multiset.count a (normalizedFactors (span {x})) ≤ if a = P then 1 else 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>p -ᵥ p2 ∈ s.direction ↔ p2 ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>(∃ p2_1 ∈ s, p -ᵥ p2 = p -ᵥ p2_1) ↔ p2 ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>x : M<VAR>x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m<VAR>y : M<VAR>hy : r ^ m • y = x<GOAL>r ^ n • r ^ (m - n) • y = x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<GOAL>HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<GOAL>HasSum (fun i => ↑(fourierBasis.repr f) i • fourierLp 2 i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<GOAL>HasSum (fun i => ↑(fourierBasis.repr f) i • (fun i => fourierBasis.repr.symm (lp.single 2 i 1)) i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>x : β<VAR>e : α ≃ { y // y ≠ x }<VAR>b : { y // y ≠ x }<GOAL>(↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>x : β<VAR>e : α ≃ { y // y ≠ x }<VAR>b : { y // y ≠ x }<GOAL>↑b = x → False
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>i : β → α<VAR>hi : Injective i<VAR>f : α → ℝ≥0<VAR>hf : Summable fun i => ↑(f i)<GOAL>tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>i : β → α<VAR>hi : Injective i<VAR>f : α → ℝ≥0<VAR>hf : Summable f<GOAL>tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u v : β → α<VAR>p : β → Prop<VAR>h : ∀ᶠ (a : β) in f, p a → u a = v a<GOAL>blimsup u f p = blimsup v f p
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>n : ℕ<VAR>t : R<VAR>ht : ‖t‖ < 1<VAR>this : Summable fun n => t ^ n<GOAL>∑ i ∈ range n, t ^ i + ∑' (i : ℕ), t ^ (i + n) = ∑ i ∈ range n, t ^ i + t ^ n * inverse (1 - t)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>n : ℕ<VAR>t : R<VAR>ht : ‖t‖ < 1<VAR>this : Summable fun n => t ^ n<GOAL>∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<GOAL>take (n + 1) (b :: l) = List.filter (fun a => elem a (take (n + 1) (b :: l))) (b :: l)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<GOAL>b :: List.filter (fun a => elem a (take n l)) l = b :: List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<GOAL>List.filter (fun a => elem a (take n l)) l = List.filter (fun a => elem a (b :: List.filter (fun a => elem a (take n l)) l)) l
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<GOAL>∀ x ∈ l, elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b✝ : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l : List α<VAR>n : ℕ<VAR>hl : (b :: l).Nodup<VAR>x : α<VAR>hx : x ∈ l<VAR>this : x ≠ b<GOAL>elem x (take n l) = elem x (b :: List.filter (fun a => elem a (take n l)) l)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>P Q R : C<VAR>f✝ f' : P ⟶ Q<VAR>g✝ g' : Q ⟶ R<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasLimit (parallelPair f 0)<VAR>w : kernel.ι f = 0<VAR>P✝ : C<VAR>g : P✝ ⟶ X<VAR>h : g ≫ f = 0<GOAL>g = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).Ψ₃ = Polynomial.map f W.Ψ₃
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>3 * X ^ 4 + C (f W.b₂) * X ^ 3 + 3 * C (f W.b₄) * X ^ 2 + 3 * C (f W.b₆) * X + C (f W.b₈) = Polynomial.map f (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈)
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (y + 1) d (x + 1) 1<VAR>yx : SqLe (x + 1) 1 y.succ d<GOAL>{ re := ↑(x + 1), im := -[y+1] } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (y + 1) d (x + 1) 1<VAR>yx : SqLe (x + 1) 1 y.succ d<VAR>t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := le_antisymm yx xy<GOAL>{ re := ↑(x + 1), im := -[y+1] } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (y + 1) d (x + 1) 1<VAR>yx : SqLe (x + 1) 1 y.succ d<VAR>t : (x + 1) * (x + 1) = d * y.succ * y.succ<GOAL>{ re := ↑(x + 1), im := -[y+1] } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (x + 1) 1 (y + 1) d<VAR>yx : SqLe (y + 1) d x.succ 1<GOAL>{ re := -[x+1], im := ↑(y + 1) } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (x + 1) 1 (y + 1) d<VAR>yx : SqLe (y + 1) d x.succ 1<VAR>t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx<GOAL>{ re := -[x+1], im := ↑(y + 1) } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>xy : SqLe (x + 1) 1 (y + 1) d<VAR>yx : SqLe (y + 1) d x.succ 1<VAR>t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)<GOAL>{ re := -[x+1], im := ↑(y + 1) } = 0
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = (G.edgeFinset \ G.incidenceFinset t ∪ image (fun x => s(x, t)) (G.neighborFinset s)) \ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>ha : G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = ((G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}).toFinset
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i j : ι<VAR>inst✝³ : K.HasHomology i<VAR>inst✝² : K.HasHomology j<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : L.HasHomology j<GOAL>opcyclesMap φ i ≫ L.opcyclesToCycles i j = K.opcyclesToCycles i j ≫ cyclesMap φ j
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>a : A<VAR>hlt : ¬D a ≤ supDegree D p<GOAL>p a = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>a : A<VAR>hlt : p a ≠ 0<GOAL>D a ≤ supDegree D p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<GOAL>BijOn f (invFunOn f s '' t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<GOAL>MapsTo f (invFunOn f s '' t) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : SurjOn f s t<VAR>y : β<VAR>hy : y ∈ t<GOAL>f (invFunOn f s y) ∈ t
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice α✝<VAR>α : Type u_6<VAR>inst✝ : ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a = v a<GOAL>limsup u f = limsup v f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice α✝<VAR>α : Type u_6<VAR>inst✝ : ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a = v a<GOAL>sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice α✝<VAR>α : Type u_6<VAR>inst✝ : ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>u v : α → β<VAR>h : ∀ᶠ (a : α) in f, u a = v a<VAR>b : β<GOAL>b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>this : (f - 0).LimZero<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>this✝ : (f - 0).LimZero<VAR>this : f + g ≈ g<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>this✝ : (f - 0).LimZero<VAR>this : f + g ≈ g<VAR>h1 : (f + g).norm = g.norm<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>this✝ : (f - 0).LimZero<VAR>this : f + g ≈ g<VAR>h1 : (f + g).norm = g.norm<VAR>h2 : f.norm = 0<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>this : (g - 0).LimZero<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>this✝ : (g - 0).LimZero<VAR>this : f + g ≈ f<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>this✝ : (g - 0).LimZero<VAR>this : f + g ≈ f<VAR>h1 : (f + g).norm = f.norm<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>this✝ : (g - 0).LimZero<VAR>this : f + g ≈ f<VAR>h1 : (f + g).norm = f.norm<VAR>h2 : g.norm = 0<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<GOAL>padicNorm p (↑(f + g) (stationaryPoint hfg)) = max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))<GOAL>padicNorm p (↑(f + g) (stationaryPoint hfg)) = max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<VAR>hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))<GOAL>ℕ
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))<GOAL>ℕ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.add P Q = W.dblU P • ![1, 1, 0]
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<GOAL>Continuous (f.val.app (Opposite.op (of PUnit.{u + 1})))
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<GOAL>Continuous (f.val.app (Opposite.op (of PUnit.{u + 1})) ∘ LightCondSet.coinducingCoprod X)
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<GOAL>∀ (i : (S : LightProfinite) × X.val.obj (Opposite.op S)), Continuous fun a => (f.val.app (Opposite.op (of PUnit.{u + 1})) ∘ LightCondSet.coinducingCoprod X) ⟨i, a⟩
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => (f.val.app (Opposite.op (of PUnit.{u + 1})) ∘ LightCondSet.coinducingCoprod X) ⟨⟨S, x⟩, a⟩
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => f.val.app (Opposite.op (of PUnit.{u + 1})) (X.val.map (LightProfinite.const S a).op x)
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<VAR>this : (fun a => f.val.app (Opposite.op (of PUnit.{u + 1})) (X.val.map (LightProfinite.const S a).op x)) = fun a => Y.val.map (LightProfinite.const S a).op (f.val.app (Opposite.op S) x)<GOAL>Continuous fun a => f.val.app (Opposite.op (of PUnit.{u + 1})) (X.val.map (LightProfinite.const S a).op x)
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<VAR>this : (fun a => f.val.app (Opposite.op (of PUnit.{u + 1})) (X.val.map (LightProfinite.const S a).op x)) = fun a => Y.val.map (LightProfinite.const S a).op (f.val.app (Opposite.op S) x)<GOAL>Continuous fun a => Y.val.map (LightProfinite.const S a).op (f.val.app (Opposite.op S) x)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>α : SmallHom W X Y<VAR>β : SmallHom W Y Z<GOAL>(equiv W L) (α.comp β) = (equiv W L) α ≫ (equiv W L) β
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>α : SmallHom W X Y<VAR>β : SmallHom W Y Z<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<GOAL>(equiv W L) (α.comp β) = (equiv W L) α ≫ (equiv W L) β
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>α : SmallHom W X Y<VAR>β : SmallHom W Y Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<GOAL>(equiv W L) (α.comp β) = (equiv W L) α ≫ (equiv W L) β
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>β : SmallHom W Y Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<VAR>α : W.Q.obj X ⟶ W.Q.obj Y<GOAL>(equiv W L) (comp ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α) β) = (equiv W L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α) ≫ (equiv W L) β
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<VAR>α : W.Q.obj X ⟶ W.Q.obj Y<VAR>β : W.Q.obj Y ⟶ W.Q.obj Z<GOAL>(equiv W L) (comp ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)) = (equiv W L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α) ≫ (equiv W L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<VAR>α : W.Q.obj X ⟶ W.Q.obj Y<VAR>β : W.Q.obj Y ⟶ W.Q.obj Z<GOAL>(homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z)) ((homEquiv W W.Q W.Q) ((homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫ (homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))))) = (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫ (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<VAR>α : W.Q.obj X ⟶ W.Q.obj Y<VAR>β : W.Q.obj Y ⟶ W.Q.obj Z<GOAL>(homEquiv W W.Q L) ((homEquiv W W.Q W.Q) ((homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫ (homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))) = (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫ (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝² : HasSmallLocalizedHom W X Y<VAR>inst✝¹ : HasSmallLocalizedHom W Y Z<VAR>inst✝ : HasSmallLocalizedHom W X Z<VAR>this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y<VAR>this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z<VAR>α : W.Q.obj X ⟶ W.Q.obj Y<VAR>β : W.Q.obj Y ⟶ W.Q.obj Z<GOAL>(homEquiv W W.Q L) ((homEquiv W W.Q W.Q) ((homEquiv W W.Q W.Q) α ≫ (homEquiv W W.Q W.Q) β)) = (homEquiv W W.Q L) α ≫ (homEquiv W W.Q L) β
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<GOAL>weightedTotalDegree' w 0 = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<GOAL>∀ (a_1 : α) (s : Multiset α), (a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ b ∈ a_1 ::ₘ s, a ∣ b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>s : Set α<GOAL>s ×ˢ univ = Prod.fst ⁻¹' s
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<GOAL>∃ σ, σ y = x