mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which runs a tactic on the main goal.
If that tactic fails, fall back to the `proc` behaviour of `cfg`.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.mainGoalProc : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  (Lean.MVarId → Lean.MetaM (List Lean.MVarId)) → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.GroupTheory.Index
/-- An additive subgroup has index two if and only if there exists `a ∉ H` such that
for all `b`, one of `a + b` and `b` belongs to `H`.  -/
AddSubgroup.index_eq_two_iff_exists_notMem_and' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a + b ∈ H ∨ b ∈ H
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instInhabitedState : {a : Std.Http.Protocol.H1.Direction} → Inhabited (Std.Http.Protocol.H1.Reader.State a)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.norm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  ‖a‖ = ‖DoubleCentralizer.toProdHom a‖
-- Std.Time.Time.PlainTime
/-- Creates a new `PlainTime` by adjusting the `nano` component to the given value.
 -/
Std.Time.PlainTime.withNanoseconds : Std.Time.PlainTime → Std.Time.Nanosecond.Ordinal → Std.Time.PlainTime
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Nat.unaryCast.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Comparable
/-- A partial order where any two elements are comparable is a linear order.  -/
linearOrderOfComprel : {α : Type u_1} →
  [inst : PartialOrder α] →
    [decLE : DecidableLE α] →
      [decLT : DecidableLT α] →
        [decEq : DecidableEq α] → (∀ (a b : α), CompRel (fun x1 x2 => x1 ≤ x2) a b) → LinearOrder α
-- Batteries.Data.Stream
Std.Stream.takeTR.loop.eq_2 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (acc : List α) (n : ℕ),
  Std.Stream.takeTR.loop s acc n.succ =
    match Std.Stream.next? s with
    | none => (acc.reverse, s)
    | some (a, s) => Std.Stream.takeTR.loop s (a :: acc) n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- A class guaranteeing that the continuous functional calculus is uniquely determined by the
properties that it is a continuous star algebra homomorphism mapping the (restriction of) the
identity to `a`. This is the necessary tool used to establish `cfcHom_comp` and the more common
variant `cfc_comp`.

This class has instances, which can be found in
`Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean`, in each of the common
cases `ℂ`, `ℝ` and `ℝ≥0` as a consequence of the Stone-Weierstrass theorem.

This class is separate from `ContinuousFunctionalCalculus` primarily because we will later use
`SpectrumRestricts` to derive an instance of `ContinuousFunctionalCalculus` on a scalar subring
from one on a larger ring (i.e., to go from a continuous functional calculus over `ℂ` for normal
elements to one over `ℝ` for selfadjoint elements), and proving this additional property is
preserved would be burdensome or impossible.  -/
ContinuousMap.UniqueHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : MetricSpace R] →
          [IsTopologicalSemiring R] →
            [ContinuousStar R] → [inst_5 : Ring A] → [StarRing A] → [TopologicalSpace A] → [Algebra R A] → Prop
-- Mathlib.Order.Interval.Finset.Defs
Finset.Icc_prod_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (x y : α × β),
  Finset.Icc x y = Finset.Icc x.1 y.1 ×ˢ Finset.Icc x.2 y.2
-- Mathlib.Tactic.Linarith.Parsing
/-- Compare monomials by first comparing their keys and then their powers.  -/
Mathlib.Tactic.Linarith.Monom.lt : Mathlib.Tactic.Linarith.Monom → Mathlib.Tactic.Linarith.Monom → Bool
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a),
  AddAction.stabilizerEquivStabilizer hg =
    (AddEquiv.addSubgroupMap (AddAut.addConj g) (AddAction.stabilizer G a)).trans (AddEquiv.addSubgroupCongr ⋯)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_neg_left`. -/
Antivary.neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f g → Monovary (-f) g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
rel_act_of_act_rel_act_of_rel_act : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] [IsTrans N r] (m : M)
  {a b c : N}, r (μ m a) (μ m b) → r b (μ m c) → r a (μ m c)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying type.  -/
GrpCat.carrier : GrpCat → Type u
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d.eq_3 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (val : ι), HomologicalComplex.extend.d K (some val) none = 0
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofSetoid.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s s_1 : Setoid α),
  s = s_1 →
    ∀ {inst_2 : DecidableRel ⇑s} [inst_3 : DecidableRel ⇑s_1], Finpartition.ofSetoid s = Finpartition.ofSetoid s_1
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_injective : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m],
  Function.Injective fun x v => Matrix.vecMul v x
-- Init.Prelude
/-- The typeclass behind the notation `a >>> b : γ` where `a : α`, `b : β`.  -/
HShiftRight : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Order.InitialSeg
RelIso.toInitialSeg_toFun : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α), f.toInitialSeg a = f a
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.objD.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.NormalizedMooreComplex.objD X n.succ =
    (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1)).factorThru
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1 + 1)).arrow (X.δ 0)) ⋯
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.isAlgebraic_adjoin_of_nonempty : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {s : Set S}, s.Nonempty → ((Algebra.adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x)
-- Mathlib.Tactic.GCongr.Core
/-- `gcongr` applies "generalized congruence" rules to recursively reduce a goal of form
`⊢ R (f a₁ ... aₙ) (f b₁ ... bₙ)` to (possibly multiple) goal(s) `⊢ Rᵢ aᵢ bᵢ`, keeping only the
distinct pairs `aᵢ ≠ bᵢ`, where `Rᵢ` is a possibly different relation (depending on the
precise rule). The relations `R`, `Rᵢ` can be any two-argument relation, including `· → ·`.

This tactic is extensible: to add a "generalized congruence" rule, tag a theorem with the attribute
`@[gcongr]`.

If a "generalized congruence" lemma has a side goal, `gcongr` will try to discharge it using
`gcongr_discharger`, which is an extensible tactic based on `positivity`. Side goals not discharged
in this way are left for the user.

* `gcongr with x y ... z` names the variables that are introduced by descending into binders (for
  example sums or suprema).
* `gcongr n`, where `n` is a natural number literal, limits the depth of the recursive applications.
  This is useful if `gcongr` is too aggressive in breaking down the goal.
* `gcongr t`, where `t` is a term with `?_` holes, performs congruence up to the holes in `t`.
  In other words, `gcongr f ?_` turns a goal `⊢ R (f x) (f y)` into `⊢ R x y` (but no further).
  This is useful if `gcongr` is too aggressive in breaking down the goal.

Examples:
```
example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
    x ^ 2 * a + c ≤ x ^ 2 * b + d := by
  -- LHS and RHS both have the form x ^ 2 * ?_ + ?_
  gcongr
  · -- New goal: ⊢ a ≤ b
    linarith
  · -- ⊢ New goal: c ≤ d
    linarith
-- Resulting proof term is:
--   add_le_add (mul_le_mul_of_nonneg_left ?_ (Even.pow_nonneg (even_two_mul 1) x)) ?_
-- where `add_le_add` and `mul_le_mul_of_nonneg_left` are generalized congruence lemmas
-- and the side goal `0 ≤ x ^ 2` is discharged by `gcongr_discharger`.
```

```
example {a b c d x : ℝ} (h : a + c + 1 ≤ b + d + 1) :
    x ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := by
  -- Using a pattern to limit the depth.
  gcongr x ^ 2 * ?_ + 5 -- or `gcongr 2`
  -- New goal: ⊢ a + c ≤ b + d
  linarith
```

```
-- Descending into binders (here: ⨆).
example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
  gcongr with i
  exact h i
```
 -/
Mathlib.Tactic.GCongr.gcongr : Lean.ParserDescr
-- Mathlib.Order.Partition.Finpartition
instDecidableEqFinpartition : {α : Type u_2} → {inst : Lattice α} → {inst_1 : OrderBot α} → {a : α} → [DecidableEq α] → DecidableEq (Finpartition a)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramPullback_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) {X Y : C} (f : X ⟶ Y) (S : (J.Cover Y)ᵒᵖ),
  (J.diagramPullback P f).app S =
    CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop ((J.pullback f).op.obj S)).index P)
      ((J.diagram P Y).obj S)
      (fun I =>
        CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P)
          (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I))
      ⋯
-- Aesop.Forward.Match.Types
Aesop.Match.instOrd : Ord Aesop.Match
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If a `BinaryFan` in the opposite category is a limit, then its `unop` is a colimit.  -/
CategoryTheory.Limits.BinaryFan.IsLimit.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)} →
        CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit c.unop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)} {hc : k' ∈ t.alter k f},
  (t.alter k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ ((f (t.get? k)).get ⋯) else t.get k' ⋯
-- Mathlib.Tactic.ITauto
/-- * `ak = .and`: `(p: A ∧ B → C) ⊢ A → B → C`
* `ak = .iff`: `(p: (A ↔ B) → C) ⊢ (A → B) → (B → A) → C`
* `ak = .eq`: `(p: (A = B) → C) ⊢ (A → B) → (B → A) → C`
 -/
Mathlib.Tactic.ITauto.Proof.curry : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanStaleDependencyParams.toJson : Lean.Lsp.LeanStaleDependencyParams → Lean.Json
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.derivWithin' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → t ⊆ s → derivWithin f₁ t =ᶠ[nhdsWithin x s] derivWithin f t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min?.bind t.get? = t.min?
-- Mathlib.InformationTheory.Hamming
Hamming.instFintypeOfDecidableEq : {ι : Type u_2} → {β : ι → Type u_3} → [DecidableEq ι] → [Fintype ι] → [(i : ι) → Fintype (β i)] → Fintype (Hamming β)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.toList.Perm t₂.toList → t₁ = t₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.RingTheory.Noetherian.Basic
LinearMap.submoduleMap.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), f.submoduleMap p = f.restrict ⋯
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If `v` is a complex infinite place, then the embedding `v.Completion →+* ℂ` is bijective.  -/
NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isComplex : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K},
  v.IsComplex → Function.Bijective ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Mathlib.Data.Fin.SuccPred
finCongr_symm_apply : ∀ {n m : ℕ} (eq : n = m) (a : Fin m), (finCongr eq).symm a = Fin.cast ⋯ a
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_take : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {n : ℕ} {p : G.Walk u u}, p.IsCycle → n < p.length → (p.take n).IsPath
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_singleton : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (b : α),
  MulAction.stabilizer G {b} = MulAction.stabilizer G b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) (w : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (idx : ℕ)
  (h_1 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinPred) →
          (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs))
  (h_2 :
    (w : ℕ) → (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)),
  (match Std.Tactic.BVDecide.BVPred.getLsbD expr idx with
    | Std.Tactic.BVDecide.BVPred.bin lhs op rhs => h_1 w lhs op rhs
    | Std.Tactic.BVDecide.BVPred.getLsbD expr idx => h_2 w expr idx) =
    h_2 w expr idx
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.rfl.inj : ∀ {done contextDependent done_1 contextDependent_1 : Bool},
  Lean.Meta.Sym.Simp.Result.rfl done contextDependent = Lean.Meta.Sym.Simp.Result.rfl done_1 contextDependent_1 →
    done = done_1 ∧ contextDependent = contextDependent_1
-- Init.Data.UInt.Bitwise
UInt8.and_le_right : ∀ {a b : UInt8}, a &&& b ≤ b
-- Mathlib.Tactic.Module
/-- Basic theoretical "normal form" object of the `match_scalars` and `module` tactics: a type
synonym for a list of ordered pairs in `R × M`, where typically `M` is an `R`-module.  This is the
form to which the tactics reduce module expressions.

(It is not a full "normal form" because the scalars, i.e. `R` components, are not themselves
ring-normalized. But this partial normal form is more convenient for our purposes.)  -/
Mathlib.Tactic.Module.NF : Type u_1 → Type u_2 → Type (max u_2 u_1)
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleWaitForDiagnostics.waitLoop : Lean.Lsp.WaitForDiagnosticsParams → Lean.Server.RequestM Lean.Server.FileWorker.EditableDocument
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `S : Set α` and `V : Set (β × β)`, we have
`UniformOnFun.gen 𝔖 S V = (S.domRestrict × S.domRestrict) ⁻¹' (UniformFun.gen S β V)`.
This is the crucial fact for proving that the family `UniformOnFun.gen S V` for `S ∈ 𝔖` and
`V ∈ 𝓤 β` is indeed a basis for the uniformity `α →ᵤ[𝔖] β` endowed with `𝒱(α, β, 𝔖, uβ)`
the uniform structure of `𝔖`-convergence, as defined in `UniformOnFun.uniformSpace`.  -/
UniformOnFun.gen_eq_preimage_restrict : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (S : Set α) (V : Set (β × β)),
  UniformOnFun.gen 𝔖 S V =
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_insert : ∀ (x y : PSet.{u_1}), x ∈ insert x y
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α],
  CompletelyDistribLattice.MinimalAxioms α → ∀ (f : (i : ι) → κ i → α), ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instTopologicalSpace : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → TopologicalSpace (A →ₜ+ B)
-- Mathlib.Topology.Separation.Basic
t0Space_iff_exists_isOpen_xor_mem : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ Xor (x ∈ U) (y ∈ U)
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation is a map that uniformly scales the edistance between any two points.  -/
«term_→ᵈ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setLIntegral_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SFinite ν], μ.AbsolutelyContinuous ν → ∀ (s : Set α), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
-- Lean.Elab.SyntheticMVars
/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved.  -/
Lean.Elab.Term.elabTermAndSynthesize : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `YonedaCollection F X` in `X`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.map₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {X : C} →
        (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
          {Y : C} →
            (X ⟶ Y) →
              CategoryTheory.OverPresheafAux.YonedaCollection F Y → CategoryTheory.OverPresheafAux.YonedaCollection F X
-- Mathlib.Topology.UrysohnsLemma
_private.Mathlib.Topology.UrysohnsLemma.0.Urysohns.CU.approx.match_1.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (motive : ℕ → Urysohns.CU P → X → Sort u_2)
  (c : Urysohns.CU P) (x : X) (h_1 : (c : Urysohns.CU P) → (x : X) → motive 0 c x)
  (h_2 : (n : ℕ) → (c : Urysohns.CU P) → (x : X) → motive n.succ c x),
  (match 0, c, x with
    | 0, c, x => h_1 c x
    | n.succ, c, x => h_2 n c x) =
    h_1 c x
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- A type alias for `QuadraticForm.LinearIsometry` to avoid confusion between the categorical and
algebraic spellings of composition.  -/
QuadraticModuleCat.Hom : {R : Type u} → [inst : CommRing R] → QuadraticModuleCat R → QuadraticModuleCat R → Type v
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.refl_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Equivalence.refl.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)
-- Init.Data.ByteArray.Lemmas
List.toByteArray_nil : [].toByteArray = ByteArray.empty
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts.  -/
CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F],
  CategoryTheory.Limits.PreservesBiproductsOfShape J F
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.trans_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant A] (P P' : HomotopicalAlgebra.Cylinder A) [inst_3 : P'.IsGood],
  (P.trans P').i₀ = CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.Limits.pushout.inl P.i₁ P'.i₀)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommRing.toRing : Lean.Meta.Sym.Arith.CommRing → Lean.Meta.Sym.Arith.Ring
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftDualIso_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (p : CategoryTheory.ExactPairing X Y), CategoryTheory.leftDualIso p p = CategoryTheory.Iso.refl X
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
/-- Zariski sheaves preserve products.  -/
AlgebraicGeometry.preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology : ∀ {F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type v)} {ι : Type u_1} [Small.{u, u_1} ι] [Small.{v, u_1} ι],
  CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F →
    CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ι) F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)} {k k' fallback : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKeyD k' fallback = k
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
volume_euclideanSpace_eq_dirac : ∀ (ι : Type u_4) [inst : Fintype ι] [inst_1 : IsEmpty ι], MeasureTheory.volume = MeasureTheory.Measure.dirac 0
-- Mathlib.Algebra.Group.Basic
mul_inv : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift.eq_1 : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M],
  FreeAddMonoid.lift =
    {
      toFun := fun f =>
        { toFun := fun l => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ },
      invFun := fun f x => f (FreeAddMonoid.of x), left_inv := ⋯, right_inv := ⋯ }