mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b)
  [inst_3 : p.IsHomLift f' φ'], p.IsHomLift g (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ')
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {f : M → G} [ContMDiffInv₀ I n G] {s : Set M} {a : M},
  ContMDiffWithinAt I' I n f s a → f a ≠ 0 → ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s a
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_self_toUnitHom : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n),
  MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) χ) = MulChar.toUnitHom χ
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.inv z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.hom z) h) =
    h
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The principal unit group of a valuation subring, as a subgroup of `Kˣ`.  -/
ValuationSubring.principalUnitGroup : {K : Type u} → [inst : Field K] → ValuationSubring K → Subgroup Kˣ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).minKey?.isSome = t.minKey?.isSome
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (-f) (-f') s x
-- Mathlib.Topology.Constructions.SumProd
IsOpenMap.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  IsOpenMap f → IsOpenMap g → IsOpenMap (Prod.map f g)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [Inhabited α] {k fallback : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.mk.inj : ∀ {rhs : Lean.Expr} {value : ℤ} {goal : Lean.MVarId} {rhs_1 : Lean.Expr} {value_1 : ℤ} {goal_1 : Lean.MVarId},
  { rhs := rhs, value := value, goal := goal } = { rhs := rhs_1, value := value_1, goal := goal_1 } →
    rhs = rhs_1 ∧ value = value_1 ∧ goal = goal_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.HasWeakLimitsOfShape.mk : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C],
  autoParam (∀ (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasWeakLimit F)
      CategoryTheory.Limits.HasWeakLimitsOfShape.hasWeakLimit._autoParam →
    CategoryTheory.Limits.HasWeakLimitsOfShape J C
-- Mathlib.Algebra.Lie.OfAssociative
/-- An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring
commutator.  -/
LieAlgebra.ofAssociativeAlgebra : {A : Type v} → [inst : Ring A] → {R : Type u} → [inst_1 : CommRing R] → [Algebra R A] → LieAlgebra R A
-- Lean.Syntax
/-- Adds the given trailing substring to a `Syntax`' existing trailing substring if they are adjacent,
otherwise returns `none`.
 -/
Lean.Syntax.addTrailing? : Lean.Syntax → Substring.Raw → Option Lean.Syntax
-- Mathlib.Order.Category.Lat
Lat.instCategory : CategoryTheory.Category.{u, u + 1} Lat
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.badReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasAdditiveReduction R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Reverses the ordering of the tree without any rebalancing.  -/
RBTree.RBNode.reverse : {α : Type u_1} → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.not : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, Measurable p → Measurable fun x => ¬p x
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.constantCoeff_largeSchroderSeries : PowerSeries.constantCoeff PowerSeries.largeSchroderSeries = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], Std.DTreeMap.Internal.Impl.contains a t = false → t.get! a = default
-- Mathlib.GroupTheory.Congruence.Defs
Con.instFunLikeForallProp.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Con.instFunLikeForallProp = { coe := fun c => ⇑c.toSetoid, coe_injective := ⋯ }
-- Mathlib.Algebra.Algebra.Hom
AlgHom.End_toSemigroup_toMul_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (φ₁ φ₂ : A →ₐ[R] A),
  φ₁ * φ₂ = φ₁.comp φ₂
-- Mathlib.Data.WSeq.Defs
/-- Returns `true` if `s` is `nil` and `false` if `s` has an element  -/
Stream'.WSeq.isEmpty : {α : Type u} → Stream'.WSeq α → Computation Bool
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unop_X : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c) (i : ι),
  X.unop.X i = Opposite.unop (X.X i)
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.headI_map : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : List Γ),
  (List.map f.f l).headI = f.f l.headI
-- Mathlib.Topology.LocallyClosed
Continuous.preimage_coborder_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (s : Set Y), f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)
-- Std.Http.Internal.IndexMultiMap
/-- Inserts multiple values for a given key, appending to any existing values.
 -/
Std.Internal.IndexMultiMap.insertMany : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [EquivBEq α] →
          [LawfulHashable α] → Std.Internal.IndexMultiMap α β → α → Array β → Std.Internal.IndexMultiMap α β
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_subset_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, intrinsicClosure 𝕜 s ⊆ ↑(affineSpan 𝕜 s)
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_iff_emod_eq_zero : ∀ {a b : ℤ}, a ∣ b ↔ b % a = 0
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.iff_inf_eq_bot : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [IsGalois F ↥A] [FiniteDimensional F ↥A] [FiniteDimensional F ↥B], A.LinearDisjoint ↥B ↔ A ⊓ B = ⊥
-- Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
PiTensorProduct.ofDirectSumEquiv_tprod_apply : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Finite ι] (x : (i : ι) → DirectSum (κ i) fun j => M i j) (p : (i : ι) → κ i),
  (PiTensorProduct.ofDirectSumEquiv ((PiTensorProduct.tprod R) x)) p = (PiTensorProduct.tprod R) fun i => (x i) (p i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false) {h' : k ∈ m₁.union m₂ ⋯ ⋯},
  (m₁.union m₂ ⋯ ⋯).get k h' = m₁.get k ⋯
-- Init.Data.String.Basic
/-- Given a position in `s`, obtain the corresponding position in `s.slice p₀ p₁ h`, or panic if `pos`
is not between `p₀` and `p₁`.
 -/
String.Pos.sliceOrPanic : {s : String} → s.Pos → (p₀ p₁ : s.Pos) → {h : p₀ ≤ p₁} → (s.slice p₀ p₁ h).Pos
-- Lean.Elab.DefView
Lean.Elab.DefKind.instance : Lean.Elab.DefKind
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `floorDiv_nonpos` instead.  -/
FloorDiv.floorDiv_nonpos : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : FloorDiv α β] ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_ne_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι} {xi : β i},
  (fun₀ | i => xi) ≠ 0 ↔ xi ≠ 0
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instZero : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : SMul R V] → [inst_2 : Zero V] → Zero (HahnModule Γ R V)
-- Init.Data.Array.Lemmas
Array.mem_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {b : β},
  b ∈ Array.filterMap f xs ↔ ∃ a ∈ xs, f a = some b
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} [inst : Inhabited β] {f : β → β},
  (m.modify k f)[k']! = if (k == k') = true then (Option.map f m[k]?).get! else m[k']!
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doReturn` which is of the form
```
"return " >> optional termParser
```
`doElems` is only used for sanity checking.  -/
Lean.Elab.Term.Do.ToCodeBlock.doReturnToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Data.FunLike.Group
/-- Coercion as an additive homomorphism.  -/
FunLike.coeAddHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) → [inst : FunLike F α β] → [inst_1 : Add F] → [inst_2 : Add β] → [IsAddApply F α β] → F →ₙ+ α → β
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_sInter : ∀ {V : Type u} {s : Set (Set (Sym2 V))}, SimpleGraph.fromEdgeSet (⋂₀ s) = sInf (SimpleGraph.fromEdgeSet '' s)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_le_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Rco.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Rco.HasRcoIntersection α] → Std.Rco α → Std.Rco α → Std.Rco α
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Check if there is already a duplicate of `result` in `results`,
for which both appear in the filtered view.  -/
_private.Mathlib.Tactic.ClickSuggestions.SectionState.0.Mathlib.Tactic.ClickSuggestions.Result.insertInArray.findDuplicate : {α : Type} →
  (α → α → Lean.MetaM Bool) →
    Mathlib.Tactic.ClickSuggestions.Result α → Array (Mathlib.Tactic.ClickSuggestions.Result α) → Lean.MetaM (Option ℕ)
-- Mathlib.Data.List.Induction
List.bidirectionalRec_singleton : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α),
  List.bidirectionalRec nil singleton cons_append [a] = singleton a
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.brecOn.go : {α : Type u} →
  {motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_1} →
    (t : Batteries.BinomialHeap.Imp.Heap α) →
      ((t : Batteries.BinomialHeap.Imp.Heap α) → Batteries.BinomialHeap.Imp.Heap.below t → motive t) →
        motive t ×' Batteries.BinomialHeap.Imp.Heap.below t
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_Option : ∀ {α : Type} {x : Option α} {h : PUnit.{1} → Option α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{1} Std.Do.PostShape.pure)},
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_right_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (y + z * x) ↔ IsRelPrime x y
-- Lean.CoreM
Lean.Core.Context.initHeartbeats : Lean.Core.Context → ℕ
-- Mathlib.Order.Hom.Bounded
instCoeTCBoundedOrderHomOfBoundedOrderHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [inst_3 : BoundedOrder α] →
              [inst_4 : BoundedOrder β] → [BoundedOrderHomClass F α β] → CoeTC F (BoundedOrderHom α β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
          P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → IsUnit (W.dblU P)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.mk.injEq : ∀ (thms : Lean.Meta.Grind.InjectiveTheoremsArray)
  (fns : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo)
  (thms_1 : Lean.Meta.Grind.InjectiveTheoremsArray)
  (fns_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo),
  ({ thms := thms, fns := fns } = { thms := thms_1, fns := fns_1 }) = (thms = thms_1 ∧ fns = fns_1)
-- Mathlib.Data.Set.Lattice
Set.iInter_plift_up : ∀ {α : Type u_1} {ι : Sort u_5} (f : PLift ι → Set α), ⋂ i, f { down := i } = ⋂ i, f i
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RioSliceData α β)) Id (Std.DTreeMap.Internal.RxoIterator α β)
        ((a : α) × β a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N] (f : M → N)
  (hf : ContMDiff IM IN (↑⊤) f) (x : M),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (ChartedSpace.locallyRingedSpaceMap f hf) x)
      (smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) =
    smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_re : ∀ (x : ℂ), (Complex.log x).re = Real.log ‖x‖
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelVAdd.left_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : VAdd G P] [IsLeftCancelVAdd G P] (a : G) (b c : P), a +ᵥ b = a +ᵥ c → b = c
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasProd_pnat_iff_hasProd_succ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℕ → M},
  HasProd (fun x => f ↑x) m ↔ HasProd (fun x => f (x + 1)) m
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The ⋆-algebra equivalence between `A` and 1×1 matrices with its entry in `A`.  -/
CStarMatrix.toOneByOne : (n : Type u_2) →
  (R : Type u_3) →
    (A : Type u_5) →
      [inst : Unique n] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Mul A] → [inst_4 : Star A] → [inst_5 : Module R A] → A ≃⋆ₐ[R] CStarMatrix n n A
-- Mathlib.Probability.Process.Adapted
/-- Progressive process. A sequence of functions `u` is said to be progressive with respect
to a filtration `f` if at each point in time `i`, `u` restricted to `Set.Iic i × Ω` is measurable
with respect to the product `MeasurableSpace` structure where the σ-algebra used for `Ω` is `f i`.
The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
usual definition for index types `ℝ≥0` or `ℕ`.  -/
MeasureTheory.IsProgressive : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : Type u_3} → [MeasurableSpace ι] → [MeasurableSpace β] → MeasureTheory.Filtration ι m → (ι → Ω → β) → Prop
-- Lean.PrettyPrinter.Formatter
/-- Execute `x` at the right-most child of the current node, if any, then advance to the left.
Runs `x` even if there are no children, in which case the current syntax node will be `.missing`.
 -/
Lean.PrettyPrinter.Formatter.visitArgs : Lean.PrettyPrinter.FormatterM Unit → Lean.PrettyPrinter.FormatterM Unit
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Retrieve the user-specified configuration options.  -/
Lean.Elab.Tactic.Omega.cfg : Lean.Elab.Tactic.Omega.OmegaM Lean.Meta.Omega.OmegaConfig
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_pi_div_two : ∀ (c : ℂ) (R : ℝ), circleMap c R (Real.pi / 2) = c + ↑R * Complex.I
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mk_eq : ∀ (x : PSet.{u_1}), ⟦x⟧ = ZFSet.mk x
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_hom_apply_down : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} (f : X ⟶ Y) (X_1 : Cᵒᵖ)
  (x : ULift.{w, v} (((CategoryTheory.sheafToPresheaf J (Type v)).obj (J.yoneda.obj X)).obj X_1)),
  ((CategoryTheory.ConcreteCategory.hom
          (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).map f).hom.app X_1))
        x).down =
    CategoryTheory.CategoryStruct.comp x.down f
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if `e` is a `OfNat.ofNat` literal of type `BitVec _` or `Fin _`.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.isOfNatFinBitVecLiteral : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_iso_inv : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).iso.inv =
    CategoryTheory.CategoryStruct.id
      (X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Data.Vector.Defs
/-- Create a vector from another with a provably equal length.  -/
List.Vector.congr : {α : Type u_1} → {n m : ℕ} → n = m → List.Vector α n → List.Vector α m
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.mk_le_mk : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
  AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁
-- Mathlib.FieldTheory.LinearDisjoint
/-- Similar to `IntermediateField.LinearDisjoint.of_le_right` but this is for abstract fields.  -/
IntermediateField.LinearDisjoint.of_le_right' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ (L' : Type u_1) [inst_7 : Field L'] [inst_8 : Algebra F L'] [inst_9 : Algebra L' L] [IsScalarTower F L' L]
      [inst_11 : Algebra L' E] [inst_12 : IsScalarTower F L' E] [IsScalarTower L' L E], A.LinearDisjoint L'
-- Lean.DocString.DeferredCheck
Lean.Doc.instInhabitedDeferredCheckSite : Inhabited Lean.Doc.DeferredCheckSite
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.norm_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (self : P ≃ᵃⁱ[𝕜] P₂) (x : V), ‖self.linear x‖ = ‖x‖
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Given a basis of a ring over itself indexed by a type `ι`, then `ι` is `Unique`.  -/
Module.Basis.unique : (R : Type u) → [inst : Semiring R] → [StrongRankCondition R] → {ι : Type u_2} → Module.Basis ι R R → Unique ι
-- Mathlib.Algebra.Group.Defs
RightCancelSemigroup.ext : ∀ {G : Type u} {x y : RightCancelSemigroup G}, Mul.mul = Mul.mul → x = y