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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b

Tactic:
padicValInt

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖x * ↑p ^ n‖ = 1

Tactic:
padicNormE.mul,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖x‖ * ‖↑p ^ n‖ = 1
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → IsIso c.fst

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ IsIso c.fst → c.fst = c.snd

Tactic:
· intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
    · simp only [assoc, hφ₁, id_comp, comp_id]
    · simp only [assoc, hφ₂, id_comp, comp_id, h]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ IsIso c.fst → c.fst = c.snd
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesColimit (span f f) (F i)
inst✝ : HasPushout f f
⊢ Epi f

Tactic:
by
  have hc := pushoutIsPushout f f
  rw [epi_iff_isIso_inl hc, h.isIso_iff]
  intro i
  exact (epi_iff_isIso_inl ((isColimitMapCoconePushoutCoconeEquiv (F i) pushout.condition).1
    (isColimitOfPreserves (F i) hc))).1 (hf i)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ (pbRepr.hom ≫ pullback.fst g g') ≫ g = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g')) ≫ g'

Tactic:
by simp [pullback.condition]

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 φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]

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 φ
hqn : n < q
⊢ φ ≫
      ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ hσ' q n (n + 1) ⋯ +
        hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) =
    0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ¬f ≈ 0

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ¬f - 0 ≈ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
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.NumberTheory.Padics.PadicNumbers

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

Tactic:
min_eq_left,

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

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else ↑x.valuation) ≤ ⊤
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
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : ⦋n✝⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map α.op ≫ X.σ i ≫ PInfty.f (n✝ + 1) = 0

Tactic:
σ_comp_PInfty,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : ⦋n✝⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map α.op ≫ 0 = 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)
⊢ ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0

Tactic:
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)

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⦌))
⊢ ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case h_p
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (PInfty.f n ≫ P.p.app (op ⦋n⦌)) ≫ 𝟙 (P.X _⦋n⦌) = 𝟙 (P.X _⦋n⦌) ≫ (PInfty.f n).f

Tactic:
simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ = Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀

Tactic:
ext K : 3
  simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]
  exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0

Tactic:
(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁,

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ 0 ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op = 0

case neg.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ F (t, x) = f₁ x

Tactic:
by
  rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))

Tactic:
apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun

Goal state after:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ

Tactic:
use p

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ
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_1 Y_1 : FundamentalGroupoid X⦄ (f_1 : X_1 ⟶ Y_1),
    (map f).map f_1 ≫ ⟦H.evalAt Y_1.as⟧ = ⟦H.evalAt X_1.as⟧ ≫ (map g).map f_1

Tactic:
by
    rintro ⟨x⟩ ⟨y⟩ p
    rcases Path.Homotopic.Quotient.mk_surjective p with ⟨p, rfl⟩
    simp only [map_map, Path.Homotopic.Quotient.mk''_eq_mk, comp_eq,
      ← Path.Homotopic.Quotient.mk_map, ← Path.Homotopic.Quotient.mk_trans]
    rw [Path.Homotopic.Quotient.eq]
    exact .map_trans_evalAt _ _

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

Goal state before:
pp: case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (((π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            𝟙
              ((π.map (TopCat.ofHom H.uliftMap)).obj
                ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 0 } }, { as := x₁ })))) ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]

Goal state after:
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' 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 Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject C)) f g

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject C)) f g
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (((π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            𝟙
              ((π.map (TopCat.ofHom H.uliftMap)).obj
                ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 1 } }, { as := x₀ })))) ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]

Goal state after:
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (CofibrantObject C))

Tactic:
by
  rintro X Y f g h
  obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
  let L := (weakEquivalences (CofibrantObject C)).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map (homMk P.p₀) = L.map (homMk P.p₁) by
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp, this]
  have := Localization.inverts L (weakEquivalences _) (homMk P.ι) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)
  simp only [← cancel_epi (L.map (homMk P.ι)), ← L.map_comp, homMk_homMk, P.ι_p₀, P.ι_p₁]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h : homRel C f g
⊢ F.map f = F.map g

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
⊢ F.map f = F.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (cofibrations Cᵒᵖ).IsStableUnderRetracts

Tactic:
by
  rw [cofibrations_op]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations (Over S)).HasFactorization (trivialFibrations (Over S))

Tactic:
rw [cofibrations_over_def, trivialFibrations_over_eq]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations C).over.HasFactorization (trivialFibrations C).over
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

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
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
⊢ ModelCategory C

Tactic:
have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by
    simpa [fibration_iff, h₂] using hf

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
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
⊢ ModelCategory C
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl

Tactic:
dif_pos rfl,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ eqToHom ⋯ ≫ s.inl = s.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: case inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.fst default) ≫ m = c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s)

Tactic:
simpa [h₁] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
let S : Finset (Fin (n + 3)) := {i, j 0}

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
⊢ False

Tactic:
have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f

Goal state after:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
this : n + 1 ≤ m
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f

Tactic:
HomotopicalAlgebra.cofibration_iff

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk

Tactic:
← cancel_mono (Subcomplex.ι _),

Goal state after:
case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 2 (by simp)).hom,
          ← Category.assoc]

Goal state after:
case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv) ≫ f₁ =
    (((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv) ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
x y : ↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X✝)
f : x ⟶ y
⊢ ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).map f =
    Eq.recOn ⋯ (Eq.recOn ⋯ (((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).map f))

Tactic:
by
      obtain ⟨f, rfl, rfl⟩ := f
      dsimp [ofNerve₂, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso,
        Quiv.isoOfEquiv, nerveHomEquiv_apply]
      simp only [comp_id, id_comp]
      rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg X✝
X Y : C
i : X✝ ⟶ Y✝
hi : W₂ i
h : r.degHom f = r.deg X✝
hp : W₁ (𝟙 X✝)
fac : 𝟙 X✝ ≫ i = f
⊢ i = f

Tactic:
simpa using fac

Goal state after: