ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>u : L<VAR>x✝ : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u<VAR>y : L<VAR>hy : y ∈ rootSpace H α<VAR>z : L<VAR>hz : z ∈ rootSpace H (-α)<VAR>hyz : ⁅y, z⁆ = u<GOAL>u ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>u : L<VAR>x✝ : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u<VAR>y : L<VAR>hy : y ∈ rootSpace H α<VAR>z : L<VAR>hz : z ∈ rootSpace H (-α)<VAR>hyz : ⁅y, z⁆ = u<GOAL>u ∈ H ↔ ↑((rootSpaceProduct R L H α (-α) 0 ⋯) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)) ∈ ↑(rootSpace H 0)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>Φ : Submodule R (Module.Dual R M)<VAR>x : M<GOAL>x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0
<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>n : Num<GOAL>↑n.bit0 = 2 * ↑n
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Ici a ↔ x ∈ Ici (r • a)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y ∈ Ici a, r * y = x) ↔ x ∈ Ici (r * a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>f ^ n ∈ 𝒜 (m * n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>f ^ n ∈ 𝒜 (n * m)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>a ∈ carrier f_deg q ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>a ∈ carrier f_deg q ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : RingHom.ker f ≤ I<GOAL>map f (sInf {J | I ≤ J ∧ J.IsMaximal}) = sInf {J | map f I ≤ J ∧ J.IsMaximal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J<GOAL>map f (sInf {J | I ≤ J ∧ J.IsMaximal}) = sInf {J | map f I ≤ J ∧ J.IsMaximal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J<GOAL>sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J<GOAL>sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})
<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✝ : Zero M<VAR>f : α → β<VAR>a : α<VAR>m : M<VAR>hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)<GOAL>comapDomain f (single (f a) m) hif = single a m
<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✝ : Zero M<VAR>f : α → β<VAR>a : α<VAR>hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)<GOAL>comapDomain f (single (f a) 0) hif = single a 0
<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✝ : Zero M<VAR>f : α → β<VAR>a : α<VAR>m : M<VAR>hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)<VAR>hm : m ≠ 0<GOAL>comapDomain f (single (f a) m) hif = single a m
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<GOAL>RespectsIso P
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<GOAL>∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>e : R ≃+* S<VAR>this : Algebra R S := e.toRingHom.toAlgebra<GOAL>P e.toRingHom
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : PropertyIsLocal P<VAR>R S : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>e : R ≃+* S<VAR>this✝ : Algebra R S := e.toRingHom.toAlgebra<VAR>this : IsLocalization.Away 1 S<GOAL>P e.toRingHom
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>h : ∀ i ∈ s, f i < 1<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, 1 ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 3 → β<GOAL>∏ i : Fin 3, f i = f 0 * f 1 * f 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 3 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.17678, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.17685, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.17692, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>f : X ⟶ Y<VAR>a : M<VAR>g : ShiftedHom Y Z a<GOAL>a + m₀ = a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.17685, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.17692, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>a : M<VAR>g : ShiftedHom Y Z a<GOAL>(mk₀ 0 ⋯ f).comp g ⋯ = f ≫ g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B✝ C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : OrderClosedTopology 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : IsClosed A<GOAL>IsClosed B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : OrderClosedTopology 𝕜<VAR>A : Set E<VAR>hA : IsClosed A<VAR>hAB : IsExposed 𝕜 A ∅<GOAL>IsClosed ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B✝ C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : OrderClosedTopology 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : IsClosed A<VAR>hB : B.Nonempty<GOAL>IsClosed B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : OrderClosedTopology 𝕜<VAR>A : Set E<VAR>hA : IsClosed A<VAR>l : E →L[𝕜] 𝕜<VAR>a : 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ l x}<VAR>hB : {x | x ∈ A ∧ a ≤ l x}.Nonempty<GOAL>IsClosed {x | x ∈ A ∧ a ≤ l x}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a a₁ a₂ : α<VAR>h₁ : r a₁ a<VAR>h₂ : r a₂ a<GOAL>∀ x' ∈ {a₁, a₂}, r x' a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a a₁ a₂ : α<VAR>h₁ : r a₁ a<VAR>h₂ : r a₂ a<GOAL>r a₁ a ∧ r a₂ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : IsConj σ τ<GOAL>σ.support.card = τ.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ.IsCycle<VAR>π : Perm α<VAR>hτ : (π * σ * π⁻¹).IsCycle<VAR>h : IsConj σ (π * σ * π⁻¹)<GOAL>σ.support.card = (π * σ * π⁻¹).support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ.IsCycle<VAR>π : Perm α<VAR>hτ : (π * σ * π⁻¹).IsCycle<VAR>h : IsConj σ (π * σ * π⁻¹)<VAR>x✝ : α<VAR>ha : x✝ ∈ σ.support<GOAL>(fun a x => π a) x✝ ha ∈ (π * σ * π⁻¹).support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ.IsCycle<VAR>π : Perm α<VAR>hτ : (π * σ * π⁻¹).IsCycle<VAR>h : IsConj σ (π * σ * π⁻¹)<VAR>b : α<VAR>hb : b ∈ (π * σ * π⁻¹).support<GOAL>π⁻¹ b ∈ σ.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ.IsCycle<VAR>π : Perm α<VAR>hτ : (π * σ * π⁻¹).IsCycle<VAR>h : IsConj σ (π * σ * π⁻¹)<VAR>b : α<VAR>hb : π⁻¹ b ∉ σ.support<GOAL>b ∉ (π * σ * π⁻¹).support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ.IsCycle<VAR>π : Perm α<VAR>hτ : (π * σ * π⁻¹).IsCycle<VAR>h : IsConj σ (π * σ * π⁻¹)<VAR>b : α<VAR>hb : σ (π⁻¹ b) = π⁻¹ b<GOAL>b ∉ (π * σ * π⁻¹).support
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<GOAL>o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)<GOAL>o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)<GOAL>r • (o.rotation ↑(π / 2)) x ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace γ<VAR>m : Measure α<VAR>f : α → Measure β<VAR>g : β → Measure γ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((m.bind f).bind g) s = (m.bind fun a => (f a).bind g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace γ<VAR>m : Measure α<VAR>f : α → Measure β<VAR>g : β → Measure γ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), (((fun m => m.bind g) ∘ f) a) s ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace γ<VAR>m : Measure α<VAR>f : α → Measure β<VAR>g : β → Measure γ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), ∫⁻ (a : β), (g a) s ∂f a ∂m
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : HasContDiffBump G<VAR>inst✝⁴ : CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : FiniteDimensional ℝ G<VAR>x₀ : G<VAR>hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀<GOAL>(φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀ = g x₀
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : HasContDiffBump G<VAR>inst✝⁴ : CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : FiniteDimensional ℝ G<VAR>x₀ : G<VAR>hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀<GOAL>∫ (t : G), ((lsmul ℝ ℝ) (φ.normed μ t)) (g x₀) ∂μ = g x₀
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hg : x ^ p = 1<VAR>hg1 : x ≠ 1<GOAL>¬IsFixedPt (fun x_1 => x * x_1) 1
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>L' : Language<VAR>φ : L →ᴸ L'<VAR>h : φ.Injective<GOAL>(φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x✝ y x : G<GOAL>∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x✝ y x : G<VAR>w : ℕ<VAR>hw1 : w > 0<VAR>hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1<GOAL>∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x✝ y x : G<VAR>w : ℕ<VAR>hw1 : w > 0<VAR>hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1<GOAL>x ^ ↑w = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x✝ y x : G<VAR>w : ℕ<VAR>hw1 : w > 0<VAR>hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1<GOAL>x ^ w = 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>c✝ c₁ c₂ p₁✝ p₂✝ p₁ p₂ c : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ c ∈ perpBisector p₂ p₁
<GOAL>Ici 2 = Ioi 0 ∩ Ici 2
<GOAL>Ioi 0 ∩ Ici 2 = Ici 2
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>x : CliffordAlgebra Q₁<GOAL>(equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁)) x = AlgEquiv.refl x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : SurjOn fa s t<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxt : fa x ∈ t<GOAL>fb (f x) ∈ fb '' (f '' s)
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∠ p₃ p₂ p₁ = π
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : E<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>((pderivCLM 𝕜 m) f) x = lineDeriv ℝ (⇑f) x m
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>Function.Injective ⇑(mixedEmbedding K)
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u<VAR>inst✝¹ : Finite α<VAR>κ : Type v<VAR>inst✝ : Finite κ<VAR>ι : Type<VAR>ιfin : Fintype ι<VAR>hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ l, IsMono C l<VAR>C : (ι → α) → κ<VAR>l : Line α ι<VAR>c : ULift.{u, v} κ<VAR>hc : ∀ (x : α), (ULift.up ∘ C) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>x : α<GOAL>C ((fun x i => (l.idxFun i).getD x) x) = c.down
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>h✝ : l.Nodup<VAR>l₁ l₂ : List α<VAR>h : Lex (fun x x_1 => x ≠ x_1) l₁.reverse l₂.reverse<GOAL>l₁ ≠ l₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ≤ 0<GOAL>n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>ha : 0 ≤ a<GOAL>n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<VAR>z : N<VAR>H : z = f.mk' x y<GOAL>z * f.toMap ↑y = f.toMap x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<VAR>z : N<VAR>H : z * f.toMap ↑y = f.toMap x<GOAL>z = f.mk' x y
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>(fun x => rexp (llr μ ν x)) =ᶠ[ae ν] fun x => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>x : α<VAR>hx : μ.rnDeriv ν x < ⊤<GOAL>rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a b c d : α<GOAL>a ⊔ b ≤ b ∧ b ≤ a ⊔ b ↔ a ≤ b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁵ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hF : IsClosed F<GOAL>μ F = 1 ↔ F = univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : ↥(Lp H 1 μ)<GOAL>‖f‖ = ∫ (a : α), ‖↑↑f a‖ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : ↥(Lp H 1 μ)<GOAL>(∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ).toReal = ∫ (a : α), ‖↑↑f a‖ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f : ↥(Lp H 1 μ)<GOAL>(∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖↑↑f a‖ ∂μ).toReal
<VAR>q : ℕ+<GOAL>Fintype.card (ZMod ↑q × ZMod ↑q) = ↑q ^ 2