ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C S0<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<VAR>this✝ : Finite ↑S<VAR>this : Finite { T // T ⊆ S }<GOAL>C S
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C ↑⟨S0, hS0⟩<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<VAR>this✝ : Finite ↑S<VAR>this : Finite { T // T ⊆ S }<GOAL>C ↑⟨S, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C ↑⟨S0, hS0⟩<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<VAR>this✝ : Finite ↑S<VAR>this : Finite { T // T ⊆ S }<VAR>s : { x // x ⊆ S }<VAR>hs : ↑s ≠ ↑⟨S, ⋯⟩<VAR>hs' : C ↑s<GOAL>∃ c > s, C ↑c
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C ↑⟨S0, hS0⟩<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<VAR>this✝ : Finite ↑S<VAR>this : Finite { T // T ⊆ S }<VAR>s : { x // x ⊆ S }<VAR>hs : ↑s ≠ ↑⟨S, ⋯⟩<VAR>hs' : C ↑s<VAR>a : α<VAR>ha' : C (insert a ↑s)<VAR>ha1 : a ∈ S<VAR>ha2 : a ∉ ↑s<GOAL>∃ c > s, C ↑c
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>m✝ : L'<GOAL>m✝ ∈ f.idealRange ↔ m✝ ∈ LieIdeal.map f ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>m✝ : L'<GOAL>m✝ ∈ LieSubmodule.lieSpan R L' ↑(LieSubalgebra.map f ⊤) ↔ m✝ ∈ LieIdeal.map f ⊤
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>s : Finset ι<VAR>h : CompleteLattice.Independent fun i => N ↑i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<VAR>p : Submodule R M<VAR>hp : p = ⨆ i ∈ s, N i<VAR>hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯<GOAL>(trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F✝ X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>F : Set α := {x | M.Basis I (insert x I)}<GOAL>M.closure I = F
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F✝ X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>F : Set α := {x | M.Basis I (insert x I)}<VAR>hIF : M.Basis I F<GOAL>M.closure I = F
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F✝ X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>F : Set α := {x | M.Basis I (insert x I)}<VAR>hIF : M.Basis I F<VAR>hF : M.Flat F<GOAL>M.closure I = F
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F✝ X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>F : Set α := {x | M.Basis I (insert x I)}<VAR>hIF : M.Basis I F<VAR>hF : M.Flat F<GOAL>∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F✝ X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>F : Set α := {x | M.Basis I (insert x I)}<VAR>hIF : M.Basis I F<VAR>hF : M.Flat F<GOAL>F ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>preNormEDS b c d 4 = d
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : UniformSpace 𝕜<GOAL>𝓤 (Matrix m n 𝕜) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : UniformSpace 𝕜<GOAL>⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (𝓤 (n → 𝕜)) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : UniformSpace 𝕜<GOAL>⨅ i, ⨅ i_1, Filter.comap ((fun a => (a.1 i_1, a.2 i_1)) ∘ fun a => (a.1 i, a.2 i)) (𝓤 𝕜) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x : 𝓞 K<GOAL>↑η ^ 2 + ↑η + 1 = 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x : 𝓞 K<GOAL>-↑η - 1 + ↑η + 1 = 0
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<VAR>hp0 : ¬p = 0<GOAL>Irreducible p ↔ Prime p
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<VAR>hp0 : ¬p = 0<VAR>h : Irreducible p<GOAL>Prime p
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<VAR>hp0 : ¬p = 0<VAR>h : Irreducible p<VAR>f : Multiset α<VAR>hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p<GOAL>Prime p
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<VAR>hp0 : ¬p = 0<VAR>h : Irreducible p<VAR>q : α<VAR>hq : p ~ᵤ q<VAR>hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p<GOAL>Prime p
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<VAR>hp0 : ¬p = 0<VAR>h : Irreducible p<VAR>q : α<VAR>hq : p ~ᵤ q<VAR>hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p<GOAL>Prime q
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → ℝ<VAR>h : Memℒp f 2 μ<GOAL>Integrable (fun x => f x ^ 2) μ
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n : ℕ<GOAL>(f x✝ y✝).coeff n = (g x✝ y✝).coeff 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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n : ℕ<GOAL>∀ (n : ℕ), (bind₁ φ) (wittPolynomial p ℤ n) = (bind₁ ψ) (wittPolynomial p ℤ 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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<GOAL>(bind₁ φ) (wittPolynomial p ℤ k) = (bind₁ ψ) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<GOAL>∀ (x : Fin 2 × ℕ → ℤ), (MvPolynomial.eval x) ((bind₁ φ) (wittPolynomial p ℤ k)) = (MvPolynomial.eval x) ((bind₁ ψ) (wittPolynomial p ℤ k))
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<GOAL>(MvPolynomial.eval x) ((bind₁ φ) (wittPolynomial p ℤ k)) = (MvPolynomial.eval x) ((bind₁ ψ) (wittPolynomial p ℤ k))
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (ghostComponent k) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })) = (ghostComponent k) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) }))<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)<GOAL>ULift.ringEquiv.symm ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k)) = ULift.ringEquiv.symm ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i))) (wittPolynomial p ℤ k) = (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i))) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i))) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
<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 : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n => peval (ψ n) ![x.coeff, y.coeff]<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ y✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : Fin 2 × ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i))) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x (0, i) }) (mk p fun i => { down := x (1, i) })).coeff) (wittPolynomial p ℤ k)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
<VAR>x : ℝ<VAR>n : ℕ<GOAL>1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
<VAR>x : ℝ<VAR>n : ℕ<GOAL>0 ≤ 2 + sqrtTwoAddSeries 0 n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : ↥(Lp E p μ)<GOAL>Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : ↥(Lp E p μ)<GOAL>Tendsto (fun b => dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : ↥(Lp E p μ)<GOAL>Tendsto (fun b => (eLpNorm (↑↑(f b) - ↑↑f_lim) p μ).toReal) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : ↥(Lp E p μ)<VAR>n : ι<GOAL>eLpNorm (↑↑(f n) - ↑↑f_lim) p μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : ↥(Lp E p μ)<VAR>n : ι<GOAL>eLpNorm (↑↑(f n - f_lim)) p μ ≠ ⊤
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f : M₁ →ₗ[R] M₁<VAR>k : ℕ<GOAL>(toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
<VAR>a : ℕ<VAR>m : Multiset ℕ<VAR>x : ℕ<VAR>hxa : x ∈ range a<VAR>hxb : x ∈ map (fun x => a + x) m<GOAL>False
<VAR>a : ℕ<VAR>m : Multiset ℕ<VAR>x : ℕ<VAR>hxa : x < a<VAR>hxb : x ∈ map (fun x => a + x) m<GOAL>False
<VAR>a : ℕ<VAR>m : Multiset ℕ<VAR>c : ℕ<VAR>left✝ : c ∈ m<VAR>hxa : a + c < a<VAR>hxb : a + c ∈ map (fun x => a + x) m<GOAL>False
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>a : P.A<VAR>f : P.B a → α<GOAL>Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>a : P.A<VAR>f : P.B a → α<GOAL>(∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) ↔ ∀ (i : P.B a), p (f i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>Exact ⇑(lTensor Q f) ⇑(lTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (lTensor Q g) = ker (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g)