mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
⊢ Presheaf.IsSheaf J (presheaf data G₀)

Tactic:
by
  rw [isSheaf_iff data]
  constructor
  · exact (Presheaf.isSheaf_of_iso_iff (compPresheafIso data G₀)).2 G₀.property
  · intro X
    refine ⟨(IsLimit.postcomposeHomEquiv
      (WalkingMulticospan.functorExt
          (fun _ ↦ presheafObjObjIso _ _ _) (fun _ ↦ presheafObjObjIso _ _ _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)) _).1
      (IsLimit.ofIsoLimit (presheafObjIsLimit data G₀ X)
        (Multifork.ext (Iso.refl _) (fun i ↦ ?_)))⟩
    simp [Multifork.ι, PreOneHypercover.multifork, MulticospanIndex.multicospan]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
⊢ W (hf.F.map g)

Tactic:
by
  obtain rfl : g = homOfLE bot_le := rfl
  induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    let : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

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

Goal state before:
pp: case succ.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
i : (c.attachCells j hj).ι
⊢ (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
⊢ (iterationFunctorObjObjRightIso I κ f j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app f) =
    (transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j

Tactic:
simp [iterationFunctorObjObjRightIso, iterationObjRightIso]

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

Goal state before:
pp: p : ℕ
q : ℚ
⊢ padicValRat p (-q) = padicValRat p q

Tactic:
by
  simp [padicValRat, padicValInt]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  intro t ht
  simp only [Finset.mem_image, Finset.mem_range] at ht
  obtain ⟨k, hk, rfl⟩ := ht
  rw [Finset.mem_erase, Nat.mem_divisors]
  refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
  exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) ↑x.num / (padicValuation p) ↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1

Tactic:
Rat.padicValuation_cast,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num / (padicValuation p) ↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num / (padicValuation p) ↑↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1

Tactic:
Rat.padicValuation_cast,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num / (Int.padicValuation p) ↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1
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:
· nth_rewrite 2 [unitCoeff_spec hx]
    simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]

Tactic:
· rw [Ideal.span_le, Set.singleton_subset_iff]
    exact p_nonunit

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
y : Φ.fiber.obj (unop Y)
⊢ (P.map g ≫ Pi.lift fun x ↦ Φ.toPresheafFiber (unop Y) x P ≫ f) ≫ Pi.π (fun t ↦ M) y =
    ((Pi.lift fun x ↦ Φ.toPresheafFiber (unop X) x P ≫ f) ≫
        Pi.map' ⇑(ConcreteCategory.hom (Φ.fiber.map g.unop)) fun x ↦ 𝟙 M) ≫
      Pi.π (fun t ↦ M) y

Tactic:
have := Φ.toPresheafFiber_w g.unop y P

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
y : Φ.fiber.obj (unop Y)
this :
  P.map g.unop.op ≫ Φ.toPresheafFiber (unop Y) y P =
    Φ.toPresheafFiber (unop X) ((ConcreteCategory.hom (Φ.fiber.map g.unop)) y) P
⊢ (P.map g ≫ Pi.lift fun x ↦ Φ.toPresheafFiber (unop Y) x P ≫ f) ≫ Pi.π (fun t ↦ M) y =
    ((Pi.lift fun x ↦ Φ.toPresheafFiber (unop X) x P ≫ f) ≫
        Pi.map' ⇑(ConcreteCategory.hom (Φ.fiber.map g.unop)) fun x ↦ 𝟙 M) ≫
      Pi.π (fun t ↦ M) y
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)

Tactic:
simpa only [sub_zero, add_sub_cancel_right] using hf

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m : s.pt ⟶ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).pt
hm : ∀ (j : R.arrows.categoryᵒᵖ), m ≫ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).π.app j = s.π.app j
⊢ m = ⋯.choose

Tactic:
dsimp at hm ⊢
      ext x
      obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
      simpa [← hm (op (Presieve.categoryMk _ _ hg))] using!
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : HasSheafify J (Type w)
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
this : Epi f
⊢ IsIso f

Tactic:
exact Balanced.isIso_of_mono_of_epi f

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ hσ' q n m hnm = 0

Tactic:
simp only [hσ', hσ]
  split_ifs
  exact zero_comp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q (q + 1) = Q q - P q ≫ Hσ q

Tactic:
by
  simp only [Q, P_succ, comp_add, comp_id]
  abel

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹

Tactic:
simp [hp.1.ne_zero, norm, padicNorm, padicValRat, padicValInt, zpow_neg,
    -Rat.cast_natCast]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)

Tactic:
· exact (HigherFacesVanish.of_P q n).comp_P_eq_self

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
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_zpow,

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.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]
  rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]
  by_cases hqn' : n + 1 < q
  · rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
  · simp only [hσ'_eq (show n + 1 = 0 + q by lia) (c_mk (n + 2) (n + 1) rfl), pow_zero,
      Fin.mk_zero, one_zsmul, eqToHom_refl, comp_id, comp_sum,
      AlternatingFaceMapComplex.obj_d_eq]
    -- All terms of the sum but the first two are zeros
    rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
    · simp only [Fin.val_zero, Fin.val_succ, Fin.val_castSucc, zero_add, pow_zero, one_smul,
        pow_one, neg_smul, comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ,
        add_neg_cancel]
    · intro j
      rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
      · simp [Fin.succ_ne_zero]
      · dsimp
        lia
      · simp only [Fin.succ_lt_succ_iff, j.succ_pos]

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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ ∑ j with ↑j < n + 1, f ≫ ((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
Finset.sum_eq_zero

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ 0 = 0

case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ ∀ x ∈ {i | ↑i < n + 1},
    f ≫ ((P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 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
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ PInfty.f i ≫ K[X].d i j =
    (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) ≫ (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ PInfty.f j

Tactic:
πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ PInfty.f i ≫ K[X].d i j =
    (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ PInfty.f j
Module: Mathlib.Topology.Homotopy.Equiv

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ ((↑h).comp ↑h.symm).Homotopic (ContinuousMap.id Y)

Tactic:
rw [toContinuousMap_comp_symm]

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₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (π.map (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
    ⟦H.evalAt x₀⟧ ≫ (π.map (TopCat.ofHom g)).map p = H.diagonalPath' p

Tactic:
by
  rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq]
  erw [H.evalAt_eq]
  dsimp only [prodToProdTopI]
  constructor
  · slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ `simp` didn't do this
    slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
    rfl
  · slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ `simp` didn't do this
    slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)

Tactic:
by simpa using mem_weakEquivalences (HoCat.pResolutionObj X)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: case inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.fst default) ≫ m = c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s)

pp: case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.snd default) ≫ m = c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s)

Tactic:
· simpa [h₁] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm

Goal state after:
case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.snd default) ≫ m = c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_1
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₁ :
  (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, ⋯⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
eq₂ :
  (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, ⋯⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, h₂⟩

Tactic:
rw [eq₁, eq₂]

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ hf.desc ≫ p = ι i j hj ≫ Λ[n + 1, i].ι ≫ b

Tactic:
by simpa using comm j hj

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

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

Tactic:
obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
    refine ⟨yonedaEquiv.symm σ, ?_⟩
    apply horn.hom_ext
    intro j hj
    rw [← h j hj, NatTrans.comp_app]
    rfl

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

Goal state before:
pp: X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    innerFibrations (terminal.from X)

Tactic:
exact ⟨fun h _ _ _ ⟨i, h0, hn⟩ ↦ h h0 hn,
    fun h _ _ h0 hn ↦ h _ (horn_ι_mem_innerHornInclusions h0 hn)⟩

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 : C
f : X ⟶ Y
hf : W₁ f
⊢ r.deg Y ≤ r.deg X

Tactic:
by
  by_cases hf' : MorphismProperty.identities C f
  · cases hf'
    rfl
  · exact (r.lt₁ f hf hf').le

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

Goal state before:
pp: case of.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
⊢ P (δ i)

Tactic:
simpa using! (δ_comp (𝟙 _) i id)

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

Goal state before:
pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.pred ⋯) = ↑t

Tactic:
simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁

Goal state after:
case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁✝ : hL.head.castSucc < t
h₂ : ¬a < ↑t
h₁ : a < ↑t
⊢ ↑(t.pred ⋯) = ↑t
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f

Tactic:
induction b using SimplexCategory.rec with | _ b

Goal state after:
case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : { len := a }.len ≤ d
b : ℕ
hb : { len := b }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
⊢ W f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsUpperSet s
a : { x // P x }
ma : a ∈ s
⊢ P ↑a ∧ ∀ ⦃b : α⦄, ↑a ≤ b → P b → b ∈ Subtype.val '' s

Tactic:
exact ⟨a.2, fun b x y ↦ by simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]⟩

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

Goal state before:
pp: case right
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
· intro t hts ht
          cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
          | inl h => exact (ht.ne_empty h).elim
          | inr h => exact ⟨v, h⟩

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
by simp [mem_finset_iff]

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ (tensorObjOf x y).len + z.len + 1 = x.len + (tensorObjOf y z).len + 1

Tactic:
simp +arith

Goal state after: