mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructions
isClosed_sigma_iff : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)},
  IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} {g : ℕ → α} {m : ℕ}
  [inst : MeasurableSingletonClass α], ∀ᶠ (n : ℕ) in Filter.atTop, (MeasureTheory.simpleFuncAux✝ f g n) (g m) = f (g m)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The proposed colimit cocone is a colimit in `CommMonCat`.  -/
CommMonCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommMonCat) →
        CategoryTheory.Limits.IsColimit (CommMonCat.FilteredColimits.colimitCocone F)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_left_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y : P}, midpoint R x y = x ↔ x = y
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_smul_le : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : Ω → ENNReal) {c : ENNReal},
  c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.continuous_lintegral_continuousMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] [inst_2 : MeasurableSpace X]
  [inst_3 : OpensMeasurableSpace X] {F : Type u_3} [inst_4 : FunLike F X NNReal] [ContinuousMapClass F X NNReal]
  (f : F), Continuous fun μ => ∫⁻ (x : X), ↑(f x) ∂↑μ
-- Mathlib.GroupTheory.Coset.Defs
/-- `α ⧸ s` is the quotient type representing the left cosets of `s`. If `s` is a normal subgroup,
`α ⧸ s` is a group  -/
QuotientGroup.instHasQuotientSubgroup : {α : Type u_1} → [inst : Group α] → HasQuotient α (Subgroup α)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.get_eq_getValue : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : PartialEquivBEq α]
  [inst_3 : LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m)
  {a : α} {h : m.contains a = true},
  Std.DHashMap.Internal.Raw₀.Const.get m a h =
    Std.Internal.List.getValue a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_mul_cancel_right : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' (x * ↑y) y = f x
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_monotone : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W), Monotone (SimpleGraph.comap ⇑f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
      (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
-- Mathlib.Data.Int.Cast.Lemmas
zsmul_eq_mul : ∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), n • a = ↑n * a
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_ground : ∀ {α : Type u_2} (M : Matroid α), M.closure M.E = M.E
-- Mathlib.Order.TypeTags
WithTop.eq_1 : ∀ (α : Type u_2), WithTop α = Option α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.union_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Mathlib.Data.Finset.Insert
Finset.pair_eq_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a, a} = {a}
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.trivialFibrations_llp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.trivialFibrations C).llp = HomotopicalAlgebra.cofibrations C
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.iSup : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_3} [Finite ι] (P : ι → AddSubmonoid M),
  (∀ (i : ι), (P i).FG) → (iSup P).FG
-- Mathlib.Topology.Instances.Rat
Int.isUniformEmbedding_coe_rat : IsUniformEmbedding Int.cast
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ico_eq_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iio a ∪ Set.Ico a b = Set.Iio b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- There are finitely many embeddings of a number field.  -/
NumberField.Embeddings.instFintypeRingHom : (K : Type u_1) →
  [inst : Field K] → (A : Type u_2) → [inst_1 : Field A] → [CharZero A] → [NumberField K] → Fintype (K →+* A)
-- Mathlib.Order.SymmDiff
compl_bihimp : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), (bihimp a b)ᶜ = symmDiff a b
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_id_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) {Y Y' Y'' : D} (g : Y ⟶ Y') (g' : Y' ⟶ Y''),
  P.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.CategoryStruct.id X) g')
      (P.map (CategoryTheory.CategoryStruct.id X) g)
-- Init.Data.UInt.Bitwise
instAssociativeUSizeHAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMul : {α : Type u} → [Mul α] → Mul (WithOne α)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instOne : {n : Type u_2} → {A : Type u_5} → [DecidableEq n] → [Zero A] → [One A] → One (CStarMatrix n n A)
-- Mathlib.Analysis.Matrix.Order
Matrix.tracePositiveLinearMap_apply : ∀ (n : Type u_3) (α : Type u_4) (𝕜 : Type u_5) [inst : Fintype n] [inst_1 : Semiring α] [inst_2 : RCLike 𝕜]
  [inst_3 : Module α 𝕜] (x : Matrix n n 𝕜), (Matrix.tracePositiveLinearMap n α 𝕜) x = x.trace
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.State.mk.injEq : ∀ (newGoals : Array Lean.MVarId) (patterns : List (Lean.TSyntax `rintroPat)) (newGoals_1 : Array Lean.MVarId)
  (patterns_1 : List (Lean.TSyntax `rintroPat)),
  ({ newGoals := newGoals, patterns := patterns } = { newGoals := newGoals_1, patterns := patterns_1 }) =
    (newGoals = newGoals_1 ∧ patterns = patterns_1)
-- Batteries.Classes.Cast
/-- Coercions such as `Nat.castCoe` that go from a concrete structure such as
`Nat` to an arbitrary ring `R` should be set up as follows:
```lean
instance : CoeTail Nat R where coe := ...
instance : CoeHTCT Nat R where coe := ...
```

It needs to be `CoeTail` instead of `Coe` because otherwise type-class
inference would loop when constructing the transitive coercion `Nat → Nat → Nat → ...`.
Sometimes we also need to declare the `CoeHTCT` instance
if we need to shadow another coercion
(e.g. `Nat.cast` should be used over `Int.ofNat`).
 -/
LibraryNote.coercion_into_rings : Batteries.Util.LibraryNote
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The set of statements accessible from initial set `S` of labels.  -/
Turing.TM2.stmts : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (Λ → Turing.TM2.Stmt Γ Λ σ) → Finset Λ → Finset (Option (Turing.TM2.Stmt Γ Λ σ))
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_eq_match_roi : ∀ {α : Type u} {r : Std.Rii α} {hu : True} [inst : LT α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.UpwardEnumerable α] [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_5 : Std.Rxi.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_7 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    match Std.PRange.least? with
    | none => pure init
    | some next => do
      let __do_lift ← f next hu init
      match __do_lift with
        | ForInStep.yield c => forIn' next<...* c fun a x acc => f a ⋯ acc
        | ForInStep.done c => pure c
-- Init.Internal.Order.Basic
Lean.Order.flat_csup_is_sup : ∀ {α : Sort u} {b : α} (c : Lean.Order.FlatOrder b → Prop),
  Lean.Order.chain c → Lean.Order.is_sup c (Lean.Order.flat_csup c)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.clift Monoid.Coprod.mk ⋯ ⋯ ⋯ ⋯ = MonoidHom.id (Monoid.Coprod M N)
-- Mathlib.Analysis.Analytic.Composition
AnalyticOnNhd.comp : ∀ {𝕜 : 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] {s : Set E} {t : Set F} {g : F → G} {f : E → F},
  AnalyticOnNhd 𝕜 g t → AnalyticOnNhd 𝕜 f s → Set.MapsTo f s t → AnalyticOnNhd 𝕜 (g ∘ f) s
-- Mathlib.Data.Ordmap.Ordnode
/-- Basic pretty printing for `Ordnode α` that shows the structure of the tree.

```
repr {3, 1, 2, 4} = ((∅ 1 ∅) 2 ((∅ 3 ∅) 4 ∅))
```  -/
Ordnode.repr : {α : Type u_2} → [Repr α] → Ordnode α → ℕ → Std.Format
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, (m.insertMany l).contains k = (m.contains k || l.contains k)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey? k =
        if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then some k else none
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instDistribMulAction_1 : {G₀ : Type u_1} →
  {M₀ : Type u_2} → [inst : Monoid G₀] → [inst_1 : AddMonoid M₀] → [DistribMulAction G₀ M₀] → DistribMulAction G₀ M₀ᵒᵈ
-- Mathlib.Topology.Order.WithTop
WithTop.tendsto_coe_atTop : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [NoMaxOrder ι],
  Filter.Tendsto WithTop.some Filter.atTop (nhds ⊤)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory FinBddDistLat fun x1 x2 => BoundedLatticeHom ↑x1.toDistLat ↑x2.toDistLat
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Compose a quadratic map with a linear function on the left.  -/
LinearMap.compQuadraticMap : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      {P : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : AddCommMonoid P] →
                    [inst_6 : Module R P] → (N →ₗ[R] P) → QuadraticMap R M N → QuadraticMap R M P
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Nat.borelSpace : BorelSpace ℕ
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_mem_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubmonoid A) (x : A), a • x ∈ a • S ↔ x ∈ S
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
`{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × Ω`, where `G` is a group acting on `X`
and `Ω = X/G` denotes the quotient of `X` by the relation `orbitRel G X`.  -/
MulAction.sigmaFixedByEquivOrbitsProdGroup : (G : Type u) →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : MulAction G X] → (g : G) × ↑(MulAction.fixedBy X g) ≃ Quotient (MulAction.orbitRel G X) × G
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_lt_nat : ∀ {o : Ordinal.{u_1}} {n : ℕ}, o.card < ↑n ↔ o < ↑n
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.decidableMemMker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] [inst_3 : DecidableEq N] (f : F) (x : M),
  AddMonoidHom.decidableMemMker f x = decidable_of_iff (f x = 0) ⋯
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheorems : Inhabited Mathlib.Meta.FunProp.LambdaTheorems
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.variable : Lean.Lsp.SemanticTokenType
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The preimage under Spec.  -/
AlgebraicGeometry.Spec.preimage : {R S : CommRingCat} → (AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R) → (R ⟶ S)
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks_fromBlocks₂₂ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α), (Matrix.fromBlocks A B C D).toBlocks₂₂ = D
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- An induction principle to deduce results for `Angle` from those for `ℝ`, used with
`induction θ using Real.Angle.induction_on`.  -/
Real.Angle.induction_on : ∀ {p : Real.Angle → Prop} (θ : Real.Angle), (∀ (x : ℝ), p ↑x) → p θ
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_smul : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F]
  [inst_9 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) →
    ∀ (c : 𝕜) (f : ↥(MeasureTheory.Lp E 1 μ)),
      (MeasureTheory.L1.setToL1 hT) (c • f) = c • (MeasureTheory.L1.setToL1 hT) f
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instAddCommGroup : (K : Type u) →
  [inst : CommRing K] →
    (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → AddCommGroup (PerfectClosure K p)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply : ∀ {J : Type v} (F : J → Type (max v u)) (j : J) (x : F j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.coproductIso F).hom)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι F j)) x) =
    ⟨j, x⟩
-- Lean.Meta.CollectMVars
/-- Auxiliary definition for `getMVarDependencies`.  -/
_private.Lean.Meta.CollectMVars.0.go : Lean.MVarId → optParam Bool false → StateRefT' IO.RealWorld (Std.HashSet Lean.MVarId) Lean.MetaM Unit
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_ne_top : ∀ {a : ENNReal}, a⁻¹ ≠ ⊤ ↔ a ≠ 0
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.GeneralLinearGroup.continuous_apply : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] {α : Type u_4} [inst_4 : TopologicalSpace α] (f : α → GL n R),
  Continuous f → ∀ (i : n), Continuous fun x => ↑(f x) i
-- Lean.Elab.PreDefinition.Structural.BRecOn
_private.Lean.Elab.PreDefinition.Structural.BRecOn.0.Lean.Elab.Structural.replaceRecApps.loop : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions →
    (recFnNames : Array Lean.Name) →
      (Lean.Expr → StateRefT' IO.RealWorld (Lean.HasConstCache recFnNames) Lean.MetaM Bool) →
        Lean.Expr → Lean.Expr → StateRefT' IO.RealWorld (Lean.HasConstCache recFnNames) Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesRightKanExtensions L` means that `G : B ⥤ D` preserves all right Kan extensions
along `L : A ⥤ C` of every functor `A ⥤ B`.  -/
CategoryTheory.Functor.PreservesRightKanExtensions : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A C → Prop
-- Mathlib.Computability.Encoding
/-- A decoding function from `List Bool` to the binary numbers.  -/
Computability.decodeNum : List Bool → Num
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.instIsDominantιCoborderRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsDominant (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycle_induction_on : ∀ {β : Type u_3} [Finite β] (P : Equiv.Perm β → Prop) (σ : Equiv.Perm β),
  P 1 →
    (∀ (σ : Equiv.Perm β), σ.IsCycle → P σ) →
      (∀ (σ τ : Equiv.Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)) → P σ
-- Lean.Data.NameTrie
Lean.NameTrie.toArray : {β : Type u_1} → Lean.NameTrie β → Array β
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G} {s : Set F},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → (m₁ == m₂) = true → m₁.Equiv m₂
-- Init.Grind.Ring.Field
/-- Raising to a negative power is the inverse of raising to the positive power.  -/
Lean.Grind.Field.zpow_neg : ∀ {α : Type u} [self : Lean.Grind.Field α] (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹
-- Mathlib.MeasureTheory.Measure.Restrict
/-- See also `MeasureTheory.ae_uIoc_iff`.  -/
MeasureTheory.ae_restrict_uIoc_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : LinearOrder α] {a b : α} {P : α → Prop},
  (∀ᵐ (x : α) ∂μ.restrict (Set.uIoc a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Set.Ioc b a), P x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_add_inter_subset_union : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.IsSheaf.isSheafFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presieve.IsSheaf J P →
    ∀ (R : CategoryTheory.Presieve X), CategoryTheory.Sieve.generate R ∈ J X → CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.Tactic.Lift
/-- `lift e to t with x` lifts the expression `e` to the type `t` by introducing a new variable `x : t`
such that `↑x = e`, and then replacing occurrences of `e` with `↑x`. `lift` requires an instance of
the class `CanLift t' t coe cond`, where `t'` is the type of `e`, and creates a side goal for the
lifting condition, of the form `⊢ cond x`, placing this on top of the goal stack.

Given an instance `CanLift β γ`, `lift` can also lift `α → β` to `α → γ`; more generally, given
`β : Π a : α, Type*`, `γ : Π a : α, Type*`, and `[Π a : α, CanLift (β a) (γ a)]`, it
automatically generates an instance `CanLift (Π a, β a) (Π a, γ a)`.

`lift` is in some sense dual to the `zify` tactic. `lift (z : ℤ) to ℕ` will change the type of an
integer `z` (in the supertype) to `ℕ` (the subtype), given a proof that `z ≥ 0`;
propositions concerning `z` will still be over `ℤ`. `zify` changes propositions about `ℕ` (the
subtype) to propositions about `ℤ` (the supertype), without changing the type of any variable.

The `norm_cast` tactic can be used after `lift` to normalize introduced casts.

* `lift e to t using h with x` uses the expression `h` to prove the lifting condition `cond e`.
  If `h` is a variable, `lift` will try to clear it from the context. If you want to keep `h` in
  the context, write `lift e to t using h with x rfl h` (see below).
* If `e` is a variable, `lift e to t` is equivalent to `lift e to t with e`. The original variable
  `e` will be cleared from the context.
* `lift e to t with x hx` adds `hx : ↑x = e` to the context (and if `e` is a variable, does not
  clear it).
* `lift e to t with x hx h` adds `hx : ↑x = e` and `h : cond e` to the context (and if `e` is a
  variable, does not clear it). In particular, `lift e to t using h with x hx h`, where `h` is a
  variable, keeps `h` in the context.
* `lift e to t with x rfl h` adds `h : cond e` to the context (and if `e` is a variable, does not
  clear it). In particular, `lift e to t using h with x rfl h`, where `h` is a variable, keeps `h`
  in the context.

Examples:
```
def P (n : ℤ) : Prop := n = 3

example (n : ℤ) (h : P n) : n = 3 := by
  lift n to ℕ
  /-
  Two goals:
  n : ℤ, h : P n ⊢ n ≥ 0
  n : ℕ, h : P ↑n ⊢ ↑n = 3
  -/
  · unfold P at h; linarith
  · exact h

example (n : ℤ) (hn : n ≥ 0) (h : P n) : n = 3 := by
  lift n to ℕ using hn
  /-
  One goal:
  n : ℕ
  h : P ↑n
  ⊢ ↑n = 3
  -/
  exact h

example (n : ℤ) (hn : n + 3 ≥ 0) (h : P (n + 3)) :
    n + 3 = n * 2 + 3 := by
  lift n + 3 to ℕ using hn with k hk
  /-
  One goal:
  n : ℤ
  k : ℕ
  hk : ↑k = n + 3
  h : P ↑k
  ⊢ ↑k = 2 * n + 3
  -/
  unfold P at h; linarith
```
 -/
Mathlib.Tactic.lift : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The map from the `mixedSpace K` to `realSpace K` that sends the values at complex places
to their norm.
 -/
NumberField.mixedEmbedding.normAtComplexPlaces : {K : Type u_1} → [inst : Field K] → NumberField.mixedEmbedding.mixedSpace K → NumberField.mixedEmbedding.realSpace K
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instHasColimitsOfHasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasColimits (AlgebraicGeometry.SheafedSpace C)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_mulLeft₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), ⇑(MeasurableEquiv.mulLeft₀ g hg) = fun x => g * x
-- Mathlib.Logic.Relation
Relation.TransGen.lift' : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} (f : α → β),
  r ≤ Function.onFun (Relation.TransGen p) f → Relation.TransGen r ≤ Function.onFun (Relation.TransGen p) f
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric_nhdsWithin' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {c : (x : α) → x ∈ s → Set α},
  IsCompact s → (∀ (x : α) (hx : x ∈ s), c x hx ∈ nhdsWithin x s) → ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ∩ s ⊆ c ↑y ⋯