ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<GOAL>orderOf f ∣ 1
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<VAR>c : ℕ<VAR>hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c<GOAL>orderOf f ∣ 1
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<VAR>c : ℕ<VAR>hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c<GOAL>1 = orderOf f * c
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<VAR>c : ℕ<VAR>hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c<GOAL>(∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = 1
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<VAR>c : ℕ<VAR>hc : (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c<GOAL>∀ (a : ι) (b : a ≠ i), (Fintype.card (H ↑⟨a, b⟩)).Coprime (Fintype.card (H i))
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a n : M<VAR>P : Submonoid M<GOAL>powers n ≤ P ↔ n ∈ P
<VAR>R : Type u_1<VAR>inst✝⁴ : Semiring R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module R S<VAR>inst✝¹ : IsScalarTower R S S<VAR>inst✝ : SMulCommClass R S S<VAR>x y : S<VAR>hc : Commute x y<GOAL>Commute (p.smeval x) (q.smeval y)
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<GOAL>lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>this : IsWellOrder (ULift.{max v w, u} α) (⇑Equiv.ulift ⁻¹'o r)<GOAL>lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>this✝ : IsWellOrder (ULift.{max v w, u} α) (⇑Equiv.ulift ⁻¹'o r)<VAR>this : IsWellOrder (ULift.{max u w, v} β) (⇑Equiv.ulift ⁻¹'o s)<GOAL>lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((fun x => (f x.fst).map x.snd ≫ 𝒰.map x.fst) ((fun x => ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.choose ⋯)⟩) x)).val.base
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<GOAL>x ∈ Set.range ⇑((fun x => (f x.fst).map x.snd ≫ 𝒰.map x.fst) ((fun x => ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.choose ⋯)⟩) x)).val.base
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<VAR>hy : (𝒰.map (𝒰.f x)).val.base y = x<GOAL>x ∈ Set.range ⇑((fun x => (f x.fst).map x.snd ≫ 𝒰.map x.fst) ((fun x => ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.choose ⋯)⟩) x)).val.base
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<VAR>hy : (𝒰.map (𝒰.f x)).val.base y = x<VAR>z : ↑↑((f (𝒰.f x)).obj ((f (𝒰.f x)).f y)).toPresheafedSpace<VAR>hz : ((f (𝒰.f x)).map ((f (𝒰.f x)).f y)).val.base z = y<GOAL>x ∈ Set.range ⇑((fun x => (f x.fst).map x.snd ≫ 𝒰.map x.fst) ((fun x => ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.choose ⋯)⟩) x)).val.base
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<VAR>hy : (𝒰.map (𝒰.f x)).val.base y = x<VAR>z : ↑↑((f (𝒰.f x)).obj ((f (𝒰.f x)).f y)).toPresheafedSpace<VAR>hz : ((f (𝒰.f x)).map ((f (𝒰.f x)).f y)).val.base z = y<GOAL>x ∈ Set.range ⇑((f (𝒰.f x)).map ((f (𝒰.f x)).f y) ≫ 𝒰.map (𝒰.f x)).val.base
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<VAR>hy : (𝒰.map (𝒰.f x)).val.base y = x<VAR>z : ↑↑((f (𝒰.f x)).obj ((f (𝒰.f x)).f y)).toPresheafedSpace<VAR>hz : ((f (𝒰.f x)).map ((f (𝒰.f x)).f y)).val.base z = y<GOAL>((f (𝒰.f x)).map ((f (𝒰.f x)).f y) ≫ 𝒰.map (𝒰.f x)).val.base z = x
<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace := Exists.choose ⋯<VAR>hy : (𝒰.map (𝒰.f x)).val.base y = x<VAR>z : ↑↑((f (𝒰.f x)).obj ((f (𝒰.f x)).f y)).toPresheafedSpace<VAR>hz : ((f (𝒰.f x)).map ((f (𝒰.f x)).f y)).val.base z = y<GOAL>(𝒰.map (𝒰.f x)).val.base (((f (𝒰.f x)).map ((f (𝒰.f x)).f y)).val.base z) = x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p n : ℕ<VAR>hp : Nat.Prime p<GOAL>cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n) ^ i
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<GOAL>cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n) ^ i
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<VAR>n_n : ℕ<VAR>n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i<GOAL>cyclotomic (p ^ (n_n + 1 + 1)) R = ∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<VAR>n_n : ℕ<VAR>n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i<GOAL>(∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * ∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R = X ^ p ^ (n_n + 1 + 1) - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<VAR>n_n : ℕ<VAR>n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i<GOAL>(∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) = X ^ p ^ (n_n + 1 + 1) - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<VAR>n_n : ℕ<VAR>n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1<GOAL>(∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) = X ^ p ^ (n_n + 1 + 1) - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : ∀ (m : ℕ), cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔ (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1<VAR>n_n : ℕ<VAR>n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1<GOAL>X ^ (p ^ (n_n + 1) * p) = X ^ p ^ (n_n + 1 + 1)
<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 : Set P<GOAL>(affineSpan k s).direction = vectorSpan k 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 : Set P<GOAL>(affineSpan k s).direction ≤ vectorSpan k 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 : Set P<GOAL>vectorSpan k s ≤ (affineSpan k s).direction
<VAR>α : Type u_1<VAR>x : α<VAR>t : Ordnode α<GOAL>Any (Eq x) t ↔ x ∈ t.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>h : x ∈ f a ∨ x ∈ g a<GOAL>x ∈ k a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>h : x ∈ f a ∨ x ∈ g a<VAR>this : (k a).Dom<GOAL>x ∈ k a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>h : x ∈ f a ∨ x ∈ g a<VAR>this : (k a).Dom<GOAL>(k a).get this = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>this : (k a).Dom<VAR>h : x ∈ f a<VAR>h' : (k a).get this ∈ f a<GOAL>(k a).get this = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>this : (k a).Dom<VAR>h : x ∈ f a<VAR>h' : (k a).get this ∈ g a<GOAL>(k a).get this = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>this : (k a).Dom<VAR>h : x ∈ g a<VAR>h' : (k a).get this ∈ f a<GOAL>(k a).get this = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<VAR>k : α →. σ<VAR>hk : Partrec k<VAR>K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)<VAR>a : α<VAR>x : σ<VAR>this : (k a).Dom<VAR>h : x ∈ g a<VAR>h' : (k a).get this ∈ g a<GOAL>(k a).get this = x
<VAR>R✝ : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : CommSemiring S✝<VAR>inst✝¹² : Semiring A<VAR>inst✝¹¹ : Semiring B<VAR>inst✝¹⁰ : Algebra R✝ S✝<VAR>inst✝⁹ : Algebra R✝ A<VAR>inst✝⁸ : Algebra R✝ B<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R✝ M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>h : FiniteType R S<VAR>inst✝ : IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R✝ : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : CommSemiring S✝<VAR>inst✝¹² : Semiring A<VAR>inst✝¹¹ : Semiring B<VAR>inst✝¹⁰ : Algebra R✝ S✝<VAR>inst✝⁹ : Algebra R✝ A<VAR>inst✝⁸ : Algebra R✝ B<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R✝ M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>h : FiniteType R S<VAR>inst✝ : IsNoetherianRing R<VAR>s : Finset S<VAR>hs : adjoin R ↑s = ⊤<GOAL>IsNoetherianRing S
<VAR>R✝ : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : CommSemiring S✝<VAR>inst✝¹² : Semiring A<VAR>inst✝¹¹ : Semiring B<VAR>inst✝¹⁰ : Algebra R✝ S✝<VAR>inst✝⁹ : Algebra R✝ A<VAR>inst✝⁸ : Algebra R✝ B<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R✝ M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>h : FiniteType R S<VAR>inst✝ : IsNoetherianRing R<VAR>s : Finset S<VAR>hs : adjoin R ↑s = ⊤<GOAL>Surjective ⇑(MvPolynomial.aeval Subtype.val).toRingHom
<VAR>R✝ : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : CommSemiring S✝<VAR>inst✝¹² : Semiring A<VAR>inst✝¹¹ : Semiring B<VAR>inst✝¹⁰ : Algebra R✝ S✝<VAR>inst✝⁹ : Algebra R✝ A<VAR>inst✝⁸ : Algebra R✝ B<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R✝ M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>h : FiniteType R S<VAR>inst✝ : IsNoetherianRing R<VAR>s : Finset S<VAR>hs : adjoin R ↑s = ⊤<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>h₁ : p.leadingCoeff = 0<GOAL>p.leadingCoeff * q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>h₁ : q.leadingCoeff = 0<GOAL>p.leadingCoeff * q.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).degree = ↑(p.natDegree + q.natDegree)
<VAR>m : ℕ∞<VAR>n : ℕ<GOAL>↑m ≤ ↑n ↔ m ≤ ↑n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>Z : C<VAR>f : M.X ⟶ Z<GOAL>M.comul ≫ (M.counit ⊗ f) = f ≫ (λ_ Z).inv
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>s : Set G<VAR>g✝ g : G<VAR>H : Subgroup G<GOAL>zpowers g ≤ H ↔ g ∈ H
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<GOAL>(MonoidHom.snd M N).comp toProd = snd
<GOAL>HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
<VAR>h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s<GOAL>HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
<VAR>h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s<VAR>h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s<GOAL>HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
<VAR>h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s<VAR>h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s<GOAL>deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrder β<VAR>x y : β<GOAL>↑(min x y) = min ↑x ↑y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>n : ℕ<GOAL>vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>n : ℕ<GOAL>∀ (x : Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x<VAR>s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b<GOAL>Icc a b ⊆ {x | f x ≤ B x}
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x<VAR>s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b<VAR>A : ContinuousOn (fun x => (f x, B x)) (Icc a b)<GOAL>Icc a b ⊆ {x | f x ≤ B x}
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x<VAR>s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b<VAR>A : ContinuousOn (fun x => (f x, B x)) (Icc a b)<VAR>this : IsClosed s<GOAL>Icc a b ⊆ {x | f x ≤ B x}
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x<VAR>s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b<VAR>A : ContinuousOn (fun x => (f x, B x)) (Icc a b)<VAR>this : IsClosed s<GOAL>∀ x ∈ {x | f x ≤ B x} ∩ Ico a b, ∀ y ∈ Ioi x, ({x | f x ≤ B x} ∩ Ioc x y).Nonempty
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∃ b, o.derivBFamily f b = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi a = a