ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<GOAL>∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj U⦄, (Sieve.functorPushforward G (G.imageSieve iUW)).arrows f → Sieve.pullback f (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈ K.sieves Y_1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>Z : D<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iZU₁ : Z ⟶ G.obj U₁<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<GOAL>Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈ K.sieves Z
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>Z : D<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iZU₁ : Z ⟶ G.obj U₁<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<GOAL>Sieve.pullback iZU₁ (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))) ∈ K.sieves Z
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>Z : D<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iZU₁ : Z ⟶ G.obj U₁<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<GOAL>Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈ K.sieves (G.obj U₁)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<GOAL>Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈ K.sieves (G.obj U₁)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<GOAL>Sieve.functorPushforward G (Sieve.equalizer (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX)) ≤ Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<VAR>U₁ : C<VAR>iU₁U : U₁ ⟶ U<VAR>iU₁W : U₁ ⟶ W<VAR>e₂ : G.map iU₁W = G.map iU₁U ≫ iUW<VAR>Z : D<VAR>U₂ : C<VAR>iU₂U₁ : U₂ ⟶ U₁<VAR>iZU₂ : Z ⟶ G.obj U₂<VAR>e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ iYX = iU₂U₁ ≫ iU₁W ≫ iWX<GOAL>(Sieve.pullback iYX S).arrows (iU₂U₁ ≫ iU₁U ≫ iUY)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<GOAL>S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<GOAL>∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄, (Sieve.functorPushforward G S).arrows f → Sieve.pullback f (Sieve.functorPushforward G S') ∈ K.sieves Y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<VAR>Y : D<VAR>Z : C<VAR>g : Z ⟶ X<VAR>i : Y ⟶ G.obj Z<VAR>hg : S.arrows g<GOAL>Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G S') ∈ K.sieves Y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<VAR>Y : D<VAR>Z : C<VAR>g : Z ⟶ X<VAR>i : Y ⟶ G.obj Z<VAR>hg : S.arrows g<GOAL>Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<VAR>Y : D<VAR>Z : C<VAR>g : Z ⟶ X<VAR>i : Y ⟶ G.obj Z<VAR>hg : S.arrows g<GOAL>Sieve.pullback (G.map g) (Sieve.functorPushforward G S') ∈ K.sieves (G.obj Z)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>S' : Sieve X<VAR>H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f S' ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y<VAR>Y : D<VAR>Z : C<VAR>g : Z ⟶ X<VAR>i : Y ⟶ G.obj Z<VAR>hg : S.arrows g<GOAL>Sieve.functorPushforward G (Sieve.pullback g S') ≤ Sieve.pullback (G.map g) (Sieve.functorPushforward G S')
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁷ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x✝ : α<VAR>s t : Set α<VAR>y✝ z : β<VAR>γ : Type u_3<VAR>inst✝⁶ : LinearOrder γ<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : OrderTopology γ<VAR>δ : Type u_4<VAR>inst✝³ : LinearOrder δ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : OrderTopology δ<VAR>ι : Type u_5<VAR>inst✝ : TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>y : α<VAR>x : ι<VAR>hf : LowerSemicontinuousAt f (g x)<VAR>hg : ContinuousAt g x<VAR>hy : g x = y<GOAL>LowerSemicontinuousAt (fun x => f (g x)) x
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>hfg : ¬f + g = 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hg : ¬g = 0<VAR>hfg : ¬f + g = 0<VAR>hf : ∃ n, (coeff (ModP K v O hv p) p n) f ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hfg : ¬f + g = 0<VAR>hf : ∃ n, (coeff (ModP K v O hv p) p n) f ≠ 0<VAR>hg : ∃ n, (coeff (ModP K v O hv p) p n) g ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ∃ n, (coeff (ModP K v O hv p) p n) f ≠ 0<VAR>hg : ∃ n, (coeff (ModP K v O hv p) p n) g ≠ 0<VAR>hfg : ∃ n, (coeff (ModP K v O hv p) p n) (f + g) ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m : ℕ<VAR>hm : (coeff (ModP K v O hv p) p m) f ≠ 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) g ≠ 0<VAR>k : ℕ<VAR>hk : (coeff (ModP K v O hv p) p k) (f + g) ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) g ≠ 0<VAR>k : ℕ<VAR>hk : (coeff (ModP K v O hv p) p k) (f + g) ≠ 0<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n k : ℕ<VAR>hk : (coeff (ModP K v O hv p) p k) (f + g) ≠ 0<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n k : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0<VAR>hk : (coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0<GOAL>valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n k : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0<VAR>hk : (coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f + (coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k ≤ max (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k) (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n k : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0<VAR>hk : (coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0<VAR>h : ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f + (coeff (ModP K v O hv p) p (max (max m n) k)) g) ≤ ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f)<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f + (coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k ≤ max (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k) (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>m n k : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0<VAR>hk : (coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0<VAR>h : ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f + (coeff (ModP K v O hv p) p (max (max m n) k)) g) ≤ ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) g)<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f + (coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k ≤ max (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k) (ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a : α<VAR>ha hb : a ∉ s<GOAL>{ ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<VAR>hab : a ≠ b<GOAL>{ ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
<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>ι : Type u_4<VAR>p : ι → P<VAR>i0 : ι<GOAL>vectorSpan k (range p) = Submodule.span k (range fun i => p i -ᵥ p i0)
<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>ι : Type u_4<VAR>p : ι → P<VAR>i0 : ι<GOAL>Submodule.span k (range ((fun x => x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i => p i -ᵥ p i0)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : Module K M<VAR>inst✝³ : LieModule K L M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<GOAL>⨆ χ, weightSpace M ⇑χ = ⊤
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : Module K M<VAR>inst✝³ : LieModule K L M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<VAR>this : ⨆ χ, weightSpace M χ = ⊤<GOAL>⨆ χ, weightSpace M ⇑χ = ⊤
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : Module K M<VAR>inst✝³ : LieModule K L M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<VAR>this : ⨆ x, weightSpace M ↑((Weight.equivSetOf K L M) x) = ⊤<GOAL>⨆ χ, weightSpace M ⇑χ = ⊤
<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>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<GOAL>{ obj := F_obj, map := fun {X X'} f => (e X (F_obj X')).symm (f ≫ (e X' (F_obj X')) (𝟙 (F_obj X'))) }.map (f ≫ f') = { obj := F_obj, map := fun {X X'} f => (e X (F_obj X')).symm (f ≫ (e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f ≫ { obj := F_obj, map := fun {X X'} f => (e X (F_obj X')).symm (f ≫ (e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f'
<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>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<GOAL>(f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) = (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫ G.map ({ obj := F_obj, map := fun {X X'} f => (e X (F_obj X')).symm (f ≫ (e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
<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>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>f' : Y✝ ⟶ Z✝<GOAL>(f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) = f ≫ f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 1<VAR>t : L.Term α<GOAL>(R.formula₁ t).Realize v ↔ RelMap R ![Term.realize v t]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 1<VAR>t : L.Term α<GOAL>(RelMap R fun i => Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ ψ : L.Formula α<VAR>v : α → M<VAR>R : L.Relations 1<VAR>t : L.Term α<VAR>x✝ : Fin 1<GOAL>Term.realize v (![t] x✝) = ![Term.realize v t] x✝
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : HasTerminal C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>f ≫ from Q = from P
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : IsLUB s x<GOAL>IsLUB (id '' s) (id x)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>M * 1 = M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>span R ↑M * span R {1} = M
<VAR>α : Type u<VAR>x : Tree α<GOAL>x.numLeaves = x.numNodes + 1