ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi a ≤ a
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<GOAL>Wbtw R x y z ↔ Wbtw R z y x
<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>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<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✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>ker (inl R M M₂) = ⊥
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric<VAR>i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves<VAR>j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves<GOAL>(PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i < (PGame.mk α✝ β✝ a✝¹ a✝).moveRight j
<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>x✝ y : G<VAR>i : ℤ<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : ℕ<GOAL>(finEquivZPowers x hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf 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✝ : Group G<VAR>x✝ y : G<VAR>i : ℤ<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : ℕ<GOAL>(finEquivPowers x hx).symm ((Equiv.Set.ofEq ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c d a b : α<GOAL>a ≤ a / b ↔ b ≤ 1
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>HasDerivAt GammaIntegral (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>HasDerivAt (mellin fun x => ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>LocallyIntegrableOn (fun x => ↑(rexp (-x))) (Ioi 0) volume
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>(fun x => ↑(rexp (-x))) =O[atTop] fun x => x ^ (-(s.re + 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>(fun x => ↑(rexp (-x))) =O[𝓝[>] 0] fun x => x ^ (-0)
<VAR>x y z : ℂ<VAR>hx : x ≠ 0<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x y z : ℂ<VAR>hx : x ≠ 0<GOAL>(if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) = if x = 0 then if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else cexp (log x * y) * 1 else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else cexp (log x * y) * 0 else if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z) else cexp (log x * y) * cexp (log x * z)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSemiring R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : ContinuousStar R<VAR>s : Set R<GOAL>(polynomialFunctions s).starClosure = adjoin R {(toContinuousMapOnAlgHom s) X}
<VAR>α β : Preord<VAR>e : ↑α ≃o ↑β<VAR>x : (forget Preord).obj α<GOAL>(↑e ≫ ↑e.symm) x = (𝟙 α) x
<VAR>α β : Preord<VAR>e : ↑α ≃o ↑β<VAR>x : (forget Preord).obj β<GOAL>(↑e.symm ≫ ↑e) x = (𝟙 β) x
<VAR>n : Type u_1<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<GOAL>(M ^ p).trace = M.trace ^ p
<VAR>n : Type u_1<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<VAR>h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)<GOAL>(M ^ p).trace = M.trace ^ p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<GOAL>leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} 𝒳<VAR>inst✝ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>f : p.obj a ⟶ p.obj b<VAR>h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯<GOAL>p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} 𝒳<VAR>inst✝ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯<GOAL>p.IsHomLift (p.map φ) φ
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>(p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>(if H : ↑(Fin.natAdd p.length i).succ < p.length then p.toFun ⟨↑(Fin.natAdd p.length i).succ, ⋯⟩ else q.toFun ⟨↑(Fin.natAdd p.length i).succ - p.length, ⋯⟩) = q.toFun i.succ
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<GOAL>IsCoprime (x ^ m) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>h : IsCoprime (x ^ m) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>h : IsCoprime (∏ _x ∈ range m, x) y<GOAL>IsCoprime x y
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : Completion α<GOAL>dist x z ≤ dist x y + dist y z
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : Completion α<GOAL>IsClosed {x | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : Completion α<GOAL>∀ (a b c : α), dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
<VAR>R n : Type<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>r : R<GOAL>{ toFun := fun A => (of fun i j => fst (A i j), of fun i j => snd (A i j)), invFun := fun d => of fun i j => (fst d i j, snd d i j), left_inv := ⋯, right_inv := ⋯ }.toFun ((algebraMap R (Matrix n n (DualNumber R))) r) = (algebraMap R (DualNumber (Matrix n n R))) r
<VAR>R n : Type<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>r : R<GOAL>(of fun i j => diagonal (fun m => r) i j, of fun i j => 0) = inl (diagonal fun m => r)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k✝ : D ⟶ E<VAR>i✝ : ι<VAR>e f g : C ⟶ D<VAR>h : Homotopy e f<VAR>k : Homotopy f g<VAR>i j : ι<VAR>w : ¬c.Rel j i<GOAL>(h.hom + k.hom) i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k✝ : D ⟶ E<VAR>i✝ : ι<VAR>e f g : C ⟶ D<VAR>h : Homotopy e f<VAR>k : Homotopy f g<VAR>i : ι<GOAL>e.f i = (dNext i) (h.hom + k.hom) + (prevD i) (h.hom + k.hom) + g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k✝ : D ⟶ E<VAR>i✝ : ι<VAR>e f g : C ⟶ D<VAR>h : Homotopy e f<VAR>k : Homotopy f g<VAR>i : ι<GOAL>(dNext i) h.hom + (prevD i) h.hom + ((dNext i) k.hom + (prevD i) k.hom + g.f i) = (dNext i) h.hom + (dNext i) k.hom + ((prevD i) h.hom + (prevD i) k.hom) + g.f i
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>hf : AEMeasurable f μ<GOAL>(μ.tilted f).rnDeriv μ =ᶠ[ae μ] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>hf : AEMeasurable f μ<GOAL>(fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x) =ᶠ[ae μ] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>hf : AEMeasurable f μ<VAR>x : α<VAR>hx : μ.rnDeriv μ x = 1<GOAL>ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>a : ι → α<VAR>hs : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)<GOAL>HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>a : ι → α<VAR>hs : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)<GOAL>HasProd ((⋃ i ∈ s, t i).mulIndicator f) (∏ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>a : ι → α<VAR>hs : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)<GOAL>HasProd (fun a => ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>¬Irreducible (x ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>hf : Injective f<GOAL>Injective (image f)
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (circumcenter t)) = circumradius t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>IsNilpotent (mulRight R a) ↔ IsNilpotent a
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝ : CommRing R<VAR>a b : lib R X<VAR>h : Rel R X a b<GOAL>Rel R X (-a) (-b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>{a} ○ {b} = if Disjoint a b then {a ⊔ b} else ∅
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CharP R 2<VAR>x y : R<GOAL>(x + y) * (x + y) = x * x + y * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<GOAL>∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) univ
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>a : M₀<VAR>m n✝ : ℕ<VAR>inst✝ : NoZeroDivisors M₀<VAR>n : ℕ<VAR>ha : a ^ (n + 1) = 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>a : M₀<VAR>m n✝ : ℕ<VAR>inst✝ : NoZeroDivisors M₀<VAR>n : ℕ<VAR>ha : a ^ n = 0 ∨ a = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B : BilinForm R M<VAR>e : M ≃ₗ[R] M'<VAR>h : ((congr e) B).Nondegenerate<GOAL>B.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B : BilinForm R M<VAR>e : M ≃ₗ[R] M'<VAR>h : ((congr e) B).Nondegenerate<GOAL>B = (congr e.symm) ((congr e) B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>M.Coindep X ↔ (∃ B, M.Base B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>X ⊆ M.E → ((∃ B, M.Base B ∧ Disjoint X B) ↔ ∃ B, M.Base B ∧ B ⊆ M.E ∧ Disjoint B X)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>x y : R₁<VAR>hy : y ∈ R₁⁰<GOAL>spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>x y : R₁<VAR>hy : y ∈ R₁⁰<VAR>this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1<GOAL>spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>x y : R₁<VAR>hy : y ∈ R₁⁰<VAR>this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1<VAR>y' : (FractionalIdeal R₁⁰ K)ˣ := Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this<VAR>coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)<GOAL>spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>x y : R₁<VAR>hy : y ∈ R₁⁰<VAR>this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1<VAR>y' : (FractionalIdeal R₁⁰ K)ˣ := Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this<VAR>coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)<GOAL>spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ ↑y' * ↑(Ideal.span {x} * I) = ↑y' * ↑(Ideal.span {y} * J)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝³ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝ : Fintype ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<VAR>b : (i : ι) → Basis (Module.Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i => Module.Free.chooseBasis R ↥(N i)<GOAL>(trace R M) f = ∑ i : ι, (trace R ↥(N i)) (f.restrict ⋯)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>a b c d : R<VAR>x : R × R<GOAL>((toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>X : Subobject B<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>h₁ : mk f ≤ X<VAR>h₂ : X ≤ mk g<GOAL>ofMkLE f X h₁ ≫ X.ofLEMk g h₂ = ofMkLEMk f g ⋯
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>X : Subobject B<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>h₁ : mk f ≤ X<VAR>h₂ : X ≤ mk g<GOAL>(underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom = (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso g).hom
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>H : ∀ (i : ι), f i < sup f<GOAL>(sup f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>H : sup f = lsub f<GOAL>(sup f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>H : sup f = lsub f<GOAL>(lsub f).cof ≤ Cardinal.lift.{v, u} #ι
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>c : ℝ<GOAL>cgf (fun x => c) μ t = log (μ Set.univ).toReal + t * c
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>c : ℝ<GOAL>log ((μ Set.univ).toReal * rexp (t * c)) = log (μ Set.univ).toReal + t * c
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>c : ℝ<GOAL>log (μ Set.univ).toReal + log (rexp (t * c)) = log (μ Set.univ).toReal + t * c
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>c : ℝ<GOAL>(μ Set.univ).toReal ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → Tropical (WithTop R)<GOAL>untrop (∑ i ∈ s, f i) = ⨅ i, untrop (f ↑i)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 S<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : S ∈ l<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : S ∈ l<VAR>hl_ne : l.NeBot<VAR>hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : S ∈ l<VAR>hl_ne : l.NeBot<VAR>hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s<VAR>t : Set α<VAR>htS : t ⊆ S<VAR>htl : t ∈ l<VAR>htU : t ×ˢ t ⊆ U<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : S ∈ l<VAR>hl_ne : l.NeBot<VAR>hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s<VAR>t : Set α<VAR>htS : t ⊆ S<VAR>htl : t ∈ l<VAR>htU : t ×ˢ t ⊆ U<VAR>i : ι<VAR>hi : t ⊆ s i<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<VAR>S : Set α := ⋃ i, s i<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : S ∈ l<VAR>hl_ne : l.NeBot<VAR>hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s<VAR>t : Set α<VAR>htS : t ⊆ S<VAR>htl : t ∈ l<VAR>htU : t ×ˢ t ⊆ U<VAR>i : ι<VAR>hi : t ⊆ s i<VAR>x : α<VAR>hxs : x ∈ s i<VAR>hlx : l ≤ 𝓝 x<GOAL>∃ x ∈ S, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.110262}<VAR>x : ↑(Iio o)<GOAL>↑x < type fun x x_1 => x < x_1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.110262}<VAR>x : ↑(Iio o)<GOAL>↑x < o
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o a : Ordinal.{?u.110262}<VAR>property✝¹ : a ∈ Iio o<VAR>b : Ordinal.{?u.110262}<VAR>property✝ : b ∈ Iio o<GOAL>{ toFun := fun x => enum (fun x x_1 => x < x_1) ↑x ⋯, invFun := fun x => ⟨typein (fun x x_1 => x < x_1) x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨a, property✝¹⟩ ≤ { toFun := fun x => enum (fun x x_1 => x < x_1) ↑x ⋯, invFun := fun x => ⟨typein (fun x x_1 => x < x_1) x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨b, property✝⟩ ↔ ⟨a, property✝¹⟩ ≤ ⟨b, property✝⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a✝ b✝ : α<VAR>a b : WithTop α<GOAL>a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a✝ b✝ : α<VAR>a b : WithTop α<GOAL>(∃ a_1, WithTop.toDual a = ↑(toDual a_1) ∧ WithTop.toDual b < ↑(toDual a_1)) ↔ ∃ p, a = ↑p ∧ ↑p < b
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>x✝¹ : Finmap β<VAR>x✝ : α<GOAL>lookup x✝ (keysLookupEquiv.symm (keysLookupEquiv x✝¹)) = (↑(keysLookupEquiv x✝¹)).2 x✝
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.sections = L.sectionsTR