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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)

Tactic:
· rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
    · norm_cast
      rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
      · norm_cast
      · apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩
    · exact_mod_cast hz
    · exact_mod_cast hp.out.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑(p ^ 1) ∣ m

Tactic:
simp only [dvd_iff_norm_le, Nat.cast_one, zpow_neg, zpow_one, not_le]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ (↑p)⁻¹ < padicNorm p ↑m
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)

Tactic:
rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by lia⟩), and_iff_right_iff_imp]

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Tactic:
padicValInt,

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a.natAbs
Module: Mathlib.CategoryTheory.Types.Epimorphisms

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
x : x✝³
y : x✝²
hy : (ConcreteCategory.hom r) y = (ConcreteCategory.hom b) x
⊢ ∃ a, (ConcreteCategory.hom l) a = x

Tactic:
obtain ⟨z, _, hz⟩ := Types.exists_of_isPullback sq _ _ hy

Goal state after:
x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
x : x✝³
y : x✝²
hy : (ConcreteCategory.hom r) y = (ConcreteCategory.hom b) x
z : x✝¹
left✝ : (ConcreteCategory.hom t) z = y
hz : (ConcreteCategory.hom l) z = x
⊢ ∃ a, (ConcreteCategory.hom l) a = x
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
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)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Presheaf.IsLocallySurjective J (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))

Tactic:
refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)

Goal state after:
case refine_2
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)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
x : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)
⊢ ∃ a, (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)))) a = x
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: case h₁
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 : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)

Tactic:
simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

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

Goal state before:
pp: case h₂
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 : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)

Tactic:
simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

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
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) ⋯ = hσ' q n (n + 1) ⋯ ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp only [AlternatingFaceMapComplex.obj_X, hσ', hσ, Int.reduceNeg, eqToHom_refl, comp_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else (-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) =
    (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
⊢ ∃ b, f ≈ const norm b

Tactic:
have cau_seq_norm_e : IsCauSeq padicNormE f := fun ε hε => by
      have h := isCauSeq f ε (mod_cast hε)
      dsimp [norm] at h
      exact mod_cast h
    -- Porting note: Padic.complete' works with `f i - q`, but the goal needs `q - f i`,
    -- using `rewrite [padicNormE.map_sub]` causes time out, so a separate lemma is created
    obtain ⟨q, hq⟩ := Padic.complete'' ⟨f, cau_seq_norm_e⟩
    exists q
    intro ε hε
    obtain ⟨ε', hε'⟩ := exists_rat_btwn hε
    norm_cast at hε'
    obtain ⟨N, hN⟩ := hq ε' hε'.1
    exists N
    intro i hi
    have h := hN i hi
    change norm (f i - q) < ε
    refine lt_trans ?_ hε'.2
    dsimp [norm]
    exact mod_cast h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Δ = Δ'

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len
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 : ℕ
hij : ¬(ComplexShape.down ℕ).Rel i j
⊢ s.d i j = 0

Tactic:
by simp only [d, K[X].shape i j hij, zero_comp, comp_zero]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected (⇑f.symm '' s) ↔ IsSimplyConnected s

Tactic:
isSimplyConnected_image

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected s ↔ IsSimplyConnected s
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adj.unit.app X)

Tactic:
by
  obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
  dsimp [HoCat.adj]
  infer_instance

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

Goal state before:
pp: 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
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ I.right k = I.right (J.snd default)

Tactic:
obtain rfl : k = J.snd default := by
            have := h.symm.le (Set.mem_univ k)
            push _ ∈ _ at this
            tauto

Goal state after:
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
s : PushoutCocone (I.fst default) (I.snd default)
hk : ¬J.snd default = J.fst default
⊢ I.right (J.snd default) = I.right (J.snd default)
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (i, j) =
    (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (j, i)

Tactic:
by
        dsimp
        rw [h.eq_inf, h.eq_inf, inf_comm]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasIterationOfShape K C
X Y : J ⥤ C
f : X ⟶ Y
hf : (W.functorCategory J).TransfiniteCompositionOfShape K f
j : J
this : W.functorCategory J ≤ W.inverseImage ((evaluation J C).obj j)
⊢ W (f.app j)

Tactic:
exact W.transfiniteCompositionsOfShape_le K _ ⟨(hf.ofLE this).map⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ Λ[n, i].toSSet _⦋1⦌

Tactic:
by
  refine edge n i j.castSucc j.succ ?_ ?_
  · simp only [← Fin.val_fin_le, Fin.val_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]
  simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
  obtain rfl | hn : n = 2 ∨ 2 < n := by
    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; lia
  · revert i j; decide
  · exact Finset.card_le_three.trans hn

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ σ₁ = σ₂

Tactic:
← Subfunctor.equalizer_eq_iff

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ Y.skeleton n ≤ Subcomplex.range i ⊔ Y.skeleton m

Tactic:
exact le_trans (Y.skeleton.monotone h) le_sup_right

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)

Tactic:
rw [dsimp% congr($(c.ι_b_ι).app (op ⦋n⦌) y)] at hx
      rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]

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

Goal state before:
pp: case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f → morphismPropertyHomMk V f

Tactic:
· rintro ⟨⟨_, _, e⟩⟩
    exact morphismPropertyHomMk_of_edge e

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
⊢ W₁.MapFactorizationData W₂ f

Tactic:
letI := (r.nonempty_unique f).some
  exact default

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

Goal state before:
pp: case zero.of
i : Fin (0 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (0 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h; exact factor_δ_σ _ _

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

Goal state before:
pp: case succ.of
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 : SimplexCategoryGenRel
f : x ⟶ mk (n + 1 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h; exact factor_δ_σ _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
by_cases h₂ : Function.Injective f.hom.toOrderHom

Goal state after:
case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ j ≫ toMk₁ i)) k = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

Tactic:
change toMk₁ i (j.predAbove k) = _

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ j ≫ toMk₁ i)) k = (ConcreteCategory.hom (toMk₁ i.succ)) k

Tactic:
change toMk₁ i (j.predAbove k) = _

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ WellFounded P.AncestralRel

Tactic:
by
  rw [wellFounded_iff_isEmpty_descending_chain]
  refine ⟨fun ⟨g, hg⟩ ↦ ?_⟩
  obtain ⟨n₀, hn₀⟩ :=
    (wellFoundedGT_iff_monotone_chain_condition (α := ℕᵒᵈ)).1
      inferInstance ⟨fun n ↦ (g n).1.dim,
        monotone_nat_of_le_succ (fun n ↦ (hg n).dim_le)⟩
  dsimp at hn₀
  refine not_strictAnti_of_wellFoundedLT (fun n ↦ f.rank (g (n₀ + n)))
    (strictAnti_nat_of_succ_lt (fun n ↦ ?_))
  rw [← add_assoc]
  exact f.lt (hg _) (by rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)])

Goal state after:
Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ IsColimit (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯))

Tactic:
refine .equivOfNatIsoOfIso ?_ _ _ ?_ (isColimitCoforkOfEffectiveEpi (f.app k)
        (pullback.cone (f.app k) (f.app k))
        (pullback.isLimit (f.app k) (f.app k)))

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd ≅
    parallelPair
        (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      (evaluation C D).obj k

case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (Cofork.ofπ (f.app k) ⋯) ≅
    ((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)
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 ι
i : ι
hi : Order.IsSuccLimit i
⊢ ⨆ j, ⨆ (_ : j < i), f.filtration j ≤ f.filtration i

Tactic:
· simp only [iSup_le_iff]
    intro j hj
    exact f.filtration_monotone hj.le

Goal state after:
Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ (Cocone.precompose
          (NatIso.ofComponents
              (fun X ↦
                WalkingParallelPair.casesOn X
                  (Iso.refl
                    ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                      WalkingParallelPair.zero))
                  (Iso.refl
                    ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                      WalkingParallelPair.one)))
              ⋯).inv).obj
      (Cofork.ofπ (f.app k) ⋯) ≅
    ((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)

Tactic:
exact Cocone.ext (Iso.refl _) <| by rintro (_ | _ | _); all_goals cat_disch

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

Goal state before:
pp: C : Type u
hC : Category.{v, u} C
inst✝ : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
h' : IsCardinalLocallyPresentable C κ
⊢ ∃ κ, ∃ (x : Fact κ.IsRegular), IsCardinalAccessibleCategory C κ

Tactic:
exact ⟨κ, hκ, inferInstance⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₁ f c) = { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

Tactic:
by
  dsimp only [Cell.type₁, mapN]
  rw [← S.cast_eq_self _ (P.dim_p c.s)]
  dsimp
  rw [S.ext_iff, c.ι_b_app_apply]
  apply yonedaEquiv_symm_app_id

Goal state after:
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
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
⊢ (P.colimitsCardinalClosure κ).ι.map (homMk (coequalizer.π φ₁ φ₂)) ≫ (CostructuredArrow.mk a).hom = j.hom

Tactic:
simp [E, a]

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

Goal state before:
pp: ⊢ IsSmall.{u, u, u + 1} innerHornInclusions

Tactic:
rw [innerHornInclusions_eq_iSup]
  have (n : ℕ) : MorphismProperty.IsSmall.{u}
    (MorphismProperty.ofHoms.{u}
      fun p : {p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2)} ↦ Λ[n + 2, p].ι) :=
    isSmall_ofHoms ..
  exact isSmall_iSup _

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

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

Tactic:
rw [← hi]

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