mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialCofibrations Cᵒᵖ).HasFactorization (fibrations Cᵒᵖ)

Tactic:
trivialCofibrations_op,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialFibrations C).op.HasFactorization (fibrations Cᵒᵖ)
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations (Over S)).HasFactorization (trivialFibrations (Over S))

Tactic:
rw [cofibrations_over_def, trivialFibrations_over_eq]
  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)
⊢ (I.fst default ≫ if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) =
    I.snd default ≫ if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr

Tactic:
simpa [h'.symm] using s.condition

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
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
⊢ c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s) = s.inr

Tactic:
by simpa using! hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n, j]

Tactic:
rw [horn_eq_iSup]
  exact le_iSup (fun (k : ({j}ᶜ : Set (Fin (n + 1)))) ↦ stdSimplex.face.{u} {k.1}ᶜ) ⟨i, h⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ n = 2 ∨ 2 < n

Tactic:
eq_comm,

Goal state after:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 = n ∨ 2 < n
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
hf : (monomorphisms (Type u)).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ monomorphisms (Type u) φ

Tactic:
simp only [functorCategory, monomorphisms.iff, mono_iff_injective] at hf ⊢
    replace hφ (j : J) := congr_hom (hφ j)
    simp only [Functor.const_obj_obj, comp_apply] at hφ
    intro x₁ y₁ h
    obtain ⟨j, x₁, y₁, rfl, rfl⟩ : ∃ (j : J) (x₁' y₁' : F₁.obj j),
        x₁ = c₁.ι.app j x₁' ∧ y₁ = c₁.ι.app j y₁' := by
      obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
      obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁
      exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩
    simp only [Functor.const_obj_obj, hφ] at h
    obtain ⟨k, α, hk⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc₂ _ _).1 h
    simp only [← NatTrans.naturality_apply] at hk
    rw [← c₁.w α, comp_apply, comp_apply, hf _ hk]

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} = Λ[2, 0]

Tactic:
apply le_antisymm
    · rw [sup_le_iff]
      constructor
      · exact face_le_horn (2 : Fin 3) 0 (by simp)
      · exact face_le_horn (1 : Fin 3) 0 (by simp)
    · rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: case a.inr
X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton d ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
exact le_trans (le_trans (by rfl) (le_iSup _ x)) le_sup_right

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

Goal state before:
pp: case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯) = p.arrow 0

Tactic:
map_mkOfSucc_zero_concat

Goal state after:
case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ p.arrow 0 = p.arrow 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) (spineToSimplex h p) = p.arrow 0

Tactic:
spineToSimplex_succ,

Goal state after:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    p.arrow 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    p.arrow 0

Tactic:
map_mkOfSucc_zero_concat

Goal state after:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ p.arrow 0 = p.arrow 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h p) = spineToSimplex h (p.interval 1 n ⋯)

Tactic:
spineToSimplex_succ,

Goal state after:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    spineToSimplex h (p.interval 1 n ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ Function.Surjective mk

Tactic:
by
  rintro ⟨⟨x⟩⟩
  exact ⟨x, rfl⟩

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_cases hf' : MorphismProperty.identities C f

Goal state after:
case pos
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
hf' : MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X

case neg
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
hf' : ¬MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X
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 X ≤ r.deg Y

Tactic:
by_cases hf' : MorphismProperty.identities C f

Goal state after:
case pos
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
hf' : MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y

case neg
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
hf' : ¬MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y
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
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.deg X ≤ r.deg Y

Tactic:
rw [← r.degHom_id X, ← e.hom_inv_id]

Goal state after:
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
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (e.hom ≫ e.inv) ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) (Fin.last (n + 1)) = 𝟙 (mk n)

pp: case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)

Tactic:
· simp only [Fin.lastCases_last]
      exact δ_comp_σ_succ

Goal state after:
case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

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

pp: case inl.inr
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.succ ≫ σ i = σ j ≫ δ j'

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

Goal state after:
case inl.inr
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.succ ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (Prod.mkHom (𝟙 (mk x)) (𝟙 (mk y)))) (homMk e))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e)))

Tactic:
← prod_id,

Goal state after:
X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 (mk x, mk y))) (homMk e))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj xyz.1)) (𝟙 xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))

Tactic:
← prod_id,

Goal state after:
X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map ((inverse (X ⊗ Y) Z).map (𝟙 ((inverse X Y).obj xyz.1, xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ :
  (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
have e₃ := inr'_eval x (tensorObjOf y z) <|
      Fin.cast (by simp +arith) <| i.natAdd (y.len + 1)

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ :
  (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
by
    ext x : 3
    exact (II.map'_map' _ _ _).symm

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

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n ↔ orderHomOfSimplex z hn = OrderHom.id

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · exact OrderHom.eq_id_of_injective _ (strictMono_orderHomOfSimplex ⟨z, h⟩ hn).injective
  · rw [nonDegenerate_iff_injective_objEquiv]
    intro h a b hab
    simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h
    rw [← h a, ← h b, Fin.ext_iff]
    change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2
    simp only [hab]

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:
rw [isCardinalPresentable_iff] at hX ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : IsCardinalPresentable X κ
⊢ IsCardinalPresentable Y κ
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X : ↑h.obj
⊢ h.functor.essImage (h.objEquiv X)

Tactic:
exact ⟨_, ⟨Iso.refl _⟩⟩

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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ A.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

Tactic:
exact Or.inl (Or.inl hx)

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✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (f.filtration m)

Tactic:
← f.iSup_filtration_iio m hm

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (⨆ i, f.filtration ↑i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
· exact Finset.min'_le _ _ (by simpa using h.symm)

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

Goal state before:
pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
obtain rfl | hi := (Fin.castSucc_lt_iff_succ_le.1 hi).eq_or_lt

Goal state after:
case inr.inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.succ)) (x.cast hd).simplex
hi : l.castSucc < l.succ
⊢ l.succ = l.castSucc ∨ l.succ = l.succ

case inr.inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi✝ : l.castSucc < i
hi : l.succ < i
⊢ i = l.castSucc ∨ i = l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
n : ℕ
⊢ SSet.homologyMap (𝟙 X) R n = 𝟙 (X.homology R n)

Tactic:
simp [SSet.homologyMap]

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

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₀

Tactic:
← cancel_mono (μIso _ _ _).inv,

Goal state after:
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) ≫
      (μIso TopCat.toSSet X TopCat.I).inv =
    TopCat.toSSet.map TopCat.ι₀ ≫ (μIso TopCat.toSSet X TopCat.I).inv
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₁

Tactic:
← cancel_mono (μIso _ _ _).inv,

Goal state after:
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) ≫
      (μIso TopCat.toSSet X TopCat.I).inv =
    TopCat.toSSet.map TopCat.ι₁ ≫ (μIso TopCat.toSSet X TopCat.I).inv
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
inst✝ : Field R
v : AbsoluteValue R ℝ
a : R
ha : v a < 1
⊢ Filter.Tendsto (fun n ↦ (equiv v).symm (1 / (1 + a ^ n))) Filter.atTop (𝓝 1)

Tactic:
simpa using! inv_one (G := WithAbs v) ▸ (tendsto_inv_iff₀ one_ne_zero).2
    (tendsto_iff_norm_sub_tendsto_zero.2 <| by simpa using! ha)

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

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

Tactic:
exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t' = ∅

Tactic:
inter_assoc,

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ (s ∩ (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t') = ∅