mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.instBEqTriggerCondition.beq : {ctx : Type u_1} →
  [BEq ctx] → Mathlib.TacticAnalysis.TriggerCondition ctx → Mathlib.TacticAnalysis.TriggerCondition ctx → Bool
-- Mathlib.Logic.Basic
exists₂_comm : ∀ {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6}
  {p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop}, (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂
-- Mathlib.Topology.Inseparable
/-- **Alias** of `specializes_of_eq`. -/
Specializes.of_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x = y → x ⤳ y
-- Mathlib.Topology.VectorBundle.Basic
/-- The projection on the base of a vector bundle created from core is an open map  -/
VectorBundleCore.isOpenMap_proj : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
  IsOpenMap Z.proj
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOpsRef.toDoOpsImpl : Lean.Elab.Do.DoOpsRef → Lean.Elab.Do.DoOps
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- A square matrix is column stochastic iff all entries are nonnegative, and left
multiplication by the vector of all 1s gives the vector of all 1s.  -/
Matrix.colStochastic : (R : Type u_3) →
  (n : Type u_4) →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring R] → [inst_3 : PartialOrder R] → [IsOrderedRing R] → Submonoid (Matrix n n R)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustOfScientific : Lean.Option Bool
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_pow : ∀ (a : ENNReal) (n : ℕ), (a ^ n).toReal = a.toReal ^ n
-- Lean.Meta.Basic
Lean.Meta.mkLevelErrorMessage : Lean.Meta.PostponedEntry → Lean.MetaM Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- Composition of `π` with `f` and with `g` agree  -/
CategoryTheory.IsSplitCoequalizer.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp π h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp π h)
-- Mathlib.RingTheory.RingHom.Flat
/-- Flat is a local property of ring homomorphisms.  -/
RingHom.Flat.propertyIsLocal : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.div_subst : ∀ {α : Type u_1} [inst : Field α] {n1 n2 k e1 e2 t1 : α}, n1 * e1 = t1 → n2 / e2 = 1 → n1 * n2 = k → k * (e1 / e2) = t1
-- Lean.Elab.Exception
Lean.Elab.throwAlreadyDeclaredUniverseLevel : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → m α
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup N} [nH : H.Normal]
  (f : G →+ N), (AddSubgroup.comap f H).Normal
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_injective : Function.Injective ENNReal.ofNNReal
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.const.sizeOf_spec : ∀ (c : Lean.Name), sizeOf (Mathlib.Tactic.Push.Head.const c) = 1 + sizeOf c
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.whiskerRight_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f) (θ.app b)) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (θ.naturality f) g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft (F.map f) (Γ.app b)) g) h)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.linearEquivConj_mulLeftRight : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (x : A₁ × A₁),
  (↑f).conj (LinearMap.mulLeftRight R x) = LinearMap.mulLeftRight R (Prod.map (⇑f) (⇑f) x)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- When `sInf s < b`, there is an element `a` in `s` with `a < b`, if `s` is nonempty and the order
is a linear order.  -/
exists_lt_of_csInf_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α},
  s.Nonempty → sInf s < b → ∃ a ∈ s, a < b
-- Init.BinderPredicates
/-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...`  -/
Lean.«binderPred≥_» : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.eq_empty_of_insertMany_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ},
  m.insertMany l = ∅ → m = ∅
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.IntermediateFieldEquivClosedSubgroup.eq_1 : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K],
  InfiniteGalois.IntermediateFieldEquivClosedSubgroup =
    { toFun := fun L => { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
      invFun := fun H => IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Std.Time.Date.Unit.Month
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.monthSizesNonLeap.eq_1 : Std.Time.Month.Ordinal.monthSizesNonLeap✝ =
  ⟨#[31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31], Std.Time.Month.Ordinal.monthSizesNonLeap._proof_1✝⟩
-- Mathlib.Data.List.Chain
List.IsChain.rel_head? : ∀ {α : Type u_1} {R : α → α → Prop} {x : α} {l : List α}, List.IsChain R (x :: l) → ∀ ⦃y : α⦄, y ∈ l.head? → R x y
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.mem_span_gramSchmidt : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  {i j : ι}, i ≤ j → f i ∈ Submodule.span 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f '' Set.Iic j)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.one_mul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.natCast 1) a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J J' : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} (F_1 : J ⟶ J') (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.map F_1).snd.app X_1 = (F_1.app X_1).snd
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The underlying modification of strong transformations.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            CategoryTheory.Pseudofunctor.StrongTrans.Hom η θ → CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x)
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯)
      (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_comp_functorι : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (a : α),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft
        (CategoryTheory.Limits.colim.ι { as := a }))
      (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom
      (CategoryTheory.Limits.Sigma.functorι a)
-- Init.Data.Option.Attach
Option.toList_attach : ∀ {α : Type u_1} (o : Option α), o.attach.toList = List.map (fun x => ⟨↑x, ⋯⟩) o.toList.attach
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_congr_norm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖) → MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.FarFromTriangleFree.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ (ε ε_1 : 𝕜),
      ε = ε_1 →
        ∀ [inst_2 : Fintype α] {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj],
          G.FarFromTriangleFree ε = G_1.FarFromTriangleFree ε_1
-- Mathlib.MeasureTheory.Group.Measure
/-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`.  -/
MeasureTheory.Measure.inv : {G : Type u_1} → [inst : MeasurableSpace G] → [Inv G] → MeasureTheory.Measure G → MeasureTheory.Measure G
-- Mathlib.Data.Int.Order.Units
Int.units_inv_eq_self : ∀ (u : ℤˣ), u⁻¹ = u
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.ofBijective_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f) (a : A),
  (BialgEquiv.ofBijective f hf) a = f a
-- Mathlib.RingTheory.DedekindDomain.Instances
/-- This is not an instance because it creates a diamond with `OreLocalization.instAlgebra`.
 -/
Localization.AtPrime.liftAlgebra : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] →
          [IsDomain S] →
            [inst_4 : Algebra R S] →
              {P : Ideal R} →
                [inst_5 : P.IsPrime] →
                  [FaithfulSMul R S] →
                    Algebra (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)
-- Mathlib.Data.Set.Finite.Powerset
Finset.coeEmb.eq_1 : ∀ {α : Type u_1}, Finset.coeEmb = { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instMulZeroClass : {α : Type u_1} → [MulZeroClass α] → MulZeroClass αᵒᵈ
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt8HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Init.MetaTypes
Lean.Meta.ExtractLetsConfig.mk.sizeOf_spec : ∀ (proofs types implicits descend underBinder usedOnly merge useContext onlyGivenNames preserveBinderNames lift : Bool),
  sizeOf
      { proofs := proofs, types := types, implicits := implicits, descend := descend, underBinder := underBinder,
        usedOnly := usedOnly, merge := merge, useContext := useContext, onlyGivenNames := onlyGivenNames,
        preserveBinderNames := preserveBinderNames, lift := lift } =
    1 + sizeOf proofs + sizeOf types + sizeOf implicits + sizeOf descend + sizeOf underBinder + sizeOf usedOnly +
              sizeOf merge +
            sizeOf useContext +
          sizeOf onlyGivenNames +
        sizeOf preserveBinderNames +
      sizeOf lift
-- Mathlib.Algebra.BigOperators.Finprod
finprod_one : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M], ∏ᶠ (x : α), 1 = 1
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.foldl_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_comp : ∀ {b₁ b₂ b₃ : ℝ → ℝ} {bs₁ bs₂ bs₃ : Tactic.ComputeAsymptotics.Basis} (f₁ : ℝ → ℝ)
  (g₁ : Tactic.ComputeAsymptotics.MultiseriesExpansion bs₁ → Tactic.ComputeAsymptotics.MultiseriesExpansion bs₂)
  (f₂ : ℝ → ℝ)
  (g₂ : Tactic.ComputeAsymptotics.MultiseriesExpansion bs₂ → Tactic.ComputeAsymptotics.MultiseriesExpansion bs₃)
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries b₁ bs₁),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map (f₂ ∘ f₁) (g₂ ∘ g₁) ms =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f₂ g₂
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f₁ g₁ ms)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.natCeil_logb_natCast : ∀ (b n : ℕ), ⌈Real.logb ↑b ↑n⌉₊ = Nat.clog b n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.comp_equiv_comp : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {K : Type v} [inst_1 : Field K] (f : F →+* K)
  {P Q : Fin 3 → F}, W.Nonsingular P → W.Nonsingular Q → (⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {x : M'}
  {y : M}, MDiffAt g y → MDiffAt f x → f x = y → d% (g ∘ f) x = d% g (f x) ∘SL mfderiv% f x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.subcomplex_le_iff : ∀ {X : SSet} {A B : X.Subcomplex}, A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.isDefaultTunnelPort : UInt16 → Bool
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- Given a family of points `p : ι' → P` and an affine basis `b`, if the matrix whose rows are the
coordinates of `p` with respect `b` has a left inverse, then `p` spans the entire space.  -/
AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Finite ι] [inst_5 : Fintype ι']
  [inst_6 : DecidableEq ι] [Nontrivial k] (p : ι' → P) {A : Matrix ι ι' k},
  A * b.toMatrix p = 1 → affineSpan k (Set.range p) = ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.values.eq_1 : ∀ {α : Type u} {β : Type v} (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.values = Std.DTreeMap.Internal.Impl.foldr (fun x v l => v :: l) [] t