ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>φ : L.Formula α<VAR>g : α → β<VAR>v : β → M<GOAL>(relabel g φ).Realize v ↔ φ.Realize (v ∘ g)
<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>φ : L.Formula α<VAR>g : α → β<VAR>v : β → M<GOAL>BoundedFormula.Realize φ (Sum.elim v (default ∘ Fin.cast ⋯) ∘ Sum.inl ∘ g) (default ∘ natAdd 0) = BoundedFormula.Realize φ (v ∘ g) default
<VAR>w x y z r : ℝ<VAR>l : List ℝ≥0<GOAL>(List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r
<VAR>w x y z r : ℝ<VAR>l : List ℝ≥0<VAR>this : ↑(List.map (fun x => x ^ r) l).prod = ↑(l.prod ^ r)<GOAL>(List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r
<VAR>w x y z r : ℝ<VAR>l : List ℝ≥0<VAR>this : (List.map toReal (List.map (fun x => x ^ r) l)).prod = (List.map toReal l).prod ^ r<GOAL>(List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r
<VAR>w x y z r : ℝ<VAR>l : List ℝ≥0<VAR>this : (List.map (toReal ∘ fun x => x ^ r) l).prod = (List.map toReal l).prod ^ r<GOAL>(List.map ((fun x => x ^ r) ∘ toReal) l).prod = (List.map toReal l).prod ^ r
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>cobounded α = cocompact α
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>IsPell (pellZd a1 (n + 1))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>o : IsPell { re := ↑a, im := 1 } := isPell_one a1<GOAL>IsPell (pellZd a1 (n + 1))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<GOAL>pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict ⋯ ≫ g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<GOAL>(pullbackConeOfLeftFst f g ≫ f).base = (Y.ofRestrict ⋯ ≫ g).base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>U : (Opens ↑↑Z)ᵒᵖ<GOAL>((pullbackConeOfLeftFst f g ≫ f).c ≫ whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U = (Y.ofRestrict ⋯ ≫ g).c.app U
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>inverse ↑u = ↑u⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>a✝ : Nontrivial α<VAR>hα : Nonempty α<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>a✝ : Nontrivial α<VAR>hα : Nonempty α<VAR>hι : IsEmpty ι<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>a✝ : Nontrivial α<VAR>hα : Nonempty α<VAR>hι : Nonempty ι<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>a✝ : Nontrivial α<VAR>hα : Nonempty α<VAR>hι : Nonempty ι<VAR>p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)<VAR>g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some<VAR>hg_seq : ∀ (b : δ), IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>a✝ : Nontrivial α<VAR>hα : Nonempty α<VAR>hι : Nonempty ι<VAR>p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)<VAR>g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some<VAR>hg_seq : ∀ (b : δ), IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)<GOAL>g =ᶠ[ae μ] g_seq
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x y : V<GOAL>y ∈ B.orthogonal (Submodule.span K {x}) ↔ y ∈ ker (B.toLinHomAux₁ x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x y : V<GOAL>(∀ (n : V), (∃ a, a • x = n) → B.IsOrtho n y) ↔ (B.toLinHomAux₁ x) y = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a * b < c * d<VAR>hc : 0 < c<VAR>hh : c ≤ a<GOAL>b < d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a * b < c * d<VAR>hc : 0 < c<VAR>hh : c ≤ a<VAR>ha : a ≠ 0<GOAL>b < d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a * b < c * d<VAR>hc : 0 < c<VAR>ha : a ≠ 0<VAR>hh : a⁻¹ ≤ c⁻¹<GOAL>b < d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a * b < c * d<VAR>hc : 0 < c<VAR>ha : a ≠ 0<VAR>hh : a⁻¹ ≤ c⁻¹<VAR>this : a⁻¹ * (a * b) < c⁻¹ * (c * d)<GOAL>b < d
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<VAR>M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<VAR>M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x<VAR>P : R := (√2)⁻¹ • (A₁ + A₀) - B₀<VAR>Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<VAR>M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x<VAR>P : R := (√2)⁻¹ • (A₁ + A₀) - B₀<VAR>Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁<VAR>w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<VAR>M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x<VAR>P : R := (√2)⁻¹ • (A₁ + A₀) - B₀<VAR>Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁<VAR>w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)<VAR>pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u<VAR>inst✝⁵ : OrderedRing R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : StarOrderedRing R<VAR>inst✝² : Algebra ℝ R<VAR>inst✝¹ : OrderedSMul ℝ R<VAR>inst✝ : StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<VAR>M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x<VAR>P : R := (√2)⁻¹ • (A₁ + A₀) - B₀<VAR>Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁<VAR>w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)<VAR>pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)<GOAL>0 ≤ √2 ^ 3 • 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>p : F[X]<VAR>hsep : p.Separable<VAR>hsplit : Splits (algebraMap F K) p<GOAL>Fintype.card ↑(p.rootSet K) = p.natDegree
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>p : F[X]<VAR>hsep : p.Separable<VAR>hsplit : Splits (algebraMap F K) p<GOAL>(p.aroots K).toFinset.card = p.natDegree
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<GOAL>↑(-↑0) = -↑↑0
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>n : ℕ<GOAL>↑(-↑(n + 1)) = -↑↑(n + 1)
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>n : ℕ<GOAL>↑(- -[n+1]) = -↑-[n+1]
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>y * inverse x * x = y
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsCyclotomicExtension {n} A B<VAR>inst✝² : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra K L<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>hcyc : IsCyclotomicExtension {p} K L<VAR>h : p ≠ 2<VAR>hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)<VAR>hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} K L<GOAL>(Algebra.norm K) (ζ - 1) = ↑↑p
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial ℕ ℤ<VAR>h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>f n = g n
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial ℕ ℤ<VAR>h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial ℕ ℤ<VAR>h : (fun n => (bind₁ f) (wittPolynomial p ℤ n)) = fun n => (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial ℕ ℤ<VAR>n : ℕ<VAR>h : ((fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n => (bind₁ f) (wittPolynomial p ℤ n)) = (fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n => (bind₁ g) (wittPolynomial p ℤ n)<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>L : List α<GOAL>IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>L : List α<VAR>h : IsUnit L.prod<GOAL>∀ m ∈ L, IsUnit m
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>m : α<VAR>L : List α<VAR>ih : IsUnit L.prod → ∀ m ∈ L, IsUnit m<VAR>h : IsUnit (m :: L).prod<GOAL>∀ m_1 ∈ m :: L, IsUnit m_1
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>m : α<VAR>L : List α<VAR>ih : IsUnit L.prod → ∀ m ∈ L, IsUnit m<VAR>h : IsUnit m ∧ IsUnit L.prod<GOAL>∀ m_1 ∈ m :: L, IsUnit m_1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(-π / 2)<GOAL>∠ p₁ p₂ p₃ = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(-π / 2)<GOAL>⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ⟦f⟧ ≠ 0<GOAL>⟦f⟧ * (⟦f⟧)⁻¹ = 1
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>⟦f⟧ * (⟦f⟧)⁻¹ = 1
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>mk (f * f.inv ⋯) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H✝ : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>H : SimpleGraph β<VAR>f : H ↪g G<VAR>h : G.CliqueFree n<GOAL>H.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H✝ : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>H : SimpleGraph β<VAR>f : H ↪g G<VAR>h : ¬H.CliqueFree n<GOAL>¬G.CliqueFree n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s t : Set (PrimeSpectrum R)<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(bind₁ fun n => (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hπ : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>iCondIndepSets m' hm' (fun i => {s i}) μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hπ : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(∀ (s_1 : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s_1, f i ∈ {s i}) → μ[(⋂ i ∈ s_1, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω => 1|m']) ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hπ : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∀ (i : ι), ∀ s_1 ∈ {s i}, MeasurableSet s_1
<VAR>α : Type u_1<VAR>m₁ m₂ : OuterMeasure α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>t : Set α<VAR>hs₁ : s ∈ (fun m => {t | MeasurableSet t}) m₁.caratheodory<VAR>hs₂ : s ∈ (fun m => {t | MeasurableSet t}) m₂.caratheodory<GOAL>(m₁ + m₂) t = (m₁ + m₂) (t ∩ s) + (m₁ + m₂) (t \ s)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroObject D<VAR>F : C ⥤ D<VAR>hF : IsZero F<VAR>X : C<VAR>G : C ⥤ D := (Functor.const C).obj 0<GOAL>IsZero (F.obj X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroObject D<VAR>F : C ⥤ D<VAR>hF : IsZero F<VAR>X : C<VAR>G : C ⥤ D := (Functor.const C).obj 0<VAR>hG : IsZero G<GOAL>IsZero (F.obj X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroObject D<VAR>F : C ⥤ D<VAR>hF : IsZero F<VAR>X : C<VAR>G : C ⥤ D := (Functor.const C).obj 0<VAR>hG : IsZero G<VAR>e : F ≅ G := hF.iso hG<GOAL>IsZero (F.obj X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ<VAR>z : α × β<GOAL>z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x✝ : α<VAR>inst✝ : DecidablePred fun x => x < c<VAR>hcb : c ≤ b<VAR>x : α<GOAL>x ∈ filter (fun x => x < c) (Ico a b) ↔ x ∈ Ico a c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x✝ : α<VAR>inst✝ : DecidablePred fun x => x < c<VAR>hcb : c ≤ b<VAR>x : α<GOAL>(a ≤ x ∧ x < c) ∧ x < b ↔ a ≤ x ∧ x < c
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>hax : 0 < a.x<VAR>n : ℤ<GOAL>0 < (a ^ n).x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : AddCommMonoid B<VAR>inst✝ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<GOAL>(∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : IsPushout f g inl inr<VAR>inst✝ : HasPushout f g<GOAL>inr ≫ h.isoPushout.hom = pushout.inr f g
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<GOAL>dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<GOAL>dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<GOAL>dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<GOAL>dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<GOAL>LinearMap.range F.dualMap ≤ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>φ : Dual K V₁<GOAL>φ ∈ LinearMap.range F.dualMap → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>φ : Dual K V₁<GOAL>(∃ y, F.dualMap y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')<GOAL>F.dualMap x ∈ dualAnnihilator W ⊔ dualAnnihilator W'