ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∉ upperClosure ↑s<VAR>ht : a ∉ upperClosure ↑t<GOAL>a ∉ upperClosure ↑s ⊓ upperClosure ↑t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₁<GOAL>(piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₁<VAR>this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯<GOAL>(piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₁<VAR>this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯<GOAL>(comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, hx⟩ = f₁ ⟨↑x, hx⟩
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i<VAR>x✝¹ : (i : ι) → s i<VAR>x✝ : (i : ι) → t i<GOAL>((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ)))).compMultilinearMap (tprod R)) x✝¹).compMultilinearMap (tprod R)) x✝ = ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) + lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))).compMultilinearMap (tprod R)) x✝¹).compMultilinearMap (tprod R)) x✝
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<GOAL>TorusIntegrable f c 0
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<GOAL>IntegrableOn (fun θ => f (const (Fin n → ℝ) c θ)) (Icc 0 fun x => 2 * π) volume
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Icc a b) = b + 1 - a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R✝ : Type u_3<VAR>S✝ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : Semiring R<VAR>inst✝ : OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>h : IsLeftRegular (abv 1)<GOAL>(fun x => abv 1 * x) (abv 1) = (fun x => abv 1 * x) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α<VAR>y₁ y₂ : β<GOAL>dist (x, y₁) (x, y₂) = dist y₁ y₂
<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>f : α → F<VAR>hμν : ν ≤ μ<VAR>hq : 0 ≤ q<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂ν ≤ ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝² : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>inst✝¹ : HasMulticoequalizer D.diagram<VAR>inst✝ : PreservesColimit D.diagram.multispan F<VAR>i : D.J<GOAL>(D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i)
<VAR>θ ψ : Angle<VAR>h : θ = ψ ∨ θ = ψ + ↑π<GOAL>|θ.cos| = |ψ.cos|
<VAR>α : Type u_1<VAR>inst✝ : Infinite α<VAR>s : Set α<VAR>h2 : #↑s < #α<GOAL>#↑sᶜ = #α
<VAR>α : Type u_1<VAR>inst✝ : Infinite α<VAR>s : Set α<VAR>h2 : #↑s < #α<GOAL>#↑s + #↑sᶜ = #α
<VAR>a b : Int<GOAL>↑(a - b) = ↑a - ↑b
<VAR>a b : Int<GOAL>↑(a - b) = normalize ((↑a).num * ↑(↑b).den - (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>htu : t ~[l] u<VAR>hvw : v ~[l] w<GOAL>(fun x => t x / v x) ~[l] fun x => u x / w x
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v✝ : K<VAR>q✝ : ℚ<VAR>v_eq_q✝ : v✝ = ↑q✝<VAR>n : ℕ<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>(of v).Terminates ↔ (of q).Terminates
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>l : List α<GOAL>takeWhile p (takeWhile p l) = takeWhile p l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>(⨅ i, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) = (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) = (⨅ i ∈ I, comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : Odd n<GOAL>¬2 ∣ n
<VAR>a✝ b c n a : ℕ<GOAL>Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
<VAR>a✝ b c n a : ℕ<GOAL>Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val
<VAR>a✝ b c n a : ℕ<GOAL>∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction₂ X Y<VAR>hφ₁ : f₁ = φ.fst.map L ⋯<VAR>hφ₂ : f₂ = φ.snd.map L ⋯<GOAL>add' W f₁ f₂ = φ.add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction₂ X Y<VAR>hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯<VAR>hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯<VAR>hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯<GOAL>add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z✝ : C<VAR>φ φ₀ : W.LeftFraction₂ X Y<VAR>hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯<VAR>hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯<VAR>hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯<VAR>Z : C<VAR>t₁ : φ₀.Y' ⟶ Z<VAR>t₂ : φ.Y' ⟶ Z<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<GOAL>add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z✝ : C<VAR>φ φ₀ : W.LeftFraction₂ X Y<VAR>hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯<VAR>hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯<VAR>hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯<VAR>Z : C<VAR>t₁ : φ₀.Y' ⟶ Z<VAR>t₂ : φ.Y' ⟶ Z<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ.add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z✝ : C<VAR>φ φ₀ : W.LeftFraction₂ X Y<VAR>hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯<VAR>hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯<VAR>hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯<VAR>Z : C<VAR>t₁ : φ₀.Y' ⟶ Z<VAR>t₂ : φ.Y' ⟶ Z<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z✝ : C<VAR>φ φ₀ : W.LeftFraction₂ X Y<VAR>hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯<VAR>hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯<VAR>hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯<VAR>Z : C<VAR>t₁ : φ₀.Y' ⟶ Z<VAR>t₂ : φ.Y' ⟶ Z<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>φ₀.add.map L ⋯ ≫ L.map (φ₀.s ≫ t₁) = φ.add.map L ⋯ ≫ L.map (φ.s ≫ t₂)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>↑(W₀.sum fun a b => hV.linearIsometryEquiv ((V a) b)) = ⇑W₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>↑(hV.linearIsometryEquiv (W₀.sum fun a => ⇑(V a))) = ⇑W₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>↑(hV.linearIsometryEquiv (hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)))) = ⇑W₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>↑(W₀.sum (lp.single 2)) = ⇑W₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<VAR>i : ι<GOAL>↑(W₀.sum (lp.single 2)) i = W₀ i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommSemiring L<VAR>inst✝¹ : Nontrivial L<VAR>inst✝ : Algebra K L<GOAL>ringChar K = ringChar L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommSemiring L<VAR>inst✝¹ : Nontrivial L<VAR>inst✝ : Algebra K L<GOAL>CharP L (ringChar L)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>x✝ : Fin (n + 1)<VAR>x : Fin n<VAR>hx : (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) x.castSucc = f x.castSucc<GOAL>(f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) x.succ = f x.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>x✝ : Fin (n + 1)<VAR>x : Fin n<VAR>hx : f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc<GOAL>f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X A : C<VAR>inst✝ : IsConnected A<VAR>h : Nonempty ↑(F.obj X)<VAR>f : X ⟶ A<VAR>Z : C<VAR>u v : A ⟶ Z<VAR>huv : f ≫ u = f ≫ v<GOAL>u = v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X A : C<VAR>inst✝ : IsConnected A<VAR>h : Nonempty ↑(F.obj X)<VAR>f : X ⟶ A<VAR>Z : C<VAR>u v : A ⟶ Z<VAR>huv : f ≫ u = f ≫ v<GOAL>(fun f_1 => F.map f_1 (F.map f (Classical.arbitrary ↑(F.obj X)))) u = (fun f_1 => F.map f_1 (F.map f (Classical.arbitrary ↑(F.obj X)))) v
<VAR>R : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>A : Type w₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>B : Type w₃<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>σ : Type u_1<VAR>f : MvPolynomial σ R →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(TensorProduct.map (AlgHom.id R B) f)
<VAR>R : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>A : Type w₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>B : Type w₃<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>σ : Type u_1<VAR>f : MvPolynomial σ R →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(AlgHom.id R B).toLinearMap
<VAR>R : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>A : Type w₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>B : Type w₃<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>σ : Type u_1<VAR>f : MvPolynomial σ R →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑f.toLinearMap
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>r : R<GOAL>Squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ IsUnit x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>r a : R<GOAL>a * a ∣ r → IsUnit a ↔ multiplicity a r ≤ 1 ∨ IsUnit a
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>r a : R<GOAL>↑2 ≤ multiplicity a r ↔ 1 < multiplicity a r
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>r a : R<GOAL>2 ≤ multiplicity a r ↔ 1 < multiplicity a r
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>r a : R<GOAL>1 + 1 ≤ multiplicity a r ↔ 1 < multiplicity a r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a✝ b c a : α<GOAL>∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(n - m).Coprime n ↔ m.Coprime n
<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<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : AddCommMonoid P<VAR>g : N →+ P<VAR>f : α → M →+ N<VAR>a : α<GOAL>liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>A : Finset α<VAR>h : A ∈ ↑(∂⁺ 𝒜)<GOAL>A.card = r + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>A : Finset α<VAR>hA : A ∈ 𝒜<VAR>i : α<VAR>hi : i ∉ A<VAR>h : insert i A ∈ ↑(∂⁺ 𝒜)<GOAL>(insert i A).card = r + 1
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
<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 : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>N' : LieSubmodule R L M'<GOAL>comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>x ^ z⁻¹ = y ↔ x = y ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>0 ≤ x ^ z⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T0Space α<VAR>s : Closeds α<VAR>hs : IsAtom s<GOAL>∃ a, ↑s = {a}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T0Space α<VAR>s : Closeds α<VAR>hs : IsAtom s<VAR>t : Set α<VAR>hts : t ⊆ ↑s<VAR>ht : t.Nonempty<VAR>ht' : IsClosed t<GOAL>t = ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T0Space α<VAR>s : Closeds α<VAR>hs : IsAtom s<VAR>t : Closeds α<VAR>hts : ↑t ⊆ ↑s<VAR>ht : (↑t).Nonempty<GOAL>↑t = ↑s
<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 → PE<VAR>a b c : k<VAR>hab : ¬a = b<VAR>hbc : ¬b = c<GOAL>((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
<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 → PE<VAR>a b c : k<VAR>hab : ¬a = b<VAR>hbc : ¬b = c<GOAL>((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c
<VAR>p n : ℕ<GOAL>padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<GOAL>(toDualMap 𝕜 E) x = (toDualMap 𝕜 E) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<GOAL>∀ (i : ι), ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<VAR>i : ι<GOAL>↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<VAR>i : ι<GOAL>((toDualMap 𝕜 E) x) (b i) = ((toDualMap 𝕜 E) y) (b i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<VAR>i : ι<GOAL>⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<VAR>i : ι<GOAL>(starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = ⟪y, b i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜<VAR>i : ι<GOAL>(starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = (starRingEnd 𝕜) ⟪b i, y⟫_𝕜
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_6<VAR>K : Type u_7<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>D✝ : BilinForm R M<VAR>D₁ : BilinForm R₁ M₁<VAR>B D : BilinForm R M<VAR>h : (fun B x y => (B x) y) B = (fun B x y => (B x) y) D<VAR>x y : M<GOAL>(B x) y = (D x) y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>C : WSeq α → Prop<VAR>a : α<VAR>s : WSeq α<VAR>M : a ∈ s<VAR>h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')<VAR>h2 : ∀ (s : WSeq α), C s → C s.think<GOAL>C s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>C : WSeq α → Prop<VAR>a : α<VAR>s : WSeq α<VAR>M : a ∈ s<VAR>h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')<VAR>h2 : ∀ (s : WSeq α), C s → C s.think<GOAL>∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')