mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
⊢ Spec.map
        (CommRingCat.ofHom
          ((algebraMap
                { R := O, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                    field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                    commSq := w }.R
                { R := O, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                    field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                    commSq := w }.K).comp
            φ'')) ≫
      awayι 𝒜 ↑i₀ ⋯ ⋯ =
    Spec.map (CommRingCat.ofHom (φ'.comp (awayMap 𝒜 ⋯ ⋯))) ≫ awayι 𝒜 ↑i ⋯ ⋯

Tactic:
simp [hφ'', SpecMap_awayMap_awayι, add_comm]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck =
    (Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)

Tactic:
rw [Precoverage.comap_comp]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)).toGrothendieck =
    (Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)
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
⊢ (coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
apply transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

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

Goal state before:
pp: case e'_2
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val

pp: case e'_3
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ d.succ i ⋯
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        (d.lift j hj
          ⟨fun x ↦
            match x with
            | op ⟨i, hi⟩ => (e i hi).val,
            ⋯⟩)) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val)

Tactic:
· dsimp
      rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]

Goal state after:
case e'_3
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ d.succ i ⋯
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        (d.lift j hj
          ⟨fun x ↦
            match x with
            | op ⟨i, hi⟩ => (e i hi).val,
            ⋯⟩)) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val)
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
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.succ i ⋯
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        (d.lift j hj
          ⟨fun x ↦
            match x with
            | op ⟨i, hi⟩ => (e i hi).val,
            ⋯⟩))

Tactic:
convert!
      (e (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)).map_succ i
        (by
          simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
          exact ⟨_, hi⟩) using 1
    · dsimp
      rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]
    · congr 1
      rw [d.map_lift _ _ _ _ hi]
      symm
      apply compatibility

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

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

Tactic:
exact mod_cast hk

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:
padicValNat_eq_emultiplicity <| factorial_ne_zero (p * n),

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : x = 0
⊢ 0 = 1 ↔ ¬↑p ∣ x

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) = 1 ↔ ¬↑p ∣ x

Tactic:
· simp_all

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) = 1 ↔ ¬↑p ∣ x
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : C
x : F.obj X
U✝ V✝ : Over X
x✝² : U✝ ⟶ V✝
x✝¹ : (Over.forget X ⋙ F).obj U✝
x✝ : x✝¹ ∈ ⇑(ConcreteCategory.hom (F.map U✝.hom)) ⁻¹' {x}
⊢ x✝¹ ∈ ⇑(ConcreteCategory.hom ((Over.forget X ⋙ F).map x✝²)) ⁻¹' ⇑(ConcreteCategory.hom (F.map V✝.hom)) ⁻¹' {x}

Tactic:
by simpa [← comp_apply, ← Functor.map_comp]

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

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

Tactic:
exact norm_eq_of_equiv_aux hf hg hfg h hlt

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
⊢ ∀ ⦃a_1 : C⦄ (g : F.obj a_1 ⟶ F.obj b), ∃ b_1 fst snd, ∃ (_ : IsPullback fst (F.map snd) (F.map f) g), P snd

Tactic:
intro Y'

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
⊢ ∀ (g : F.obj Y' ⟶ F.obj b), ∃ b_1 fst snd, ∃ (_ : IsPullback fst (F.map snd) (F.map f) g), P snd
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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ n + 1 ≤ ↑j + (q + 1)

Tactic:
by simpa only [← add_assoc] using le_add_right hj

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
k : ℕ
hk : k < q
⊢ φ ≫ X.δ ⟨a + 2 + k, ⋯⟩ = 0

Tactic:
convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)

Goal state after:
case e'_2
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
k : ℕ
hk : k < q
⊢ a + 2 + k = ↑⟨a + k + 1, ⋯⟩.succ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
· rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]
    exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

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

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
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
⊢ unop A₁.fst = unop A₂.fst

Tactic:
rw [h₁]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.ι (unop A.fst).len ≫ X.map A.e.op) ≫ X.map p = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op

Tactic:
rw [assoc, ← X.map_comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ s.ι (unop A.fst).len ≫ X.map (A.e.op ≫ p) = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty

Tactic:
by
  ext n
  dsimp [N₂Γ₂ToKaroubiIso]
  simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]
  convert! comp_id _
  apply (Γ₀.splitting X).hom_ext'
  intro A
  rw [Splitting.ι_desc]
  erw [comp_id, id_comp]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
subst h
    simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
    dsimp
    simp only [id_comp, comp_id]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
· subst h
    simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
    dsimp
    simp only [id_comp, comp_id]

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } =
    𝟙 (N₁.obj X)

Tactic:
ext n
    simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f,
      HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_f]

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

Goal state before:
pp: case e_a
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
A : Splitting.IndexSet (op ⦋j⦌)
⊢ (S₁.s.cofan (op ⦋j⦌)).inj A ≫ Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
rw [cofan_inj_naturality_symm_assoc Φ A]

Goal state after:
case e_a
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
A : Splitting.IndexSet (op ⦋j⦌)
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g)
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g

Tactic:
CofibrantObject.toHoCat_map_eq_iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  homRel C (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f)
    (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g)
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g
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 C).IsStableUnderRetracts

Tactic:
rw [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).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ Fibration f

Tactic:
rw [fibration_iff]
  apply rlp_of_isIso

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

Goal state before:
pp: case e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inr) x₂ = (ConcreteCategory.hom e.hom.hom) ((ConcreteCategory.hom c.inr) x₂)

Tactic:
· exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
case a
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1) ∧ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
simp only [sup_le_iff, iSup_le_iff]
    constructor
    · exact X.skeleton.monotone (by simp)
    · intro x
      apply X.ofSimplex_le_skeleton _ (by simp)

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ⨆ n, (skeletonOfMono i) n = ⊤

Tactic:
apply le_antisymm (by simp)
  rw [← Y.iSup_skeleton, iSup_le_iff]
  intro n
  exact le_trans (skeleton_le_skeletonOfMono i n) (le_iSup _ n)

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

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ (Subcomplex.range i ≤ Subcomplex.range i ⊔ Y.skeleton (n + 1) ∧
      Y.skeleton n ≤ Subcomplex.range i ⊔ Y.skeleton (n + 1)) ∧
    ∀ (i_1 : ↑(Y.nonDegenerate n)),
      ↑i_1 ∉ (Subcomplex.range i).obj (op ⦋n⦌) → Subcomplex.ofSimplex ↑i_1 ≤ Subcomplex.range i ⊔ Y.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f.unop))) =
    ↑⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩

Tactic:
exact c.b_app_ι_app_objEquiv_symm_val _

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d) = ⊤

Tactic:
rw [← top_le_iff]
  rintro ⟨n⟩ ⟨x, hx⟩ _
  simp only [skeletonOfMono_succ, Subfunctor.range_obj, Set.mem_range, not_exists,
    Subfunctor.max_obj, Subfunctor.iSup_obj, Set.iUnion_coe_set, Set.mem_union, Set.mem_iUnion,
    exists_prop] at hx
  simp only [Subfunctor.toFunctor_obj, Subfunctor.max_obj, Subfunctor.range_obj,
    Subfunctor.homOfLe_app, TypeCat.hom_ofHom]
  obtain hx | ⟨y, hy₁, hy₂, f, rfl⟩ := hx
  · exact Or.inl ⟨⟨x, hx⟩, rfl⟩
  · let c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := by simpa }
    refine Or.inr ⟨c.ιSigmaStdSimplex.app _ (stdSimplex.objEquiv.symm f.unop), ?_⟩
    rw [Subtype.ext_iff]
    exact c.b_app_ι_app_objEquiv_symm_val _

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

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

Tactic:
simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 2 3 (by simp)).hom,
          ← Category.assoc]

Goal state after:
case «0»
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 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv) ≫ f₀ =
    (((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv) ≫ f₁
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: 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)) (h : j ≠ i),
      (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
        (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
use sx.spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀

Goal state after:
case h
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)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
⊢ spineToSimplex h (X.spine n s) = s

Tactic:
induction n with
  | zero => simp [spineToSimplex_zero]
  | succ n hn =>
    exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])

Goal state after: