mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property E.shrink

Tactic:
rwa [PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ heq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ (F.map b ≫ p) ≫ (data (F.obj X₀)).f i = F.map c

Tactic:
simp only [assoc, fac, hc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
⊢ ∀ (y : (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯

Tactic:
· intro y hy
      rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
⊢ z = 0

Tactic:
have : (ShortComplex.mk _ _ (cokernel.condition b)).Exact :=
    ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel b)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
⊢ z = 0
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
x : J
h₁ : x ∈ Ici j
h₂ : ⟨b, hb'⟩ < ⟨x, h₁⟩
h₃ : ⟨x, h₁⟩ < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
refine ⟨x, h₂, h₃⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
rw [ofCocone_obj_eq _ _ hi]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
hi : IsMin ⊥
e₁ e₂ : d.Extension val₀ ⊥
h₁ : e₁.val = val₀
h₂ : e₂.val = val₀
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ : e₁.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
h₂ : e₂.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]

Goal state after:
case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ : e₁.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
h₂ : e₂.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
⊢ d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]

Goal state after:
case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
⊢ d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩ =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
⊢ padicValInt p 0 = 0

Tactic:
simp [padicValInt]

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

Goal state before:
pp: p : ℕ
⊢ padicValInt p 1 = 0

Tactic:
simp [padicValInt]

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

Goal state before:
pp: p n : ℕ
⊢ padicValInt p ↑n = padicValNat p n

Tactic:
simp [padicValInt]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f

Tactic:
apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := ⋯
this : IsIso t.arrow
⊢ Arrow.mk ((functor hG (Subobject.mk f) J).map (homOfLE ⋯)) ≅ Arrow.mk f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫ (Subobject.mk f).arrow =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow

Tactic:
Subobject.ofLE_arrow,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).arrow =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p (p ^ n) = n

Tactic:
rw [padicValNat.pow p, padicValNat_self, mul_one]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬p ^ (padicValNat p n + 1) ∣ n

Tactic:
rw [padicValNat_dvd_iff_le hn, not_le]
  exact Nat.lt_succ_self _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : WithZero (Multiplicative ℤ)
⊢ ∃ a, (padicValuation p) a = x

Tactic:
induction x with
  | zero => simp
  | coe x =>
    induction x with | ofAdd x
    simp_rw [Rat.padicValuation, WithZero.exp, Valuation.coe_mk, MonoidWithZeroHom.coe_mk]
    rcases le_or_gt 0 x with (hx | hx)
    · exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩
    · exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩

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

Goal state before:
pp: case pos
p : ℕ
a : ℤ
hp : p = 1
⊢ ↑p ^ padicValInt p a ∣ a

pp: case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
· rw [hp, Nat.cast_one, one_pow]; exact one_dvd _

Goal state after:
case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
⊢ ∀ {X_1 : Schemeᵒᵖ} (x y : ToType ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj X_1)),
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) x =
        (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) y →
      Presheaf.equalizerSieve x y ∈ zariskiTopology (unop X_1)

Tactic:
by
    rintro ⟨U⟩ (α β : U ⟶ _) h
    replace h : (yonedaGluedToSheaf hf).hom.app _ α = (yonedaGluedToSheaf hf).hom.app _ β := h
    have mem := (glueData hf).openCover.mem_grothendieckTopology
    refine GrothendieckTopology.superset_covering _ ?_
      (zariskiTopology.intersection_covering (zariskiTopology.pullback_stable α mem)
        (zariskiTopology.pullback_stable β mem))
    rintro V (γ : _ ⟶ U) ⟨⟨W₁, a, _, ⟨i⟩, fac₁⟩, ⟨W₂, b, _, ⟨j⟩, fac₂⟩⟩
    change γ ≫ α = γ ≫ β
    replace h : (yonedaGluedToSheaf hf).hom.app _ (γ ≫ α) =
        (yonedaGluedToSheaf hf).hom.app _ (γ ≫ β) := by dsimp at h; simp [h]
    rw [← fac₁, ← fac₂] at h ⊢
    apply comp_toGlued_eq
    simpa [Scheme.GlueData.openCover_X, yonedaEquiv_naturality] using h

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) < ε / 3 + ε / 3
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3

Tactic:
simpa only [sub_add_sub_cancel]

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (P 0).f (n + 1) = φ

Tactic:
simp only [P_zero]

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (𝟙 K[X]).f (n + 1) = φ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
by
      have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
      rw [eq_padicNorm]
      norm_cast
      -- Porting note: `Nat.cast_zero` instead of another `norm_cast` call
      rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
        padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast]
      apply inv_le_one_of_one_le₀
      norm_cast
      apply one_le_pow
      exact hp.1.pos

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

Goal state before:
pp: case zero
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n : ℕ
⊢ G.map ((P 0).f n) = (P 0).f n

Tactic:
simp only [P_zero]

Goal state after:
case zero
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n : ℕ
⊢ G.map ((𝟙 K[X]).f n) = (𝟙 K[((whiskering C D).obj G).obj X]).f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0

Tactic:
by
  rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]

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

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X).f 0 ≫ 𝟙 (X.obj (Opposite.op { len := 0 })) = (inclusionOfMooreComplexMap X).f 0

Tactic:
simp only [comp_id]

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

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X =
    ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            N₁ ⋙
              (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
        P).X

pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
                P).d
            i j

Tactic:
· ext n
      · rfl
      · dsimp
        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
                P).d
            i j
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
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          ((toKaroubi (SimplicialObject C)).obj X).decompId_p

Tactic:
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
    NatTrans.comp_app]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }
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 X✝)⁻¹ = f Z✝ * (f Y✝)⁻¹ * f Y✝ * (f X✝)⁻¹

Tactic:
mul_left_inj,

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✝ * (f Y✝)⁻¹ * f Y✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ mk p₁ = mk p₂

Tactic:
replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)

Goal state after:
case mpr
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₁ = mk p₂
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
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ toHoCat.map (homMk f) = toHoCat.map (homMk g)

Tactic:
apply toHoCat_map_eq

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X : C
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ homRel C (homMk f) (homMk 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 : C
⊢ LeftHomotopyRel (resolutionMap (𝟙 X) ≫ pResolutionObj X) (𝟙 (mk (resolutionObj X)).obj ≫ pResolutionObj X)

Tactic:
simpa using .refl _

Goal state after:
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 .refl _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f g : X ⟶ Y
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom

Tactic:
homRel_iff_rightHomotopyRel,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f g : X ⟶ Y
⊢ RightHomotopyRel f.hom g.hom ↔ LeftHomotopyRel f.hom g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject.HoCat C
f g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map f =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map g
⊢ f = g

Tactic:
obtain ⟨Y, rfl⟩ := BifibrantObject.toHoCat_obj_surjective Y
  obtain ⟨f, rfl⟩ := BifibrantObject.toHoCat.map_surjective f
  obtain ⟨g, rfl⟩ := BifibrantObject.toHoCat.map_surjective g
  change toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g) at h
  rw [CofibrantObject.toHoCat_map_eq_iff,
    CofibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff] at h
  rw [BifibrantObject.toHoCat_map_eq_iff,
    BifibrantObject.homRel_iff_rightHomotopyRel,
    ← RightHomotopyClass.mk_eq_mk_iff]
  apply (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    _ (iBifibrantResolutionObj X).hom).1
  simpa using! h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : BifibrantObject C
f : X₁ ⟶ X₂
⊢ f ≫ BifibrantObject.homMk (mk X₂.obj).iBifibrantResolutionObj.hom =
    BifibrantObject.homMk (mk X₁.obj).iBifibrantResolutionObj.hom ≫
      bifibrantResolutionMap (BifibrantObject.ιCofibrantObject.map f)

Tactic:
have := (ObjectProperty.ι _).congr_map
          (bifibrantResolutionMap_fac (CofibrantObject.homMk f.hom)).symm
        ext : 1
        dsimp
        exact this

Goal state after: