mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.hexagon_forward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.braiding Y).hom (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) (X.braiding Z).hom))
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.of_mul_of : ∀ {α : Type u} [inst : Mul α] (x y : α), FreeAbelianGroup.of x * FreeAbelianGroup.of y = FreeAbelianGroup.of (x * y)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_equiv_sup : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  {a₁ b₁ a₂ b₂ : CauSeq α abs}, a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⊔ b₁ ≈ a₂ ⊔ b₂
-- Mathlib.Order.Bounded
Set.bounded_gt_Ioc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Ioc a b)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Product of two continuous homomorphisms on different spaces.  -/
ContinuousAddMonoidHom.prodMap : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      {D : Type u_5} →
        [inst : AddMonoid A] →
          [inst_1 : AddMonoid B] →
            [inst_2 : AddMonoid C] →
              [inst_3 : AddMonoid D] →
                [inst_4 : TopologicalSpace A] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace C] →
                      [inst_7 : TopologicalSpace D] → (A →ₜ+ C) → (B →ₜ+ D) → A × B →ₜ+ C × D
-- Std.Sat.AIG.CNF
/-- Add the CNF for a `Decl.gate` to the state.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addGate : {aig : Std.Sat.AIG ℕ} →
  {lhs rhs : Std.Sat.AIG.Fanin} →
    (state : Std.Sat.AIG.toCNF.State✝ aig) →
      {hlb : lhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state)).size} →
        {hrb : rhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state)).size} →
          (idx : ℕ) →
            (h : idx < aig.decls.size) →
              aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs →
                (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[lhs.gate] = true →
                  (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[rhs.gate] = true →
                    { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out idx h }
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.stx : Lean.Elab.Term.SyntheticMVarDecl → Lean.Syntax
-- Batteries.Data.List.Basic
/-- `tails l` is the list of terminal segments of `l`.
```
tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]
```
 -/
List.tails : {α : Type u_1} → List α → List (List α)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mono_iff_injective : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B),
  CategoryTheory.Mono f ↔ Function.Injective ⇑(Rep.Hom.hom f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.ProjectiveSpectrum.comap.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f f_1 : 𝒜 →+*ᵍ ℬ) (e_f : f = f_1)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)),
  AlgebraicGeometry.ProjectiveSpectrum.comap f hf = AlgebraicGeometry.ProjectiveSpectrum.comap f_1 ⋯
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below.cons : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {a : s.Pos}
  {motive : (a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1 → Prop}
  (middlePos endPos : s.Pos) (a_1 : String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a middlePos)
  (a_2 : String.Slice.Pattern.Model.IsLongestRevMatchAt pat middlePos endPos),
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below a_1 →
    motive middlePos a_1 → String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below ⋯
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_X_left : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R],
  MvPolynomial.aeval MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_apply : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : WithBot (σ →₀ ℕ)), m.toWithBotSyn a = WithBot.map (⇑m.toSyn) a
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C),
  (CategoryTheory.FunctorToTypes.coprod F G).obj a = (F.obj a ⊕ G.obj a)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_center : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A],
  ↑(NonUnitalStarSubalgebra.center R A) = Set.center A
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr_eq_1 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : x = Ordering.lt → motive Ordering.lt)
  (h_2 : x = Ordering.eq → motive Ordering.eq) (h_3 : x = Ordering.gt → motive Ordering.gt) (heq_1 : x = Ordering.lt),
  (match h : x with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) ≍
    h_1 heq_1
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instSurjectiveCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.Surjective g], AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.map_mk : ∀ {K : Type u_1} [inst : Field K] (x : K) (hx : x ∈ integralClosure ℤ K),
  (algebraMap (NumberField.RingOfIntegers K) K) ⟨x, hx⟩ = x
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.im_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (f : CategoryTheory.Arrow C), CategoryTheory.Abelian.im.obj f = CategoryTheory.Abelian.image f.hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.toArray_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.keys.toArray = m.keysArray
-- Mathlib.Logic.Relation
Relation.Map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (r : α → β → Prop) (f : α → γ) (g : β → δ) (c : γ)
  (d : δ), Relation.Map r f g c d = ∃ a b, r a b ∧ f a = c ∧ g b = d
-- Mathlib.Order.Lattice
sup_left_idem : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ (a ⊔ b) = a ⊔ b
-- Std.Do.WP.Basic
Std.Do.ReaderT.instWP : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} → {ρ : Type u} → [Std.Do.WP m ps] → Std.Do.WP (ReaderT ρ m) (Std.Do.PostShape.arg ρ ps)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.nonempty : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [Nontrivial R]
  (w : Convexity.StdSimplex R M), Nonempty M
-- Mathlib.LinearAlgebra.Dual.Defs
/-- That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$.
This is the definition of the dual annihilator of the submodule $W$.  -/
Submodule.dualRestrict_ker_eq_dualAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (W : Submodule R M), W.dualRestrict.ker = W.dualAnnihilator
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Whiskering a 2-square with a natural transformation at the top.  -/
CategoryTheory.TwoSquare.whiskerTop : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        {T' : CategoryTheory.Functor C₁ C₂} →
                          CategoryTheory.TwoSquare T' L R B → (T ⟶ T') → CategoryTheory.TwoSquare T L R B
-- Lean.Elab.Import
Lean.Elab.headerToImports : Lean.Elab.HeaderSyntax → optParam Bool true → Array Lean.Import
-- Mathlib.AlgebraicGeometry.Sites.Affine
/-- The `Spec` functor from affine `P`-schemes over `S` to `P`-schemes over `S` is dense
if `P` is local at the source.  -/
AlgebraicGeometry.Scheme.isCoverDense_toOver_Spec : ∀ {S : AlgebraicGeometry.Scheme} (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.IsMultiplicative]
  [AlgebraicGeometry.IsZariskiLocalAtSource P] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P AlgebraicGeometry.Scheme.Spec S).IsCoverDense
    (AlgebraicGeometry.Scheme.smallGrothendieckTopology P S)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.insertMany t l) k = Std.ExtDTreeMap.Const.get? t k
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.injective_map : ∀ {X : SSet} [X.Nonsingular] {n : ℕ},
  ∀ x ∈ X.nonDegenerate n,
    ∀ {m : SimplexCategory} {f g : m ⟶ { len := n }},
      (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (X.map g.op)) x →
        f = g
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instCanonicallyOrderedAdd : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  CanonicallyOrderedAdd (FractionalIdeal S P)
-- Mathlib.CategoryTheory.GuitartExact.Over
/-- Given `F : C ⥤ D` and `X : C`, this is the `2`-square
```
    Over.post F
Over X ⥤ Over (F.obj X)
 |          |
 v          v
 C     ⥤    D
       F
```
with `Over.forget` as vertical functors.  -/
CategoryTheory.TwoSquare.overPost : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (X : C) →
            CategoryTheory.TwoSquare (CategoryTheory.Over.post F) (CategoryTheory.Over.forget X)
              (CategoryTheory.Over.forget (F.obj X)) F
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instLawfulUpwardEnumerable : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerable (BitVec n)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points in strict order on the same line, and a fourth point, the angles at the
fourth point between the second and third or first and third points have the same sign.  -/
Sbtw.oangle_sign_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P} (p₄ : P),
  Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Dependent recursor for `fix F`  -/
MvQPF.Fix.drec : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] →
      {α : TypeVec.{u} n} →
        {β : MvQPF.Fix F α → Type u} →
          ((x : F (α ::: Sigma β)) → β (MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) →
            (x : MvQPF.Fix F α) → β x
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C} {X : C}
  {R : CategoryTheory.Presieve X}, R ∈ P.precoverage.coverings X ↔ ∃ E, P.property E ∧ R = E.presieve₀
-- Mathlib.Algebra.Order.Monoid.NatCast
lt_add_one : ∀ {α : Type u_1} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
  [AddLeftStrictMono α] (a : α), a < a + 1
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.derivMetricTensorAux_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  (σ τ : (x : M) → V x) {x : M} (X₀ : TangentSpace I x),
  (CovariantDerivative.derivMetricTensorAux✝ I cov σ τ x) X₀ =
    ((d% fun x => inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ ((↑cov σ x) X₀) (τ x) - inner ℝ (σ x) ((↑cov τ x) X₀)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_singleton_iff : ∀ {k m n : ℤ}, (m<...n).toArray = #[k] ↔ n = m + 2 ∧ m + 1 = k
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.functor.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Abelian.FreydMitchell.functor C =
    (CategoryTheory.Abelian.FreydMitchell.F✝ C).comp
      ((CategoryTheory.Abelian.FreydMitchell.G✝ C).comp (CategoryTheory.Abelian.FreydMitchell.H✝ C))
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- The homotopy path class of 0 → 1 in `ULift I`  -/
unitInterval.uhpath01 : FundamentalGroupoid.fromTop { down := 0 } ⟶ FundamentalGroupoid.fromTop { down := 1 }
-- Init.Data.String.Basic
String.data_eq_nil_iff : ∀ {b : String}, b.toList = [] ↔ b = ""
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.image_mem_functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (R : CategoryTheory.Presieve X) {f : Y ⟶ X},
  R f → CategoryTheory.Presieve.functorPushforward F R (F.map f)
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.div_left : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {s t : Set α},
  IsUpperSet t → IsLowerSet (s / t)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.exp_mul : ∀ (x y : ℝ), Real.exp (x * y) = Real.exp x ^ y
-- Lean.Elab.Do.Basic
/-- Return `let $k.resultName : PUnit := PUnit.unit; $(← k.k)`, ensuring that the result type of `k.k`
is `PUnit` and then immediately zeta-reduce the `let`.
 -/
Lean.Elab.Do.DoElemCont.continueWithUnit : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.sum.match_1.eq_1 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (u v : V)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_1 : V ⊕ W) → motive x x_1),
  (match Sum.inl u, Sum.inl v with
    | Sum.inl u, Sum.inl v => h_1 u v
    | Sum.inr u, Sum.inr v => h_2 u v
    | x, x_1 => h_3 x x_1) =
    h_1 u v
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.approxOn_range_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] [inst_4 : Zero α] [inst_5 : Preorder α] {f : β → α},
  0 ≤ f →
    ∀ {hfm : Measurable f} [inst_6 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (n : ℕ),
      0 ≤ MeasureTheory.SimpleFunc.approxOn f hfm (Set.range f ∪ {0}) 0 ⋯ n
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H}
  {x : H}, MDiffAt[s] ↑I x
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (a b : R),
  PowerSeries.rescale (a * b) = (PowerSeries.rescale b).comp (PowerSeries.rescale a)
-- Mathlib.Combinatorics.Additive.SubsetSum
_private.Mathlib.Combinatorics.Additive.SubsetSum.0.Finset.subsetSum.eq_1 : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] (A : Finset M),
  A.subsetSum = Finset.image (fun B => B.sum id) A.powerset
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : MeasureTheory.Measure α} (c c' : ENNReal),
  c ≠ ⊤ →
    c' ≠ ⊤ →
      μ ≤ c • μ' →
        μ' ≤ c' • μ →
          ∀ (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C')
            (f : α → E), MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Rio α → Std.DTreeMap.Internal.Unit.RioSliceData α
-- Mathlib.Algebra.Order.AddTorsor
instContravariantClassHSMulLeOfIsOrderedCancelSMul : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : LE P] [inst_2 : SMul G P] [IsOrderedCancelSMul G P],
  ContravariantClass G P (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsBase.mem_of_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsBase B → M.IsColoop e → e ∈ B
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion : ∀ {X Y S X' Y' S' : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X')
  (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  [AlgebraicGeometry.IsOpenImmersion i₁] [AlgebraicGeometry.IsOpenImmersion i₂] [CategoryTheory.Mono i₃],
  AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_lt_of_dist_lt_modulus : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f : C(α, β)) (ε : ℝ) (h : 0 < ε) {a b : α}, dist a b < f.modulus ε h → dist (f a) (f b) < ε
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.hom_ext : ∀ {X Y : TwoP} {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Batteries.Lean.EStateM
/-- Map a function over an `EStateM.Result`, preserving states and errors.  -/
EStateM.Result.map : {ε σ α β : Type u_1} → (α → β) → EStateM.Result ε σ α → EStateM.Result ε σ β
-- Mathlib.Algebra.Category.ModuleCat.Semi
LinearMap.comp_id_semiModuleCat : ∀ {R : Type u_1} [inst : Semiring R] {G : SemimoduleCat R} {H : Type u} [inst_1 : AddCommMonoid H] [inst_2 : Module R H]
  (f : ↑G →ₗ[R] H), f ∘ₗ SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.id G) = f
-- Mathlib.Logic.Small.Set
small_powerset : ∀ {α : Type u1} (s : Set α) [Small.{u, u1} ↑s], Small.{u, u1} ↑(𝒫 s)
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.GeometricallyReduced.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced f → AlgebraicGeometry.GeometricallyReduced f
-- Mathlib.Topology.DiscreteSubset
IsClosed.tendsto_coe_cofinite_of_isDiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsClosed s → IsDiscrete s → Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.rTensorBot_tmul_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (a : ↥A), A.rTensorBot (a ⊗ₜ[R] 1) = a
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιInv.eq_1 : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ExteriorAlgebra.ιInv = TrivSqZeroExt.sndHom R M ∘ₗ ExteriorAlgebra.toTrivSqZeroExt.toLinearMap
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → t.minKey?.isSome = true
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceDefault : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.of.congr_simp : ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Module.Finite R S] [inst_4 : Algebra.Etale R S],
  CommAlgCat.FiniteEtale.of R S = CommAlgCat.FiniteEtale.of R S
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instFaithfulPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y), (CategoryTheory.Subobject.pullback f).Faithful
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_eq_eraseManyEntries! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h : t₁.Balanced),
  ↑(t₁.eraseManyEntries t₂ h) = ↑(t₁.eraseManyEntries! t₂)
-- Mathlib.Order.Filter.Lift
Filter.monotone_lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder γ] {f : γ → Filter α} {g : γ → Set α → Filter β},
  Monotone f → Monotone g → Monotone fun c => (f c).lift (g c)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.inter m₂).get? k = m₁.get? k
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is an infinite basis for a module `M`,
then every maximal linearly independent set has the same cardinality as `b`.

This proof (along with some of the lemmas above) comes from
[Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]
 -/
maximal_linearIndependent_eq_infinite_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} (b : Module.Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v),
  i.Maximal → Cardinal.mk κ = Cardinal.mk ι
-- Mathlib.Data.Set.Image
Set.image_compl_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Bijective f → f '' sᶜ = (f '' s)ᶜ