mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ (X.fst ⊗ Y.fst) ◁ f ≫
      (α_ X.fst Y.fst U' ≪≫
          X.fst ◁ᵢ Y.snd.β U' ≪≫ (α_ X.fst U' Y.fst).symm ≪≫ X.snd.β U' ▷ᵢ Y.fst ≪≫ α_ U' X.fst Y.fst).hom =
    (α_ X.fst Y.fst U ≪≫ X.fst ◁ᵢ Y.snd.β U ≪≫ (α_ X.fst U Y.fst).symm ≪≫ X.snd.β U ▷ᵢ Y.fst ≪≫ α_ U X.fst Y.fst).hom ≫
      f ▷ (X.fst ⊗ Y.fst)

Tactic:
dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
        calc
          _ = 𝟙 _ ⊗≫
            (X.1 ◁ (Y.1 ◁ f ≫ (HalfBraiding.β Y.2 U').hom)) ⊗≫
              (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by monoidal
          _ = 𝟙 _ ⊗≫
            X.1 ◁ (HalfBraiding.β Y.2 U).hom ⊗≫
              (X.1 ◁ f ≫ (HalfBraiding.β X.2 U').hom) ▷ Y.1 ⊗≫ 𝟙 _ := by
            rw [HalfBraiding.naturality]; monoidal
          _ = _ := by rw [HalfBraiding.naturality]; monoidal

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

Goal state before:
pp: case mpr
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m → (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m

Tactic:
rintro ⟨⟨x₁, rfl⟩, ⟨x₂, rfl⟩⟩
    exact ⟨⟨x₁, x₂⟩, rfl⟩

Goal state after:
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✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
f : X ⟶[Type v] Y
g : Y ⟶[Type v] Z
⊢ (ConcreteCategory.hom (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f)).toFun (f, g) =
    (ConcreteCategory.hom
          (((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z))).toFun
      (f, g)

Tactic:
exact F.map_comp f g

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (β_ Y X).inv = T.unionProd S

Tactic:
apply image_β_hom

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc ⟨i, hi⟩).op))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) x

Tactic:
spineToSimplex_arrow

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ Path.arrow
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ⟨i, hi⟩ =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k

Goal state after:
case succ.comp_of.inr.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

case succ.comp_of.inr.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯ =
    mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯

Tactic:
ext y
      obtain ⟨y, rfl⟩ := mk_surjective y
      simpa using homMk_comp_homMk (h.tensor (.idCompId y))

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ IsLUB x✝ (sSup x✝)

Tactic:
constructor
    · intro K hK _ ht
      exact Or.inl (Set.mem_biUnion hK ht)
    · intro L hL _ ht
      cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v

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

Goal state before:
pp: m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
x : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)
⊢ (Hom.toOrderHom (Quiver.Hom.unop (op (Hom.mk { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ })))) x =
    (Hom.toOrderHom
        (op (Hom.mk { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ }) ≫
            op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ })).unop)
      x

Tactic:
exact (II.map'_map' _ _ _).symm

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

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : x ∉ (Δ[p] ⊗ Δ[q]).degenerate n
⊢ False

Tactic:
rw [← mem_nonDegenerate_iff_notMem_degenerate,
      nonDegenerate_iff_strictMono_objEquiv,
      ← strictMono_orderHomOfSimplex_iff _ rfl] at hx

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : StrictMono ⇑(orderHomOfSimplex x ⋯)
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
y : ↑h.pairing.II
x : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) y
⊢ f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ (↑x).dim = (↑y).dim → f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x

Goal state after:
X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
y : ↑h.pairing.II
x : h.ι
hxy : h.pairing.AncestralRel (h.equivII x) y
⊢ (↑(h.equivII x)).dim = (↑y).dim → f.rank (h.equivII.symm (h.equivII x)) < f.rank (h.equivII.symm y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ (↑x).IsUniquelyCodimOneFace (↑(h.pairing.p x)).toS

Tactic:
by
    obtain ⟨s, rfl⟩ := h.equivII.surjective x
    simpa using h.isUniquelyCodimOneFace s

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ (↑↑t₁).toS = (↑↑t₂).toS

Tactic:
← hφ,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ψ (φ t₁) = (↑↑t₂).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ψ (φ t₁) = (↑↑t₂).toS

Tactic:
← hφ,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ ψ (φ t₁) = ψ (φ t₂)
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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i = ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
apply le_antisymm
  · conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff]
    refine ⟨?_, fun j hj c ↦ ?_⟩
    · refine le_trans ?_ (le_iSup _ ⊥)
      exact le_trans (by simp) (le_iSup _ hi.bot_lt)
    · refine le_trans ?_ (le_iSup _ (Order.succ j))
      refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))
      exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)
  · simp only [iSup_le_iff]
    intro j hj
    exact f.filtration_monotone hj.le

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i ≤ f.filtration m

Tactic:
simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ∀ a < m, f.filtration a ≤ f.filtration m
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι := { app := fun g ↦ ((ConcreteCategory.hom (f.app (op g.left))) { down := g.hom }).down, naturality := ⋯ } }
X : C
x : (yoneda.obj Y).obj (F.op.obj (op X))
this :
  ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app (CostructuredArrow.mk x) ≫ (F.denseAt Y).desc c =
    c.ι.app (CostructuredArrow.mk x)
⊢ (ConcreteCategory.hom (((restrictedULiftYoneda F).map ((F.denseAt Y).desc c)).app (op X))).toFun { down := x } =
    (ConcreteCategory.hom (f.app (op X))).toFun { down := x }

Tactic:
dsimp [c] at this

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
  { pt := Z,
    ι := { app := fun g ↦ ((ConcreteCategory.hom (f.app (op g.left))) { down := g.hom }).down, naturality := ⋯ } }
X : C
x : (yoneda.obj Y).obj (F.op.obj (op X))
this :
  (𝟙 (F.obj X) ≫ x) ≫
      (F.denseAt Y).desc
        { pt := Z,
          ι :=
            { app := fun g ↦ ((ConcreteCategory.hom (f.app (op g.left))) { down := g.hom }).down, naturality := ⋯ } } =
    ((ConcreteCategory.hom (f.app (op X))) { down := x }).down
⊢ (ConcreteCategory.hom (((restrictedULiftYoneda F).map ((F.denseAt Y).desc c)).app (op X))).toFun { down := x } =
    (ConcreteCategory.hom (f.app (op X))).toFun { down := x }
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
this :
  Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X

Tactic:
have : IsIso (colimit.desc _ (E.coconeAt X)) := hS₁.isIso_of_mono _ (fun Y hY g ↦ by
      let γ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X :=
        CostructuredArrow.mk (Y := ⟨Y, P.le_colimitsCardinalClosure  _ _ hY⟩) (by exact g)
      exact ⟨colimit.ι (CostructuredArrow.proj _ _ ⋙ (P.colimitsCardinalClosure κ).ι) γ,
        by simp [γ, E]⟩)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
this✝ :
  Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
this :
  IsIso
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X
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 t : Type₁ k n
h : s.δ = t.δ
⊢ s = t

Tactic:
generalize hs : s.δ = u

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h : s.δ = t.δ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hs : s.δ = u
⊢ s = t
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.succ
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1)
hx : IsIndex x ⋯ i.succ
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
refine ⟨{ x := x, d := d, hd := hd, index := i, isIndex := hx }, Or.inl ?_⟩

Goal state after:
case neg.succ
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1)
hx : IsIndex x ⋯ i.succ
⊢ x.toS =
    { dim := { x := x, d := d, hd := hd, index := i, isIndex := hx }.d + 1,
      simplex := ({ x := x, d := d, hd := hd, index := i, isIndex := hx }.x.cast ⋯).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
⊢ IsIso ((X.homology₀Iso R).hom ≫ Sigma.desc fun x ↦ 𝟙 R)

Tactic:
simp only [isIso_comp_left_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
⊢ IsIso (Sigma.desc fun x ↦ 𝟙 R)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
⊢ x.subcomplex ⊓ y.subcomplex ≤
    Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)

Tactic:
Subcomplex.le_iff_contains_nonDegenerate

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
⊢ ∀ (n : ℕ) (x_1 : ↑(X.nonDegenerate n)),
    ↑x_1 ∈ (x.subcomplex ⊓ y.subcomplex).obj (op ⦋n⦌) →
      ↑x_1 ∈ (Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)).obj (op ⦋n⦌)
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
n : ℕ
x : ↑s
⊢ (fun x ↦ ⟨(c ^ n)⁻¹ • ↑x, ⋯⟩) ((fun x ↦ ⟨c ^ n • ↑x, ⋯⟩) x) = x

Tactic:
simp [smul_smul, inv_mul_cancel₀ (cn_ne n)]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
⊢ #↑s = #E

Tactic:
by
  /- As `s` is a neighborhood of `0`, the space is covered by the rescaled sets `c^n • s`,
  where `c` is any element of `𝕜` with norm `> 1`. All these sets are in bijection and have
  therefore the same cardinality. The conclusion follows. -/
  obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1
  have cn_ne : ∀ n, c ^ n ≠ 0 := by
    intro n
    apply pow_ne_zero
    rintro rfl
    simp only [norm_zero] at hc
    exact lt_irrefl _ (hc.trans zero_lt_one)
  have A : ∀ (x : E), ∀ᶠ n in (atTop : Filter ℕ), x ∈ c ^ n • s := by
    intro x
    have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) := by
      have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc
      exact Tendsto.smul_const this x
    rw [zero_smul] at this
    filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
    exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn
  have B : ∀ n, #(c ^ n • s :) = #s := by
    intro n
    have : (c ^ n • s :) ≃ s :=
    { toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
      invFun := fun x ↦ ⟨(c^n) • x.1, smul_mem_smul_set x.2⟩
      left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel₀ (cn_ne n)]
      right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel₀ (cn_ne n)] }
    exact Cardinal.mk_congr this
  apply (Cardinal.mk_of_countable_eventually_mem A B).symm

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
rw [← this] at hg

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hg : AnalyticAt 𝕜 (g ∘ f) (r (f x))
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
⊢ False

Tactic:
let ⟨q, ⟨hq₁, hq₂⟩⟩ := exists_rat_btwn h_lt

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q
hq₂ : ↑q < log (w b) / log (w a)
⊢ False