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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hr]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : r = 0
⊢ padicNorm p (q / r) = padicNorm p q / padicNorm p r

Tactic:
simp [hr]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
have h1 := min_le_padicValRat_add (p := p) hqr
  have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)
  have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)
  rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
  rw [add_comm] at h3
  omega

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
by
  have h1 := min_le_padicValRat_add (p := p) hqr
  have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)
  have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)
  rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
  rw [add_comm] at h3
  omega

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = ↑p ^ (-↑x.valuation)

Tactic:
by
  simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]

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

Goal state before:
pp: p : ℕ
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
by
  by_cases hp : p = 1
  · rw [hp, Nat.cast_one, one_pow]; exact one_dvd _
  rw [padicValInt_dvd_iff_of_ne_one hp]
  exact Or.inr le_rfl

Goal state after:
Module: Mathlib.CategoryTheory.Types.Epimorphisms

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

Tactic:
obtain ⟨y, hy⟩ := hr (b x)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max f.norm g.norm = g.norm

Tactic:
rw [hcl]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max 0 g.norm = g.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ max f.norm g.norm = f.norm

Tactic:
rw [hcl]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ max f.norm 0 = f.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ ∀ (k : ℕ), padicNorm p (↑g k) = padicNorm p (↑f k)

Tactic:
by simp only [h, forall_const]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
hpg : padicNorm p (↑g (stationaryPoint hg)) = padicNorm p (↑g i)
⊢ padicNorm p (↑f (stationaryPoint ⋯)) = padicNorm p (↑g (stationaryPoint ⋯))

Tactic:
rw [hpf, hpg, h]

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

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ q

Tactic:
induction q using Quotient.inductionOn

Goal state after:
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
r : ℚ_[p]
a✝ : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ ⟦a✝⟧
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ 0 ≫ eqToHom ⋯ = 0

Tactic:
exact zero_comp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ Hσ q = Hσ q ≫ (alternatingFaceMapComplex C).map f

Tactic:
by
    unfold Hσ
    rw [nullHomotopicMap'_comp, comp_nullHomotopicMap']
    congr
    ext n m hnm
    simp only [alternatingFaceMapComplex_map_f, hσ'_naturality]

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

Goal state before:
pp: case mp
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 φ

pp: case mpr
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⦌
⊢ HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ

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

Goal state after:
case mpr
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⦌
⊢ HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ (Q (q + 1)).f n = (Q q).f n

Tactic:
simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]

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

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⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ (𝟙 (X _⦋n + 1⦌) + (Hσ q).f (n + 1))) ≫ X.δ j.succ = 0

Tactic:
simp only [comp_add, add_comp, comp_id]

Goal state after:
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⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ φ ≫ X.δ j.succ + (φ ≫ (Hσ q).f (n + 1)) ≫ X.δ j.succ = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ α₂ : { α // Epi α }
h₁ : Δ₁.len = Δ₁.len ∧ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩)) ≍ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₂⟩))
⊢ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩ ≫ eqToHom ⋯)) = ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₂⟩))

Tactic:
exact eq_of_heq h₁.2

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

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → A.fst = Δ

Tactic:
intro h
    rw [← unop_inj_iff]
    ext
    exact h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = K.d Δ.len Δ'.len

Tactic:
by
  unfold mapMono
  suffices Δ ≠ Δ' by
    simp only [dif_neg this, dif_pos hi]
  rintro rfl
  simpa only [left_eq_add, Nat.one_ne_zero] using hi.1

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

Goal state before:
pp: case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝

Tactic:
rw [ih]

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

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l

Tactic:
rw [ih]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
set G : C(I × I, Y) := F.toContinuousMap.comp (.prodMap (.id _) p)
  set p₁ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans (.refl _) .id) (.trans .id (.refl _))
  set p₂ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans .id (.refl _)) (.trans (.refl _) .id)
  set Fsq : p₁.Homotopy p₂ :=
    Path.Homotopic.prodHomotopy (.trans (.reflTrans _) (.symm <| .transRefl _))
      (.trans (.transRefl _) (.symm <| .reflTrans _))
  refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
  all_goals aesop (add simp Path.trans_apply)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x }.as { as := y }.as
⊢ Path.Homotopic.Quotient.mk ((p.map (⋯ : Continuous ⇑f)).trans (H.evalAt y)) =
    Path.Homotopic.Quotient.mk ((H.evalAt x).trans (p.map (⋯ : Continuous ⇑g)))

Tactic:
Path.Homotopic.Quotient.eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x }.as { as := y }.as
⊢ ((p.map (⋯ : Continuous ⇑f)).trans (H.evalAt y)).Homotopic ((H.evalAt x).trans (p.map (⋯ : Continuous ⇑g)))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case η
X✝ : Type u_1
Y✝ : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y✝
f g : C(X✝, Y✝)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hequiv : X ≃ₕ Y
⊢ 𝟭 (FundamentalGroupoid X) ≅ map hequiv.toFun ⋙ map hequiv.invFun

Tactic:
simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂

Tactic:
← G.map_comp,

Goal state after:
case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map (s ≫ f₁) = G.map s ≫ G.map f₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map (s ≫ f₁) = G.map s ≫ G.map f₂

Tactic:
← G.map_comp,

Goal state after:
case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map (s ≫ f₁) = G.map (s ≫ f₂)
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences (Over S)).IsStableUnderRetracts

Tactic:
weakEquivalences_over_def,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences C).over.IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences (Over S)).HasTwoOutOfThreeProperty

Tactic:
weakEquivalences_over_def,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences C).over.HasTwoOutOfThreeProperty
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ (ConcreteCategory.hom ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌))) (stdSimplex.objEquiv.symm q) ∈
    (Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))).obj (op ⦋m⦌)

Tactic:
← Subcomplex.ofSimplex_le_iff

Goal state after:
case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Subcomplex.ofSimplex
      ((ConcreteCategory.hom ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌))) (stdSimplex.objEquiv.symm q)) ≤
    Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
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₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
y₁ : c₁.pt
j : J
x₁ : F₁.obj j
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) y₁
⊢ ∃ j_1 x₁' y₁', (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j_1)) x₁' ∧ y₁ = (hom (c₁.ι.app j_1)) y₁'

Tactic:
obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁

Goal state after:
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₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ : F₁.obj j
l : J
y₁ : F₁.obj l
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) ((hom (c₁.ι.app l)) y₁)
⊢ ∃ j_1 x₁' y₁', (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j_1)) x₁' ∧ (hom (c₁.ι.app l)) y₁ = (hom (c₁.ι.app j_1)) y₁'
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case refine_1
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
⊢ ∃ i_1 a, (0 < a ∧ a < Fin.last (i_1 + 2)) ∧ Arrow.mk Λ[n + 2, i].ι = Arrow.mk Λ[i_1 + 2, a].ι

Tactic:
use n, i

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

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ sx.spineToDiagonal (X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (ConcreteCategory.hom (X.map (diag 2).op)) ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
⊢ (fun x ↦
        { app := fun X ↦ ↾fun a ↦ { app := fun Y f ↦ x.app Y ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ },
          naturality := ⋯ })
      ((fun φ ↦
          { app := fun X a ↦ ((ConcreteCategory.hom (φ.app X)) a).app X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ })
        φ) =
    φ

Tactic:
ext X a Y f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X : C
a : A.obj X
Y : C
f : X ⟶ Y
⊢ ((ConcreteCategory.hom
              (((fun x ↦
                      {
                        app := fun X ↦
                          ↾fun a ↦ { app := fun Y f ↦ x.app Y ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ },
                        naturality := ⋯ })
                    ((fun φ ↦
                        {
                          app := fun X a ↦
                            ((ConcreteCategory.hom (φ.app X)) a).app X (𝟙 (Opposite.unop (Opposite.op X))),
                          naturality := ⋯ })
                      φ)).app
                X)).toFun
          a).app
      Y f =
    ((ConcreteCategory.hom (φ.app X)).toFun a).app Y f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
f : (nerveFunctor₂.obj X✝).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })
⊢ ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ } =
    Eq.recOn ⋯ (Eq.recOn ⋯ (((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ }))

Tactic:
dsimp [ofNerve₂, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso,
        Quiv.isoOfEquiv, nerveHomEquiv_apply]

Goal state after:
X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
f : (nerveFunctor₂.obj X✝).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })
⊢ 𝟙
        (ComposableArrows.left
          ((oneTruncation₂.map (nerveFunctor₂.map F)).obj
            ((ConcreteCategory.hom
                ((nerveFunctor₂.obj X✝).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op))
              f))) ≫
      ComposableArrows.hom
          ((oneTruncation₂.map (nerveFunctor₂.map F)).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ }).edge ≫
        𝟙
          (ComposableArrows.right
            ((oneTruncation₂.map (nerveFunctor₂.map F)).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ }).edge) =
    (ReflQuiv.forget.map F).map
      (𝟙
          (ComposableArrows.left
            ((ConcreteCategory.hom
                ((nerveFunctor₂.obj X✝).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op))
              f)) ≫
        ComposableArrows.hom f ≫ 𝟙 (ComposableArrows.right f))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ ⊤ ≤ W

Tactic:
rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]
    rintro _ _ _ ⟨_, _, e⟩
    exact hW e

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

Goal state before:
pp: case of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
⊢ P (σ i)

Tactic:
· simpa using! (σ_comp (𝟙 _) i id)

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

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

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Goal state after:
case inl.inl
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ j x' : SimplexCategoryGenRel
g : x✝ ⟶ j
g' : j ⟶ x'
hg : degeneracies.multiplicativeClosure g
hg' : degeneracies g'
h_rec : ∃ L m b, ∃ (h₁ : mk m = j) (h₂ : x✝ = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ g = standardσ L ⋯
⊢ ∃ L m b, ∃ (h₁ : mk m = x') (h₂ : x✝ = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ g ≫ g' = standardσ L ⋯

Tactic:
| @comp_of _ j x' g g' hg hg' h_rec =>

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

Goal state before:
pp: case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
rw [← epi_iff_surjective] at h₁

Goal state after:
case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Epi f.hom
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f