ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : R →+* S<VAR>s : Set A<VAR>hfs : s.Finite<VAR>his : ∀ x ∈ s, IsIntegral R x<VAR>x✝ : ∀ x ∈ ∅, IsIntegral R x<VAR>x : A<GOAL>x ∈ span R ↑{1} ↔ x ∈ Subalgebra.toSubmodule (Algebra.adjoin R ∅)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : R →+* S<VAR>s✝ : Set A<VAR>hfs : s✝.Finite<VAR>his✝ : ∀ x ∈ s✝, IsIntegral R x<VAR>a : A<VAR>s : Set A<VAR>x✝¹ : a ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG<VAR>his : ∀ x ∈ insert a s, IsIntegral R x<GOAL>(Subalgebra.toSubmodule (Algebra.adjoin R (insert a s))).FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : R →+* S<VAR>s✝ : Set A<VAR>hfs : s✝.Finite<VAR>his✝ : ∀ x ∈ s✝, IsIntegral R x<VAR>a : A<VAR>s : Set A<VAR>x✝¹ : a ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG<VAR>his : ∀ x ∈ insert a s, IsIntegral R x<GOAL>(Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R {a})).FG
<VAR>n : ℕ<GOAL>cos (↑n * (2 * ↑π) + ↑π) = -1
<VAR>k : ℕ<GOAL>ascFactorial 0 (k + 1).succ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>n✝ : ℕ<VAR>s t : Finset α<VAR>n : ℕ<VAR>m : Sym α n<GOAL>m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>this : DecidableEq ι := σ.decidableEq<GOAL>∀ (x y : M₁ (σ.symm i)), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>this : DecidableEq ι := σ.decidableEq<GOAL>∀ (x y : M₁ (σ.symm (σ (σ.symm i)))), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>this : DecidableEq ι := σ.decidableEq<VAR>x y : M₁ (σ.symm (σ (σ.symm i)))<GOAL>(⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>c : R<VAR>this : DecidableEq ι := σ.decidableEq<GOAL>∀ (x : M₁ (σ.symm i)), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>c : R<VAR>this : DecidableEq ι := σ.decidableEq<GOAL>∀ (x : M₁ (σ.symm (σ (σ.symm i)))), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι'<VAR>m : (i : ι') → M₁ (σ.symm i)<VAR>i : ι'<VAR>c : R<VAR>this : DecidableEq ι := σ.decidableEq<VAR>x : M₁ (σ.symm (σ (σ.symm i)))<GOAL>(⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>this : DecidableEq ι' := σ.symm.decidableEq<GOAL>∀ (x y : M₁ i), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>this : DecidableEq ι' := σ.symm.decidableEq<GOAL>∀ (x y : M₁ (σ.symm (σ i))), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>this : DecidableEq ι' := σ.symm.decidableEq<VAR>x y : M₁ (σ.symm (σ i))<GOAL>(⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) = (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>this : DecidableEq ι' := σ.symm.decidableEq<GOAL>∀ (x : M₁ i), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>this : DecidableEq ι' := σ.symm.decidableEq<GOAL>∀ (x : M₁ (σ.symm (σ i))), (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>this : DecidableEq ι' := σ.symm.decidableEq<VAR>x : M₁ (σ.symm (σ i))<GOAL>(⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M₂<VAR>inst✝ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f₁ f₂ : MultilinearMap R M₁ M₂<VAR>x✝ : (i : ι') → M₁ (σ.symm i)<GOAL>((fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }) (f₁ + f₂)) x✝ = ((fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }) f₁ + (fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }) f₂) x✝
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M₂<VAR>inst✝ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>c : S<VAR>f : MultilinearMap R M₁ M₂<VAR>x✝ : (i : ι') → M₁ (σ.symm i)<GOAL>({ toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (c • f)) x✝ = ((RingHom.id S) c • { toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun f) x✝
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M₂<VAR>inst✝ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R M₁ M₂<VAR>x✝ : (i : ι) → M₁ i<GOAL>((fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_add' := ⋯, map_smul' := ⋯ }) ({ toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun f)) x✝ = f x✝
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M₂<VAR>inst✝ : SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<VAR>x✝ : (i : ι') → M₁ (σ.symm i)<GOAL>({ toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_add' := ⋯, map_smul' := ⋯ }) f)) x✝ = f x✝
<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 : Finset α<VAR>h : mulSupport f ⊆ ↑s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i
<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 : Finset α<VAR>h : mulSupport f ⊆ ↑s<VAR>A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i
<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 : Finset α<VAR>h : mulSupport f ⊆ ↑s<VAR>A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f<VAR>this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i
<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 : Finset α<VAR>h : mulSupport f ⊆ ↑s<VAR>A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f<VAR>this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)<GOAL>∏ i ∈ Finset.map Equiv.plift.symm.toEmbedding s, f i.down = ∏ i ∈ s, f i
<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 : Finset α<VAR>h : mulSupport f ⊆ ↑s<VAR>A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f<VAR>this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)<GOAL>∏ x ∈ s, f (Equiv.plift.symm x).down = ∏ i ∈ s, f i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<GOAL>constantCoeff (M.toMvPolynomial i) = 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>-Ioc a b = Ico (-b) (-a)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝ : PredOrder ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>hi_min : ¬IsMin i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝ : PredOrder ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>hi_min : ¬IsMin i<VAR>this : {ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i)<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝ : PredOrder ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>hi_min : ¬IsMin i<VAR>this : {ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i)<GOAL>MeasurableSet (τ ⁻¹' Set.Iic (pred i))
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → E<VAR>c : PE<VAR>a b : k<GOAL>slope (fun x => f x +ᵥ c) a b = slope f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : Setoid α<VAR>h : ∀ (x y : α), r x y → s.Rel x y<GOAL>EqvGen.Setoid r ≤ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : Setoid α<VAR>h : ∀ (x y : α), r x y → s.Rel x y<GOAL>sInf {s | ∀ ⦃x y : α⦄, r x y → s.Rel x y} ≤ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<VAR>h : ¬a₁ = a₂<VAR>ha₂ : a₂ ∈ l.keys<VAR>b₁ : β a₁<VAR>l₁ l₂ : List (Sigma β)<VAR>a₁_nin_l₁ : a₁ ∉ l₁.keys<VAR>x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys<VAR>ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys<VAR>h' : a₂ ∈ l₁.keys<GOAL>kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<VAR>h : ¬a₁ = a₂<VAR>ha₂ : a₂ ∈ l.keys<VAR>b₁ : β a₁<VAR>l₁ l₂ : List (Sigma β)<VAR>a₁_nin_l₁ : a₁ ∉ l₁.keys<VAR>x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys<VAR>ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys<VAR>h' : a₂ ∉ l₁.keys<GOAL>kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<VAR>h : ¬a₁ = a₂<VAR>ha₁ : a₁ ∈ l.keys<VAR>ha₂ : a₂ ∉ l.keys<GOAL>kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<VAR>h : ¬a₁ = a₂<VAR>ha₁ : a₁ ∉ l.keys<GOAL>kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (Fin 0 → α) → Prop<GOAL>Exists P ↔ ∃ x, P x
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (Fin 0 → α) → Prop<GOAL>P Fin.elim0 ↔ P finZeroElim
<VAR>m n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>P : (Fin n.succ → α) → Prop<GOAL>Exists P ↔ ∃ x, P x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : MulOneClass β<VAR>f : α → β<VAR>hf : IsMonoidHom f<VAR>γ : Type u_1<VAR>inst✝ : MulOneClass γ<VAR>g : β → γ<VAR>hg : IsMonoidHom g<GOAL>g (f 1) = 1
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l[i]? = some x
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>(∃ i, i ≠ k ∧ ∃ x_1, l[i]? = some x) ↔ ∃ i, i ≠ k ∧ l[i]? = some x
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>l : List α<VAR>k i : Nat<GOAL>(∃ x_1, l[i]? = some x) ↔ l[i]? = some x
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f
<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<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n : ℕ<GOAL>(f x✝).coeff n = (g x✝).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<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 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<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 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<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<GOAL>∀ (x : ℕ → ℤ), (MvPolynomial.eval x) ((bind₁ φ) (wittPolynomial p ℤ k)) = (MvPolynomial.eval x) ((bind₁ ψ) (wittPolynomial p ℤ k))