ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁷ : DecidableEq n<VAR>inst✝⁶ : DecidableEq p<VAR>inst✝⁵ : DecidableEq q<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype p<VAR>inst✝¹ : Fintype q<VAR>inst✝ : Fintype l<GOAL>indefiniteDiagonal (Unit ⊕ l) l R = (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : NumDenSameDeg 𝒜 x<GOAL>(Quotient.mk'' y1 * Quotient.mk'' y2).val = val (Quotient.mk'' y1) * val (Quotient.mk'' y2)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : NumDenSameDeg 𝒜 x<GOAL>Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk (↑y1.num * ↑y2.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>hb : AddLECancellable b<VAR>hc : AddLECancellable c<VAR>hba : b ≤ a<VAR>hca : c ≤ a<GOAL>a - b = a - c ↔ b = c
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>((gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>((curry (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) ∘ₗ ↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm ∘ₗ LinearMap.lTensor (⨁ (i : ι), 𝒜 i) (↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) ∘ₗ LinearMap.rTensor (⨁ (i : ι), ℬ i) ↑(gradedComm R ℬ 𝒜) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)))) (a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>(map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i))) ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm (a₁ ⊗ₜ[R] (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) ((gradedComm R ℬ 𝒜) ((lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] b₂))) = (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>(map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i))) ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm (a₁ ⊗ₜ[R] (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) (((-1) ^ (i₂ * j₁) • (lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) = (-1) ^ (i₂ * j₁) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>(map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i))) ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm (a₁ ⊗ₜ[R] (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) ((↑↑((-1) ^ (i₂ * j₁)) • (lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) = ↑↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>↑↑((-1) ^ (i₂ * j₁)) • (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i))) ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm (a₁ ⊗ₜ[R] (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) (((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) = ↑↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
<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₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₁<GOAL>(piecewise h₁ h₂ h f g hfg) 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₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₁<GOAL>(if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = f ⟨x, hx⟩
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.Equation P ↔ P y ^ 2 = P x ^ 3
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<VAR>b : R<VAR>hb : b ∈ AddSubmonoid.closure ↑S<GOAL>∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ x ∈ ↑S, ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * x ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * 0 ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ (x y : R), (∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * x ∈ AddSubmonoid.closure ↑S) → (∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * y ∈ AddSubmonoid.closure ↑S) → ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * (x + y) ∈ AddSubmonoid.closure ↑S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : Type u_3<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : CharZero k<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<GOAL>↑(↑m / ↑n) = ↑m / ↑n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.addY P Q = (P x * Q z) ^ 3 * Q y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>-((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3)) - W'.a₁ * ((P x * Q z) ^ 2 * Q x) * (P x * Q z * Q z) - W'.a₃ * (P x * Q z * Q z) ^ 3 = (P x * Q z) ^ 3 * Q y
<VAR>m : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ 2 * m ^ 2<GOAL>p = 2 ∨ p ∣ m.natAbs
<VAR>m : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ 2 * m ^ 2<VAR>hp2 : p ∣ Int.natAbs 2<GOAL>p = 2 ∨ p ∣ m.natAbs
<VAR>m : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ 2 * m ^ 2<VAR>hpp : p ∣ (m ^ 2).natAbs<GOAL>p = 2 ∨ p ∣ m.natAbs
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Finite M<VAR>G : Type u_2<VAR>inst✝ : Group G<GOAL>commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Finite M<VAR>G : Type u_2<VAR>inst✝ : Group G<GOAL>↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
<VAR>R : Type ?u.47046<VAR>S : Type ?u.47049<VAR>M : Type ?u.47052<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>x : ↥(B.dualSubmodule N)<VAR>r : R<VAR>m : ↥N<GOAL>(algebraMap R S) ({ toFun := B.dualSubmoduleParing x, map_add' := ⋯ }.toFun (r • m)) = (algebraMap R S) ((RingHom.id R) r • { toFun := B.dualSubmoduleParing x, map_add' := ⋯ }.toFun m)
<VAR>R : Type ?u.47046<VAR>S : Type ?u.47049<VAR>M : Type ?u.47052<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>r : R<VAR>x : ↥(B.dualSubmodule N)<VAR>y : ↥N<GOAL>(algebraMap R S) (({ toFun := fun x => { toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (r • x)) y) = (algebraMap R S) (((RingHom.id R) r • { toFun := fun x => { toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun x) y)
<VAR>x✝ y x : ℝ<VAR>h₂ : x ∈ Icc (-(π / 2)) (π / 2)<GOAL>arcsin (sin x) = x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>a : 𝕜'<VAR>x✝ : 𝕜<GOAL>logDeriv (fun x => a) x✝ = 0 x✝
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : b ≠ c<GOAL>(swap a b * swap a c).IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : b ≠ c<GOAL>(swap a b * swap a c).support = {a, b, c}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : b ≠ c<GOAL>∀ x ∈ (swap a b).support ⊔ (swap a c).support, x ∈ {a, b, c}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : b ≠ c<VAR>x : α<VAR>hx : x ∈ {a, b, c}<GOAL>x ∈ (swap a b * swap a c).support
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<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>N : LieSubmodule R L M<VAR>x✝ : L<VAR>φ : R<VAR>k : ℕ<VAR>x : L<GOAL>MapsTo ⇑(((toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<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>N : LieSubmodule R L M<VAR>x✝ : L<VAR>φ : R<VAR>k : ℕ<VAR>x : L<GOAL>MapsTo (⇑((toEnd R L M) x - (algebraMap R (Module.End R M)) φ))^[k] ↑N ↑N
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<GOAL>↑↑1 = ↑1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<GOAL>↑↑1 = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<GOAL>↑⋯.unit = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<VAR>x : E<VAR>xF : x ∉ F<VAR>hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<VAR>x : E<VAR>xF : x ∉ F<VAR>hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖<VAR>x0 : x ≠ 0<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<VAR>x : E<VAR>xF : x ∉ F<VAR>hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖<VAR>x0 : x ≠ 0<VAR>d : 𝕜<VAR>d0 : d ≠ 0<VAR>dxlt : ‖d • x‖ < R<VAR>ledx : R / ‖c‖ ≤ ‖d • x‖<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<VAR>x : E<VAR>xF : x ∉ F<VAR>hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖<VAR>x0 : x ≠ 0<VAR>d : 𝕜<VAR>d0 : d ≠ 0<VAR>dxlt : ‖d • x‖ < R<VAR>ledx : R / ‖c‖ ≤ ‖d • x‖<VAR>y : E<VAR>hy : y ∈ F<VAR>y' : E := d⁻¹ • y<GOAL>1 ≤ ‖d • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>Rpos : 0 < R<VAR>this : ‖c‖ / R < 1<VAR>x : E<VAR>xF : x ∉ F<VAR>hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖<VAR>x0 : x ≠ 0<VAR>d : 𝕜<VAR>d0 : d ≠ 0<VAR>dxlt : ‖d • x‖ < R<VAR>ledx : R / ‖c‖ ≤ ‖d • x‖<VAR>y : E<VAR>hy : y ∈ F<VAR>y' : E := d⁻¹ • y<VAR>yy' : y = d • y'<GOAL>1 ≤ ‖d • x - y‖
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>x : α<VAR>h : (#α).ord = type r<GOAL>(typein r x).card < #α
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>x : α<VAR>h : (#α).ord = type r<GOAL>typein r x < type r
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>ι : Type u_1<VAR>u : Finset ι<VAR>A : ι → 𝕜 → F<VAR>A' : ι → F<VAR>h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x<GOAL>HasStrictDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>ma mb : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hma : Tendsto ma f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ 0<VAR>hmb : Tendsto mb f (𝓝 b)<VAR>hb : b ≠ ⊤ ∨ a ≠ ⊤<GOAL>Tendsto (fun a => ma a / mb a) f (𝓝 (a / b))
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>τ f = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>τ (f ^ n) = ↑m ↔ ∃ x, (f ^ n) x = x + ↑m
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>s : Set S<VAR>t : Set M<GOAL>s • span R t = span R (s • t)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>inst✝² : MonoCoprod D<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>A B : C<VAR>c : BinaryCofan A B<VAR>h : IsColimit c<VAR>c' : BinaryCofan (F.obj ((pair A B).obj { as := WalkingPair.left })) (F.obj ((pair A B).obj { as := WalkingPair.right })) := BinaryCofan.mk (F.map c.inl) (F.map c.inr)<GOAL>Mono c.inl
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>inst✝² : MonoCoprod D<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>A B : C<VAR>c : BinaryCofan A B<VAR>h : IsColimit c<VAR>c' : BinaryCofan (F.obj ((pair A B).obj { as := WalkingPair.left })) (F.obj ((pair A B).obj { as := WalkingPair.right })) := BinaryCofan.mk (F.map c.inl) (F.map c.inr)<GOAL>Mono (F.map c.inl)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>inst✝² : MonoCoprod D<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>A B : C<VAR>c : BinaryCofan A B<VAR>h : IsColimit c<VAR>c' : BinaryCofan (F.obj ((pair A B).obj { as := WalkingPair.left })) (F.obj ((pair A B).obj { as := WalkingPair.right })) := BinaryCofan.mk (F.map c.inl) (F.map c.inr)<GOAL>Mono c'.inl
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>inst✝² : MonoCoprod D<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>A B : C<VAR>c : BinaryCofan A B<VAR>h : IsColimit c<VAR>c' : BinaryCofan (F.obj ((pair A B).obj { as := WalkingPair.left })) (F.obj ((pair A B).obj { as := WalkingPair.right })) := BinaryCofan.mk (F.map c.inl) (F.map c.inr)<GOAL>IsColimit c'
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>inst✝² : MonoCoprod D<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>A B : C<VAR>c : BinaryCofan A B<VAR>h : IsColimit c<VAR>c' : BinaryCofan (F.obj ((pair A B).obj { as := WalkingPair.left })) (F.obj ((pair A B).obj { as := WalkingPair.right })) := BinaryCofan.mk (F.map c.inl) (F.map c.inr)<GOAL>∀ (j : Discrete WalkingPair), c.ι.app j ≫ (eqToIso ⋯).hom = (BinaryCofan.mk c.inl c.inr).ι.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h1s : support f ⊆ s<GOAL>IntegrableOn f s μ ↔ Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h1s : support f ⊆ s<VAR>h : IntegrableOn f s μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h1s : support f ⊆ s<VAR>h : IntegrableOn f s μ<VAR>x : α<VAR>hx : x ∉ s<GOAL>f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h1s : support f ⊆ s<VAR>h : IntegrableOn f s μ<VAR>x : α<VAR>hx : f x ≠ 0<GOAL>x ∈ s