mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ Epi f

Tactic:
← Sheaf.isLocallySurjective_iff_epi

Goal state after:
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)
⊢ Sheaf.IsLocallySurjective f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hxy, if_pos rfl]

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤ ⊤
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hx, if_pos rfl, min_eq_right, zero_add]

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑y.valuation) ≤ ⊤
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (functor ⋙ inverse).map φ ≫ { f := { f := fun n ↦ Q.p.f n, comm' := ⋯ }, comm := ⋯ } =
    { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ } ≫ (𝟭 (Karoubi (HomologicalComplex C c))).map φ

Tactic:
ext
        dsimp
        simp only [HomologicalComplex.comp_p_d, HomologicalComplex.p_comp_d]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
exact hom_heq_of_cons_eq_cons h

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f⁻¹ * f = 𝟙 x

Tactic:
inv_mul_cancel,

Goal state after:
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ 1 = 𝟙 x
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ = f Z✝ * ((f Y✝)⁻¹ * f Y✝)

Tactic:
inv_mul_cancel,

Goal state after:
M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ = f Z✝ * 1
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift

Tactic:
let h := factorizationData (trivialCofibrations C) (fibrations C)
      (pullback.lift f i sq.w)
    have sq' : CommSq h.i i (h.p ≫ pullback.snd _ _) (𝟙 B) := .mk
    have h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g) := by simpa
    have h₂ := comp_mem _ _ _ h.hp ((fibrations C).of_isPullback
      (IsPullback.of_hasPullback p g) (mem_fibrations p))
    rw [← fibration_iff] at h₂
    have : WeakEquivalence (h.p ≫ pullback.snd p g) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_precomp _ _ _ h.hi.2 h₁
    exact ⟨⟨{ l := sq'.lift ≫ h.p ≫ pullback.fst p g
              fac_right := by
                rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right] }⟩⟩

Goal state after:
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
n : SimplexCategoryᵒᵖ
⊢ ∀ (i j : ι), (V i j).obj n = (U i).obj n ⊓ (U j).obj n

Tactic:
simp [h.eq_inf]

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

Goal state before:
pp: case inl
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi✝ : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
hi : n < i
⊢ a ∈ Δ[n].degenerate i

Tactic:
simp [Δ[n].degenerate_eq_univ_of_hasDimensionLT (n + 1) i]

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

Goal state before:
pp: n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
i : Fin (n + 1 + 1)
y : unop m ⟶ ⦋n⦌
hx : (ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∈ ∂Δ[n + 1].obj m
⊢ (ConcreteCategory.hom (f.app m)).toFun
      ⟨(ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)), hx⟩ =
    (ConcreteCategory.hom (g.app m)).toFun
      ⟨(ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)), hx⟩

Tactic:
exact ConcreteCategory.congr_hom (congr_app (h i) _) _

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

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
⊢ False

Tactic:
have := Finset.mem_univ (Fin.last _ : Fin (n + 4))

Goal state after:
case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ univ
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

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

Tactic:
refine ⟨stdSimplex.triangle
    (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
  · simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]
  · simp only [Fin.mk_le_mk, add_le_add_iff_left, one_le_two]
  -- this was produced using `simp? [horn_eq_iSup]`
  simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set,
    Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff,
    Nat.reduceAdd, mem_compl, mem_singleton, exists_prop]
  have hS : ¬ ({i, (⟨k, by lia⟩ : Fin (n + 4)), (⟨k + 1, by lia⟩ : Fin (n + 4)),
      (⟨k + 2, by lia⟩ : Fin (n + 4))} = Finset.univ) := fun hS ↦ by
    obtain ⟨i, hi⟩ := i
    by_cases hk : k = 0
    · subst hk
      have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this
      simp only [Fin.lt_def, Fin.val_last] at hₙ
      lia
    · have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto
  rw [Finset.eq_univ_iff_forall, not_forall] at hS
  obtain ⟨l, hl⟩ := hS
  simp only [mem_insert, mem_singleton, not_or] at hl
  refine ⟨l, hl.1, fun a ↦ ?_⟩
  fin_cases a
  · exact Ne.symm hl.2.1
  · exact Ne.symm hl.2.2.1
  · exact Ne.symm hl.2.2.2

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) s✝))

Tactic:
apply Rel'.inr_inl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : (ConcreteCategory.hom g) s✝ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) w✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
apply Rel'.inr_inl

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

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
hf : ∃ i, MorphismProperty.ofHoms (fun i_1 ↦ Λ[i + 1, i_1].ι) g✝
⊢ HasLiftingProperty g✝ (terminal.from Z)

Tactic:
obtain ⟨n, ⟨i⟩⟩ := hf

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι (terminal.from Z)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃

Tactic:
obtain rfl := H x₃ y₃ hx₃ hy₃ eq
    rfl

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

Goal state before:
pp: case inl
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx✝ : x ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨x, hx✝⟩ ∈ ⊤.obj (op n)
hx : x ∈ ((skeletonOfMono i) d).obj (op n)
⊢ ⟨x, hx✝⟩ ∈ Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))

Tactic:
exact Or.inl ⟨⟨x, hx⟩, rfl⟩

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ ≫ φ).op)) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ

Tactic:
← tr_comp',

Goal state after:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i ≫ φ.hom) ⋯ hₘ).op)) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ
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✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝

Tactic:
change (eHomEquiv V) (P.ι.map (f ≫ g)) = _

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✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eHomEquiv V) (P.ι.map (f ≫ g)) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ P f

Tactic:
suffices generators.multiplicativeClosure ≤ P by
    rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
  intro _ _ f hf
  induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (comp_δ (𝟙 _) i id)
    · simpa using! (comp_σ (𝟙 _) i id)
  | id n => exact id
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (comp_δ f i hrec)
    · simpa using! (comp_σ f i hrec)

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

Goal state before:
pp: case H
y : SimplexCategoryGenRel
n✝ : ℕ
h : (mk n✝).len = y.len
⊢ mk n✝ = y

Tactic:
cases y

Goal state after:
case H.H
n✝¹ n✝ : ℕ
h : (mk n✝¹).len = (mk n✝).len
⊢ mk n✝¹ = mk n✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j) = σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a)

Tactic:
convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind)

Goal state after:
case e'_2.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 2) a) = a

case e'_2.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) j) = j

case e'_3.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1 + 1) (j + 1)) = j + 1

case e'_3.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) a) = a
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ IsLUB x✝ (sSup x✝)

Tactic:
by
    constructor
    · intro K hK _ ht
      exact Or.inl (Set.mem_biUnion hK ht)
    · intro L hL _ ht
      cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v

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

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
intro h i
    by_contra!
    exact i.castSucc_ne_last (h i.castSucc (by simpa))

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

Goal state before:
pp: case pos.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc

pp: case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)

Tactic:
· simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
        constructor
        · obtain hx | rfl := hx.lt_or_eq
          · rwa [Fin.succAbove_of_castSucc_lt]
          · simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
        · intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]

Goal state after:
case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.S
hxy' :
  { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }
⊢ x.IsUniquelyCodimOneFace y

Tactic:
simpa using hxy'.of_iso e.symm

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.castSucc < x.succ

Tactic:
simpa only [Fin.castSucc_lt_succ_iff] using hi.le

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
⊢ P.rank' hy = ⨆ x, P.rank' ⋯ + 1

Tactic:
change P.rank' (Acc.intro y fun _ => hy.inv) = _

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
⊢ P.rank' ⋯ = ⨆ x, P.rank' ⋯ + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
⊢ innerAnodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp
  let sq₁₃ := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom i p
  rw [internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃]
  apply hj
  rw [← innerFibration_iff] at hp ⊢
  exact innerFibration_pullbackObjObjπ sq₁₃

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x : WalkingIso
⊢ C

Tactic:
by induction x; exacts [X, Y]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x.toS = s.x.toS

Tactic:
rw [← s.x.toS.cast_eq_self s.hd, S.ext_iff']

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ ∃ (h : (ht.type₁ ⋯).x.dim = (s.x.cast ⋯).dim), ((ht.type₁ ⋯).x.cast h).simplex = (s.x.cast ⋯).simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
x : X _⦋0⦌
⊢ X.ιChainComplex x ≫ fromChainComplexXZero X R = Sigma.ι (fun x ↦ R) (mk x)

Tactic:
simp [π₀.fromChainComplexXZero, ιChainComplex]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ { hom := pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯,
          inv :=
            (ρ_ X.left).inv ≫
              pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
                (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom),
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      X.hom =
    (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
· refine pushout.hom_ext ?_ (by simp)
    apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ (X □ Arrow.mk (initial.to (𝟙_ C))) ≅ X

Tactic:
refine Arrow.isoMk ?_ (ρ_ X.right) ?_
  · refine Iso.mk ?_ ((ρ_ X.left).inv ≫ pushout.inr _ _) ?_ ?_
    · refine pushout.desc ?_ (ρ_ X.left).hom ?_
      · exact (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to _
      · apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext
    · refine pushout.hom_ext ?_ (by simp)
      apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext
    · simp
  · refine pushout.hom_ext ?_ (by simp)
    apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Goal state after: