ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(Lp.simpleFunc E 1 μ)<GOAL>Memℒp (↑(Lp.simpleFunc.toSimpleFunc f)) 1 μ
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y z a b : α<VAR>x : ↑(Icc (a ⊓ b) a)<GOAL>a ⊓ (↑x ⊔ b) = ↑x
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y z a b : α<VAR>x : ↑(Icc b (a ⊔ b))<GOAL>a ⊓ ↑x ⊔ b = ↑x
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y✝ z a b : α<VAR>x y : ↑(Icc (a ⊓ b) a)<GOAL>{ toFun := fun x => ⟨↑x ⊔ b, ⋯⟩, invFun := fun x => ⟨a ⊓ ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x ≤ { toFun := fun x => ⟨↑x ⊔ b, ⋯⟩, invFun := fun x => ⟨a ⊓ ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } y ↔ x ≤ y
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y✝ z a b : α<VAR>x y : ↑(Icc (a ⊓ b) a)<GOAL>↑x ⊔ b ≤ ↑y ⊔ b ↔ x ≤ y
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y✝ z a b : α<VAR>x y : ↑(Icc (a ⊓ b) a)<GOAL>↑x ⊔ b ≤ ↑y ⊔ b ↔ ↑x ≤ ↑y
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y✝ z a b : α<VAR>x y : ↑(Icc (a ⊓ b) a)<VAR>h : ↑x ⊔ b ≤ ↑y ⊔ b<GOAL>↑x ≤ ↑y
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x✝ y✝ z a b : α<VAR>x y : ↑(Icc (a ⊓ b) a)<VAR>h : ↑x ⊔ b ≤ ↑y ⊔ b<GOAL>a ⊓ (↑x ⊔ b) ≤ a ⊓ (↑y ⊔ b)
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x : α<VAR>x✝ : x ∣ 1<VAR>y : α<VAR>h : 1 = x * y<GOAL>y * x = 1
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f✝ g : α → E<VAR>s : Set α<VAR>x✝ : α<VAR>f : E → F<VAR>hf : AntilipschitzWith K f<VAR>x y : E<GOAL>‖x / y‖ ≤ ↑K * ‖f x / f y‖
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>a : G ⧸ stabilizer G s<GOAL>a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ a ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>a : G<GOAL>↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>a : G<GOAL>↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>a : G<VAR>this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)<GOAL>↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<VAR>a : G<VAR>this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)<VAR>h : QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s<GOAL>a • s = s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>f'' : X'' ⟶ Y''<VAR>g'' : X'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>inst✝² : HasPushout f g<VAR>inst✝¹ : HasPushout f' g'<VAR>inst✝ : HasPushout f'' g''<VAR>e₁ : f ≫ i₂ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₁ ≫ g'<VAR>e₃ : f' ≫ j₂ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₁ ≫ g''<GOAL>f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>f'' : X'' ⟶ Y''<VAR>g'' : X'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>inst✝² : HasPushout f g<VAR>inst✝¹ : HasPushout f' g'<VAR>inst✝ : HasPushout f'' g''<VAR>e₁ : f ≫ i₂ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₁ ≫ g'<VAR>e₃ : f' ≫ j₂ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₁ ≫ g''<GOAL>g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''
<VAR>x y : ℝ<GOAL>tanh (-x) = -tanh x
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>IsLprojection X (P * Q)
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>∀ (x : X), ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<VAR>x : X<GOAL>‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<VAR>x : X<GOAL>‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<VAR>x : X<GOAL>‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x : FractionRing K[X]<GOAL>(toFractionRingRingEquiv K).symm x = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)).toRingEquiv x
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>C a * X = (monomial 1) a
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>range (f.prod g) ≤ (range f).prod (range g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>∀ ⦃x : M₂ × M₃⦄ (x_1 : M), Pi.prod (⇑f) (⇑g) x_1 = x → (∃ y, f y = x.1) ∧ ∃ y, g y = x.2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<GOAL>(∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<GOAL>𝓝 (f z₀) ≤ map f (𝓝 z₀)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h3 : AnalyticOn ℂ f (closedBall z₀ ρ)<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<VAR>h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<VAR>h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀<VAR>h8 : (sphere z₀ r).Nonempty<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<VAR>h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀<VAR>h8 : (sphere z₀ r).Nonempty<VAR>h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r)<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<VAR>h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀<VAR>h8 : (sphere z₀ r).Nonempty<VAR>h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r)<VAR>x : ℂ<VAR>hx : x ∈ sphere z₀ r<VAR>hfx : IsMinOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) x<GOAL>∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r✝ m : ℝ<VAR>hf : AnalyticAt ℂ f z₀<VAR>h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀<VAR>R : ℝ<VAR>hR : 0 < R<VAR>h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀<VAR>h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀<VAR>h3 : DiffContOnCl ℂ f (ball z₀ ρ)<VAR>r : ℝ := ρ ⊓ R<VAR>hr : 0 < r<VAR>h5 : closedBall z₀ r ⊆ closedBall z₀ ρ<VAR>h6 : DiffContOnCl ℂ f (ball z₀ r)<VAR>h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀<VAR>h8 : (sphere z₀ r).Nonempty<VAR>h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r)<VAR>x : ℂ<VAR>hx : x ∈ sphere z₀ r<VAR>hfx : IsMinOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) x<GOAL>ball (f z₀) (‖f x - f z₀‖ / 2) ⊆ f '' closedBall z₀ R
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>p : Submodule R M<VAR>x✝¹ x✝ : ↥p<GOAL>I (((B.domRestrict₁₂ p p) x✝¹) x✝) = ((B.domRestrict₁₂ p p) x✝) x✝¹
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>p : Submodule R M<VAR>x✝¹ x✝ : ↥p<GOAL>I ((B ↑x✝¹) ↑x✝) = (B ↑x✝) ↑x✝¹
<VAR>𝕜 : Type u<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>inst✝⁴ : StarRing 𝕜<VAR>inst✝³ : TrivialStar 𝕜<VAR>inst✝² : StarAddMonoid F<VAR>inst✝¹ : ContinuousStar F<VAR>inst✝ : StarModule 𝕜 F<VAR>f' : F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => star (f x)) (star f') x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>X : Type u_4<VAR>inst✝¹² : Monoid M<VAR>S : Submonoid M<VAR>inst✝¹¹ : OreSet S<VAR>inst✝¹⁰ : MulAction M X<VAR>inst✝⁹ : SMul R X<VAR>inst✝⁸ : SMul R M<VAR>inst✝⁷ : IsScalarTower R M M<VAR>inst✝⁶ : IsScalarTower R M X<VAR>inst✝⁵ : SMul R' X<VAR>inst✝⁴ : SMul R' M<VAR>inst✝³ : IsScalarTower R' M M<VAR>inst✝² : IsScalarTower R' M X<VAR>inst✝¹ : SMul R R'<VAR>inst✝ : IsScalarTower R R' M<VAR>r : R<VAR>x : OreLocalization S X<GOAL>(r • 1 /ₒ 1) • x = r • x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Zero (α i)<VAR>inst✝³ : (i : ι) → PartialOrder (α i)<VAR>inst✝² : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>x : ι<VAR>hx : x ∈ (f.rangeIcc g).support<GOAL>x ∈ f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Zero (α i)<VAR>inst✝³ : (i : ι) → PartialOrder (α i)<VAR>inst✝² : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>x : ι<VAR>hx : x ∈ (f.rangeIcc g).support<VAR>h : x ∉ f.support ∪ g.support<GOAL>False
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Zero (α i)<VAR>inst✝³ : (i : ι) → PartialOrder (α i)<VAR>inst✝² : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>x : ι<VAR>hx : x ∈ (f.rangeIcc g).support<VAR>h : x ∉ f.support ∪ g.support<GOAL>(f.rangeIcc g) x = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Zero (α i)<VAR>inst✝³ : (i : ι) → PartialOrder (α i)<VAR>inst✝² : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>x : ι<VAR>hx : x ∈ (f.rangeIcc g).support<VAR>h : x ∉ f.support ∪ g.support<GOAL>Icc 0 0 = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>hdvd : DvdNotUnit a (minpoly A x)<GOAL>(Polynomial.aeval x) a ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>hdvd : DvdNotUnit a (minpoly A x)<VAR>ha : (Polynomial.aeval x) a = 0<GOAL>a.natDegree < (minpoly A x).natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<GOAL>a.natDegree < (minpoly A x).natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<VAR>hcm : c.Monic<GOAL>a.natDegree < (minpoly A x).natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<VAR>hcm : c.Monic<GOAL>a.natDegree < a.natDegree + c.natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<VAR>hcm : c.Monic<GOAL>0 < c.natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<VAR>hcm : c.Monic<VAR>h : c.natDegree ≤ 0<GOAL>IsUnit c
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>ha : (Polynomial.aeval x) a = 0<VAR>left✝ : a ≠ 0<VAR>c : A[X]<VAR>hu : ¬IsUnit c<VAR>he : minpoly A x = a * c<VAR>hcm : c.Monic<VAR>h : c.natDegree ≤ 0<GOAL>IsUnit 1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<GOAL>LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<GOAL>LinearIndependent R ![x, y]
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<GOAL>∀ (g : Fin (Nat.succ 0).succ → R), ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 → ∀ (i : Fin (Nat.succ 0).succ), g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<VAR>g : Fin (Nat.succ 0).succ → R<VAR>hg : ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0<GOAL>∀ (i : Fin (Nat.succ 0).succ), g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<VAR>g : Fin (Nat.succ 0).succ → R<VAR>hg : g 0 • x + g 1 • y = 0<GOAL>∀ (i : Fin (Nat.succ 0).succ), g i = 0