mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The morphism `numeratorHom` is a monoid localization map in the case of commutative `R`.  -/
OreLocalization.localizationMap : (R : Type u_1) → [inst : CommMonoid R] → (S : Submonoid R) → S.LocalizationMap (OreLocalization S R)
-- Mathlib.RingTheory.Perfection
PerfectionMap.lift_apply : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p]
  [inst_3 : PerfectRing R p] (S : Type u₂) [inst_4 : CommSemiring S] [inst_5 : CharP S p] (P : Type u₃)
  [inst_6 : CommSemiring P] [inst_7 : CharP P p] [inst_8 : PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π)
  (f : R →+* S), (PerfectionMap.lift p R S P π m) f = (↑m.equiv.symm).comp ((Perfection.lift p R S) f)
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk_d_2_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁
-- Mathlib.Algebra.Lie.Basis.Basic
_private.Mathlib.Algebra.Lie.Basis.Basic.0.LieAlgebra.Basis.cartan_lie_mem_lieSpan_e : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) {x y : L},
  x ∈ H → y ∈ LieSubalgebra.lieSpan R L (Set.range b.e) → ⁅x, y⁆ ∈ LieSubalgebra.lieSpan R L (Set.range b.e)
-- Std.Do.SPred.DerivedLaws
ULift.down_ite : ∀ {α : Type u_1} {φ : Prop} [inst : Decidable φ] (t e : α),
  (if φ then { down := t } else { down := e }).down = if φ then t else e
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- A vector in `(𝕜 ∙ u)ᗮ` is orthogonal to `u`.  -/
Submodule.mem_orthogonal_singleton_iff_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {u v : E}, v ∈ (𝕜 ∙ u)ᗮ ↔ inner 𝕜 v u = 0
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.instFibrationSndOfIsFibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange]
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct X Y] [hX : HomotopicalAlgebra.IsFibrant X],
  HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.snd
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.max_bi.congr_simp : ∀ {α : Type u_1} [inst : Finite α] [inst_1 : Nonempty α] (b b_1 : α → ℝ),
  b = b_1 → AkraBazziRecurrence.max_bi b = AkraBazziRecurrence.max_bi b_1
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.coeStream : {α : Type u} → Coe (Stream' α) (Stream'.WSeq α)
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation.X_inv`. -/
FunctionField.inftyValuation.X_inv : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)],
  (RatFunc.inftyValuation F) (1 / RatFunc.X) = WithZero.exp (-1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.empty.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty = Std.DTreeMap.Internal.Impl.leaf
-- Init.Data.BitVec.Bitblast
BitVec.msb_add : ∀ {w : ℕ} {x y : BitVec w}, (x + y).msb = (x.msb ^^ (y.msb ^^ BitVec.carry (w - 1) x y false))
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_inf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A} {x : A},
  x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancel : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly
-- Mathlib.Algebra.Group.Nat.TypeTags
Nat.ofAdd_mul : ∀ (a b : ℕ), Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.iSup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Sort u_5} [Countable ι] {f : ι → δ → α}, (∀ (i : ι), Measurable (f i)) → Measurable fun b => ⨆ i, f i b
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_copy : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Core
Std.LawfulLeftIdentity.toLeftIdentity : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → β} {o : outParam α} [self : Std.LawfulLeftIdentity op o],
  Std.LeftIdentity op o
-- Init.Data.Int.Order
Int.le_antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.single_mapDomainOfBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) (g : G) (r : R),
  AddMonoidAlgebra.single ((AddMonoidAlgebra.mapDomainOfBialgHom f) g) r = f (AddMonoidAlgebra.single g r)
-- Mathlib.Algebra.Group.WithOne.Basic
/-- `WithZero.coe` as a bundled morphism  -/
WithZero.coeAddHom : {α : Type u} → [inst : Add α] → α →ₙ+ WithZero α
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) ⁻¹' Set.uIcc b c = Set.uIcc (b + a) (c + a)
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
 -/
Std.Iter.Partial.toList : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter.Partial β → List β
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDFReal_def : ∀ (x₀ : ℝ) (γ : NNReal) (x : ℝ), ProbabilityTheory.cauchyPDFReal x₀ γ x = Real.pi⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹
-- Mathlib.Order.WithBot
WithTop.exists_ne_top : ∀ {α : Type u_1} {p : WithTop α → Prop}, (∃ x, x ≠ ⊤ ∧ p x) ↔ ∃ x, p ↑x
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.Red.reduce_left : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
-- Mathlib.Order.Rel.GaloisConnection
/-- The pair of functions `toDual ∘ leftDual` and `rightDual ∘ ofDual` forms a Galois connection.  -/
SetRel.gc_leftDual_rightDual : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β),
  GaloisConnection (⇑OrderDual.toDual ∘ R.leftDual) (R.rightDual ∘ ⇑OrderDual.ofDual)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.USize.toBitVec_ite : ∀ {c : Prop} {t e : USize} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.RingTheory.SimpleModule.Basic
RingEquiv.isSemisimpleRing : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S) [IsSemisimpleRing R], IsSemisimpleRing S
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.mulActionHom_embedding.congr_simp : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f f_1 : α →ₑ[σ] β} (e_f : f = f_1) (ι : Type u_5)
  (hf : Function.Injective ⇑f),
  Function.Injective.mulActionHom_embedding ι hf = Function.Injective.mulActionHom_embedding ι ⋯
-- Mathlib.Order.Interval.Set.OrdConnected
IsAntichain.ordConnected : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α}, IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.OrdConnected
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation on `ℂ_[p]` has rank one.  -/
PadicComplex.instRankOneNNRealV : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Valued.v.RankOne
-- Std.Sat.AIG.CNF
/-- A cache so that we don't generate CNF for an AIG node more than once.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.cache : {aig : Std.Sat.AIG ℕ} →
  (self : Std.Sat.AIG.toCNF.State✝ aig) → Std.Sat.AIG.toCNF.Cache✝ aig (Std.Sat.AIG.toCNF.State.cnf✝ self)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts**. For improper integrals, see
`MeasureTheory.integral_mul_deriv_eq_deriv_mul`,
`MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul`,
and `MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul`.  -/
intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Counting.0.SimpleGraph.finsetWalkLength.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.conj_conj : ∀ (z : Complex.UnitDisc), star (star z) = z
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.interSmaller : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.union_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF), m₂.Equiv m₃ → (m₁.union m₂ ⋯ ⋯).Equiv (m₁.union m₃ ⋯ ⋯)
-- Init.Data.Order.Ord
Nat.instLawfulEqOrd : Std.LawfulEqOrd ℕ
-- Mathlib.Algebra.Homology.Factorizations.Basic
/-- A morphism of cochain complexes `φ` in an abelian category satisfies
`degreewiseEpiWithInjectiveKernel φ` if for any `i : ℤ`, the morphism
`φ.f i` is an epimorphism with an injective kernel.  -/
CochainComplex.degreewiseEpiWithInjectiveKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.MorphismProperty (CochainComplex C ℤ)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_disjiUnion : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι)
  (h : (↑s).PairwiseDisjoint t), ∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x
-- Mathlib.Analysis.MeanInequalitiesPow
NNReal.add_rpow_le_rpow_add : ∀ {p : ℝ} (a b : NNReal), 1 ≤ p → a ^ p + b ^ p ≤ (a + b) ^ p
-- Mathlib.Tactic.NoncommRing
/-- `noncomm_ring` simplifies expressions in not-necessarily-commutative rings in the main goal
then tries closing it by "cheap" (reducible) `rfl`.
This tactic supports the operators `+`, `*`, `-`, `^` and `•` (for scalar multiplication by
natural numbers or integers).

If the ring is commutative, prefer the `ring` tactic instead, which is more powerful and efficient.
The tactic is implemented as a combination of `simp only [...]` and `abel`. The precise invocation
of `simp only` can be customized using the options listed below.

Limitation: numeric powers are unfolded entirely with `pow_succ` and can easily exceed the
maximum recursion depth.

* `noncomm_ring [h]` adds the term `h` as simplification lemma, rewriting from left to right.
  Multiple arguments can be combined as `noncomm_ring [h₁, ..., hₙ]`.
* `noncomm_ring [← h]` adds the term `h` as simplification lemma, rewriting from right to left.
* `noncomm_ring [*]` simplifies using all hypotheses in the local context.
* `noncomm_ring (config := cfg)` uses `cfg` as configuration for the simplification step.
  See `Lean.Meta.Simp.Config` for more details.
* `noncomm_ring (discharger := tac)` uses the tactic sequence `tac` to discharge assumptions
  to the simplification lemmas. This only applies to user-supplied lemmas, since the default lemmas
  used by `noncomm_ring` do not require a discharger.

Example:
```lean
example {R : Type*} [Ring R] (a b c : R) : a * (b + c + c - b) = 2 * a * c := by
  noncomm_ring
```
 -/
Mathlib.Tactic.NoncommRing.noncomm_ring : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Bimon C} (f : X ⟶ Y),
  ((CategoryTheory.Bimon.toMonComon C).map f).hom = (CategoryTheory.Bimon.toComon C).map f
-- Mathlib.Data.PNat.Xgcd
/-- Properties of division with remainder for a / b.  -/
PNat.XgcdType.rq_eq : ∀ (u : PNat.XgcdType), u.r + (u.bp + 1) * u.q = u.ap + 1
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.trans : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {Γ''₀ : Type u_6}
  [inst_3 : LinearOrderedAddCommMonoidWithTop Γ''₀] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀}
  {v₃ : AddValuation R Γ''₀}, v₁.IsEquiv v₂ → v₂.IsEquiv v₃ → v₁.IsEquiv v₃
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Galois insertion between `adjoin` and `SetLike.coe`.  -/
NonUnitalAlgebra.gi : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] → GaloisInsertion (NonUnitalAlgebra.adjoin R) SetLike.coe
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_eq_top_of_countable : ∀ {α : Type u_6} [inst : TopologicalSpace α] [T0Space α] [Countable α], borel α = ⊤
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.functorOp_map : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat}
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {X Y : Iᵒᵖ} (f : X ⟶ Y),
  (Profinite.Extend.functorOp c).map f = CategoryTheory.CostructuredArrow.homMk (F.map f.unop).op ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an `AddGroup` inherits an integer scaling.  -/
AddSubgroupClass.instZSMul : {M : Type u_5} →
  {S : Type u_6} → [inst : SubNegMonoid M] → [inst_1 : SetLike S M] → [AddSubgroupClass S M] → {H : S} → SMul ℤ ↥H
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.refl_toAdjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Equivalence.refl.toAdjunction = CategoryTheory.Adjunction.id
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.mk.inj : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  {map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map = f.map)
      SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam}
  {δ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map = g.map)
      SSet.PtSimplex.RelStruct.δ_succ_map._autoParam}
  {δ_map_of_lt :
    autoParam (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)), i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam}
  {map_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map_1 = f.map)
      SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam}
  {δ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map_1 = g.map)
      SSet.PtSimplex.RelStruct.δ_succ_map._autoParam}
  {δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)), i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam},
  { map := map, δ_castSucc_map := δ_castSucc_map, δ_succ_map := δ_succ_map, δ_map_of_lt := δ_map_of_lt,
        δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_map := δ_castSucc_map_1, δ_succ_map := δ_succ_map_1, δ_map_of_lt := δ_map_of_lt_1,
        δ_map_of_gt := δ_map_of_gt_1 } →
    map = map_1
-- Mathlib.Data.ZMod.Basic
ZModModule.sub_eq_add : ∀ {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod 2) G] (x y : G), x - y = x + y
-- Mathlib.Topology.Algebra.Order.UpperLower
IsLowerSet.interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsLowerSet s → IsLowerSet (interior s)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂)
  (i : I₁) (i_1 : I₂),
  (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).hom.app X).f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((X.X i).X i_1)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_lt_nnnorm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] (r : NNReal), ∃ x, r < ‖x‖₊
-- Aesop.Builder.Tactic
Aesop.RuleBuilder.tacticCore : Lean.Name ⊕ Lean.TSyntax `Lean.Parser.Tactic.tacticSeq →
  Option Aesop.IndexingMode → Aesop.PhaseSpec → Lean.MetaM Aesop.LocalRuleSetMember
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.intCast n => h_2 n
    | Lean.Grind.CommRing.Expr.natCast n => h_3 n
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | x => h_5 x) =
    h_4 x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.equivOplax_symm_apply : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ),
  CategoryTheory.Oplax.StrongTrans.Modification.equivOplax.symm Γ = Γ.toOplax
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.of_subsingleton : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [Subsingleton ι] {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.Kernel.iIndepFun f κ μ
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.subst.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    {β : Type u_4} →
      (motive : L.Term α → (α → L.Term β) → Sort u_5) →
        (x : L.Term α) →
          (x_1 : α → L.Term β) →
            ((a : α) → (tf : α → L.Term β) → motive (FirstOrder.Language.var a) tf) →
              ((l : ℕ) →
                  (f : L.Functions l) →
                    (ts : Fin l → L.Term α) → (tf : α → L.Term β) → motive (FirstOrder.Language.func f ts) tf) →
                motive x x_1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.mk.inj : ∀ {waiters : Array Lean.Meta.SynthInstance.Waiter} {answers : Array Lean.Meta.SynthInstance.Answer}
  {waiters_1 : Array Lean.Meta.SynthInstance.Waiter} {answers_1 : Array Lean.Meta.SynthInstance.Answer},
  { waiters := waiters, answers := answers } = { waiters := waiters_1, answers := answers_1 } →
    waiters = waiters_1 ∧ answers = answers_1
-- Init.Data.BitVec.Lemmas
BitVec.msb_allOnes : ∀ {w : ℕ}, 0 < w → (BitVec.allOnes w).msb = true
-- Mathlib.Topology.Algebra.UniformFilterBasis
/-- The uniform space structure associated to an abelian group filter basis via the associated
topological abelian group structure is compatible with its group structure.  -/
AddGroupFilterBasis.isUniformAddGroup : ∀ {G : Type u_1} [inst : AddCommGroup G] (B : AddGroupFilterBasis G), IsUniformAddGroup G
-- Init.System.IO
/-- A reference to an opened file.

File handles wrap the underlying operating system's file descriptors. There is no explicit operation
to close a file: when the last reference to a file handle is dropped, the file is closed
automatically.

Handles have an associated read/write cursor that determines where reads and writes occur in the
file.
 -/
IO.FS.Handle : Type
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The multiplicative homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the
fraction `r /ₒ 1`.  -/
OreLocalization.numeratorHom : {R : Type u_1} → [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → R →* OreLocalization S R
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.X₂ = (Y ⊞ Z)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π, with a "cospherical or collinear" conclusion.  -/
EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq : ∀ {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},
  2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
    EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}