mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app (Arrow.mk f))).right.hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality
    (homOfLE (Order.le_succ j))

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app (Arrow.mk f))).right.hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).F.map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j ≫
      ((Functor.const κ.ord.ToType).obj (iteration I κ)).map (homOfLE ⋯)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (monomorphisms C).HasFunctorialFactorization (monomorphisms C).rlp

Tactic:
by
  have hG := isSeparator_separator C
  rw [← generatingMonomorphisms_rlp hG, ← llp_rlp_monomorphisms hG,
    ← generatingMonomorphisms_rlp hG]
  infer_instance

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
· rw [add_comm, max_comm]
    exact this (le_of_not_ge hle)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

Tactic:
rw [zpow_neg, inv_inv, zpow_natCast]
    apply lt_of_lt_of_le hk
    norm_cast
    apply le_of_lt
    convert! Nat.lt_pow_self _ using 1
    exact hp.1.one_lt

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

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

Tactic:
apply Nat.cast_injective (R := ℕ∞)

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(padicValNat p (p * n)!) = ↑(padicValNat p n ! + n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p (↑(g - 0) j) < ε

Tactic:
simpa [h] using hi _ hj

Goal state after:
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)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : yoneda.map a ≫ f i = yoneda.map b ≫ f j
⊢ a ≫ toGlued hf i = b ≫ toGlued hf j

Tactic:
rw [← (hf i).rep.lift'_fst a b h, assoc]
  conv_rhs => rw [← (hf i).rep.lift'_snd a b h, assoc]
  congr 1
  exact ((glueData hf).glue_condition i j).symm.trans (by simp [toGlued])

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 a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ i)) • (φ ≫ X.δ (Fin.cast ⋯ i)) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

Tactic:
Fin.sum_trunc

Goal state after:
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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

case hf
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
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j))) •
        (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ ⟨a, ⋯⟩ =
      0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
cast_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 = 1
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
have h₁₄ := Idempotents.natTrans_eq
    ((𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)) ◫
      (natTransPInfty_f (Karoubi C) n)) Y

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app Y =
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
        Y.decompId_i ≫
      (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app
          { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } ≫
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
          Y.decompId_p
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ↑p ^ (-(x * y).valuation) = ↑p ^ (-x.valuation) * ↑p ^ (-y.valuation)
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
← zpow_add₀ hp_pos.ne',

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ↑p ^ (-(x * y).valuation) = ↑p ^ (-x.valuation + -y.valuation)
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)

Tactic:
simp only [s.cofan_inj_comp_app, h]

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
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
⊢ { F := F₁, f := f₁, comm := c₁ } = { F := F₂, f := f₁, comm := c₂ }

Tactic:
simp only [mk.injEq, and_true]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
⊢ F₁ = F₂
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ ((obj K).map θ ≫ (splitting K).desc Δ fun A ↦ f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) =
    ((splitting K).desc Δ' fun A ↦ f.f (unop A.fst).len ≫ ((splitting K').cofan Δ').inj A) ≫ (obj K').map θ

Tactic:
by
    apply (Γ₀.splitting K).hom_ext'
    intro A
    simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc,
      assoc, Obj.map_on_summand' K' _ θ]
    apply Obj.Termwise.mapMono_naturality_assoc

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0

Tactic:
by
  rw [SimplicialObject.Splitting.IndexSet.eqId_iff_mono] at hA
  rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]

Goal state after:
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:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
        rw [← h] at h₁
        exact h₁ rfl)

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
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + k + 1
⊢ PInfty.f n ≫ X.map i.op = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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

Tactic:
change n = m + 1 at hk

Goal state after:
case mk.zero
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
hk : n = m + 1
⊢ 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₁.inv.app X ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
Γ₂N₁_inv,

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₁.natTrans.app X ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk (a✝ i)).map { toFun := fun p ↦ p i, continuous_toFun := ⋯ } = Quotient.mk (a✝ i)

Tactic:
pi_lift

Goal state after:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (Quotient.mk (Path.pi a✝)).map { toFun := fun p ↦ p i, continuous_toFun := ⋯ } = Quotient.mk (a✝ i)
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:
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.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mpr
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 : A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A

Tactic:
exact le_antisymm (equalizer_le f g) h

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

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈ ∂Δ[n + 1].obj (op ⦋m⦌)

Tactic:
apply face_singleton_compl_le_boundary i

Goal state after:
case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈ (stdSimplex.face {i}ᶜ).obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
intro x
      apply X.ofSimplex_le_skeleton _ (by simp)

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

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ (isColimit i).desc hf.multicofork = f j hj

Tactic:
← cancel_epi (stdSimplex.faceSingletonComplIso j).inv

Goal state after:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
convert! h₁₂

Goal state after:
case e'_2
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
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 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv) ≫ f₀ =
    (((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv) ≫ f₃

Tactic:
convert! h₁₂

Goal state after:
case e'_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 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

case e'_3
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 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (0 + 1)
⊢ f.vertex i = g.vertex i

Tactic:
fin_cases i; exact h

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
· obtain _ | n := n
    · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
      obtain rfl : k = 0 := by omega
      fin_cases i <;> contradiction
    · /- We construct the triangle in the standard simplex as a 2-simplex in
      the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
      it suffices to inhabit `Λ[n + 3, i] _⦋2⦌`. -/
      let triangle : (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ :=
        horn.primitiveTriangle i h₀ hₙ k (by grind)
      /- The interval spanning from `k` to `k + 2` is equivalently the spine
      of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
      have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by grind) =
          X.spine 2 (σ₀.app _ triangle) := by
        ext m
        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
        rw [← dsimp% σ₀.naturality_apply]
        apply congr_arg
        apply Subtype.ext
        ext a : 1
        fin_cases a <;> fin_cases m <;> rfl
      rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]
      simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]
      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
      dsimp
      apply congr_arg
      apply Subtype.ext
      ext z : 1
      dsimp [horn.face]
      rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]
      dsimp [CosimplicialObject.δ]
      rw [SSet.yonedaEquiv_map]
      simp only [Equiv.apply_symm_apply, triangle]
      rw [mkOfSucc_δ_eq heq]
      fin_cases z <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    𝟙 (ForgetEnrichment.of W X)

Tactic:
rw [← ForgetEnrichment.homOf_eId, TransportEnrichment.eId_eq, ForgetEnrichment.homTo_id]

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to V X))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V X))
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ (ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom =
    (FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f

Tactic:
ext1; exact Paths.ext_functor (V := Quiv.of v) (by cat_disch) (by cat_disch)

Goal state after: