ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>hdiv : p ∣ q<VAR>hdeg : q.natDegree ≤ p.natDegree<GOAL>p = C q.leadingCoeff * p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z Z' : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<VAR>γ : Z ≅ Z'<GOAL>((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ Z<GOAL>α.symm ≪≫ α ≪≫ β = β
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>firstDiff x y < shortestPrefixDiff x s
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<GOAL>firstDiff x y < shortestPrefixDiff x s
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<GOAL>firstDiff x y < Nat.find A
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Disjoint s (cylinder x (Nat.find A))<GOAL>firstDiff x y < Nat.find A
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A ≤ firstDiff x y<GOAL>¬Disjoint s (cylinder x (Nat.find A))
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A ≤ firstDiff x y<GOAL>(s ∩ cylinder x (Nat.find A)).Nonempty
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A ≤ firstDiff x y<GOAL>y ∈ cylinder x (Nat.find A)
<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>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A ≤ firstDiff x y<GOAL>x ∈ cylinder y (Nat.find A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α ↪ β<VAR>a : α<VAR>s : Finset α<GOAL>map f (insert a s) = insert (f a) (map f s)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>inst✝⁷ : NormedAddCommGroup H<VAR>inst✝⁶ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝⁵ : NontriviallyNormedField 𝕝<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝕝<VAR>A✝ : Type u_8<VAR>inst✝³ : NormedRing A✝<VAR>inst✝² : NormedAlgebra 𝕜 A✝<VAR>A : Type u_9<VAR>inst✝¹ : NormedCommRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → A<VAR>c : E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∏ n ∈ N, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>inst✝⁷ : NormedAddCommGroup H<VAR>inst✝⁶ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝⁵ : NontriviallyNormedField 𝕝<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝕝<VAR>A✝ : Type u_8<VAR>inst✝³ : NormedRing A✝<VAR>inst✝² : NormedAlgebra 𝕜 A✝<VAR>A : Type u_9<VAR>inst✝¹ : NormedCommRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → A<VAR>c : E<VAR>h : ∀ n ∈ ∅, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∏ n ∈ ∅, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>inst✝⁷ : NormedAddCommGroup H<VAR>inst✝⁶ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝⁵ : NontriviallyNormedField 𝕝<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝕝<VAR>A✝ : Type u_8<VAR>inst✝³ : NormedRing A✝<VAR>inst✝² : NormedAlgebra 𝕜 A✝<VAR>A : Type u_9<VAR>inst✝¹ : NormedCommRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → A<VAR>c : E<VAR>a : α<VAR>B : Finset α<VAR>aB : a ∉ B<VAR>hB : (∀ n ∈ B, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun z => ∏ n ∈ B, f n z) c<VAR>h : ∀ n ∈ insert a B, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∏ n ∈ insert a B, f n z) c
<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>g : L.obj Y ⟶ L.obj Z<GOAL>add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
<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>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<GOAL>add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
<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>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<GOAL>add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
<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>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : (RightFraction.mk α.s ⋯ β.f).f ≫ γ.s = (RightFraction.mk α.s ⋯ β.f).s ≫ γ.f<GOAL>add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
<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>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
<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>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>α.add.map L ⋯ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).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>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>f₁ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).fst.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>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>f₂ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).snd.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>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>(α.add.comp₀ β γ).map L ⋯ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).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>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>β : W.LeftFraction Y Z<VAR>hβ : g = β.map L ⋯<VAR>γ : W.LeftFraction α.Y' β.Y'<VAR>hγ : β.f ≫ γ.s = α.s ≫ γ.f<GOAL>(LeftFraction.mk ((α.f + α.f') ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯ = (LeftFraction.mk (α.f ≫ γ.f + α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>v : α →₀ M<GOAL>equivMapDomain e.symm (equivMapDomain e v) = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>v : α →₀ M<GOAL>equivMapDomain (Equiv.refl α) v = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>v : β →₀ M<GOAL>equivMapDomain e (equivMapDomain e.symm v) = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>v : β →₀ M<GOAL>equivMapDomain (Equiv.refl β) v = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>a b : α →₀ M<GOAL>{ toFun := equivMapDomain e, invFun := equivMapDomain e.symm, left_inv := ⋯, right_inv := ⋯ }.toFun (a + b) = { toFun := equivMapDomain e, invFun := equivMapDomain e.symm, left_inv := ⋯, right_inv := ⋯ }.toFun a + { toFun := equivMapDomain e, invFun := equivMapDomain e.symm, left_inv := ⋯, right_inv := ⋯ }.toFun b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>e : α ≃ β<VAR>a b : α →₀ M<GOAL>mapDomain (⇑e) (a + b) = mapDomain (⇑e) a + mapDomain (⇑e) b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>factors 1 = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>Multiset.Rel ?m.115710 (factors 1) 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>Type ?u.115707
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>α → ?m.115709 → Prop
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>(factors 1).prod ~ᵤ Multiset.prod 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>(factors 1).prod ~ᵤ 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>n : ℕ<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<GOAL>∑ i : PointsWithCircumcenterIndex n, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 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>n : ℕ<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<GOAL>((if i₁ ∈ univ then {i₁} else ∅) ∪ if i₂ ∈ univ then {i₂} else ∅).card • 1 + (filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ).card • 0 + -1 = 1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>inst✝³⁵ : NontriviallyNormedField 𝕜<VAR>inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝³³ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝³² : NormedAddCommGroup F₁<VAR>inst✝³¹ : NormedSpace 𝕜 F₁<VAR>inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)<VAR>inst✝²⁶ : NormedAddCommGroup F₂<VAR>inst✝²⁵ : NormedSpace 𝕜 F₂<VAR>inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝²³ : (x : B) → TopologicalSpace (E₂ x)<VAR>inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>inst✝²⁰ : NormedAddCommGroup EB<VAR>inst✝¹⁹ : NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>inst✝¹⁸ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁷ : TopologicalSpace B<VAR>inst✝¹⁶ : ChartedSpace HB B<VAR>EM : Type u_10<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁹ : FiberBundle F₁ E₁<VAR>inst✝⁸ : VectorBundle 𝕜 F₁ E₁<VAR>inst✝⁷ : FiberBundle F₂ E₂<VAR>inst✝⁶ : VectorBundle 𝕜 F₂ E₂<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁵ : SmoothVectorBundle F₁ E₁ IB<VAR>inst✝⁴ : SmoothVectorBundle F₂ E₂ IB<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<GOAL>SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>inst✝³⁵ : NontriviallyNormedField 𝕜<VAR>inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝³³ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝³² : NormedAddCommGroup F₁<VAR>inst✝³¹ : NormedSpace 𝕜 F₁<VAR>inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)<VAR>inst✝²⁶ : NormedAddCommGroup F₂<VAR>inst✝²⁵ : NormedSpace 𝕜 F₂<VAR>inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝²³ : (x : B) → TopologicalSpace (E₂ x)<VAR>inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>inst✝²⁰ : NormedAddCommGroup EB<VAR>inst✝¹⁹ : NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>inst✝¹⁸ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁷ : TopologicalSpace B<VAR>inst✝¹⁶ : ChartedSpace HB B<VAR>EM : Type u_10<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁹ : FiberBundle F₁ E₁<VAR>inst✝⁸ : VectorBundle 𝕜 F₁ E₁<VAR>inst✝⁷ : FiberBundle F₂ E₂<VAR>inst✝⁶ : VectorBundle 𝕜 F₂ E₂<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁵ : SmoothVectorBundle F₁ E₁ IB<VAR>inst✝⁴ : SmoothVectorBundle F₂ E₂ IB<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<GOAL>SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>inst✝³⁵ : NontriviallyNormedField 𝕜<VAR>inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝³³ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝³² : NormedAddCommGroup F₁<VAR>inst✝³¹ : NormedSpace 𝕜 F₁<VAR>inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)<VAR>inst✝²⁶ : NormedAddCommGroup F₂<VAR>inst✝²⁵ : NormedSpace 𝕜 F₂<VAR>inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝²³ : (x : B) → TopologicalSpace (E₂ x)<VAR>inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>inst✝²⁰ : NormedAddCommGroup EB<VAR>inst✝¹⁹ : NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>inst✝¹⁸ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁷ : TopologicalSpace B<VAR>inst✝¹⁶ : ChartedSpace HB B<VAR>EM : Type u_10<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁹ : FiberBundle F₁ E₁<VAR>inst✝⁸ : VectorBundle 𝕜 F₁ E₁<VAR>inst✝⁷ : FiberBundle F₂ E₂<VAR>inst✝⁶ : VectorBundle 𝕜 F₂ E₂<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁵ : SmoothVectorBundle F₁ E₁ IB<VAR>inst✝⁴ : SmoothVectorBundle F₂ E₂ IB<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<VAR>h₂ : SmoothOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)<GOAL>SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(closureCommutatorRepresentatives G) ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>x y : (a : α) → Perm (β a)<VAR>h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y<VAR>a : α<VAR>b : β a<GOAL>(x a) b = (y a) b
<VAR>m n : ℕ<GOAL>↑(m * n) = ↑m * ↑n
<VAR>α : Type u_1<VAR>l l₁✝ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l₁ : List α<VAR>head✝ : α<VAR>tail✝ : List α<VAR>h : ¬a ∈ head✝ :: tail✝<GOAL>(a :: l₁).bagInter (head✝ :: tail✝) = l₁.bagInter (head✝ :: tail✝)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<GOAL>diam ((convexHull ℝ) s) = diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ι → ℝ<VAR>hpos : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ<VAR>hε'c : HasSum (fun i => ε' ↑i) c<VAR>hcε : c ≤ ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ι → ℝ<VAR>hpos : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ<VAR>hε'c : HasSum (fun i => ε' ↑i) c<VAR>hcε : c ≤ ε<VAR>t : Finset ι<VAR>ht : ↑t ⊆ s<GOAL>∑ i ∈ t, ε' i ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ι → ℝ<VAR>hpos : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ<VAR>hε'c : HasSum (fun i => ε' ↑i) c<VAR>hcε : c ≤ ε<VAR>t : Finset ι<VAR>ht : ↑t ⊆ s<GOAL>∑ x ∈ Finset.subtype (fun x => x ∈ s) t, ε' ↑x ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Countable<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ι → ℝ<VAR>hpos : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ<VAR>hε'c : HasSum (fun i => ε' ↑i) c<VAR>hcε : c ≤ ε<VAR>t : Finset ι<VAR>ht : ↑t ⊆ s<GOAL>∀ i ∉ Finset.subtype (fun x => x ∈ s) t, 0 ≤ ε' ↑i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o✝ : Ordinal.{u}<VAR>ho✝ : o✝.IsLimit<VAR>hsC✝ : contained C o✝<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<GOAL>LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o✝ : Ordinal.{u}<VAR>ho✝ : o✝.IsLimit<VAR>hsC✝ : contained C o✝<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<GOAL>LinearIndependent (ι := ↑(range C)) ℤ ((fun p => ↑p) ∘ (range_equiv C ho hsC).toFun) ↔ LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p