mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
⊢ f ≫ g = f ≫ g' → g = g'

Tactic:
h

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ False

Tactic:
apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
    exact lt_of_le_of_ne hle h

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 i) = padicNorm p (↑g i)

Tactic:
h

Goal state after:
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 (↑g i) = padicNorm p (↑g i)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ const (padicNorm p) q ≈ const (padicNorm p) r

Tactic:
heq

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ const (padicNorm p) r ≈ const (padicNorm p) r
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ ↑q = ↑r

Tactic:
h

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ ↑r = ↑r
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 : ι
i j : (glueData hf).J
⊢ yonedaEquiv.symm (yonedaEquiv (yoneda.map (⋯.fst' (f j)) ≫ f i)) =
    yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map ((⋯.fst' (f i)).op ≫ (⋯.symmetry ⋯).op))) (yonedaEquiv (f j)))

Tactic:
Equiv.symm_apply_apply,

Goal state after:
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 : ι
i j : (glueData hf).J
⊢ yoneda.map (⋯.fst' (f j)) ≫ f i =
    yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map ((⋯.fst' (f i)).op ≫ (⋯.symmetry ⋯).op))) (yonedaEquiv (f j)))
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 : ι
i j : (glueData hf).J
⊢ yoneda.map (⋯.fst' (f j)) ≫ f i =
    yonedaEquiv.symm (yonedaEquiv (yoneda.map (⋯.symmetry ⋯) ≫ yoneda.map (⋯.fst' (f i)) ≫ f j))

Tactic:
Equiv.symm_apply_apply,

Goal state after:
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 : ι
i j : (glueData hf).J
⊢ yoneda.map (⋯.fst' (f j)) ≫ f i = yoneda.map (⋯.symmetry ⋯) ≫ yoneda.map (⋯.fst' (f i)) ≫ f j
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
⊢ a ≫ f = b ≫ f → a = b

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ a = b
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ b ≫ f = yoneda.map (𝟙 X) ≫ a ≫ f

Tactic:
by simp [← h]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
⊢ ↑(padicNormE (x✝ - y✝)) = 0 → x✝ = y✝

Tactic:
h

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(padicNormE (x✝ - y✝)) = 0
⊢ x✝ = y✝
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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

Tactic:
rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
    exact ⟨a, by lia⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑n).valuation = ↑(padicValInt p n)

Tactic:
rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ (φ ≫ X.σ ⟨b, ⋯⟩) ≫ X.δ j.succ = 0

Tactic:
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
    zero_comp]
  · intro hj'
    simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right,
      nonpos_iff_eq_zero, add_eq_zero, false_and, reduceCtorEq] at hj
  · dsimp
    rw [Fin.lt_def, Fin.val_succ]
    linarith

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

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ

Tactic:
h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

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

Tactic:
h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ (unop Δ).len = (unop Δ).len
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

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

Tactic:
h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop Δ).len
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

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

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

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f

Tactic:
h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₂.f = Φ₂.f
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₁.f n = Φ₂.f n

Tactic:
h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₂.f n = Φ₂.f n
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (⦋0⦌.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom θ) x = (SimplexCategory.Hom.toOrderHom θ) y → x = y

Tactic:
h

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (⦋0⦌.len + 1)
h : (SimplexCategory.Hom.toOrderHom θ) x = (SimplexCategory.Hom.toOrderHom θ) y
⊢ x = y
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

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

Tactic:
· have := PInfty_f_add_QInfty_f (n + 1) =≫ f
      rw [Category.id_comp] at this
      rw [degeneraciesVanish_succ_iff, ← this]
      simp [hf]

Goal state after:
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
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌))

Tactic:
slice_rhs 1 1 => rw [← id_comp (K[X].d i j)]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    (𝟙 (K[X].X i) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌))
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
⊢ { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } =
    𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)

Tactic:
by
    ext n
    simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f,
      cofan_inj_πSummand_eq_id]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ PInfty.f (unop (Splitting.IndexSet.id (op ⦋n⦌)).fst).len ≫
      P.p.app (Splitting.IndexSet.id (op ⦋n⦌)).fst ≫
        ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj
            (Splitting.IndexSet.id (op ⦋n⦌)) ≫
          (Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app P.X)).f.app (op ⦋n⦌) ≫
            ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫
              P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
dsimp [toKaroubi]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ PInfty.f n ≫
      P.p.app (op ⦋n⦌) ≫
        ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj
            (Splitting.IndexSet.id (op ⦋n⦌)) ≫
          ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).desc (op ⦋n⦌) fun A ↦
              PInfty.f (unop A.fst).len ≫ ((Γ₀.splitting K[P.X]).cofan (op ⦋n⦌)).inj A) ≫
            ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫
              P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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

Tactic:
h

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

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
hx : ↑x ≤ 2⁻¹
⊢ p ⟨if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), ⋯⟩ =
    { toFun := (fun t ↦ if t ≤ 1 / 2 then p.extend (2 * t) else p.symm.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯ }
      x

Tactic:
| inl hx =>

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 ≫ f₁) = G.map (s ≫ f₂)

Tactic:
h

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.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:
by
  apply toHoCat_map_eq
  rw [homRel_iff_rightHomotopyRel]
  apply LeftHomotopyRel.rightHomotopyRel
  rw [← LeftHomotopyClass.mk_eq_mk_iff] at h ⊢
  exact (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence
    (X := X) (g := pResolutionObj Y)).injective h

Goal state after:
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
inst✝ : IsFibrant Y
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
by
  wlog _ : IsCofibrant Y generalizing Y
  · obtain ⟨Y', _, p, _, _⟩ := CofibrantObject.HoCat.exists_resolution Y
    have _ : IsFibrant Y' := isFibrant_of_fibration p
    have hY' := this Y' inferInstance
    simp only [← bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom] at hY' ⊢
    have := Localization.inverts L (weakEquivalences _) p
      (by rwa [← weakEquivalence_iff])
    rw [← Function.Bijective.of_comp_iff _
      (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence _ p)]
    convert! (Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))).bijective.comp hY'
    ext f
    obtain ⟨f, rfl⟩ := f.mk_surjective
    simp
  wlog _ : IsFibrant X generalizing X
  · obtain ⟨X', i, _, _, _⟩ : ∃ (X' : C) (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i ∧
        IsFibrant X' :=
      ⟨_, FibrantObject.HoCat.iResolutionObj X, inferInstance, inferInstance, inferInstance⟩
    have _ := isCofibrant_of_cofibration i
    have hX' := this X' inferInstance
    have := Localization.inverts L (weakEquivalences _) i
      (by rwa [← weakEquivalence_iff])
    rw [← Function.Bijective.of_comp_iff _
      (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence Y i)]
    convert! (Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'
    ext f
    obtain ⟨f, rfl⟩ := f.mk_surjective
    simp
  let E := Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences _)
  let e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
    Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
      (weakEquivalences _)
  have : rightHomotopyClassToHom L =
      (BifibrantObject.HoCat.homEquivRight.trans (E.fullyFaithfulFunctor.homEquiv.trans
        (Iso.homCongr (e.app (.mk X)) (e.app (.mk Y))))) := by
    ext f
    obtain ⟨f, rfl⟩ := RightHomotopyClass.mk_surjective f
    exact (NatIso.naturality_1 e (BifibrantObject.homMk f)).symm
  rw [this]
  exact Equiv.bijective _

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

Goal state before:
pp: case mk
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
inst✝ : IsFibrant Y
w✝ : LeftHomotopyClass X Y
f : X ⟶ Y
⊢ ∃ a, L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)

Tactic:
exact ⟨f, rfl⟩

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

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

Tactic:
rw [cofibrations_op, trivialFibrations_op]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (fibrations C).op.HasFactorization (trivialCofibrations C).op
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
⊢ sq.HasLift

Tactic:
by
  let sq' := sq.map (Over.forget _)
  dsimp at sq'
  exact ⟨⟨{
    l := Over.homMk sq'.lift
      (by rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r])
  }⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
f g : K ⟶ L
⊢ homRel C f g → toHoCat.map f = toHoCat.map g

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
f g : K ⟶ L
h : homRel C f g
⊢ toHoCat.map f = toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
⊢ homRel C f g → bifibrantResolution'.map f = bifibrantResolution'.map g

Tactic:
h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ bifibrantResolution'.map f = bifibrantResolution'.map g
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ Subfunctor.equalizer f g

Tactic:
h

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ A
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i} = Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall] at h ⊢; intro j
    apply Or.imp _ id (h j)
    intro hj
    exact Set.range_comp_subset_range _ _ hj

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
⊢ (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
      (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩ →
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) ⟨y, hy⟩

Tactic:
h

Goal state after:
case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
      (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) ⟨y, hy⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3.«1»
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) ((fun i ↦ i) ⟨1, ⋯⟩) = l

Tactic:
exact Ne.symm hl.2.2.1

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv.symm (yonedaEquiv (Subfunctor.lift (stdSimplex.δ j) ⋯)) ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
Equiv.symm_apply_apply,

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ Subfunctor.lift (stdSimplex.δ j) ⋯ ≫ Λ[n + 1, i].ι = stdSimplex.δ j