mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map t)) v = u

Tactic:
refine (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv.injective ?_

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv ((ConcreteCategory.hom (Φ.obj.fiber.map t)) v) =
    (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv u
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f_1)) y = φ

Tactic:
| _ X f
     => 

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f_1)) y = φ
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
⊢ relative F P (F.map f)

Tactic:
by
  apply relative.of_exists
  intro Y' g
  obtain ⟨g, rfl⟩ := F.map_surjective g
  exact ⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩

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

Goal state before:
pp: case hbc.h₁.hbc.h₁
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 j) < ε / 3

Tactic:
padicNormE.map_sub

Goal state after:
case hbc.h₁.hbc.h₁
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 (↑f j - ↑(limSeq f j)) < ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (↑(↑(lim' f) i) - ↑f i) < ε / 2

Tactic:
padicNormE.map_sub

Goal state after:
case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (↑f i - ↑(↑(lim' f) i)) < ε / 2
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (↑f i - x) < ε

Tactic:
padicNormE.map_sub

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (x - ↑f i) < ε
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
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
w✝² : C
w✝¹ : w✝² ⟶ a
w✝ : F.obj w✝² ⟶ F.obj a
pbRepr :
  IsPullback w✝ (F.map w✝¹) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
⊢ ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        pullback.fst (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (⊤_ D)) ⋯ ⋯)) ≫
      pullback.diagonal (terminal.from X) =
    ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        pullback.snd (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (⊤_ D)) ⋯ ⋯)) ≫
      pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
        ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
        (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
        (𝟙 (⊤_ D)) ⋯ ⋯

Tactic:
rw [assoc]; simp [pullback.condition]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (f.preComp g).φ = g.app (op ⦋n + 1⦌) ≫ f.φ

Tactic:
unfold φ preComp
  simp only [PInfty_f, comp_add]
  congr 1
  · simp
  · simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ ∑ j, f ≫ (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n = 0

Tactic:
Fintype.sum_eq_zero

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ 0 = 0

case mpr.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ ∀ (a : IndexSet (op ⦋n⦌)), f ≫ (s.πSummand a ≫ (s.cofan (op ⦋n⦌)).inj a) ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X =
    ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            N₁ ⋙
              (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
        P).X

Tactic:
ext n
      · rfl
      · dsimp
        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (Set.IccExtend extend._proof_1 (⇑F.curry) (2 * ↑x.1)) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

Tactic:
Set.IccExtend_of_mem

Goal state after:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (F.curry ⟨2 * ↑x.1, ?pos.hx✝⟩) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 ∈ Set.Icc 0 1
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (Set.IccExtend extend._proof_1 (⇑G.curry) (2 * ↑x.1 - 1)) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

Tactic:
Set.IccExtend_of_mem

Goal state after:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.curry ⟨2 * ↑x.1 - 1, ?neg.hx✝⟩) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 - 1 ∈ Set.Icc 0 1
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ f₀ x = f₁ x

Tactic:
← F.eq_fst 1 hx,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ F (1, x) = f₁ 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
⊢ ContractibleSpace (X × Y)

Tactic:
by
  obtain ⟨hX⟩ := hequiv_unit' (X := X)
  obtain ⟨hY⟩ := hequiv_unit' (X := Y)
  refine ⟨⟨(hX.prodCongr hY).trans ?_⟩⟩
  exact (Homeomorph.prodUnique Unit Unit).toHomotopyEquiv

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

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧

Tactic:
by
  apply Path.Homotopic.hpath_hext
  exact hfg

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (trivialCofibrations C).HasFactorization (fibrations C)

Tactic:
by rw [h₁', h₂]; infer_instance

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

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ A
⊢ False

pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]

Tactic:
· replace h := h.trans hA
    rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h
    apply h
    rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]

Goal state after:
case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasIterationOfShape K C
⊢ (W.functorCategory J).transfiniteCompositionsOfShape K ≤ W.functorCategory J

Tactic:
by
    rintro X Y f ⟨hf⟩ j
    have : W.functorCategory J ≤ W.inverseImage ((evaluation _ _).obj j) := fun _ _ _ h ↦ h _
    exact W.transfiniteCompositionsOfShape_le K _ ⟨(hf.ofLE this).map⟩

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

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯ ∈ Λ[n + 3, i].obj (op ⦋2⦌)

Tactic:
simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set,
    Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff,
    Nat.reduceAdd, mem_compl, mem_singleton, exists_prop]

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: ⊢ I ≤ monomorphisms SSet

Tactic:
rintro _ _ _ ⟨n⟩
  exact monomorphisms.infer_property _

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

Goal state before:
pp: case inl
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
h₁ : ∃ x₂, (ConcreteCategory.hom r) x₂ = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

pp: case inr
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
· exact Or.inl h₁

Goal state after:
case inr
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f)) = f.interval j l hjl

Tactic:
spine_map_subinterval,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (X.spine n (sx.spineToSimplex f)).interval j l hjl = f.interval j l hjl
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ range (f₁ ⊗ₘ f₂) = (range f₁).prod (range f₂)

Tactic:
by
  ext m ⟨y₁, y₂⟩
  constructor
  · rintro ⟨⟨x₁, x₂⟩, h⟩
    rw [Prod.eq_iff_fst_eq_snd_eq] at h
    exact ⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩
  · rintro ⟨⟨x₁, rfl⟩, ⟨x₂, rfl⟩⟩
    exact ⟨⟨x₁, x₂⟩, rfl⟩

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

Goal state before:
pp: V : Truncated 2
x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ homMk e₀₁ ≫ homMk e₁₂ = homMk e₀₂

Tactic:
by
  simpa [homMk] using! CategoryTheory.Quotient.sound _
    (OneTruncation₂.HoRel₂.of_compStruct h)

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
this : Unique (W₁.MapFactorizationData W₂ f) := ⋯.some
⊢ W₁.MapFactorizationData W₂ f

Tactic:
exact default

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

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
· rw [hz, Eq.comm]
        rw [map'_eq_castSucc_iff] at hz ⊢
        constructor
        · refine hy.1.trans ?_
          simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
          exact g.monotone (by simpa using hz.1)
        · intro i hi
          exact hy.2 (f i) (by simpa using hz.2 i hi)

Goal state after:
case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ

Tactic:
· rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

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

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

Tactic:
Fin.succAbove_of_le_castSucc _ _ (by simpa),

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = x.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } (Fin.last (n + 1)) = i.succ.castSucc.succAbove (Fin.last (n + 1))

Tactic:
· simp [map'_last]

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i j : Fin (n + 2)
hij : (ConcreteCategory.hom (SimplicialObject.δ X i)) x = (ConcreteCategory.hom (SimplicialObject.δ X j)) x
⊢ i = j

Tactic:
by
  apply SimplexCategory.δ_injective
  apply stdSimplex.objEquiv.symm.injective
  have := mono' x hx
  exact injective_of_mono ((yonedaEquiv.symm x).app _) hij

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)

Tactic:
rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_weakRankFunction]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ Nonempty (P.pairing.WeakRankFunction ℕ) ↔ Nonempty (P.WeakRankFunction ℕ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ strongInnerAnodyneExtensions ≤ innerAnodyneExtensions

Tactic:
rintro X Y f ⟨_, P, _, _⟩
  rw [← Subfunctor.toRange_ι f]
  exact comp_mem _ _ _ (.of_isIso _) P.innerAnodyneExtensions

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
⊢ HasLiftingProperty sq₁₂.ι f₃ ↔ HasLiftingProperty f₂ sq₁₃.π

Tactic:
simp only [Arrow.hasLiftingProperty_iff]
  constructor
  · intro h β
    obtain ⟨α, rfl⟩ := (adj₂.arrowHomEquiv sq₁₂ sq₁₃).surjective β
    exact ⟨adj₂.liftStructEquiv sq₁₂ sq₁₃ α (h α).some⟩
  · intro h α
    exact ⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩

Goal state after: