mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.plus_quotient_obj_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ),
  HomotopyCategory.plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔ CochainComplex.plus C K
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ W'.negY Q * P 2 ^ 3 → W'.dblZ P ≠ 0
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr_mul_sr : ∀ {n : ℕ} (i j : ZMod n), DihedralGroup.sr i * DihedralGroup.sr j = DihedralGroup.r (j - i)
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_id : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : InvolutiveStar R] [inst_2 : AddCommMonoid E]
  [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E] [inst_6 : TopologicalSpace E]
  [inst_7 : ContinuousStar E],
  star (WithConv.toConv (ContinuousLinearMap.id R E)) = WithConv.toConv (ContinuousLinearMap.id R E)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalNonAssocCommRing : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalNonAssocCommRing R] → [IsTopologicalRing R] → NonUnitalNonAssocCommRing (SeparationQuotient R)
-- Mathlib.Data.ZMod.Basic
ZMod.val_add_val_of_le : ∀ {n : ℕ} [NeZero n] {a b : ZMod n}, n ≤ a.val + b.val → a.val + b.val = (a + b).val + n
-- Std.Time.Format.Modifier
Std.Time.instReprZoneName.repr : Std.Time.ZoneName → ℕ → Std.Format
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_zsmul : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (n : ℤ) (φ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (n • φ) = n • TopModuleCat.Hom.hom φ
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.checkAux.checkForall : Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Unit Lean.MetaM Unit
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_rename_of_injective : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ},
  Function.Injective f → ((MvPolynomial.rename f) p).degrees = Multiset.map f p.degrees
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkFromSMatch.mkAlts : Lean.Elab.Deriving.Context →
  Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_prod : ∀ {α : Type u_4} {β : Type u_5}, IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.add : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr
-- Init.Grind.ToInt
/-- The embedding takes `0` to `0`.  -/
Lean.Grind.ToInt.Zero.toInt_zero : ∀ {α : Type u} {inst : Zero α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Zero α I], ↑0 = 0
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listDecode.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_2} (motive : List (α ⊕ (i : ℕ) × L.Functions i) → Sort u_4) (a : α)
  (l : List (α ⊕ (i : ℕ) × L.Functions i)) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inl a :: l))
  (h_3 : (n : ℕ) → (f : L.Functions n) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inr ⟨n, f⟩ :: l)),
  (match Sum.inl a :: l with
    | [] => h_1 ()
    | Sum.inl a :: l => h_2 a l
    | Sum.inr ⟨n, f⟩ :: l => h_3 n f l) =
    h_2 a l
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.pi.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremType.pi = 1
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.mk.inj : ∀ {kind : WantedRefKind✝} {binderType : Lean.TSyntax `term} {isClass : Bool} {deps : Array WantedDep✝}
  {transparent : Option (Lean.TSyntax `term)} {kind_1 : WantedRefKind✝} {binderType_1 : Lean.TSyntax `term}
  {isClass_1 : Bool} {deps_1 : Array WantedDep✝} {transparent_1 : Option (Lean.TSyntax `term)},
  { kind := kind, binderType := binderType, isClass := isClass, deps := deps, transparent := transparent } =
      { kind := kind_1, binderType := binderType_1, isClass := isClass_1, deps := deps_1,
        transparent := transparent_1 } →
    kind = kind_1 ∧ binderType = binderType_1 ∧ isClass = isClass_1 ∧ deps = deps_1 ∧ transparent = transparent_1
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instSMul : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] → (v : Valuation R Γ₀) → {S : Type u_3} → [SMul S R] → SMul S (WithVal v)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (f : α ↪o β) (g : β ↪o γ),
  ⇑(f.comp g) = ⇑g ∘ ⇑f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel κ.snd
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a `LocalizerMorphism` is a localized equivalence, then any compatible functor
between the localized categories is an equivalence.  -/
CategoryTheory.LocalizerMorphism.isEquivalence : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [h : Φ.IsLocalizedEquivalence] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G],
  G.IsEquivalence
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instAdditiveTopModuleCatInvariantsFunctor : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type v} [inst_2 : Group G],
  (TopRep.invariantsFunctor k G).Additive
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.MonicDegreeEq.map.eq_1 : ∀ {R : Type u} {S : Type v} {n : ℕ} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial.MonicDegreeEq R n)
  (f : R →+* S), p.map f = ⟨Polynomial.map f ↑p, ⋯⟩
-- Mathlib.Algebra.Lie.Normalizer
LieIdeal.idealizer_eq_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  LieSubmodule.idealizer I = LieSubmodule.normalizer I
-- Mathlib.CategoryTheory.Action.Limits
Action.instPreservesFiniteLimitsForgetOfHasFiniteLimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteLimits V], CategoryTheory.Limits.PreservesFiniteLimits (Action.forget V G)
-- Lean.DocString.Add
/-- The result of elaborating a Verso docstring, which consists of the docstring contents paired with a
set of deferred checks.
 -/
Lean.VersoDocResult : Type
-- Mathlib.CategoryTheory.Distributive.Cartesian
CategoryTheory.IsCartesianDistributive.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C],
  CategoryTheory.IsCartesianDistributive C = CategoryTheory.IsCartesianDistributive C
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_div_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g / h) μ μ
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instMin : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Min (LieSubmodule R L M)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKeyD_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.minKeyD fallback = k ↔
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux.eq_1 : ∀ (R : Type u₁) {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι),
  Algebra.Generators.H1Cotangent.δAux R Q =
    ((Finsupp.lsum R) fun f =>
        ↑R ((TensorProduct.mk S T Ω[S⁄R]) (f.prod fun x1 x2 => Q.val x1 ^ x2)) ∘ₗ ↑(KaehlerDifferential.D R S)) ∘ₗ
      ↑(AddMonoidAlgebra.coeffLinearEquiv R)
-- Init.Data.Array.Find
Array.finRev?_push : ∀ {α : Type} {p : α → Bool} {a : α} {xs : Array α},
  Array.findRev? p (xs.push a) = (Option.guard p a).or (Array.findRev? p xs)
-- Mathlib.Algebra.Lie.Subalgebra
/-- Given two nested Lie subalgebras `K ⊆ K'`, we can view `K` as a Lie subalgebra of `K'`,
regarded as Lie algebra in its own right.  -/
LieSubalgebra.ofLe : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → {K K' : LieSubalgebra R L} → K ≤ K' → LieSubalgebra R ↥K'
-- Mathlib.Data.Finset.Empty
Finset.eq_empty_iff_forall_notMem : ∀ {α : Type u_1} {s : Finset α}, s = ∅ ↔ ∀ (x : α), x ∉ s
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toAddHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N], Function.Injective AddMonoidHom.toAddHom
-- Lean.Elab.Term.TermElabM
/-- `true` when inside a `meta section`.  -/
Lean.Elab.Term.Context.isMetaSection : Lean.Elab.Term.Context → Bool
-- Init.Data.SInt.Bitwise
Int32.not_zero : ~~~0 = -1
-- Mathlib.Probability.CDF
ProbabilityTheory.cdf_measure_stieltjesFunction : ∀ (f : StieltjesFunction ℝ),
  Filter.Tendsto (↑f) Filter.atBot (nhds 0) →
    Filter.Tendsto (↑f) Filter.atTop (nhds 1) → ProbabilityTheory.cdf f.measure = f
-- Mathlib.Data.Finset.Insert
Finset.Nontrivial.instDecidablePred : {α : Type u_1} → DecidablePred Finset.Nontrivial
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.unitOfList l) k = if l.contains k = true then some () else none
-- Init.Data.Range.Polymorphic.PRange
Std.Rii.instDecidableMem : {α : Type u} → {r : Std.Rii α} → {a : α} → Decidable (a ∈ r)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : (t.modify k f).isEmpty = false},
  (t.modify k f).minKey he = if cmp (t.minKey ⋯) k = Ordering.eq then k else t.minKey ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).minKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Ring.BooleanRing
Bool.mul_eq_and : ∀ (b c : Bool), b * c = (b && c)
-- Mathlib.NumberTheory.HeckeRing.Defs
IsHeckeTriple.mk : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G},
  H₁.toSubmonoid ≤ Δ →
    H₂.toSubmonoid ≤ Δ →
      H₁.Commensurable H₂ → Δ ≤ (Subgroup.Commensurable.commensurator H₂).toSubmonoid → IsHeckeTriple Δ H₁ H₂
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.whiskerLeft_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) {β β' : b ⟶ c}
  (y : β ⟶ β'), (CategoryTheory.Bicategory.whiskerLeft α y).τl = CategoryTheory.Bicategory.whiskerLeft α.l y.τl
-- Mathlib.Data.Set.Card.Arithmetic
Set.Finite.ncard_biUnion_le : ∀ {α : Type u_1} {ι : Type u_2} {t : Set ι},
  t.Finite → ∀ (s : ι → Set α), (⋃ i ∈ t, s i).ncard ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
-- Lean.Elab.DeclNameGen
/-- If `e` is an application of a projection to a parent structure, returns the term being projected.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.getParentProjArg : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Parser.Extension
Lean.Parser.parserAlias2kindRef : IO.Ref (Lean.NameMap Lean.SyntaxNodeKind)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayMap_awayToSection : ∀ {σ : 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 (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))
      (AlgebraicGeometry.Proj.awayToSection 𝒜 x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f)
      ((AlgebraicGeometry.Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhdsWithin_eq_image' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    Filter.map (↑(extChartAt I x)) (nhdsWithin y s) =
      nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x) '' ((extChartAt I x).source ∩ s))
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiff.curry_left : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N},
  ContMDiff (I.prod I') J n (Function.uncurry f) → ∀ {y : M'}, ContMDiff I J n fun x => f x y
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mk.inj : ∀ {n : Type u_1} {R : Type u₂} {i j : n} {hij : i ≠ j} {c : R} {i_1 j_1 : n} {hij_1 : i_1 ≠ j_1} {c_1 : R},
  { i := i, j := j, hij := hij, c := c } = { i := i_1, j := j_1, hij := hij_1, c := c_1 } → i = i_1 ∧ j = j_1 ∧ c = c_1
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntUInt16UintOfNatNat : Lean.Grind.ToInt UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_add : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), ↑(-a) + ↑a = 0
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.snd` is `C^n`  -/
ContDiff.snd' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : F → G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => f x.2
-- Mathlib.Algebra.Group.Int.Units
Int.eq_of_mul_eq_one : ∀ {u v : ℤ}, u * v = 1 → u = v
-- Mathlib.Tactic.Linter.TacticDocumentation
/-- Does this tactic have a docstring, or an `extensionDoc` defined later?  -/
_private.Mathlib.Tactic.Linter.TacticDocumentation.0.isNonemptyDoc : Lean.Elab.Tactic.Doc.TacticDoc → Bool
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- **Alias** of `two_mul_le_add_sq`.

---

Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings.  -/
two_mul_le_add_pow_two : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R] (a b : R), 2 * a * b ≤ a ^ 2 + b ^ 2
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.instReprGenPatternInfo.repr : Lean.Meta.Grind.GenPatternInfo → ℕ → Std.Format
-- Init.Data.Array.Lemmas
Array.getElem?_singleton : ∀ {α : Type u_1} {a : α} {i : ℕ}, #[a][i]? = if i = 0 then some a else none
-- Lean.ToExpr
Lean.instToExprUInt64 : Lean.ToExpr UInt64
-- Mathlib.Computability.TuringMachine.Computable
/-- The type of statements (functions) corresponding to this TM.  -/
Turing.FinTM2.Stmt : Turing.FinTM2 → Type
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.fixedParamPerms : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Elab.FixedParamPerms
-- Mathlib.Algebra.Group.Defs
add_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), (m + n) • a = m • a + n • a
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.pow_apply : ∀ {M : Type u_1} [inst : Monoid M] (n : M) (m : ℕ), Submonoid.pow n m = ⟨n ^ m, ⋯⟩
-- Init.Core
Sum.inr.inj : ∀ {α : Type u} {β : Type v} {val val_1 : β}, Sum.inr val = Sum.inr val_1 → val = val_1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_cast_right : ∀ {α : Sort u_1} {n m : ℕ} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ) (h : m' = m),
  Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ Fin.cast ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ Std.DHashMap.Const.insertMany m l},
  Std.DHashMap.Const.get (Std.DHashMap.Const.insertMany m l) k h = Std.DHashMap.Const.get m k ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.measurableSet_limsup : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (s n)) → MeasurableSet (Filter.limsup s Filter.atTop)
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.surjective_compr₂_of_equiv : ∀ {R : Type u_2} [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} {Qₗ : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : AddCommMonoid Qₗ]
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
  (g : Pₗ ≃ₗ[R] Qₗ), Function.Surjective ⇑f → Function.Surjective ⇑(f.compr₂ ↑g)
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.mk : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i},
  (∀ ⦃i : ι⦄ (x : F i), f ⋯ x = x) →
    (∀ ⦃k j i : ι⦄ (hkj : k ≤ j) (hji : j ≤ i) (x : F i), f hkj (f hji x) = f ⋯ x) → InverseSystem f
-- Mathlib.Data.Nat.Choose.Multinomial
List.multinomial_cons : ∀ (x : ℕ) (l : List ℕ), (x :: l).multinomial = (x + l.sum).choose x * l.multinomial
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.nodup_of_pairwise_disjoint : ∀ {α : Type u_1} {l : List (Equiv.Perm α)}, 1 ∉ l → List.Pairwise Equiv.Perm.Disjoint l → l.Nodup
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.wrap : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_one : ∀ (n : ℕ), SimplexCategory.σ₀Iter 1 ⋯ = SimplexCategory.σ 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.ChoiceInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo), sizeOf { toElabInfo := toElabInfo } = 1 + sizeOf toElabInfo
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contDiffWithinAtProp_id : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  (x : H), ContDiffWithinAtProp I I n id Set.univ x
-- Init.Data.Vector.Lemmas
Vector.push_eq_push : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs ys : Vector α n}, xs.push a = ys.push b ↔ a = b ∧ xs = ys
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.nontrivial_iff : ∀ {G : Type u_1} [inst : Group G], Nontrivial (Subgroup G) ↔ Nontrivial G
-- Mathlib.Data.Sym.Basic
Sym.attach_map_coe : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n), Sym.map Subtype.val s.attach = s
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_inf_hom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
/-- The (distinguished) triangle in the derived category of `C` given by a
short exact short complex in `C`.  -/
CategoryTheory.ShortComplex.ShortExact.singleTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex C} → S.ShortExact → CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_mem_eq_self_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ x ∈ l, l.formPerm x = x ↔ l.length ≤ 1
-- Mathlib.RingTheory.PicardGroup
Submodule.unitsQuotEquivRelPic_symm_apply : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] (a : ↥(CommRing.relPic R A)),
  (Submodule.unitsQuotEquivRelPic R A).symm a =
    (QuotientGroup.congr (Submodule.unitsToPic R A).ker (Units.map ↑(Submodule.spanSingleton R)).range
        (MulEquiv.refl (Submodule R A)ˣ) ⋯)
      ((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R A)).symm ((MulEquiv.subgroupCongr ⋯).symm a))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDistribMulAction' : {α : Type u_1} →
  {l : Filter α} →
    {M : Type u_5} →
      {N : Type u_6} →
        [inst : Monoid M] → [inst_1 : AddMonoid N] → [DistribMulAction M N] → DistribMulAction (l.Germ M) (l.Germ N)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (c : BitVec w) (curr : ℕ)
  (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr) (hfoo : aig.decls.size ≤ aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig c curr s hcurr).get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasFiniteLimitsInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Ind C)