mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
      (CategoryTheory.Bicategory.associator f g h').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
-- Init.Data.Order.Classes
Std.IsPartialOrder.mk : ∀ {α : Type u} [inst : LE α] [toIsPreorder : Std.IsPreorder α],
  (∀ (a b : α), a ≤ b → b ≤ a → a = b) → Std.IsPartialOrder α
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.continuousSMul : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] (S : Subalgebra R A) (X : Type u_2) [inst_4 : TopologicalSpace X]
  [inst_5 : MulAction A X] [ContinuousSMul A X], ContinuousSMul (↥S) X
-- Mathlib.Combinatorics.Digraph.Orientation
/-- Orientation-forgetting map from `Digraph` to `SimpleGraph` that gives an unoriented edge if
both orientations are present.
 -/
Digraph.toSimpleGraphStrict : {V : Type u_1} → Digraph V → SimpleGraph V
-- Mathlib.Topology.Algebra.Affine
/-- If `f` is an affine map, then its linear part is continuous iff `f` is continuous.  -/
AffineMap.continuous_linear_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [inst : AddCommGroup V]
  [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P]
  [inst_5 : AddCommGroup W] [inst_6 : TopologicalSpace W] [inst_7 : AddTorsor W Q] [inst_8 : TopologicalSpace Q]
  [IsTopologicalAddTorsor Q] [inst_10 : Ring R] [inst_11 : Module R V] [inst_12 : Module R W] {f : P →ᵃ[R] Q},
  Continuous ⇑f.linear ↔ Continuous ⇑f
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ofHom_comp : ∀ {X Y Z : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : Fintype X] [inst_3 : DistribLattice Y]
  [inst_4 : BoundedOrder Y] [inst_5 : Fintype Y] [inst_6 : DistribLattice Z] [inst_7 : BoundedOrder Z]
  [inst_8 : Fintype Z] (f : BoundedLatticeHom X Y) (g : BoundedLatticeHom Y Z),
  FinBddDistLat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (FinBddDistLat.ofHom f) (FinBddDistLat.ofHom g)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.contCat : Lean.PrettyPrinter.Parenthesizer.State → Lean.Name
-- Init.Data.Nat.Div.Basic
Nat.div_add_mod : ∀ (m n : ℕ), n * (m / n) + m % n = m
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → a ∉ t
-- Std.Do.WP.Basic
Std.Do.PredTrans.mk.congr_simp : ∀ {ps : Std.Do.PostShape} {α : Type u} (trans trans_1 : Std.Do.PostCond α ps → Std.Do.Assertion ps)
  (e_trans : trans = trans_1) (conjunctiveRaw : Std.Do.PredTrans.Conjunctive trans),
  { trans := trans, conjunctiveRaw := conjunctiveRaw } = { trans := trans_1, conjunctiveRaw := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.coe_mrangeRestrict : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} [inst_1 : AddZeroClass N] (f : M →+ N) (x : M),
  ↑(f.mrangeRestrict x) = f x
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- The supremum of the empty set is special-cased to `⊥`  -/
ConditionallyCompleteLinearOrderBot.csSup_empty : ∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderBot α], sSup ∅ = ⊥
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex.g = CategoryTheory.Limits.biprod.desc inl inr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.isUnit_iff_inverse_mul_cancel : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), IsUnit x ↔ Ring.inverse x * x = 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.freeMonoidCongr_symm_of : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β) (b : β),
  (FreeMonoid.freeMonoidCongr e.symm) (FreeMonoid.of b) = FreeMonoid.of (e.symm b)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_5 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ)
  (f : L.BoundedFormula α (x + 1)),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f.all =
    (h x (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f)).all
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.sSup_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] (s : Set (Colex ((i : ι) → α i))) (i : ι), sSup s i = ⨆ e, ↑e i
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
ContinuousWithinAt.compMeasurePreservingLp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {Z : Type u_4} [inst_12 : TopologicalSpace Z]
  {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {s : Set Z} {z : Z},
  ContinuousWithinAt f s z →
    ContinuousWithinAt g s z →
      ∀ (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν),
        p ≠ ⊤ → ContinuousWithinAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s z
-- Mathlib.RingTheory.OreLocalization.OreSet
OreLocalization.nonempty_oreSet_iff : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R},
  Nonempty (OreLocalization.OreSet S) ↔
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
-- Std.Tactic.Do.Syntax
/-- Experimental Sym-based drop-in for `mvcgen`; see `mvcgen` for documentation.  -/
Lean.Parser.Tactic.vcgen : Lean.ParserDescr
-- Lean.Environment
Lean.readModuleData : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α}, t.isEmpty = true → t.get? a = none
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.intRfl : Lean.Expr
-- Mathlib.Algebra.Group.Prod
MonoidHom.inr.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.inr M N = { toFun := fun y => (1, y), map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstArgInfo.mk.inj : ∀ {isProof isInstance isProof_1 isInstance_1 : Bool},
  { isProof := isProof, isInstance := isInstance } = { isProof := isProof_1, isInstance := isInstance_1 } →
    isProof = isProof_1 ∧ isInstance = isInstance_1
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_5 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (v : Lean.Grind.Linarith.Var),
  Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.var v) = Lean.Grind.Linarith.Var.denote ctx v
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.args : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Array Lean.Expr
-- Mathlib.GroupTheory.Nilpotent
/-- The proof that `upperCentralSeriesStep N` is the preimage of the centre of `G/N` under
the canonical surjection.  -/
Subgroup.upperCentralSeriesStep_eq_comap_center : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = Subgroup.comap (QuotientGroup.mk' N) (Subgroup.center (G ⧸ N))
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_conj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α}, (τ * σ * τ⁻¹).cycleType = σ.cycleType
-- Mathlib.Algebra.Star.StarAlgHom
Pi.evalStarAlgHom_apply : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : (i : ι) → Star (A i)] (a : (i : ι) → A i),
  (Pi.evalStarAlgHom R A j) a = (Pi.evalNonUnitalStarAlgHom R A j).toFun a
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.moduleCatLeftHomologyData.H = ModuleCat.of R (↥(ModuleCat.Hom.hom S.g).ker ⧸ S.moduleCatToCycles.range)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.nat_card : ∀ {n : ℕ}, Nat.card (DihedralGroup n) = 2 * n
-- Lean.DocString.Types
Lean.Doc.instHashableMathMode.hash : Lean.Doc.MathMode → UInt64
-- Mathlib.Data.PNat.Order
PNat.instSuccOrder : SuccOrder ℕ+
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformlyOn.div₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → TendstoLocallyUniformlyOn (F / G) (f / g) l s
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a left extension is a Kan extension across an isomorphism
of extensions.  -/
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} → {s t : CategoryTheory.Bicategory.LeftExtension f g} → s.IsAbsKan → (s ≅ t) → t.IsAbsKan
-- Mathlib.Algebra.Group.Commute.Basic
Commute.zpow_self : ∀ {G : Type u_1} [inst : Group G] (a : G) (n : ℤ), Commute (a ^ n) a
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_biUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_copy : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w')
  (h : u ∈ (p.copy hv hw).support), (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.semigroup : {α : Type u} → [AddSemigroup α] → Semigroup (Multiplicative α)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  (S : NonUnitalStarSubalgebra R B) (f : F) (x : A), x ∈ NonUnitalStarSubalgebra.comap f S ↔ f x ∈ S
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.Limits.pullback.fst f I.subschemeι) =
    (I.comap f).subschemeι
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) →
      ∀ {g : α → ℝ},
        MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun x => g x * (f x).toReal) μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₆_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.c₆ = W.a₁ ^ 6
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instCoePadic : {p : ℕ} → [hp : Fact (Nat.Prime p)] → Coe ℤ_[p] ℚ_[p]
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator_projectiveSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.IsSeparator
    (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator✝ C)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_3.splitter : (motive : Std.Tactic.BVDecide.Gate → Sort u_1) →
  (g : Std.Tactic.BVDecide.Gate) →
    (Unit → motive Std.Tactic.BVDecide.Gate.and) →
      (Unit → motive Std.Tactic.BVDecide.Gate.xor) →
        (Unit → motive Std.Tactic.BVDecide.Gate.beq) → (Unit → motive Std.Tactic.BVDecide.Gate.or) → motive g
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_sub_preimage_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s t : Set β}, ⇑m ⁻¹' s - ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s - t)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_sub : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] {a b : G →₀ k}, { coeff := a - b } = { coeff := a } - { coeff := b }
-- Mathlib.Algebra.Star.Prod
Prod.instStarMul : {R : Type u} → {S : Type v} → [inst : Mul R] → [inst_1 : Mul S] → [StarMul R] → [StarMul S] → StarMul (R × S)
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.instInhabitedOffset.default : Lean.Meta.Sym.Offset
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.mulCharEquiv_symm_apply_apply : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (m : Mˣ) (χ : MulChar M R),
  ((MulChar.mulCharEquiv M R).symm m) χ = χ ↑m
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `M` and `N` are submodules in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] N →ₗ[R] S` induced by multiplication in `S`.  -/
Submodule.mulMap : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (M N : Submodule R S) → TensorProduct R ↥M ↥N →ₗ[R] S
-- Mathlib.Data.Stream.Init
Stream'.append_take_drop : ∀ {α : Type u} (n : ℕ) (s : Stream' α), Stream'.take n s ++ₛ Stream'.drop n s = s
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_ringInverse : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  CFC.sqrt (Ring.inverse a) = Ring.inverse (CFC.sqrt a)
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv_apply : ∀ {X Y : Type u} (f g : X ⟶ Y) (x : Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.coequalizerIso f g).inv)
      (Function.Coequalizer.mk (⇑(CategoryTheory.ConcreteCategory.hom f)) (⇑(CategoryTheory.ConcreteCategory.hom g))
        x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coequalizer.π f g)) x
-- Lean.Elab.Tactic.Try
/-- `simp` tactic syntax generator  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkSimpStx : Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
CategoryTheory.Iso.toIsometryEquiv_refl : ∀ {R : Type u} [inst : CommRing R] {X : QuadraticModuleCat R},
  (CategoryTheory.Iso.refl X).toIsometryEquiv = QuadraticMap.IsometryEquiv.refl X.form
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.point_mem_closedInterior_faceOpposite_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [Nontrivial k] [ZeroLEOneClass k] {n : ℕ} [inst_7 : NeZero n]
  (s : Affine.Simplex k P n) {i j : Fin (n + 1)}, s.points j ∈ (s.faceOpposite i).closedInterior ↔ j ≠ i
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.pointwise_smul_le_pointwise_smul_iff : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S T : Submonoid M}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.Logic.Equiv.Set
/-- An empty set is equivalent to the `Empty` type.  -/
Equiv.Set.empty : (α : Type u_3) → ↑∅ ≃ Empty
-- Mathlib.Order.KrullDimension
Order.coheight_coe_withTop : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.coheight ↑x = Order.coheight x + 1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt_symmₗ : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Pretrivialization.linearMapAt R e b) ((Bundle.Pretrivialization.symmₗ R e b) y) = y
-- Mathlib.Algebra.Group.Defs
/-- If all multiplications cancel then every element is regular.  -/
IsRegular.all : ∀ {R : Type u_2} [inst : Mul R] [IsCancelMul R] (g : R), IsRegular g
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.ofList = Equiv.refl (List α)
-- Mathlib.Control.Functor.Multivariate
MvFunctor.LiftR_RelLast_iff : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u_1} [inst : MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : Type u}
  (rr : β → β → Prop) (x y : F (α ::: β)), MvFunctor.LiftR' (α.RelLast' rr) x y ↔ MvFunctor.LiftR (α.RelLast rr) x y
-- Mathlib.GroupTheory.HNNExtension
/-- A recursor to induct on a `NormalWord`, by proving the property is preserved under `cons`  -/
HNNExtension.NormalWord.consRecOn : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        {motive : HNNExtension.NormalWord d → Sort u_4} →
          (w : HNNExtension.NormalWord d) →
            ((g : G) → motive (HNNExtension.NormalWord.ofGroup g)) →
              ((g : G) →
                  (u : ℤˣ) →
                    (w : HNNExtension.NormalWord d) →
                      (h1 : w.head ∈ d.set u) →
                        (h2 :
                            ∀ u' ∈ Option.map Prod.fst w.toList.head?,
                              w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
                          motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)) →
                motive w
-- Mathlib.Data.Nat.Cast.Defs
AddMonoidWithOne.toAddMonoid : {R : Type u_2} → [self : AddMonoidWithOne R] → AddMonoid R
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 1),
  CategoryTheory.ComposableArrows.mk₁ X.hom = X
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- The path 0 ⟶ 1 in `ULift I`  -/
unitInterval.upath01 : Path { down := 0 } { down := 1 }
-- Mathlib.Algebra.Group.Units.Equiv
/-- Left multiplication in a `Group` is a permutation of the underlying type.  -/
Equiv.mulLeft : {G : Type u_5} → [Group G] → G → Equiv.Perm G
-- Mathlib.Data.Int.Order.Units
/-- **Alias** of `Int.units_sq`. -/
Int.units_pow_two : ∀ (u : ℤˣ), u ^ 2 = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.singleton_eq_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {p : α × β},
  {p} = ∅.insert p.1 p.2
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.eq_1 : ∀ {E : Type u_1} [inst : MeasurableSpace E] {Ω : Type u_2} {x : MeasurableSpace Ω} (X : Ω → E) (s : Set E)
  (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E),
  MeasureTheory.pdf.IsUniform X s ℙ μ = (MeasureTheory.Measure.map X ℙ = μ[|s])
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_sub : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f g : AdicCompletion I M), ↑(f - g) = ↑f - ↑g
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight_tmul_single : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (i : ι) (m : M) (n : N),
  (TensorProduct.finsuppRight R S M N ι) (m ⊗ₜ[R] fun₀ | i => n) = fun₀ | i => m ⊗ₜ[R] n
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_iff_le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instReprOrigin : Repr Lean.Meta.Origin
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀.  -/
dense_sInter_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {S : Set (Set X)},
  (∀ s ∈ S, IsOpen s) → S.Countable → (∀ s ∈ S, Dense s) → Dense (⋂₀ S)
-- Init.Data.Nat.Fold
/-- `Nat.dfold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
* `Nat.dfold f 3 init = init |> f 0 |> f 1 |> f 2`
The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α i → α (i + 1)`.
 -/
Nat.dfold : (n : ℕ) →
  {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} →
    ((i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) → α 0 ⋯ → α n ⋯
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.tensoringLeft_linear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C] (X : C),
  CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).functor.obj X).left = X.left
-- Mathlib.Data.Set.Card
Set.finite_of_encard_eq_coe : ∀ {α : Type u_1} {s : Set α} {k : ℕ}, s.encard = ↑k → s.Finite