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

Goal state before:
pp: case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
h₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
⊢ e₁.val = e₂.val

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂

Goal state after:
case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ : e₁.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
h₂ : e₂.val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
⊢ e₁.val = e₂.val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
h₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val,
        ⋯⟩
⊢ e₁.val = e₂.val

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂

Goal state after:
case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
⊢ e₁.val = e₂.val
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ (generatingMonomorphisms G).pushouts ((⋯.functor ⋙ functor hG A₀ J).map (homOfLE ⋯))

Tactic:
by
    dsimp [MonoOver.forget]
    convert!
      pushouts_ofLE_le_largerSubobject hG (transfiniteIterate (largerSubobject hG) k.1 A₀) using 2
    all_goals
      rw [Set.Iic.succ_eq_of_not_isMax hk,
        transfiniteIterate_succ _ _ _ (Set.not_isMax_coe _ hk)]

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
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)

Tactic:
hqreq,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p ((q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den))
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p < 1

Tactic:
rw [padicNorm_p hp, inv_lt_one_iff₀]

Goal state after:
p : ℕ
hp : 1 < p
⊢ ↑p ≤ 0 ∨ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ ¬p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]

Goal state after:
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)
  · simp
  obtain ⟨k, rfl⟩ := h
  obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
  rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑↑z‖ = 1 ↔ IsCoprime z ↑p

Tactic:
coe_intCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = 1 ↔ IsCoprime z ↑p
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑↑z‖ < 1 ↔ ↑p ∣ z

Tactic:
coe_intCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ < 1 ↔ ↑p ∣ z
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → n ≤ x.valuation

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

Tactic:
Nat.mul_add

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.natAbs ≠ 0

Tactic:
rwa [Int.natAbs_ne_zero]

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.natAbs ≠ 0

Tactic:
rwa [Int.natAbs_ne_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r

Tactic:
by
    trans
      max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
        ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)
    · induction q, r using Quotient.inductionOn₂; apply PadicSeq.norm_nonarchimedean
    · apply max_le_add_of_nonneg
      · induction q using Quotient.inductionOn; apply PadicSeq.norm_nonneg
      · induction r using Quotient.inductionOn; apply PadicSeq.norm_nonneg

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0

Tactic:
← Fin.succ_zero_eq_one,

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ (Fin.succ 0) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
by
    ring_nf at this
    rw [← padicNormE.eq_padic_norm']
    exact mod_cast this

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

Goal state before:
pp: case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) + padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε

Tactic:
rw [← add_thirds ε]
    apply _root_.add_lt_add
    · suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]
      apply lt_of_le_of_lt
      · apply padicNormE.add_le
      · apply _root_.add_lt_add
        · rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj
        · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)
    · apply mod_cast hN (max N N2)
      apply le_max_left

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

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

Tactic:
by
  rw [← @Rat.cast_natCast ℝ _ p]
  rw [← @Rat.cast_natCast ℚ_[p] _ p]
  simp [hp.1.ne_zero, norm, padicNorm, padicValRat, padicValInt, zpow_neg,
    -Rat.cast_natCast]

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✝ X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C).map f ≫ PInfty = PInfty ≫ (alternatingFaceMapComplex C).map f

Tactic:
by
    ext n
    exact PInfty_f_naturality n f

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

Goal state before:
pp: case neg.e_a.e_s
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
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ≠ ⟨q, ⋯⟩ ∧ i < q + 1 ↔ i < q

Tactic:
ne_eq,

Goal state after:
case neg.e_a.e_s
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
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬⟨i, hi⟩ = ⟨q, ⋯⟩ ∧ i < q + 1 ↔ i < q
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 : ℕ
⊢ (id X n).φ = 𝟙 (X _⦋n + 1⦌)

Tactic:
simp only [← P_add_Q_f (n + 1) (n + 1), φ]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) ≫ (id X n).a + ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev =
    (P (n + 1)).f (n + 1) + (Q (n + 1)).f (n + 1)
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.σ 0 ≫ X.δ 1 ≫ X.σ 0 +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 ≫ 𝟙 (X _⦋1⦌) + -X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0

Tactic:
SimplicialObject.δ_comp_σ_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.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 ≫ 𝟙 (X _⦋1⦌) + -X.σ 0 ≫ 𝟙 (X _⦋1⦌)))) = 0
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.σ 0 ≫ X.δ 1 ≫ X.σ 0 + (-X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.castSucc 0) + (X.σ 0 + -X.σ 0))) = 0

Tactic:
← Fin.succ_zero_eq_one,

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.σ 0 ≫ X.δ (Fin.succ 0) ≫ X.σ 0 +
        (-X.σ 0 ≫ X.σ (Fin.succ 0) ≫ X.δ (Fin.castSucc 0) + (X.σ 0 + -X.σ 0))) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)

Tactic:
by rw [Isδ₀.iff]

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
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
  obtain rfl := SimplexCategory.image_eq fac
  congr
  · exact SimplexCategory.image_ι_eq fac
  · dsimp only [SimplicialObject.Splitting.IndexSet.pull]
    congr
    exact SimplexCategory.factorThruImage_eq fac

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (({ app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
              { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ }).app
          X).f ≫
      inclusionOfMooreComplexMap X =
    ((𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))).app X).f ≫ inclusionOfMooreComplexMap X

Tactic:
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X =
    ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p ≫ inclusionOfMooreComplexMap X
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F G : ReflPrefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ F = G

Tactic:
obtain ⟨⟨F_obj⟩⟩ := F

Goal state after:
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
F_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := F_obj, map := map✝, map_id := map_id✝ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ { obj := F_obj, map := map✝, map_id := map_id✝ } = G
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F G : U ⥤rq V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e

Goal state after:
U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F : U ⥤rq V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f
Module: Mathlib.Topology.Homotopy.Equiv

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ ((↑h.symm).comp ↑h).Homotopic (ContinuousMap.id X)

Tactic:
symm_comp_toContinuousMap

Goal state after:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ (ContinuousMap.id X).Homotopic (ContinuousMap.id X)
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
h' : Y ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk.mk
X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
a : Path x₀ y₀
b : Path x₁ y₁
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀)) a) (Quot.mk (⇑(Homotopic.setoid x₁ y₁)) b)

Tactic:
exact mk a b

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝¹ x✝ : CofibrantObject C
f : x✝¹ ⟶ x✝
⊢ homMk (resolutionMap (ι.map f)) ≫ { hom := pResolutionObj (ι.obj x✝) } = { hom := pResolutionObj (ι.obj x✝¹) } ≫ f

Tactic:
by
    ext : 1
    exact HoCat.resolutionMap_fac f.hom

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ IsIso (BifibrantObject.toHoCat.map (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom))

Tactic:
have : WeakEquivalence (C := BifibrantObject C)
      (BifibrantObject.homMk ((mk X.obj).iBifibrantResolutionObj).hom) := by
    simp only [BifibrantObject.weakEquivalence_homMk_iff]
    infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
this : WeakEquivalence (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom)
⊢ IsIso (BifibrantObject.toHoCat.map (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ ¬Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ∪ {i} ≠ Set.univ

Tactic:
ne_eq,

Goal state after:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ ¬¬Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ∪ {i} = Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∉ Λ[n + 1, j].obj (op ⦋n⦌) ↔ i = j

Tactic:
simp [objEquiv_symm_δ_mem_horn_iff.{u}]

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

Goal state before:
pp: case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∈ Δ[n].degenerate n

Tactic:
rw [mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_top_dim]
      rintro rfl
      exact h (le_antisymm (by simp) (by simpa [← ofSimplex_objEquiv_symm_id]))

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ j ∈ (Λ[n, i].op.preimage (stdSimplex.opIso ⦋n⦌).inv).obj (op ⦋d⦌) ↔ j ∈ Λ[n, i.rev].obj (op ⦋d⦌)

Tactic:
simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_horn_iff_notMem_range, Set.mem_range, not_exists, ne_eq,
    exists_prop, stdSimplex.opObjEquiv_opObjEquiv_symm_apply]

Goal state after:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) ↔ ∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1
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
z₂ : X₂
hyz : Rel' f g (Sum.inr ((ConcreteCategory.hom g) s)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr z₂)

Tactic:
rw [inr_rel'_inr_iff] at hyz
        subst hyz
        apply Rel'.inl_inr

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

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ σ₀ = Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ

Tactic:
apply horn.hom_ext

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h) =
      (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    InnerFibration (terminal.from X)

Tactic:
innerFibration_iff

Goal state after:
X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    innerFibrations (terminal.from X)
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (p ≫ terminal.from Y)

Tactic:
innerFibration_iff

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ innerFibrations (p ≫ terminal.from Y)