mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (ForgetEnrichment.homTo W (f ≫ g) ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝)) =
    ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
      ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
apply_fun ForgetEnrichment.homTo W

Goal state after:
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W (f ≫ g) ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)))

case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Function.Injective (ForgetEnrichment.homTo W)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ homMk e₀₁ ≫ homMk e₁₂ = homMk e₀₂

Tactic:
simpa [homMk] using! CategoryTheory.Quotient.sound _
    (OneTruncation₂.HoRel₂.of_compStruct h)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ morphismPropertyHomMk V = (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V)

Tactic:
ext _ _ f

Goal state after:
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ morphismPropertyHomMk V f ↔ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicL f g
⊢ HomotopicL g f

Tactic:
rcases hfg with ⟨hfg⟩
  exact Quasicategory₂.fill31 hfg (idComp (id y)) (compId f)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
⊢ x✝ = ⋯ ▸ ⋯ ▸ 𝟙rq default

Tactic:
by
    let : Subsingleton (((truncation 2).obj Δ[0]).obj (.op ⦋1⦌2)) :=
      inferInstanceAs (Subsingleton (ULift.{_, 0} (⦋1⦌ ⟶ ⦋0⦌)))
    ext
    exact this.allEq _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ ∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h

Tactic:
use rfl

Goal state after:
case h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ 𝟙 x✝ = eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
Fin.castSucc_lt_iff_succ_le

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
⊢ W = ⊤

Tactic:
ext a b f

Goal state after:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f ↔ ⊤ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
⊢ ∃ a, toMk₁ a = f

Tactic:
· refine ⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
    dsimp [toMk₁_apply]
    rw [if_pos (by simp)]
    obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩
    fin_cases j
    · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/
      simp_all
    · exact (hS ⟨i, by simpa [S]⟩).elim

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ i.predAbove j < x

Tactic:
rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl]
    exact s.val.notMem

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y z : X.N
h : x ≤ y
h' : y ≤ z
⊢ monoOfLE h ≫ monoOfLE h' = monoOfLE ⋯

Tactic:
by
  symm
  simp [monoOfLE_eq_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Subcomplex.range f = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
rw [range_eq_iSup_of_isColimit (coproductIsCoproduct X) f]

Goal state after:
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ c.horn.image c.map < (↑(P.p c.s)).subcomplex

Tactic:
lt_iff_le_and_ne

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ c.horn.image c.map ≤ (↑(P.p c.s)).subcomplex ∧ c.horn.image c.map ≠ (↑(P.p c.s)).subcomplex
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
k k' : K
φ : k ⟶ k'
⊢ (ConcreteCategory.hom ((F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).map φ))
      ((fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k)) k) =
    (fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k)) k'

Tactic:
by
        dsimp
        rw [NatTrans.naturality_apply, ← hα φ]

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.obj
f : (𝟭 C).obj (h.objEquiv x) ⟶ (𝟭 C).obj (h.objEquiv y)
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := h.objEquiv y, hom := f }

Tactic:
obtain ⟨f, rfl⟩ := h.homEquiv.surjective f

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.obj
f : ↑(h.hom x y)
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := h.objEquiv y, hom := h.homEquiv f }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ c.ιSigmaStdSimplex ≫ f.b j = c.mapToSucc

Tactic:
by
  simp [b]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
hy :
  ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)) ∈
    (f.filtration j).obj (op ⦋d⦌)
⊢ b ∈ ((f.filtration j).preimage x.map).obj (op ⦋d⦌)

Tactic:
rwa [x.ι_b_app_apply] at hy

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case inst
X : SSet
inst✝ : X.Finite
⊢ ∀ (k : Discrete X.N), IsCardinalPresentable ((Discrete.functor fun s ↦ Δ[s.dim]).obj k) Cardinal.aleph0

Tactic:
· rintro s
      dsimp
      infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ strongAnodyneExtensions (f ≫ e)

Tactic:
refine ⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance⟩

Goal state after:
X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.castSucc < (x.cast hd).simplex.1 i
⊢ min x hd ≤ i

Tactic:
Fin.castSucc_lt_iff_succ_le

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.succ ≤ (x.cast hd).simplex.1 i
⊢ min x hd ≤ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
i : Fin (d + 1)
hi : (x.cast hd).simplex.2 (l.castSucc.succAbove i) = j
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

Tactic:
· exact ⟨_, hi⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
i : Fin (d + 1)
hi : (x.cast hd).simplex.1 (l.castSucc.succAbove i) = j
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j

Tactic:
· exact ⟨_, hi⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi : i.castSucc < min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ

Tactic:
Fin.castSucc_lt_iff_succ_le

Goal state after:
case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi : i.succ ≤ min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
s : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hds : s.dim = d + 1
is : Fin (d + 1)
hs : IsIndex s hds is.succ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
h₁ :
  { x := s, d := d, hd := hds, index := is, isIndex := hs } ≠ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := s, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₃ :
  (pairingCore k n).dim { x := s, d := d, hd := hds, index := is, isIndex := hs } =
    (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (finset { x := s, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card

Tactic:
obtain ⟨ds, s, hs₁, hs₂, rfl⟩ := Subcomplex.N.mk_surjective s

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is : Fin (d + 1)
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hdt : t.dim = d' + 1
it : Fin (d' + 1)
ht : IsIndex t hdt it.succ
ds : ℕ
s : (Δ[m + 1] ⊗ Δ[n]) _⦋ds⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate ds
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋ds⦌)
hds : (Subcomplex.N.mk s hs₁ hs₂).dim = d + 1
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) hds is.succ
h₁ :
  { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs } ≠
    { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := t, d := d', hd := hdt, index := it, isIndex := ht }
h₃ :
  (pairingCore k n).dim { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs } =
    (pairingCore k n).dim { x := t, d := d', hd := hdt, index := it, isIndex := ht }
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := hds, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := t, d := d', hd := hdt, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case hᵣ
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ sq₁₂.inr ≫
      (𝟭 C₃).map
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₂
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ ((𝟭 C₂).map ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.snd

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case refine_2.inr
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
this : (orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯) (Fin.last (p + 1)) = OrderHom.id (Fin.last (p + 1))
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ (Fin.last (p + 1)).succ), hs✝⟩

Tactic:
simp only [Fin.succ_last, orderHomOfSimplex_coe,
          OrderHom.id_coe, id_eq, Fin.ext_iff, Fin.val_last,
          stdSimplex.objMk₁_of_castSucc_lt (Fin.last (p + 2))
            (Fin.last (p + 1)) (by simp),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] at this

Goal state after:
case refine_2.inr
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
this : ↑(s₁ (Fin.last (p + 1))) = p + 1
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ (Fin.last (p + 1)).succ), hs✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.castSucc < j
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
Fin.castSucc_lt_iff_succ_le

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
⊢ stdSimplex.δ j ≫ h.map = const x
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos.inr.inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : w b ≠ 1
⊢ v b ^ ((log (v b))⁻¹ * log (w b)) = w b

Tactic:
rpow_mul (v.nonneg _),

Goal state after:
case pos.inr.inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : w b ≠ 1
⊢ (v b ^ (log (v b))⁻¹) ^ log (w b) = w b
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = f x
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0

Tactic:
filter_upwards [hUo.mem_nhds hUx] with y hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = f x
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
y : 𝕜
hy : y ∈ U
⊢ deriv f y = 0
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ Surjective f

Tactic:
apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 0) _
    have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
    let p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ Set.range f
    have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) := by
      have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
      refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
      refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
      exact subset_univ _
    refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_
    exact fun R h y hy => h hy

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

Tactic:
by_cases h₂f : Function.HasFiniteMulSupport F
  · simpa [finprod_eq_prod F h₂f] using prod (by aesop)
  · exact finprod_of_not_hasFiniteMulSupport h₂f ▸ const (1 : 𝕜') x

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r

Tactic:
smeval_ascPochhammer_int_ofNat r n

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
h₁ : sᶜ.Countable
h₁' : Countable ↑sᶜ
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h₃ : ContinuousOn f s
⊢ Measurable f

Tactic:
exact .of_union_range_cover (.subtype_coe h₂.measurableSet) (.subtype_coe h₁.measurableSet)
    (by simp [-mem_compl_iff]) h₃.domRestrict.measurable (measurable_of_countable _)

Goal state after: