mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
  simpa [hk] using padicNorm.values_discrete hk'

Goal state after:
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
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
· rw [J.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map]
    refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)
    obtain ⟨x, rfl⟩ := (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm.surjective x
    obtain ⟨i, y, rfl⟩ := hf Φ x
    refine ⟨Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w}.obj (U i)) i)
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app _ y), ?_⟩
    have := ConcreteCategory.congr_hom
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality (f i)) y
    dsimp at this ⊢
    rw [this, ← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i, Functor.map_comp]
    rfl

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

Goal state before:
pp: case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
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
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom ((pullback.snd f (shrinkYonedaEquiv.symm s) ≫ shrinkYonedaEquiv.symm s).app (op V))) v =
    (ConcreteCategory.hom (F₂.map g.op)) s

Tactic:
dsimp at hv ⊢

Goal state after:
case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
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
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op V)))
      ((ConcreteCategory.hom ((pullback.snd f (shrinkYonedaEquiv.symm s)).app (op V))) v) =
    (ConcreteCategory.hom (F₂.map g.op)) s
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ fst ≫ f = F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p

Tactic:
symm

Goal state after:
case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p = fst ≫ f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε

Tactic:
refine (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ ?_
  have h := Classical.choose_spec (rat_dense' (f i) (div_nat_pos i))
  refine lt_of_lt_of_le h ((div_le_iff₀' <| mod_cast succ_pos _).mpr ?_)
  rw [right_distrib]
  apply le_add_of_le_of_nonneg
  · exact (div_le_iff₀ hε).mp (le_trans (le_of_lt hN) (mod_cast hi))
  · apply le_of_lt
    simpa

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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ ↑⟨a, ⋯⟩ + (q + 1)

Tactic:
simp only [hnaq, add_assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ + ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0

Tactic:
add_eq_zero_iff_eq_neg,

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ =
    -(((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
by
  have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
  have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
  have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
  rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev - (P q).f (n + 1) ≫ (Hσ q).f (n + 1) =
    ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
symm

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev - (P q).f (n + 1) ≫ (Hσ q).f (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (x * y).addValuationDef = x.addValuationDef + y.addValuationDef

Tactic:
simp only [addValuationDef]
  by_cases hx : x = 0
  · rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]
  · by_cases hy : y = 0
    · rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
    · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ q' ∈ {i | ↑i < q + 1}

Tactic:
simp [q']

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

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
· subst h₂
    simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K]

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ N.map (Γ₂N₂.hom.app P) ≫ N₂Γ₂.hom.app (N.obj P) = 𝟙 (N.obj P)

Tactic:
symm

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := ⋯
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := ⋯
⊢ 𝟙 (N.obj P) = N.map (Γ₂N₂.hom.app P) ≫ N₂Γ₂.hom.app (N.obj P)
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⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ f ≫ PInfty.f n = 0

Tactic:
rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_zero]

Goal state after:
case mpr.h
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⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ ∀ (a : IndexSet (op ⦋n⦌)), f ≫ (s.πSummand a ≫ (s.cofan (op ⦋n⦌)).inj a) ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
conv_rhs => rw [← id_comp (s.πSummand _)]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))
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 : ℕ
⊢ PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
symm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))

Tactic:
hom_comp_eq_id

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (Γ₂N₂.natTrans.app P) = inv (N₂Γ₂.inv.app (N₂.obj P))
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
dsimp [toHoCat]; infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
dsimp [toHoCat]; infer_instance

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:
by simp [h.eq_inf]

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤

Tactic:
constructor
  · rintro rfl
    exact ⟨by rfl, (boundary_lt_top n).ne⟩
  · rintro ⟨h₁, h₂⟩
    exact le_antisymm (by rwa [le_boundary_iff]) h₁

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

Goal state before:
pp: case refine_2.inl
⊢ ∀ {i : Fin (2 + 1)} (j : Fin 2), 0 < ↑i → ↑i < 2 → #{i, j.castSucc, j.succ} ≤ 2

Tactic:
decide

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:
rw [← Subfunctor.equalizer_eq_iff]
  apply le_antisymm (Subfunctor.equalizer_le σ₁ σ₂)
  simp only [horn_eq_iSup, iSup_le_iff,
    Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
    ← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]
  intro j hj
  exact (Subfunctor.mem_equalizer_iff σ₁ σ₂ (face i j hj)).2 (by apply h)

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

Goal state before:
pp: case mk.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₁ : X₁
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inl x₁)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inl x₁))

pp: case mk.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inr x₂))

Tactic:
· exact ConcreteCategory.congr_hom h₁ x₁

Goal state after:
case mk.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inr x₂))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
· exact Rel'.inl_inl _ _ h

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

Goal state before:
pp: case inl_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) y₀✝))

pp: case inl_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
w✝¹ w✝ : S
h' : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h'' : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
· exact Rel'.inl_inl _ _ h

Goal state after:
case inl_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
w✝¹ w✝ : S
h' : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h'' : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) y₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

Tactic:
symm

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) y₀))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
symm

Goal state after:
case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 1 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case commg
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case comminl
⊢ (stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₁ ≫ (Iso.refl Λ[2, 0].toSSet).hom

Tactic:
decide

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

Goal state before:
pp: case comminr
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 0].toSSet).hom

Tactic:
decide

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

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ innerFibrations (terminal.from X) ↔ innerFibrations p

Tactic:
symm

Goal state after:
X Y : SSet
p : X ⟶ Y
hY : IsTerminal Y
⊢ innerFibrations p ↔ innerFibrations (terminal.from X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 1).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 0 1 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case commg
⊢ (stdSimplex.faceSingletonIso 1).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 1 2 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case comminl
⊢ (stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₁ ≫ (Iso.refl Λ[2, 1].toSSet).hom

Tactic:
decide

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

Goal state before:
pp: case comminr
⊢ (stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₁₂ ≫ (Iso.refl Λ[2, 1].toSSet).hom

Tactic:
decide

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

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case commg
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 1 2 ⋯).hom

Tactic:
decide

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

Goal state before:
pp: case comminl
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom

Tactic:
decide

Goal state after: