mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)

Tactic:
exact this (le_of_not_ge hle)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
rw [padicValNat.eq_zero_of_not_dvd dvd]
    lia

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ IsUnit ↑r.den

Tactic:
rw [isUnit_iff]
  apply le_antisymm (r.den : ℤ_[p]).2
  rw [← not_lt, coe_natCast]
  intro norm_denom_lt
  have hr : ‖(r * r.den : ℚ_[p])‖ = ‖(r.num : ℚ_[p])‖ := by
    congr
    rw_mod_cast [@Rat.mul_den_eq_num r]
  rw [padicNormE.mul] at hr
  have key : ‖(r.num : ℚ_[p])‖ < 1 := by
    calc
      _ = _ := hr.symm
      _ < 1 * 1 := mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one
      _ = 1 := mul_one 1
  have : ↑p ∣ r.num ∧ (p : ℤ) ∣ r.den := by
    simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
    exact ⟨key, norm_denom_lt⟩
  apply hp_prime.1.not_dvd_one
  rwa [← r.reduced.gcd_eq_one, Nat.dvd_gcd_iff, ← Int.natCast_dvd, ← Int.natCast_dvd_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ x

Tactic:
unitCoeff_spec hx

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ x.valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, ‖↑x' k - ↑(const norm x'.lim) j‖ < ↑p ^ (-↑n)
hin : n < i
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

Tactic:
specialize hi i le_rfl i le_rfl
        specialize hx hin.le
        have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
        rw [sub_add_sub_cancel] at this
        exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p (↑(g - 0) j) < ε

Tactic:
by simpa [h] using hi _ hj

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
⊢ ∀ (i j : (glueData hf).J),
    (ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i)) =
      (ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j))

Tactic:
by
      intro i j
      apply yonedaEquiv.symm.injective
      dsimp only [glueData_V, glueData_J, glueData_U, glueData_f, glueData_t]
      rw [yonedaEquiv_naturality, Equiv.symm_apply_apply,
        Functor.map_comp_apply, yonedaEquiv_naturality, yonedaEquiv_naturality,
        Equiv.symm_apply_apply, ← Functor.map_comp_assoc,
        Functor.relativelyRepresentable.symmetry_fst, ((hf i).rep.isPullback' (f j)).w]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : 0 < ↑ε'
hε'r : ↑ε' < ε
⊢ 0 < ε'

Tactic:
simpa using hε'l

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ↑↑p ^ (-PadicSeq.valuation f) = ↑p ^ (-PadicSeq.valuation f)

Tactic:
Rat.cast_natCast

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ↑p ^ (-PadicSeq.valuation f) = ↑p ^ (-PadicSeq.valuation f)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Tactic:
rw [← X.δ_comp_δ''_assoc]
    swap
    · rw [Fin.le_iff_val_le_val]
      dsimp
      lia
    simp only [← assoc, v j (by lia), zero_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
by_cases h₄ : Isδ₀ i'

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
by
  conv_rhs => rw [← id_comp (s.πSummand _)]
  symm
  rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      (Γ₂N₂.inv ≫ Γ₂N₂.hom).app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      (𝟙 (N₂ ⋙ Γ₂)).app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F G : U ⥤rq V
e : F = G
X : U
⊢ F.obj X = G.obj X

Tactic:
by cases e; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯

Tactic:
dsimp only [prodToProdTopI, uhpath01, hcast]

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ =
    eqToHom ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
        eqToHom ⋯
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
by
  refine ⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
  rw [← RightHomotopyClass.mk_eq_mk_iff]
  exact (bijective_rightHomotopyClassToHom L X Y).1 (by simpa)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj

Tactic:
rw [weakEquivalence_iff_of_objectProperty]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : BifibrantObject C
f : X₁ ⟶ X₂
this :
  (cofibrantObjects C).ι.map (homMk f.hom ≫ (mk X₂.obj).iBifibrantResolutionObj) =
    (cofibrantObjects C).ι.map ((mk X₁.obj).iBifibrantResolutionObj ≫ homMk (bifibrantResolutionMap (homMk f.hom)).hom)
⊢ (f ≫ BifibrantObject.homMk (mk X₂.obj).iBifibrantResolutionObj.hom).hom =
    (BifibrantObject.homMk (mk X₁.obj).iBifibrantResolutionObj.hom ≫
        bifibrantResolutionMap (ObjectProperty.homMk f.hom)).hom

Tactic:
exact this

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

Goal state before:
pp: case neg.inr
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
        obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩
        exact face_le_horn _ _ (by rintro rfl; tauto)

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
by
  rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]

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

Goal state before:
pp: case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
exact le_sup_right

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

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
⊢ innerHornInclusions f✝ ↔ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : innerHornInclusions f✝
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝

case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : ∃ i i_1, Arrow.mk f✝ = Arrow.mk Λ[i + 2, ↑i_1].ι
⊢ innerHornInclusions f✝

Tactic:
obtain ⟨n, ⟨i, h0, hn⟩, _, _⟩ := h

Goal state after:
case refine_2
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
⊢ innerHornInclusions Λ[n + 2, ↑⟨i, ⋯⟩].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
exact le_sup_right

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

Goal state before:
pp: case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
exact le_sup_right

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x : ↑(Y.nonDegenerate d)
n : ℕ
⊢ ↑x ∈ ((skeletonOfMono i) n).obj (op ⦋d⦌) ↔ ↑x ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌))) ∨ d < n

Tactic:
by
  simp [skeletonOfMono, mem_skeleton_obj_iff_of_nonDegenerate]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ (Y.skeleton n).obj (op ⦋d⦌) ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)

Tactic:
exact le_sup_right

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ h).op)) (sx.spineToSimplex m h f) = f.vertex i

Tactic:
← spine_vertex,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ (X.spine m h (sx.spineToSimplex m h f)).vertex i = f.vertex i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i).op)) (sx.spineToSimplex f) = f.vertex i

Tactic:
← spine_vertex,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ (X.spine n (sx.spineToSimplex f)).vertex i = f.vertex i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (f.map σ).arrow k = (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌))) (f.arrow k)

Tactic:
Path.map_arrow

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌))) (f.arrow k) =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌))) (f.arrow k)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      (((λ_ (𝟙_ V)).inv ≫ (λ_ (𝟙_ V)).hom) ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
Iso.inv_hom_id,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      (𝟙 (𝟙_ V) ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
h : (mk x).as.as = (mk y).as.as
⊢ mk x = mk y

Tactic:
obtain rfl : x = y := h

Goal state after:
V : Truncated 2
x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ mk x = mk x
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 h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
⊢ HomotopicR f h

Tactic:
by
  rcases hfg with ⟨hfg⟩
  rcases hgh with ⟨hgh⟩
  exact Quasicategory₂.fill31 (idComp (id x)) hfg hgh

Goal state after:
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ r.degHom (f ≫ g) ≤ r.degHom f

Tactic:
by
  have ⟨_, f₁, f₂, _, _, h_fac, h_deg⟩ := r.exists_fac f
  rw [h_deg, ← h_fac, Category.assoc]
  exact r.degHom_le f₁ (f₂ ≫ g)

Goal state after:
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:
rw [Fin.castSucc_lt_iff_succ_le] at h

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.GeneratorsRelations.EpiMono

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

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
    rw [Fin.castSucc_lt_castSucc_iff] at h
    obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
    rw [← Fin.le_castSucc_iff] at h
    exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

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

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)

Tactic:
· 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: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 2)
hi : i ∈ finset f x
⊢ y.castSucc ≤ i

Tactic:
obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last

Goal state after:
case mpr.inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y.castSucc ≤ i.castSucc

case mpr.inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g))
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))

Tactic:
simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j

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 t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = (↑(P.p t)).toS

Tactic:
← (P.p t).val.cast_eq_self (P.isUniquelyCodimOneFace t).dim_eq

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = ((↑(P.p t)).cast ⋯).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
⊢ WellFounded h.pairing.AncestralRel

Tactic:
have := IsRegular.wf h
    rw [wellFounded_iff_isEmpty_descending_chain] at this ⊢
    exact ⟨fun ⟨f, hf⟩ ↦ this.false
      ⟨fun n ↦ h.equivII.symm (f n), fun n ↦ by simpa [ancestralRel_iff] using hf n⟩⟩

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{?u.4, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ (⊥_ SSet).Finite

Tactic:
apply finite_of_isColimit (initialIsInitial (C := SSet.{u}))

Goal state after:
J : Type u_1
inst✝¹ : Category.{?u.4, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ ∀ (j : Discrete PEmpty.{1}), ((Functor.empty SSet).obj j).Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ X₃ X₄ : SSet
inst✝¹ : X₁.Finite
inst✝ : X₂.Finite
d₁ : ℕ
h✝¹ : X₁.HasDimensionLT d₁
d₂ : ℕ
h✝ : X₂.HasDimensionLT d₂
⊢ (X₁ ⊗ X₂).Finite

Tactic:
exact finite_of_hasDimensionLT _ (d₁ + d₂) (fun _ _ ↦ inferInstance)

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

Goal state before:
pp: case a.notMem.refine_2.refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
ht : s = ↑c.s ∨ s = ↑(P.p c.s)
hs : (↑c.s).subcomplex ≤ c.horn.image c.map
⊢ False

Tactic:
exact c.subcomplex_not_le_image_horn hs

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 Ω)
X Y : C
⊢ Nonempty ((X ⟶ Y) ↪ Ω)

Tactic:
refine ⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩

Goal state after:
κ : 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 Ω)
X Y : C
⊢ Function.Injective fun f ↦ Arrow.mk f
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
G : C' ⥤ C
inst✝ : G.IsEquivalence
x✝ : (G ⋙ F).IsDense
e : G.inv ⋙ G ⋙ F ≅ F := (G.inv.associator G F).symm ≪≫ isoWhiskerRight G.asEquivalence.counitIso F ≪≫ F.leftUnitor
⊢ F.IsDense

Tactic:
exact of_iso e

Goal state after:
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
G : D ⥤ C'
inst✝ : G.IsEquivalence
x✝ : (F ⋙ G).IsDense
e : (F ⋙ G) ⋙ G.inv ≅ F := F.associator G G.inv ≪≫ F.isoWhiskerLeft G.asEquivalence.unitIso.symm ≪≫ F.rightUnitor
⊢ F.IsDense

Tactic:
exact of_iso e

Goal state after: