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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) k i ⋯ hij =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk

Tactic:
arrowMap_extendToSucc _ _ _ _ _ _ hij',

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowMap iter.F k i ⋯ hij' =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J
  rw [isStableUnderTransfiniteCompositionOfShape_iff] at this
  exact le_trans (transfiniteCompositionsOfShape_monotone J W.le_llp_rlp) this

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

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
val₀ : F.obj (op ⊥)
⊢ ↑(d.sectionsMk val₀) (op ⊥) = val₀

Tactic:
by
  simpa using! (default : d.Extension val₀ ⊥).map_zero

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : q = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
by simpa [hq] using h

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
exact sum_lt hs hF

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

Goal state before:
pp: case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)

Tactic:
exact padicValRat.lt_add_of_lt
      (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
      (hF _ (by simp [Finset.mem_insert, true_or]))
      (Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi)))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b

Tactic:
by
  rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
    Nat.sub_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).valuation = ↑x.valuation + ↑y.valuation

Tactic:
simp [← valuation_coe, Padic.valuation_mul (coe_ne_zero.2 hx) (coe_ne_zero.2 hy)]

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

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

Tactic:
padicValNat_factorial <| lt_succ_of_lt <| lt_add_one (log p n)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico 1 (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
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
hc : IsColimit (PushoutCocone.mk (pushout.inl f f) (pushout.inr f f) ⋯)
⊢ Epi f

Tactic:
rw [epi_iff_isIso_inl hc, h.isIso_iff]

Goal state after:
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
hc : IsColimit (PushoutCocone.mk (pushout.inl f f) (pushout.inr f f) ⋯)
⊢ ∀ (i : I), IsIso ((F i).map (PushoutCocone.mk (pushout.inl f f) (pushout.inr f f) ⋯).inl)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
exact if hfg : f + g ≈ 0 then by
    have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
    simpa only [hfg, norm]
  else
    if hf : f ≈ 0 then by
      have hfg' : f + g ≈ g := by
        change LimZero (f - 0) at hf
        change LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel_right] using hf
      have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
      have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
      have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
      rw [this, hcfg]
    else
      if hg : g ≈ 0 then by
        have hfg' : f + g ≈ f := by
          change LimZero (g - 0) at hg
          change LimZero (f + g - f); · simpa only [add_sub_cancel_left, sub_zero] using hg
        have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
        have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
        have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
        rw [this, hcfg]
      else norm_nonarchimedean_aux hfg hf hg

Goal state after:
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
this : ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b
Z✝ : Cᵒᵖ ⥤ Type v₁
x✝³ x✝² : Z✝ ⟶ F
h : x✝³ ≫ f = x✝² ≫ f
x✝¹ : C
x✝ : yoneda.obj x✝¹ ⟶ Z✝
⊢ (x✝ ≫ x✝³) ≫ f = (x✝ ≫ x✝²) ≫ f

Tactic:
by simp only [assoc, h]

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

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

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 ⋯ (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, ⋯⟩

Tactic:
· rintro ⟨k, hk⟩
    suffices φ ≫ X.δ (⟨a + 2 + k, by lia⟩ : Fin (n + 2)) = 0 by
      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
    convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)
    dsimp
    lia

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, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ QInfty.f n = 0

Tactic:
dsimp only [QInfty]
  simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id,
    PInfty_f_idem, sub_self]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (𝟙 K[X] - PInfty).f n ≫ PInfty.f n = 0

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_comp, id_comp,
    PInfty_f_idem, sub_self]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < a
⊢ ‖f.lim‖ ≤ a

Tactic:
calc
    ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
    _ ≤ max ‖f.lim - f N‖ ‖f N‖ := nonarchimedean _ _
    _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑p ^ (-padicValRat p q)

Tactic:
← Rat.cast_natCast,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑↑p ^ (-padicValRat p q)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
← Rat.cast_natCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑↑n).valuation = ↑(padicValNat p n)
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
| ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev - (P q).f (n + 1) ≫ (Hσ q).f (n + 1)

Tactic:
rw [sub_eq_add_neg, add_comm]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
| -(P q).f (n + 1) ≫ (Hσ q).f (n + 1) + ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case mpr
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)

Tactic:
rintro rfl
    exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩

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
X : SimplicialObject C
n : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
obtain _ | n := n
  · simp
  · simp [degeneraciesVanish_succ_iff, hf.σ_comp_assoc]

Goal state after:
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 : ℕ
⊢ ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
by
  rw [PInfty_f]
  rcases n with _ | n
  · simpa only [P_f_0_eq] using! comp_id _
  · exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self

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
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
this : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ j₁ = 0

Tactic:
by simp only [Fin.ext_iff, Fin.val_zero]; lia

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
⊢ (toKaroubi (ChainComplex C ℕ)).map (s.fromNondegComplex ≫ s.toNondegComplex) =
    (toKaroubi (ChainComplex C ℕ)).map (𝟙 s.nondegComplex)

Tactic:
by simp [toNondegComplex, fromNondegComplex]

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
⊢ (toKaroubi (ChainComplex C ℕ)).map (s.toNondegComplex ≫ s.fromNondegComplex) =
    (toKaroubi (ChainComplex C ℕ)).map PInfty

Tactic:
by simp [toNondegComplex, fromNondegComplex]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f (unop (Splitting.IndexSet.id (op ⦋j⦌)).fst).len ≫
      (S₂.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
rw [Splitting.cofan_inj_πSummand_eq_id]

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f (unop (Splitting.IndexSet.id (op ⦋j⦌)).fst).len ≫
      𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
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⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      ((Γ₀.splitting (N₂.obj P).X).desc (op ⦋n⦌) fun A ↦
          (PInfty.f (unop A.fst).len ≫ P.p.app A.fst) ≫
            ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj A) ≫
        ((Γ₂N₂ToKaroubiIso.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:
rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]

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 (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⦌)
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p ≍ p

Tactic:
by
  rw [Path.cast_eq_cast]
  exact _root_.cast_heq _ _

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

Goal state before:
pp: A : TopCat
B : TopCat
⊢ prodToProdTop A B ≫ (projLeft A B).prod' (projRight A B) = 𝟙 (CategoryTheory.Grpd.of (↑(π.obj A) × ↑(π.obj B)))

Tactic:
by
    change prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 _
    apply CategoryTheory.Functor.hext; · intros; ext <;> simp <;> rfl
    rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩
    have : Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
      Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
        And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
    cat_disch

Goal state after:
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)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)

Tactic:
Functor.map_inv,

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 : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
this : WeakEquivalence (pushout.inl f i ≫ h.i)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := pushout.inr f i ≫ h.i ≫ sq'.lift
              fac_left := by
                simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left }⟩⟩

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

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    ⟦Path.refl Y✝.as⟧

Tactic:
exact Quotient.sound ⟨(Path.Homotopy.reflSymmTrans f).symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl x₁)

Tactic:
apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr x₂)

Tactic:
apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : X₁ ⊕ X₂
⊢ Rel' f g x x

Tactic:
apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
k : J
α : j ⟶ k
hk : (hom (F₂.map α)) ((hom (f.app j)) x₁) = (hom (F₂.map α)) ((hom (f.app j)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁

Tactic:
simp only [← NatTrans.naturality_apply] at hk

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
k : J
α : j ⟶ k
hk : (hom (f.app k)) ((hom (F₁.map α)) x₁) = (hom (f.app k)) ((hom (F₁.map α)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) x₀✝))

Tactic:
apply Rel'.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))

Tactic:
apply Rel'.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
hs : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s✝ : S
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) z
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) z

Tactic:
obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
        · apply Rel'.inr_inl
        · obtain rfl := (mono_iff_injective f).1 inferInstance h'
          rw [h]
          apply Rel'.inr_inl
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Rel'.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))

Tactic:
apply Rel'.inl_inr

Goal state after: