ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<GOAL>|(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<GOAL>|(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<VAR>b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b<GOAL>|(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<VAR>b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b<VAR>bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))<GOAL>|(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<VAR>b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b<VAR>bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))<GOAL>|((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| = |↑(b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<VAR>b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b<VAR>bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))<GOAL>|((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| = |(algebraMap ℤ ℚ) (b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : IsDedekindDomain R<VAR>inst✝⁹ : Module.Free ℤ R<VAR>inst✝⁸ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K<VAR>inst✝³ : Algebra ℚ K<VAR>inst✝² : NoZeroDivisors K<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal R⁰ K<VAR>bI : Basis ι ℤ ↥↑I<VAR>this : Nontrivial K<VAR>b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b<VAR>bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))<GOAL>|((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| = |(b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI)).det| / |↑((Algebra.norm ℤ) ↑I.den)|
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.primeFactorsList ++ b.primeFactorsList).prod = a * b
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>∀ p ∈ a.primeFactorsList ++ b.primeFactorsList, Prime p
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p 0) 1) ^ p ^ 0 = 1
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<GOAL>1 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s t : Set α<GOAL>Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.prev x hx = l'.prev x ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.reverse.next x ⋯ = l'.reverse.next x ⋯
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q R : C<VAR>f : Q ⟶ R<VAR>a : P ⟶ Q<VAR>h : a ≫ f = 0<GOAL>pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a)) = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)<GOAL>Step L₁ L₂
<VAR>b : ℂ<VAR>x : ℝ<GOAL>‖cexp (-b * ↑x ^ 2)‖ = rexp (-b.re * x ^ 2)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hf : HasIntegral I l f vol y<GOAL>HasIntegral I l (-f) vol (-y)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D<VAR>inst✝¹⁰ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>A' : Type u_4<VAR>inst✝¹ : NormedCommRing A'<VAR>inst✝ : NormedAlgebra 𝕜 A'<VAR>f g : E → A<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D<VAR>inst✝¹⁰ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>A' : Type u_4<VAR>inst✝¹ : NormedCommRing A'<VAR>inst✝ : NormedAlgebra 𝕜 A'<VAR>f g : E → A<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) univ x‖ ≤ ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<GOAL>(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<GOAL>(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<VAR>u : (Matrix n n R)ˣ := P.nonsingInvUnit h'<GOAL>(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<VAR>u : (Matrix n n R)ˣ := P.nonsingInvUnit h'<VAR>v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯<GOAL>(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<VAR>u : (Matrix n n R)ˣ := P.nonsingInvUnit h'<VAR>v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯<VAR>x : Matrix n n R := A₁ᵀ * Pᵀ * J<VAR>y : Matrix n n R := J * P * A₂<GOAL>x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<VAR>u : (Matrix n n R)ˣ := P.nonsingInvUnit h'<VAR>v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯<VAR>x : Matrix n n R := A₁ᵀ * Pᵀ * J<VAR>y : Matrix n n R := J * P * A₂<GOAL>x * ↑u = ↑v * y ↔ ↑v⁻¹ * x * ↑u = y
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>P : Matrix n n R<VAR>h : IsUnit P<VAR>h' : IsUnit P.det<VAR>u : (Matrix n n R)ˣ := P.nonsingInvUnit h'<VAR>v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯<VAR>x : Matrix n n R := A₁ᵀ * Pᵀ * J<VAR>y : Matrix n n R := J * P * A₂<GOAL>x * ↑u = ↑v * y ↔ ↑v⁻¹ * (x * ↑u) = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>f✝ : ι →₀ α<VAR>i✝ : ι<VAR>a : α<VAR>f : ι →₀ α<VAR>i : ι<GOAL>i ∈ f.support ↔ (fun i => {f i}) i ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>f✝ : ι →₀ α<VAR>i✝ : ι<VAR>a : α<VAR>f : ι →₀ α<VAR>i : ι<GOAL>f i = 0 ↔ (fun i => {f i}) i = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => f x * r) l atBot ↔ 0 < r
<VAR>x y : ℝ<GOAL>↑(sin (2 * x)) = ↑(2 * sin x * cos x)
<VAR>x y : ℂ<GOAL>sin x ^ 2 + cos x ^ 2 = cosh (x * I) ^ 2 - sinh (x * I) ^ 2
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>H : ¬M.IsTwoBlockDiagonal<VAR>hM : M (inr ()) (inr ()) = 0<GOAL>∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) = 0<VAR>H : (¬∀ (i : Fin r) (j : Unit), of (fun i j => M (inl i) (inr j)) i j = 0 i j) ∨ ¬∀ (i : Unit) (j : Fin r), of (fun i j => M (inr i) (inl j)) i j = 0 i j<GOAL>∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹ * A = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<VAR>val✝ : Invertible A<GOAL>A⁻¹ * A = 1
<VAR>a b c d m n : ℤ<VAR>hmn : m ∣ n<GOAL>n / m ∣ n
<VAR>a b c d n : ℤ<VAR>hmn : 0 ∣ n<GOAL>n / 0 ∣ n
<VAR>a b c d m n : ℤ<VAR>hmn : m ∣ n<VAR>hm : m ≠ 0<GOAL>n / m ∣ n
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>p p' : Submodule R P<VAR>q q' : Submodule R Q<VAR>hp : p ≤ p'<VAR>hq : q ≤ q'<GOAL>range (mapIncl p q) ≤ range (mapIncl p' q')
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>p p' : Submodule R P<VAR>q q' : Submodule R Q<VAR>hp : p ≤ p'<VAR>hq : q ≤ q'<GOAL>Submodule.span R (Set.image2 (fun x x_1 => x ⊗ₜ[R] x_1) ↑p ↑q) ≤ Submodule.span R (Set.image2 (fun x x_1 => x ⊗ₜ[R] x_1) ↑p' ↑q')
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℤ<VAR>h : x * x = ↑d * y * y<GOAL>x = 0 ∧ y = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℤ<VAR>h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)<GOAL>x = 0 ∧ y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n✝ m l n : ℕ<VAR>hn : 1 < n<GOAL>(range n).Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n✝ m l n : ℕ<VAR>hn : 1 < n<GOAL>(Set.Iio n).Nontrivial
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>hstart : start ≤ min stop as.size<VAR>tru : Prop<VAR>fal : Nat → Prop<VAR>h0 : fal start<VAR>hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])<GOAL>SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (anyM p as start stop)
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>hstart : start ≤ min stop as.size<VAR>tru : Prop<VAR>fal : Nat → Prop<VAR>h0 : fal start<VAR>hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])<GOAL>SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (anyM.loop p as (min stop as.size) ⋯ start)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>h : Cauchy l<GOAL>Cauchy ↑(Ultrafilter.of l)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>h : Cauchy l<VAR>this : l.NeBot<GOAL>Cauchy ↑(Ultrafilter.of l)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>h : Cauchy l<VAR>this✝ : l.NeBot<VAR>this : ↑(Ultrafilter.of l) ≤ l<GOAL>Cauchy ↑(Ultrafilter.of l)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hn : upcrossingsBefore a b f N ω < n<GOAL>upperCrossingTime a b f N n ω = N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hn : upcrossingsBefore a b f N ω < n<GOAL>¬upperCrossingTime a b f N n ω < N
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<GOAL>dimH s = ↑(finrank ℝ E)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<VAR>e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ<GOAL>dimH s = ↑(finrank ℝ E)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<VAR>e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ<GOAL>dimH (⇑e '' s) = ↑(finrank ℝ E)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<VAR>e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ<GOAL>dimH (⇑e '' s) ≤ ↑(finrank ℝ E)