mathlib-initiative/mathlib-tactics huggingface dataset:
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ X.σ 0 ≫ ((-1) ^ ↑0 • X.δ 0) + φ ≫ X.σ 0 ≫ ((-1) ^ ↑(Fin.succ 0) • X.δ (Fin.succ 0)) = 0

pp: case neg.h
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
hqn' : ¬n + 1 < q
⊢ ∀ (a : Fin (n + 1)), φ ≫ X.σ 0 ≫ ((-1) ^ ↑a.succ.succ • X.δ a.succ.succ) = 0

Tactic:
· simp only [Fin.val_zero, Fin.val_succ, Fin.val_castSucc, zero_add, pow_zero, one_smul,
        pow_one, neg_smul, comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ,
        add_neg_cancel]

Goal state after:
case neg.h
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
hqn' : ¬n + 1 < q
⊢ ∀ (a : Fin (n + 1)), φ ≫ X.σ 0 ≫ ((-1) ^ ↑a.succ.succ • X.δ a.succ.succ) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
simp_all [inv_le_inv₀]

Goal state after:
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
⊢ 0 ≤ max 0 (exp (-x✝.valuation))

Tactic:
simp_all [inv_le_inv₀]

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

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

Tactic:
simp_all [inv_le_inv₀]

Goal state after:
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
⊢ 0 ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))

Tactic:
simp_all [inv_le_inv₀]

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

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

Tactic:
simp_all [inv_le_inv₀]

Goal state after:
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
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max 0 (exp (-x✝.valuation))

Tactic:
simp_all [inv_le_inv₀]

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

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ ((-1) ^ ↑0 • X.δ 0 + (-1) ^ ↑1 • X.δ 1) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0

Tactic:
Fin.sum_univ_succ,

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ ((-1) ^ ↑0 • X.δ 0 + (-1) ^ ↑1 • X.δ 1) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ((-1) ^ ↑0 • X.δ 0 + ∑ i, (-1) ^ ↑i.succ • X.δ i.succ)) =
    0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
simp_all [inv_le_inv₀]

Goal state after:
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
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))

Tactic:
simp_all [inv_le_inv₀]

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.DoldKan.Faces

Goal state before:
pp: case neg.inr.H
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
ham'' : a = m
⊢ ⟨a + 1, ⋯⟩ = j.castSucc

Tactic:
ext
      cases j
      dsimp
      dsimp only [Nat.succ_eq_add_one] at *
      lia

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

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

Tactic:
rw [← unop_inj_iff]

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

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → Mono A.e

pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono A.e → A.EqId

Tactic:
· intro h
    dsimp at h
    subst h
    dsimp only [id, e]
    infer_instance

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono A.e → A.EqId
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
⊢ mapMono K (𝟙 Δ) = 𝟙 (K.X Δ.len)

Tactic:
by
  unfold mapMono
  simp only [eqToHom_refl, dite_eq_ite, if_true]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
n : ℕ
hn : IsIso (f.app (op ⦋n⦌))
⊢ IsIso (f.app (op ⦋n + 1⦌))

Tactic:
use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }

Goal state after:
case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
n : ℕ
hn : IsIso (f.app (op ⦋n⦌))
⊢ f.app (op ⦋n + 1⦌) ≫
        { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1), b := fun i ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i }.φ =
      𝟙 (X _⦋n + 1⦌) ∧
    { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1), b := fun i ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i }.φ ≫
        f.app (op ⦋n + 1⦌) =
      𝟙 (Y _⦋n + 1⦌)
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
| _ m
   => 

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
⊢ PInfty.f n ≫ X.map i.op = 0
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
X : SimplicialObject C
⊢ ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫
      (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X =
    (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
Compatibility.υ_hom_app,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫
      Preadditive.DoldKan.equivalence.unitIso.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
        Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    (𝟙 (N₁ ⋙ Γ₂)).app X
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
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ (((N₁ ⋙ Γ₂).obj X).X.map θ ≫ (Γ₀.splitting K[X]).desc Δ' fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) =
    ((Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫
      ((toKaroubi (SimplicialObject C)).obj X).X.map θ

Tactic:
by
            apply (Γ₀.splitting K[X]).hom_ext'
            intro A
            change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _
            simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc,
              Splitting.ι_desc]
            erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]
            dsimp only [toKaroubi]
            simp only [← X.map_comp]
            congr 2
            simp only [← op_comp]
            exact Quiver.Hom.unop_inj (A.fac_pull θ)

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

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
by
  rw [Hom.cast_eq_iff_heq]
  exact hom_heq_of_cons_eq_cons h

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

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

Tactic:
apply mul_le_one₀

Goal state after:
case pos.right.ha
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case hb₀
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.2

case hb
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 2 * ↑x.2 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg.right
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ≤ 1

Tactic:
apply mul_le_one₀

Goal state after:
case neg.right.ha
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 ≤ 1

case hb₀
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.2

case hb
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 2 - 2 * ↑x.2 ≤ 1
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)
⊢ f ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.s =
    s ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.f

Tactic:
have := adj.unit.naturality s

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₁
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 : (𝟭 C₁).map s ≫ adj.unit.app X = adj.unit.app T ≫ (G ⋙ F).map s
⊢ f ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.s =
    s ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.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 : CofibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
by
  dsimp
  rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]
  infer_instance

Goal state after:
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)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((cofibrations D).inverseImage e.functor).HasFactorization (trivialFibrations C)

Tactic:
h₂'

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)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((cofibrations D).inverseImage e.functor).HasFactorization ((trivialFibrations D).inverseImage e.functor)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ ∀ (n_1 : ℕ) (x : ↑(Δ[n + 1].nonDegenerate n_1)), ↑x ∈ A.obj (op ⦋n_1⦌) → ↑x ∈ Λ[n + 1, i].obj (op ⦋n_1⦌)

Tactic:
intro d x hx

Goal state after:
case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : ↑(Δ[n + 1].nonDegenerate d)
hx : ↑x ∈ A.obj (op ⦋d⦌)
⊢ ↑x ∈ Λ[n + 1, i].obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
⊢ ∃ j, S = {j}ᶜ

Tactic:
by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij

Tactic:
← cancel_epi (stdSimplex.faceSingletonComplIso.{u} j).hom,

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).hom ≫ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij =
    (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        x₁ = (ConcreteCategory.hom f) x₀ ∧ x₁ = (ConcreteCategory.hom f) y₀

pp: case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) y₀✝ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) x₀ ∧
          (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀

Tactic:
· exact Or.inl rfl

Goal state after:
case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) y₀✝ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) x₀ ∧
          (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case mk
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m⦌, property := hm }))).toFun x

Tactic:
| _ m
   => 

Goal state after:
case mk
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m⦌, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ f.vertex j = g.vertex j

Tactic:
rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.succ)

Tactic:
simp only [← f.arrow_tgt i]

Goal state after:
n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ })))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (f.arrow i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ).op)) ((ConcreteCategory.hom (X.map φ.op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp',
    SimplexCategory.const_comp]

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

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i ≫ subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
const_subinterval_eq

Goal state after:
case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ (α_ (F.obj (P ⟶[V] Q)) (F.obj (Q ⟶[V] R)) (F.obj (R ⟶[V] S))).inv ≫
      (μ F (P ⟶[V] Q) (Q ⟶[V] R) ≫ F.map (eComp V P Q R)) ▷ F.obj (R ⟶[V] S) ≫
        μ F (P ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)

Tactic:
comp_whiskerRight,

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ (α_ (F.obj (P ⟶[V] Q)) (F.obj (Q ⟶[V] R)) (F.obj (R ⟶[V] S))).inv ≫
      (μ F (P ⟶[V] Q) (Q ⟶[V] R) ▷ F.obj (R ⟶[V] S) ≫ F.map (eComp V P Q R) ▷ F.obj (R ⟶[V] S)) ≫
        μ F (P ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : ⟦f.comp g⟧ = ⟦h⟧
⊢ f.CompStruct g h

Tactic:
rw [Quotient.eq_iff_equiv] at fac

Goal state after:
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : f.comp g ≈ h
⊢ f.CompStruct g h
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
e : X ≅ Y
⊢ X = Y

Tactic:
exact (r.unique (f := e.hom)
    (.mk X (𝟙 X) e.hom (by simp) (W₁.id_mem X) (r.prop₂_of_iso e))
    (.mk Y e.hom (𝟙 Y) (by simp) (r.prop₁_of_iso e) (W₂.id_mem Y))).choose

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

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi e

Tactic:
induction he with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance

Goal state after: