mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Tactics
/-- The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the
functional induction principle.

The tactic invocation
```
fun_induction f x₁ ... xₙ y₁ ... yₘ
```
where `f` is a function defined by non-mutual structural or well-founded recursion, is equivalent to
```
induction y₁, ... yₘ using f.induct_unfolding x₁ ... xₙ
```
where the arguments of `f` are used as arguments to `f.induct_unfolding` or targets of the
induction, as appropriate.

The form
```
fun_induction f
```
(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
these arguments. An application of `f` is eligible if it is saturated and the arguments that will
become targets are free variables.

The forms `fun_induction f x y generalizing z₁ ... zₙ` and
`fun_induction f x y with | case1 => tac₁ | case2 x' ih => tac₂` work like with `induction.`

Under `set_option tactic.fun_induction.unfolding true` (the default), `fun_induction` uses the
`f.induct_unfolding` induction principle, which will try to automatically unfold the call to `f` in
the goal. With `set_option tactic.fun_induction.unfolding false`, it uses `f.induct` instead.
 -/
Lean.Parser.Tactic.funInduction : Lean.ParserDescr
-- Mathlib.NumberTheory.Real.Irrational
Irrational.intCast_sub : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), Irrational (↑m - x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_real : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ), NumberField.mixedEmbedding.logMap (c • 1) = 0
-- Mathlib.Algebra.Order.Kleene
add_eq_right_iff_le : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, a + b = b ↔ a ≤ b
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.value : Lean.Meta.Closure.MkValueTypeClosureResult → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_surjective : Function.Surjective Complex.cos
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Ico : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Ico i j = Set.Ico (Fin.castLE h i) (Fin.castLE h j)
-- Lean.Util.CollectLevelMVars
/-- Collects all universe level metavariables present in `e`.
Result is in `Lean.CollectLevelMVars.State.result`.
 -/
Lean.collectLevelMVars : Lean.CollectLevelMVars.State → Lean.Expr → Lean.CollectLevelMVars.State
-- Mathlib.Analysis.Normed.Module.Basic
NormedAlgebra.toAlgebra : {𝕜 : Type u_6} →
  {𝕜' : Type u_7} → {inst : NormedField 𝕜} → {inst_1 : SeminormedRing 𝕜'} → [self : NormedAlgebra 𝕜 𝕜'] → Algebra 𝕜 𝕜'
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_pow_add_C_ne_zero : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] {n : ℕ}, 0 < n → ∀ (a : R), Polynomial.X ^ n + Polynomial.C a ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_map_subtype : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate.congr_simp : ∀ {n : Type v} {α : Type w} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : CommRing α]
  (A A_1 : Matrix n n α),
  A = A_1 → ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → A.adjugate a a_2 = A_1.adjugate a_1 a_3
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.closure_preimage_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (s : Set N),
  AddSubgroup.closure (⇑f ⁻¹' s) ≤ AddSubgroup.comap f (AddSubgroup.closure s)
-- Init.Data.Fin.Fold
/-- Inner loop for `Fin.foldlM`.
```
Fin.foldlM.loop n f xᵢ i = do
  let xᵢ₊₁ ← f xᵢ i
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ
```
 -/
_private.Init.Data.Fin.Fold.0.Fin.foldlM.loop : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → (n : ℕ) → (α → Fin n → m α) → α → ℕ → m α
-- Mathlib.Computability.Encoding
Computability.Γ'.bit.injEq : ∀ (b b_1 : Bool), (Computability.Γ'.bit b = Computability.Γ'.bit b_1) = (b = b_1)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_continuous_toLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous (WithLp.toLp p)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.id_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.Hom.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.csInf_image_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : Preorder α] {f : α → β},
  Monotone f → ∀ {s : Set α} {c : α}, c ∈ s → BddBelow s → sInf (f '' s) ≤ f c
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_roi_eq_toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo + 1)...Std.Slice.size xs)
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValueD_filter_containsKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getValueD k l₁ fallback else fallback
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.denote_toPoly_go : ∀ {k : ℕ} {p : Nat.Internal.Linear.Poly} (ctx : Nat.Internal.Linear.Context) (e : Nat.Internal.Linear.Expr),
  Nat.Internal.Linear.Poly.denote ctx (Nat.Internal.Linear.Expr.toPoly.go k e p) =
    k * Nat.Internal.Linear.Expr.denote ctx e + Nat.Internal.Linear.Poly.denote ctx p
-- Init.SimpLemmas
Bool.or_eq_true : ∀ (a b : Bool), ((a || b) = true) = (a = true ∨ b = true)
-- Mathlib.Topology.Gluing
TopCat.GlueData.ofOpenSubsets_toGlueData_t : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α)
  (i j :
    { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i),
        V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
        t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
        t_inter := ⋯, cocycle := ⋯ }.J),
  (TopCat.GlueData.ofOpenSubsets U).t i j = TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  (φ' : S' ⟶ R) (X : Dᵒᵖ),
  (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').obj X =
    CommRingCat.KaehlerDifferential (φ'.app X)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_inj : ∀ {R : Type u_1} [inst : Semiring R] {a b : R}, SkewPolynomial.C a = SkewPolynomial.C b ↔ a = b
-- Mathlib.Order.CompleteLattice.Basic
Prod.fst_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst_1 : SupSet β] (s : Set (α × β)),
  (sSup s).1 = sSup (Prod.fst '' s)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRingRingEquiv.eq_1 : ∀ (K : Type u) [inst : CommRing K],
  RatFunc.toFractionRingRingEquiv K =
    { toFun := RatFunc.toFractionRing, invFun := RatFunc.ofFractionRing, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
      map_add' := ⋯ }
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.top_mem : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ⊤ ∈ ρ.invtSubmodule
-- Mathlib.Logic.Encodable.Basic
Encodable.decodeSubtype.eq_1 : ∀ {α : Type u_1} {P : α → Prop} [encA : Encodable α] [decP : DecidablePred P] (v : ℕ),
  Encodable.decodeSubtype v = (Encodable.decode v).bind fun a => if h : P a then some ⟨a, h⟩ else none
-- Init.Data.List.Nat.TakeDrop
List.take_eq_append_getElem_of_pos : ∀ {α : Type u_1} {i : ℕ} {l : List α} (h₁ : 0 < i) (h₂ : i < l.length),
  List.take i l = List.take (i - 1) l ++ [l[i - 1]]
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The identity morphism on a monoid object.  -/
CategoryTheory.Mon.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.Mon C) → M.Hom M
-- Mathlib.Data.Finsupp.Order
Finsupp.instPosSMulReflectLE : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : Zero β]
  [inst_3 : Preorder β] [inst_4 : SMulZeroClass α β] [PosSMulReflectLE α β], PosSMulReflectLE α (ι →₀ β)
-- Init.Data.Order.MinMaxOn
max_apply_eq_max : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [DecidableLE α] [inst_2 : Max α] [Std.LawfulOrderLeftLeaningMax α]
  [inst_4 : Max β] [inst_5 : LE β] [DecidableLE β] [Std.LawfulOrderLeftLeaningMax β] (f : α → β) {a b : α},
  (f b ≤ f a ↔ b ≤ a) → f a ⊔ f b = f (a ⊔ b)
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `GaloisCoinsertion.u_biSup_of_l_u_eq_self`. -/
GaloisCoinsertion.u_biSup_of_lu_eq_self : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α),
  (∀ (i : ι) (hi : p i), l (u (f i hi)) = f i hi) → u (⨆ i, ⨆ (hi : p i), f i hi) = ⨆ i, ⨆ (hi : p i), u (f i hi)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addCommSemigroup : {α : Type u} → [CommSemigroup α] → AddCommSemigroup (Additive α)
-- Mathlib.Order.Circular
OrderDual.sbtw : (α : Type u_1) → [h : SBtw α] → SBtw αᵒᵈ
-- Mathlib.Topology.DiscreteSubset
codiscrete_eq_cofinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [CompactSpace X], Filter.codiscrete X = Filter.cofinite
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.adjSylvester_comp_sylveserMap : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n),
  f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id
-- Mathlib.Logic.Equiv.Defs
Equiv.instTrans : Trans Equiv Equiv Equiv
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Equivalence relation identifying two nonempty compact sets which are isometric  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorff.0.GromovHausdorff.IsometryRel : TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) → TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) → Prop
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.strictUniversalPropertyFixedTargetId_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3)
  [inst_1 : CategoryTheory.Category.{v_3, u_3} E] (hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C)
  (F : CategoryTheory.Functor C E) (x : W.IsInvertedBy F),
  (CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW).lift F x = F
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrable_add_of_disjoint : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f g : α → E},
  Disjoint (Function.support f) (Function.support g) →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.StronglyMeasurable g →
        (MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.dual_map : ∀ {X Y : FinPartOrd} (f : X ⟶ Y), FinPartOrd.dual.map f = FinPartOrd.ofHom (OrderHom.dual (PartOrd.Hom.hom f.hom))
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.splitter : {n : ℕ} →
  (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) →
    (x x_1 : Fin (n + 1 + 1)) →
      (x_2 : x ≤ x_1) →
        ((isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x) →
          ((isLt : 0 < n + 1 + 1) →
              (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x) →
            ((isLt : 0 < n + 1 + 1) →
                (j : ℕ) →
                  (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x) →
              ((i : ℕ) →
                  (hi : i + 1 < n + 1 + 1) →
                    (j : ℕ) →
                      (hj : j + 1 < n + 1 + 1) →
                        (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij) →
                motive x x_1 x_2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k : α}, (t.erase k)[k]! = default
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)} (it : Std.IterM Id β),
  (Std.IterM.filterMapWithPostcondition f it).toListRev =
    List.reverse <$> List.filterMapM (fun x => (f x).run) it.toList.run
-- Mathlib.Data.Fin.Tuple.Basic
Fin.exists_iff_castSucc : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∃ i, P i) ↔ P (Fin.last n) ∨ ∃ i, P i.castSucc
-- Mathlib.Topology.Covering.Quotient
isAddQuotientCoveringMap_quotientMk_of_properlyDiscontinuousVAdd : ∀ {E : Type u_1} [inst : TopologicalSpace E] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G E]
  [ContinuousConstVAdd G E] [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] [IsCancelVAdd G E],
  IsAddQuotientCoveringMap (Quotient.mk (AddAction.orbitRel G E)) G
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological monoids, as a
`MonoidHom`. Similar to `MonoidHom.compLeftContinuous`.  -/
MonoidHom.compLeftContinuousBounded : {β : Type v} →
  {γ : Type w} →
    (α : Type u_3) →
      [inst : TopologicalSpace α] →
        [inst_1 : PseudoMetricSpace β] →
          [inst_2 : Monoid β] →
            [inst_3 : BoundedMul β] →
              [inst_4 : ContinuousMul β] →
                [inst_5 : PseudoMetricSpace γ] →
                  [inst_6 : Monoid γ] →
                    [inst_7 : BoundedMul γ] →
                      [inst_8 : ContinuousMul γ] →
                        (g : β →* γ) →
                          {C : NNReal} →
                            LipschitzWith C ⇑g → BoundedContinuousFunction α β →* BoundedContinuousFunction α γ
-- Mathlib.Algebra.Order.CauSeq.Basic
rat_mul_continuous_lemma : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Ring β]
  (abv : β → α) [IsAbsoluteValue abv] {ε K₁ K₂ : α},
  0 < ε →
    ∃ δ > 0,
      ∀ {a₁ a₂ b₁ b₂ : β},
        abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type Aₙ₋₁ (rank n-1, corresponding to sl(n)).  -/
CartanMatrix.A : (n : ℕ) → Matrix (Fin n) (Fin n) ℤ
-- Mathlib.Data.TypeVec
TypeVec.prod.fst.eq_2 : ∀ (n : ℕ) (x_4 x_5 : TypeVec.{u} n.succ), TypeVec.prod.fst Fin2.fz = Prod.fst
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.brecOn.go : {motive : (a : ℕ) → Std.Tactic.BVDecide.BVExpr a → Sort u} →
  {a : ℕ} →
    (t : Std.Tactic.BVDecide.BVExpr a) →
      ((a : ℕ) → (t : Std.Tactic.BVDecide.BVExpr a) → Std.Tactic.BVDecide.BVExpr.below t → motive a t) →
        motive a t ×' Std.Tactic.BVDecide.BVExpr.below t
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.iInter : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)},
  (∃ n, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) → ProbabilityTheory.CondIndepSets m' hm' (⋂ n, s n) s' μ
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.mk.sizeOf_spec : ∀ (task : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))) (cancel : IO Unit),
  sizeOf { task := task, cancel := cancel } = 1 + sizeOf task
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleObjXSelf.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V), HomologicalComplex.singleObjXSelf c j A = HomologicalComplex.singleObjXIsoOfEq c j A j ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Special case of `Topology.IsClosedEmbedding.map_tprod`, logically weaker but possibly easier
to apply in practice.  -/
Function.LeftInverse.map_tprod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {G : Type u_4} (f : β → α) [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] [T2Space γ]
  {g : G} [inst_5 : FunLike G α γ] [MonoidHomClass G α γ],
  Continuous ⇑g →
    ∀ {g' : γ → α}, Continuous g' → Function.LeftInverse g' ⇑g → g (∏'[L] (b : β), f b) = ∏'[L] (b : β), g (f b)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsIsoOfEquiv_inv_apply : ∀ {R S : Type v} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S) (x : R),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsIsoOfEquiv e).inv) x = e x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An equality `a = b` coming from the core.
`p₁` and `p₂` are the polynomials corresponding to `a` and `b`.
 -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core : Lean.Expr → Lean.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {v : β k}, t.WF → (⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Monotone.const_nsmul : ∀ {β : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : Preorder β] [AddLeftMono M]
  [AddRightMono M] {f : β → M}, Monotone f → ∀ (n : ℕ), Monotone fun a => n • f a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.average_density_near_total_density : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts} {A B : Finset (Finset α)},
          A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts →
            B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts →
              |(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) -
                    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))| ≤
                ε ^ 5 / 49
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Auxiliary definition of `isLimitMultifork`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {S : C} →
            {E : J.OneHypercover S} →
              {F : CategoryTheory.Sheaf J A} →
                (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) → c.pt ⟶ F.obj.obj (Opposite.op S)
-- Mathlib.Data.NNRat.Defs
NNRat.toNNRat_mono : Monotone Rat.toNNRat
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instDistribMulAction : {M : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace A] →
      [inst_1 : Monoid M] →
        [inst_2 : AddMonoid A] →
          [inst_3 : DistribMulAction M A] →
            [inst_4 : ContinuousAdd A] → [ContinuousConstSMul M A] → DistribMulAction M (SeparationQuotient A)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Ici : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R},
  Nat.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊
-- Init.PropLemmas
/-- `∧` distributes over `∨` (on the left).  -/
and_or_left : ∀ {a b c : Prop}, a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.nonempty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F s : Set X} {n : ℕ},
  F.Nonempty → Dynamics.IsDynCoverOf T F U n s → s.Nonempty
-- Mathlib.Tactic.MinImports
/-- `getId stx` takes as input a `Syntax` `stx`.
If `stx` contains a `declId`, then it returns the `ident`-syntax for the `declId`.
If `stx` is a nameless instance, then it also tries to fetch the `ident` for the instance.
Otherwise it returns `.missing`.  -/
Mathlib.Command.MinImports.getId : Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Syntax
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.netMaxcard T F U n = ⨆ s, ⨆ (_ : Dynamics.IsDynNetIn T F U n ↑s), ↑s.card
-- Mathlib.Util.Export
Lean.Export.alloc : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Lean.Export.OfState α] → α → Lean.ExportM ℕ
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- The radius of a simple graph is the minimum eccentricity of any vertex.  -/
SimpleGraph.radius : {α : Type u_1} → SimpleGraph α → ℕ∞
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.of_hasInitial : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C],
  CategoryTheory.IsCofiltered C
-- Mathlib.GroupTheory.Torsion
/-- A nontrivial torsion-free abelian group is not torsion.  -/
not_isMulTorsion_of_isMulTorsionFree : ∀ {G : Type u_1} [inst : CommGroup G] [Nontrivial G] [IsMulTorsionFree G], ¬IsMulTorsion G
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addEntries : Array Lean.Meta.SimpEntry → Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G],
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftPropAt Q (↑(chartAt H x).symm) (↑(chartAt H x) x)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go.match_1.splitter : (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) →
  (lhsTerms rhsTerms : Lean.Meta.Grind.SolverTerms) →
    ((x : Lean.Meta.Grind.SolverTerms) → motive Lean.Meta.Grind.SolverTerms.nil x) →
      ((x : Lean.Meta.Grind.SolverTerms) →
          (x = Lean.Meta.Grind.SolverTerms.nil → False) → motive x Lean.Meta.Grind.SolverTerms.nil) →
        ((id₁ : ℕ) →
            (lhs : Lean.Expr) →
              (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                (id₂ : ℕ) →
                  (rhs : Lean.Expr) →
                    (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                      motive (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms)
                        (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)) →
          motive lhsTerms rhsTerms
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mkₐ_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (a : AdicCompletion.AdicCauchySequence I R) (n : ℕ),
  ↑((AdicCompletion.mkₐ I) a) n = (Ideal.Quotient.mk (I ^ n • ⊤)) (↑a n)