mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (generatingMonomorphisms G).HasSmallObjectArgument

Tactic:
obtain ⟨κ, hκ', hκ⟩ := HasCardinalLT.exists_regular_cardinal.{w} (Subobject G)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
⊢ (generatingMonomorphisms G).HasSmallObjectArgument
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp.llp = monomorphisms C

Tactic:
refine le_antisymm ?_ (le_llp_rlp _)
  rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]
  trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
  · apply retracts_monotone
    apply transfiniteCompositions_monotone
    apply pushouts_monotone
    apply coproducts_monotone
    apply generatingMonomorphisms_le_monomorphisms
  · simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q) ∨ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p r)

Tactic:
left

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1

Tactic:
simp [norm_le_one z, nonunits, isUnit_iff]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ! ≤ (p - 1) * padicValNat p n !

Tactic:
conv_lhs => rw [← one_mul (padicValNat p n !)]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 1 * padicValNat p n ! ≤ (p - 1) * padicValNat p n !
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
h' : (Int.padicValuation p) x.num < 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num

Tactic:
rw [Int.padicValuation_lt_one_iff] at h h'

Goal state after:
case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : ↑p ∣ ↑x.den
h' : ↑p ∣ x.num
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Ext.mk₀
      ((let __Equiv := Ext.homEquiv₀;
        { toEquiv := __Equiv, map_add' := ⋯ })
        ((map f 0) x)) =
    Ext.mk₀
      ((let __Equiv := Ext.homEquiv₀;
          { toEquiv := __Equiv, map_add' := ⋯ })
          x ≫
        f)

Tactic:
simp only [AddEquiv.coe_mk, Ext.mk₀_homEquiv₀_apply, Ext.mk₀_homEquiv₀_apply, ← Ext.mk₀_comp_mk₀]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (map f 0) x = Ext.comp x (Ext.mk₀ f) ⋯
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ f.norm = g.norm

Tactic:
by
  rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]
  · exact mod_cast (Fact.out : p.Prime).pos
  · exact mod_cast (Fact.out : p.Prime).ne_one

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
⊢ ∃ z, a.norm = ↑p ^ (-z)

Tactic:
let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
  simpa [hk] using padicNorm.values_discrete hk'

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst✝ : HasPullback f f
hc : IsLimit (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯)
⊢ Mono f

Tactic:
rw [mono_iff_isIso_fst hc, h.isIso_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst✝ : HasPullback f f
hc : IsLimit (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯)
⊢ ∀ (i : I), IsIso ((F i).map (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯).fst)
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b✝ : C
f' : F.obj b✝ ⟶ Y
hf' : F.relativelyRepresentable f'
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
c : C
a b : c ⟶ hf'.pullback g
h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g
h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g
⊢ F.map a ≫ hf'.fst g = F.map b ≫ hf'.fst g

Tactic:
simpa [map_fst'] using F.congr_map h₁

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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ (P q).f (n + 1) = φ ↔ HigherFacesVanish q φ

Tactic:
constructor
  · intro hφ
    rw [← hφ]
    apply HigherFacesVanish.of_comp
    apply HigherFacesVanish.of_P
  · exact HigherFacesVanish.comp_P_eq_self

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X

Tactic:
ext (_ | n)
  · dsimp
    simp only [comp_id]
  · exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self

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 : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop ≫ 𝟙 (unop (op (unop A.fst)))

Tactic:
rw [comp_id, fac]; rfl

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

Goal state before:
pp: case mpr
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⦌
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0 → f ≫ PInfty.f n = 0

Tactic:
intro h
    rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_zero]
    intro A
    by_cases hA : A.EqId
    · dsimp at hA
      subst hA
      rw [assoc, reassoc_of% h, zero_comp]
    · simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i)

Tactic:
ext; simp [inf'_apply]

Goal state after:
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 : ℕ
⊢ s.fromNondegComplex.f n = s.ι n ≫ PInfty.f n

Tactic:
simp [fromNondegComplex, fullyFaithfulToKaroubi,
    cofan, IndexSet.id, IndexSet.e]

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G).symm (t, snd✝) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)

Tactic:
symm_apply,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G) (σ (t, snd✝).1, (t, snd✝).2) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)
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
⊢ Function.Surjective L.map

Tactic:
intro f
  obtain ⟨⟨f⟩, rfl⟩ := (bijective_leftHomotopyClassToHom L X Y).2 f
  exact ⟨f, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
hF : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
⊢ ∀ (x y : BifibrantObject C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
by rwa [inverts_iff_factors] at hF

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

Goal state before:
pp: case neg
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : ↑(stdSimplex.nonDegenerateEquiv'.symm ⟨S, hS⟩) ∈ A.obj (op ⦋d⦌)
⊢ ↑(stdSimplex.nonDegenerateEquiv'.symm ⟨S, hS⟩) ∈ Λ[n + 1, i].obj (op ⦋d⦌)

Tactic:
simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢

Goal state after:
case neg
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
⊢ stdSimplex.face S ≤ Λ[n + 1, i]
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.mk (Rel f g) x)) = Quot.mk (Rel f g) x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout' f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.mk (Rel' f g) x)) = Quot.mk (Rel' f g) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d n : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h : ↑⟨x, hx⟩ ∈ (X.skeleton n).obj (op ⦋d⦌)
⊢ d < n

Tactic:
simp only [skeleton, OrderHom.coe_mk, Subfunctor.iSup_obj,
    Set.iUnion_coe_set, Set.mem_iUnion, exists_prop] at h

Goal state after:
X : SSet
d n : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h : ∃ i, ∃ i_1 ∈ X.nonDegenerate ↑i, x ∈ (Subcomplex.ofSimplex i_1).obj (op ⦋d⦌)
⊢ d < n
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face {↑j}ᶜ ⊓ stdSimplex.face {↑k}ᶜ

Tactic:
rw [stdSimplex.face_inter_face]
    congr
    aesop

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

Goal state before:
pp: n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.succ

Tactic:
by
    fin_cases i
    · exact p.arrow_tgt 0
    · exact q.arrow_tgt 0

Goal state after:
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' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ (λ_ (X' ⟶[V] Z)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Z) ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
rw [leftUnitor_inv_naturality_assoc, whisker_exchange_assoc]

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' : C
f : X ⟶ X'
Y Z : C
⊢ (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Z)).inv ≫
      (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Z) ≫ (X ⟶[V] X') ◁ eComp V X' Y Z ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z
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 Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
            (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
              (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
associator_inv_naturality_right_assoc,

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 Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
            (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).inv ≫
              ((X ⟶[V] Y) ⊗ Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ F.obj (P ⟶[V] Q) ◁ μ F (Q ⟶[V] R) (R ⟶[V] S) ≫
      μ F (P ⟶[V] Q) ((Q ⟶[V] R) ⊗ R ⟶[V] S) ≫
        F.map ((α_ (P ⟶[V] Q) (Q ⟶[V] R) (R ⟶[V] S)).inv ≫ (eComp V P Q R ▷ R ⟶[V] S) ≫ eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)

Tactic:
e_assoc,

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ F.obj (P ⟶[V] Q) ◁ μ F (Q ⟶[V] R) (R ⟶[V] S) ≫
      μ F (P ⟶[V] Q) ((Q ⟶[V] R) ⊗ R ⟶[V] S) ≫ F.map ((P ⟶[V] Q) ◁ eComp V Q R S ≫ eComp V P Q S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
X✝ Y✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
⊢ (id W C).forget.map f ≫ (Iso.refl ((id W C).forget.obj Y✝)).hom =
    (Iso.refl ((id W C).forget.obj X✝)).hom ≫ (𝟭 (ForgetEnrichment W C)).map f

Tactic:
by simp [forget]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Terminal

Goal state before:
pp: ⊢ HasTerminal Cat

Tactic:
have : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1}) := {
    subsingleton _ _ := { allEq _ _ := eq_of_comp_right_eq (congrFun rfl) }
    eq_of_hom _ := rfl
  }

Goal state after:
this : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1})
⊢ HasTerminal Cat
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

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

Tactic:
left

Goal state after:
case id
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ ∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_δ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ ∃ z_1 e_1 m_1, ∃ (_ : P_σ e_1) (_ : P_δ m_1), (e ≫ m) ≫ δ j = e_1 ≫ m_1

Tactic:
exact ⟨z, e, m ≫ δ j, he, P_δ.comp_mem _ _ hm (P_δ.δ _), by simp⟩

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)

Tactic:
by
      ext y
      obtain ⟨y, rfl⟩ := y.mk_surjective
      simp
      rfl

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)

Tactic:
by
      ext y
      obtain ⟨y, rfl⟩ := y.mk_surjective
      simp
      rfl

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

Goal state before:
pp: x y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x ⊗ y✝ ⟶ z✝
y z : SimplexCategory
f g : WithInitial.star ⊗ WithInitial.of y ⟶ WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ : inr WithInitial.star (WithInitial.of y) ≫ f = inr WithInitial.star (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
by
      simp only [inr, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        id_star_whiskerRight] at h₂
      simpa [Category.id_comp f, Category.id_comp g] using h₂

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

Goal state before:
pp: case inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

pp: case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))

Tactic:
· obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
    · rw [hy]
      rw [map'_eq_castSucc_iff] at hy
      obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
      · rw [hz, Eq.comm]
        rw [map'_eq_castSucc_iff] at hz ⊢
        constructor
        · refine hy.1.trans ?_
          simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
          exact g.monotone (by simpa using hz.1)
        · intro i hi
          exact hy.2 (f i) (by simpa using hz.2 i hi)
      · rw [hz, Eq.comm]
        rw [map'_eq_last_iff] at hz ⊢
        intro i
        exact hy.2 (f i) (by simpa using hz i)
    · rw [Eq.comm, hx, map'_last]
      rw [map'_eq_last_iff] at hx ⊢
      intro i
      apply hx

Goal state after:
case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (II.δ i).unop = (σ i).op.unop

Tactic:
ext : 3; apply II.map'_succAboveOrderEmb

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑(P.p s)).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑(P.p s)).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }

Tactic:
refine ⟨s, Or.inl ?_⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
⊢ h.type₁ s ≠ h.type₂ t

Tactic:
by
  simpa only [ne_eq, N.ext_iff, SSet.N.ext_iff] using! h.type₁_ne_type₂' s t

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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ ⨆ j, ⨆ (_ : j < i), ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
refine le_trans ?_ (le_iSup _ j)

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ ⨆ (_ : j < i), ⨆ c, (↑(P.p c.s)).subcomplex