mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ c.multispanIndex.left (i₁, i₂)

Tactic:
dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ Function.LeftInverse (Quot.lift (Quot.mk (Rel f g)) ⋯) (Quot.lift (Quot.mk (Rel' f g)) ⋯)

Tactic:
rintro ⟨x⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ Function.RightInverse (Quot.lift (Quot.mk (Rel f g)) ⋯) (Quot.lift (Quot.mk (Rel' f g)) ⋯)

Tactic:
rintro ⟨x⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨ ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄

Tactic:
obtain ⟨j, x, rfl⟩ := jointly_surjective_of_isColimit h.isColimit x₄
  obtain (_ | _ | _) := j
  · exact Or.inl ⟨t x, by simp; rfl⟩
  · exact Or.inl ⟨x, rfl⟩
  · exact Or.inr ⟨x, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
inst✝ : X.Quasicategory
⊢ InnerFibration (terminal.from X)

Tactic:
by
  rwa [← quasicategory_iff_innerFibration]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
⊢ IsPushout t l r b

Tactic:
by
  obtain ⟨φ, hφ₁, hφ₂⟩ := pushout.exists_desc t l r b
    (by simp only [← cancel_mono k, Category.assoc, facr, facb, h₁.w])
  have := mono_of_isPushout_of_isPullback (IsPushout.of_hasPushout t l) h₁
    (k := φ ≫ k) (by cat_disch) (by cat_disch) H
  have : IsIso φ := by
    rw [isIso_iff_bijective]
    refine ⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩
    have hx₄ := Set.mem_univ x₄
    simp only [← h₂, Set.sup_eq_union, Set.mem_union, Set.mem_range] at hx₄
    obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl⟩) := hx₄
    · exact ⟨_, ConcreteCategory.congr_hom hφ₁ x₂⟩
    · exact ⟨_, ConcreteCategory.congr_hom hφ₂ x₃⟩
  exact IsPushout.of_iso (IsPushout.of_hasPushout t l)
    (Iso.refl _) (Iso.refl _) (Iso.refl _) (asIso φ) (by simp) (by simp)
    (by simpa) (by simpa)

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
⊢ ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ X),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
intro n i σ₀ h₀ hₙ

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∃ σ,
    ∀ (j : Fin (n + 3)) (h : j ≠ i),
      (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
        (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ ∀ (X : ↑chosenTerminal),
    ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X = x✝.obj X

Tactic:
· intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f g : X ⟶ Y
w : f.f = g.f
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
g : X ⟶ Y
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝, comm := comm✝ }.f = g.f
⊢ { f := f✝, comm := comm✝ } = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: K : SSet
φ : 𝟙_ SSet ⟶ K
Δ : SimplexCategoryᵒᵖ
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op))
      ((ConcreteCategory.hom (φ.app (Opposite.op ⦋0⦌))) PUnit.unit) =
    (ConcreteCategory.hom (φ.app Δ)) PUnit.unit

Tactic:
rw [← NatTrans.naturality_apply]

Goal state after:
K : SSet
φ : 𝟙_ SSet ⟶ K
Δ : SimplexCategoryᵒᵖ
⊢ (ConcreteCategory.hom (φ.app Δ))
      ((ConcreteCategory.hom ((𝟙_ SSet).map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) PUnit.unit) =
    (ConcreteCategory.hom (φ.app Δ)) PUnit.unit
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ X Y : C
i : X✝ ⟶ Y✝
hi : W₂ i
hp : W₁ (𝟙 X✝)
hf h : r.degHom i = r.deg X✝
fac : 𝟙 X✝ ≫ i = i
⊢ W₂ i

Tactic:
exact hi

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

Goal state before:
pp: case H.H
n✝¹ n✝ : ℕ
h : (mk n✝¹).len = (mk n✝).len
⊢ mk n✝¹ = mk n✝

Tactic:
simp only [mk_len] at h

Goal state after:
case H.H
n✝¹ n✝ : ℕ
h : n✝¹ = n✝
⊢ mk n✝¹ = mk n✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
hx : faces f✝
⊢ (∃ (h : x✝ = y✝), f✝ = eqToHom h) ∨ x✝.len < y✝.len

Tactic:
| of _ hx =>

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (IsRelLowerSet s fun x ↦ True) ↔ IsLowerSet s

Tactic:
grind [IsLowerSet, IsRelLowerSet]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (x ⊗ WithInitial.star)

Tactic:
by
  cases x <;>
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (WithInitial.star ⊗ x)

Tactic:
by
  cases x <;>
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ f k ≤ { as := f j.as }.as

Tactic:
exact f.monotone (I.le_right k hk)

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ x ≤ y

Tactic:
have := hxy.δ_index rfl
  simp only [cast_simplex_rfl] at this
  rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
    ← this]
  exact ⟨(SimplexCategory.δ _).op, rfl⟩

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

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

Tactic:
· rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.I ∪ h.II = Set.univ

Tactic:
ext s
    have := h.surjective s
    simp only [I, II, Set.mem_union, Set.mem_range, Set.mem_univ, iff_true]
    aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.pairing.p (h.equivII x) = h.equivI x

Tactic:
by
  simp [pairing]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.pairing.p.symm (h.equivI x) = h.equivII x

Tactic:
by
  simp [pairing]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0

Tactic:
let γ₁ (x : Fin (n + 1) × Fin (n + 2)) := (x.2.castSucc, x.1.succ)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ Sᶜ
⊢ x.2 ≤ x.1.castSucc

Tactic:
simpa [S] using hx

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : isCardinalPresentable C κ X
⊢ isCardinalPresentable C κ Y

Tactic:
by
    rw [isCardinalPresentable_iff] at hX ⊢
    exact h.isCardinalPresentable κ

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
⊢ x.1.castSucc < x.2

Tactic:
simpa [S] using hx

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
h₁ : κ'.IsRegular
h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun x ↦ Arrow J) (fun x ↦ κ.ord.ToType) i) κ'
⊢ κ < κ'

Tactic:
by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
e : C ≃ ↑(Set.range ⇑f₁) := Equiv.ofInjective ⇑f₁ ⋯
x✝¹ x✝ : ↑(Set.range ⇑f₁)
⊢ ↑(Set.range ⇑(f₂ (e.symm x✝¹) (e.symm x✝))) ≃ (e.symm x✝¹ ⟶ e.symm x✝)

Tactic:
by simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
e : C ≃ ↑(Set.range ⇑f₁) := Equiv.ofInjective ⇑f₁ ⋯
x✝¹ x✝ : ↑(Set.range ⇑f₁)
⊢ ↑(Set.range ⇑(f₂ (e.symm x✝¹) (e.symm x✝))) ≃ (e.symm x✝¹ ⟶ e.symm x✝)

Tactic:
by simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm

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

Goal state before:
pp: ⊢ strongAnodyneExtensions ≤ anodyneExtensions

Tactic:
rintro X Y f ⟨_, P, _⟩

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions f
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
rw [Fin.castSucc_lt_iff_succ_le, ← simplex_fst_min x hd]
    exact stdSimplex.monotone_apply _ h

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

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

Tactic:
rw [← hl.simplex_fst_succ]
    exact stdSimplex.monotone_apply _ hi

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.castSucc.rev)) (yonedaEquiv h.map))) =
    f.op.map

Tactic:
← stdSimplex.yonedaEquiv_δ_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.castSucc.rev ≫ h.map))) = f.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.succ.rev)) (yonedaEquiv h.map))) =
    fg.op.map

Tactic:
← stdSimplex.yonedaEquiv_δ_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.succ.rev ≫ h.map))) = fg.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.succ.succ.rev)) (yonedaEquiv h.map))) =
    g.op.map

Tactic:
← stdSimplex.yonedaEquiv_δ_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.succ.succ.rev ≫ h.map))) = g.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv ((ConcreteCategory.hom (SimplicialObject.δ X.op k.rev)) (yonedaEquiv h.map))) = const x

Tactic:
← stdSimplex.yonedaEquiv_δ_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (stdSimplex.δ k.rev ≫ h.map))) = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv ((ConcreteCategory.hom (SimplicialObject.δ X.op k.rev)) (yonedaEquiv h.map))) = const x

Tactic:
← stdSimplex.yonedaEquiv_δ_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (stdSimplex.δ k.rev ≫ h.map))) = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphI.symm 0 = stdSimplex.vertex 0

Tactic:
by
  simp [← TopCat.stdSimplexHomeomorphI_vertex_zero]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ a ≤ #α

Tactic:
obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l

Goal state after:
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ a ≤ #α
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
j : ι
hj : j ≠ i
this : 1 < (v j) a⁻¹
⊢ Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)

Tactic:
simpa [c] using (tendsto_div_one_add_pow_nhds_zero this).mul_const _

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2.inr.inr.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_one_lt ha.1 ha.2 ha_gt hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ ↑n ≤ analyticOrderAt (-f) z₀ ↔ ↑n ≤ analyticOrderAt f z₀

Tactic:
simp only [natCast_le_analyticOrderAt, hf, hf.neg]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (-f) z = (z - z₀) ^ n • g z) ↔
    ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z