mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Q (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
Q_succ,

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
⊢ (Q q - P q ≫ Hσ q).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg.e_a.e_s
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, ⋯⟩
⊢ {i | ↑i < q + 1}.erase q' = {i | ↑i < q}

Tactic:
· ext ⟨i, hi⟩
        simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
        lia

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ ↑⟨a, ⋯⟩.succ < ↑j.succ

Tactic:
simpa using

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
⊢ a < ↑j
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ x✝¹.valuation ≤ (x✝¹ + x✝).valuation ∨ x✝.valuation ≤ (x✝¹ + x✝).valuation

Tactic:
simpa using

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ x✝¹.valuation ≤ (x✝¹ + x✝).valuation ∨ x✝.valuation ≤ (x✝¹ + x✝).valuation
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 α }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁ : Δ₁.len = Δ₂.len ∧ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩)) ≍ ⇑(Hom.toOrderHom (e ⟨op Δ₂, α₂⟩))
⊢ Δ₁.len = Δ₂.len

Tactic:
simpa using

Goal state after:
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 α }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁ : Δ₁.len = Δ₂.len ∧ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩)) ≍ ⇑(Hom.toOrderHom (e ⟨op Δ₂, α₂⟩))
⊢ Δ₁.len = Δ₂.len
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
⊢ False

Tactic:
simpa using

Goal state after:
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
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty.f 0 =
    (((dNext 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) + (prevD 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f 0

Tactic:
simpa using

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (K[X].X 0) = (homotopyPToId X (0 + 1 + 1)).hom 0 (0 + 1) ≫ K[X].d (0 + 1) 0 + (𝟙 K[X]).f 0
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) =
    (((dNext (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
        (prevD (n + 1)) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f (n + 1)

Tactic:
simpa using

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (P (n + 1 + 1)).f (n + 1) =
    K[X].d (n + 1) n ≫ (homotopyPToId X (n + 1 + 1)).hom n (n + 1) +
        (homotopyPToId X (n.succ + 1)).hom n.succ (n.succ + 1) ≫ K[X].d (n + 1 + 1) (n + 1) +
      𝟙 (K[X].X (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInftyToNormalizedMooreComplex X = 𝟙 ((normalizedMooreComplex A).obj X)

Tactic:
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f (n + 1) ≫ f = 0

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Goal state after:
case succ.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ QInfty.f (n + 1) ≫ f = 0

case succ.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : QInfty.f (n + 1) ≫ f = 0
⊢ DegeneraciesVanish f
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 : Karoubi (HomologicalComplex C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n
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 ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (K.d i j).f ≫ (K.d j k).f = 0

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (K.d i j).f ≫ (K.d j k).f = 0
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi (Karoubi C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi (Karoubi C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)

Tactic:
simpa using

Goal state after:
case h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬i = 0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
h : Isδ₀ (SimplexCategory.δ j.succ)
⊢ j.succ = 0

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
h : Isδ₀ (SimplexCategory.δ j.succ)
⊢ j.succ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ PInfty.f (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0

Tactic:
exact (HigherFacesVanish.of_P (m + 1) m).comp_δ_eq_zero j h₂ (by lia)

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

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using

Goal state after:
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
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
⊢ s.toKaroubiNondegComplexIsoN₁.hom.f ≫ PInfty = s.toKaroubiNondegComplexIsoN₁.hom.f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ s.toKaroubiNondegComplexIsoN₁.hom.f ≫ PInfty = s.toKaroubiNondegComplexIsoN₁.hom.f
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
⊢ IsIso Γ₂N₂.natTrans

Tactic:
have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) := by
    intro P
    have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
    exact isIso_of_reflects_iso _ N₂

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
this : ∀ (P : Karoubi (SimplicialObject C)), IsIso (Γ₂N₂.natTrans.app P)
⊢ IsIso Γ₂N₂.natTrans
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: X✝ Y✝ : MonCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toCat.map a₁✝ = toCat.map a₂✝
⊢ Hom.hom a₁✝ = Hom.hom a₂✝

Tactic:
simpa using

Goal state after:
X✝ Y✝ : MonCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toCat.map a₁✝ = toCat.map a₂✝
⊢ Hom.hom a₁✝ = Hom.hom a₂✝
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 using

Goal state after:
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
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
⊢ map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid Y)

Tactic:
simpa using

Goal state after:
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
⊢ map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid Y)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
⊢ Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x

Tactic:
simpa using

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
⊢ (mk p₁).trans (mk p₂).symm = Path.Homotopic.Quotient.refl x
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ ≍ ⟦p₂⟧

Tactic:
obtain rfl : x₁ = x₃ := by convert! hp 1 <;> simp

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ ≍ ⟦p₂⟧
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
by
  rw [simply_connected_iff_paths_homotopic']
  constructor
  · -- Forward: all paths homotopic implies all loops null-homotopic
    intro ⟨hpc, hall⟩
    exact ⟨hpc, fun x γ => hall γ (Path.refl x)⟩
  · -- Backward: all loops null-homotopic implies all paths homotopic
    intro ⟨hpc, hloops⟩
    refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
    -- Work in the quotient where structural steps can be done by simp
    rw [← eq]
    replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)
    have h : trans ⟦p₁⟧ (symm ⟦p₂⟧) = refl x := by
      simpa using hloops x (p₁.trans p₂.symm)
    calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ x ∈ s
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

Tactic:
constructor
    · apply mul_nonneg <;> grind
    · rw [mul_assoc]
      apply mul_le_one₀ <;> grind

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

Goal state before:
pp: 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 Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this✝ : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = s ≫ adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)

Tactic:
rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]

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

Goal state before:
pp: 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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ G.IsLocalization W

Tactic:
simpa using

Goal state after:
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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ G.IsLocalization W
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ LeftHomotopyRel (resolutionMap (𝟙 X) ≫ pResolutionObj X) (𝟙 (mk (resolutionObj X)).obj ≫ pResolutionObj X)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ LeftHomotopyRel (pResolutionObj X) (pResolutionObj X)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ LeftHomotopyRel (resolutionMap (f ≫ g) ≫ pResolutionObj X₃)
    (((homMk (resolutionMap f)).hom ≫ (homMk (resolutionMap g)).hom) ≫ pResolutionObj X₃)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ LeftHomotopyRel (pResolutionObj X₁ ≫ f ≫ g) (pResolutionObj X₁ ≫ f ≫ g)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences C x✝
⊢ (weakEquivalences (HoCat C)).inverseImage resolution x✝

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences C x✝
⊢ WeakEquivalence x✝
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R : (localizerMorphism C).LeftResolution X
⊢ WeakEquivalence R.w

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R : (localizerMorphism C).LeftResolution X
⊢ weakEquivalences C R.w
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)
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
Y : C
inst✝ : IsFibrant Y
h✝ : IsCofibrant Y
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
wlog _ : IsFibrant X generalizing X

Goal state after:
case inr
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
⊢ Function.Bijective (rightHomotopyClassToHom L)

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✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
⊢ Function.Bijective (rightHomotopyClassToHom L)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
x✝³ x✝² : BifibrantObject C
x✝¹ x✝ : x✝³ ⟶ x✝²
h : homRel C x✝¹ x✝
⊢ (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝¹ =
    (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
x✝³ x✝² : BifibrantObject C
x✝¹ x✝ : x✝³ ⟶ x✝²
h : homRel C x✝¹ x✝
⊢ LeftHomotopyRel x✝¹.hom x✝.hom