ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (a * c)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (a * c)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (c * b)⁆)) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (-⁅L c, L (b * b)⁆ + -⁅L b, L (c * c)⁆)) = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>U W : Submodule K V<VAR>h : IsCompl U W<GOAL>finrank K ↥U + finrank K ↥W = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>U W : Submodule K V<VAR>h : IsCompl U W<GOAL>finrank K ↥⊤ = finrank K V
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h : s ∩ mulSupport f = ↑t ∩ mulSupport f<VAR>x : α<VAR>hxf : f x ≠ 1<GOAL>x ∈ s ↔ x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h : s ∩ mulSupport f = ↑t ∩ mulSupport f<VAR>x : α<VAR>hxf : x ∈ mulSupport f<GOAL>x ∈ s ↔ x ∈ t
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x : R<VAR>I J : Ideal R<GOAL>I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f.degree < ↑s.card<VAR>degree_g_lt : g.degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>degree_g_lt : g ∈ degreeLT R s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>degree_g_lt : g ∈ degreeLT R s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>(f - g).degree < ↑s.card
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>degree_g_lt : g ∈ degreeLT R s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>f - g ∈ degreeLT R s.card
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Cone (Discrete.functor f)<VAR>m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt<VAR>w : ∀ (j : Discrete J), m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π.app j = s.π.app j<VAR>x : ↑s.pt<GOAL>m x = (lift f s) x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Cone (Discrete.functor f)<VAR>m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.pt<VAR>w : ∀ (j : Discrete J), m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => LinearMap.proj j.as }.π.app j = s.π.app j<VAR>x : ↑s.pt<VAR>j : J<GOAL>m x j = (lift f s) x j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hα : ((fun x => (ofLex x).1) '' s).IsPWO<VAR>hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO<VAR>f : ℕ → Lex (α × β)<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x => (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)<VAR>hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO<VAR>f : ℕ → Lex (α × β)<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x => (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)<VAR>hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO<VAR>f : ℕ → Lex (α × β)<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : Monotone fun n => (ofLex f (g n)).1<GOAL>∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x => (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)<VAR>hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO<VAR>f : ℕ → Lex (α × β)<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : Monotone fun n => (ofLex f (g n)).1<VAR>hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1<GOAL>∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<VAR>hb : b ∈ s<GOAL>eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<VAR>hb : b ∈ s<VAR>A : IsGreatest (s ∩ Icc a b) b<GOAL>eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<VAR>hb : b ∈ s<VAR>A : IsGreatest (s ∩ Icc a b) b<VAR>B : IsLeast (s ∩ Icc b c) b<GOAL>eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>↑((Opens.map (D.ι j).base).obj (⋯.functor.obj U)) = ↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>⇑(D.ι j).base ⁻¹' (⇑(D.ι i).base '' ↑U) = ⇑(D.f j i).base '' (⇑(D.t j i).base ⁻¹' (⇑(D.f i j).base ⁻¹' ↑U))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>⇑((D.mapGlueData (forget C)).ι j ≫ (D.gluedIso (forget C)).inv) ⁻¹' (⇑((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv) '' ↑U) = ⇑(D.f j i).base '' (⇑(D.t j i).base ⁻¹' (⇑(D.f i j).base ⁻¹' ↑U))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>(⇑(preservesColimitIso (forget C) D.diagram.multispan).inv ∘ ⇑(HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv) ∘ ⇑((D.mapGlueData (forget C)).ι j) ⁻¹' (⇑(D.gluedIso (forget C)).inv ∘ ⇑((D.mapGlueData (forget C)).ι i) '' ↑U) = ⇑(D.f j i).base '' (⇑(D.t j i).base ⁻¹' (⇑(D.f i j).base ⁻¹' ↑U))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>⇑((D.mapGlueData (forget C)).ι j) ⁻¹' (⇑(preservesColimitIso (forget C) D.diagram.multispan).inv ∘ ⇑(HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv ⁻¹' (⇑(D.gluedIso (forget C)).inv '' (⇑((D.mapGlueData (forget C)).ι i) '' ↑U))) = ⇑(D.f j i).base '' (⇑(D.t j i).base ⁻¹' (⇑(D.f i j).base ⁻¹' ↑U))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>⇑((D.mapGlueData (forget C)).ι j) ⁻¹' (⇑((D.mapGlueData (forget C)).ι i) '' ↑U) = ⇑(D.f j i).base '' (⇑(D.t j i).base ⁻¹' (⇑(D.f i j).base ⁻¹' ↑U))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>Function.Injective (⇑(preservesColimitIso (forget C) D.diagram.multispan).inv ∘ ⇑(HasColimit.isoOfNatIso (D.diagramIso (forget C))).inv)
<GOAL>∀ o ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, o.Nonempty → (o ∩ {x | Irrational x}).Nonempty
<GOAL>∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → o.Nonempty → (o ∩ {x | Irrational x}).Nonempty
<VAR>a b : ℚ<VAR>hlt : a < b<VAR>a✝ : (Ioo ↑a ↑b).Nonempty<GOAL>(Ioo ↑a ↑b ∩ {x | Irrational x}).Nonempty
<VAR>a b : ℚ<VAR>hlt : a < b<VAR>a✝ : (Ioo ↑a ↑b).Nonempty<GOAL>({x | Irrational x} ∩ Ioo ↑a ↑b).Nonempty
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.dens 1 = gp.b
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>nndist x y = 0 ↔ x = y
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝¹ : IsAffine U<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V ⟶ X<VAR>f' : V ⟶ U<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<GOAL>Q.diagonal f'
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝¹ : IsAffine U<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V ⟶ X<VAR>f' : V ⟶ U<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>Q.diagonal f'
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝¹ : IsAffine U<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V ⟶ X<VAR>f' : V ⟶ U<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>Q.diagonal (pullback.snd f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U✝ V✝ : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝¹ : IsAffine U✝<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V✝ ⟶ X<VAR>f' : V✝ ⟶ U✝<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>U V : Scheme<VAR>f₁ : U ⟶ pullback f g<VAR>f₂ : V ⟶ pullback f g<VAR>hU : IsAffine U<VAR>hV : IsAffine V<VAR>hf₁ : IsOpenImmersion f₁<VAR>hf₂ : IsOpenImmersion f₂<GOAL>Q (pullback.mapDesc f₁ f₂ (pullback.snd f g))
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U✝ V✝ : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝¹ : IsAffine U✝<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V✝ ⟶ X<VAR>f' : V✝ ⟶ U✝<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>U V : Scheme<VAR>f₁ : U ⟶ pullback f g<VAR>f₂ : V ⟶ pullback f g<VAR>hU : IsAffine U<VAR>hV : IsAffine V<VAR>hf₁ : IsOpenImmersion f₁<VAR>hf₂ : IsOpenImmersion f₂<GOAL>Q ((pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g))
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U✝ V✝ : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝¹ : IsAffine U✝<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V✝ ⟶ X<VAR>f' : V✝ ⟶ U✝<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>U V : Scheme<VAR>f₁ : U ⟶ pullback f g<VAR>f₂ : V ⟶ pullback f g<VAR>hU : IsAffine U<VAR>hV : IsAffine V<VAR>hf₁ : IsOpenImmersion f₁<VAR>hf₂ : IsOpenImmersion f₂<VAR>e_1✝ : pullback (pullback.diagonal f) (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g ⋯ ⋯) = pullback (pullback.diagonal f) (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g ⋯ ⋯)<VAR>e_2✝ : pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)<GOAL>(pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g) = pullback.snd (pullback.diagonal f) (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g ⋯ ⋯)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U✝ V✝ : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝¹ : IsAffine U✝<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V✝ ⟶ X<VAR>f' : V✝ ⟶ U✝<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>U V : Scheme<VAR>f₁ : U ⟶ pullback f g<VAR>f₂ : V ⟶ pullback f g<VAR>hU : IsAffine U<VAR>hV : IsAffine V<VAR>hf₁ : IsOpenImmersion f₁<VAR>hf₂ : IsOpenImmersion f₂<GOAL>IsAffine (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝² : HasAffineProperty P Q<VAR>X Y U✝ V✝ : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝¹ : IsAffine U✝<VAR>inst✝ : IsOpenImmersion g<VAR>iV : V✝ ⟶ X<VAR>f' : V✝ ⟶ U✝<VAR>h : IsPullback iV f' f g<VAR>H : P.diagonal f<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>U V : Scheme<VAR>f₁ : U ⟶ pullback f g<VAR>f₂ : V ⟶ pullback f g<VAR>hU : IsAffine U<VAR>hV : IsAffine V<VAR>hf₁ : IsOpenImmersion f₁<VAR>hf₂ : IsOpenImmersion f₂<GOAL>IsOpenImmersion (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g ⋯ ⋯)
<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 t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a✝ : α<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>has : a ∉ s<GOAL>InjOn f (insert a s) ↔ InjOn f s ∧ f a ∉ f '' s
<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 t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a✝ : α<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>has : a ∉ s<GOAL>(InjOn f s ∧ InjOn f {a} ∧ ∀ x ∈ s, ∀ y ∈ {a}, f x ≠ f y) ↔ InjOn f s ∧ f a ∉ f '' s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<VAR>this : Nonempty ↥H<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<VAR>this : Nonempty ↥H<VAR>h' : Nat.card ↥H ≠ 0<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<VAR>this✝ : Nonempty ↥H<VAR>h' : Nat.card ↥H ≠ 0<VAR>this : Finite G<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<VAR>this✝² : Nonempty ↥H<VAR>h' : Nat.card ↥H ≠ 0<VAR>this✝¹ : Finite G<VAR>this✝ : Fintype G<VAR>this : Fintype ↥H<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>this✝² : Nonempty ↥H<VAR>h' : Nat.card ↥H ≠ 0<VAR>this✝¹ : Finite G<VAR>this✝ : Fintype G<VAR>this : Fintype ↥H<VAR>h : Fintype.card ↥H = Fintype.card G<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>this✝² : Nonempty ↥H<VAR>h' : Nat.card ↥H ≠ 0<VAR>this✝¹ : Finite G<VAR>this✝ : Fintype G<VAR>this : Fintype ↥H<VAR>h : Fintype.card ↥H = Fintype.card G<GOAL>Fintype.card ↑↑H = Fintype.card ↥H
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s : ↥S<VAR>t : R<VAR>hst : t * ↑s ∈ S<GOAL>r /ₒ s = t • r /ₒ ⟨t * ↑s, hst⟩
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s : ↥S<VAR>t : R<VAR>hst : t * ↑s ∈ S<GOAL>(r, s) ≈ (t • r, ⟨t * ↑s, hst⟩)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>r : α → α → Prop<VAR>inst✝ : IsTrans α r<VAR>f : Fin (n + 1) → α<VAR>a : α<GOAL>((fun x x_1 => x < x_1) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R<VAR>hf : ∀ (φ : MvPolynomial σ R), f φ = φ<VAR>x : σ → R<GOAL>comap f x = x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R<VAR>hf : ∀ (φ : MvPolynomial σ R), f φ = φ<VAR>x : σ → R<GOAL>f = AlgHom.id R (MvPolynomial σ R)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R<VAR>hf : ∀ (φ : MvPolynomial σ R), f φ = φ<VAR>x : σ → R<VAR>φ : σ<GOAL>f (X φ) = (AlgHom.id R (MvPolynomial σ R)) (X φ)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>c : 𝕜<GOAL>HasSum f c ↔ HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>c : 𝕜<GOAL>HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c) → HasSum f c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>c : 𝕜<VAR>h₁ : HasSum (fun x => re (f x)) (re c)<VAR>h₂ : HasSum (fun x => im (f x)) (im c)<GOAL>HasSum f c
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>r : R<VAR>x✝ : IsUnit (X - C r)<VAR>g : R[X]<VAR>_hfg : (X - C r) * g = 1<VAR>hgf : g * (X - C r) = 1<GOAL>0 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<GOAL>↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<GOAL>filter (fun x => a ≠ x) ↑m + ↑(replicate (count a ↑m) a) = ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<VAR>b : α<GOAL>count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<VAR>b : α<GOAL>((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<GOAL>((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Sym α n<VAR>b : α<VAR>h : a ≠ b<GOAL>((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑(∂ 𝒜).card / ↑((Fintype.card α).choose (r - 1))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>hr' : Fintype.card α < r<GOAL>↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑(∂ 𝒜).card / ↑((Fintype.card α).choose (r - 1))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>hr' : r ≤ Fintype.card α<GOAL>↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑(∂ 𝒜).card / ↑((Fintype.card α).choose (r - 1))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>hr' : r ≤ Fintype.card α<VAR>h𝒜 : 𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1)<GOAL>↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑(∂ 𝒜).card / ↑((Fintype.card α).choose (r - 1))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>hr' : r ≤ Fintype.card α<VAR>h𝒜 : 𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1)<GOAL>𝒜.card * (Fintype.card α).choose (r - 1) ≤ (∂ 𝒜).card * (Fintype.card α).choose r
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>hr' : r ≤ Fintype.card α<VAR>h𝒜 : 𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1)<GOAL>0 < (Fintype.card α).choose r
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>hr : r ≠ 0<VAR>hr' : r ≤ Fintype.card α<VAR>h𝒜 : 𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1)<GOAL>0 < (Fintype.card α).choose (r - 1)
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ ↑n
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ n