mathlib-initiative/mathlib-tactics huggingface dataset:
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:
apply relative.of_exists

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
⊢ ∀ ⦃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
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
· rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
e

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
a b c d e : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) + ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X _⦋n + 1⦌) = 0

Tactic:
simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
      add_neg_cancel]

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

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

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ (x * y).valuation = x.valuation + y.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ x⁻¹.valuation = -x.valuation

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : ↑p ≠ 1
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → A.EqId

Tactic:
· intro h
    rcases A with ⟨_, ⟨f, hf⟩⟩
    simp only at h
    subst h
    refine ext _ _ rfl ?_
    simp only [eqToHom_refl, comp_id]
    exact eq_id_of_epi f

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ isoN₁ = Γ₂N₁

Tactic:
dsimp only [isoN₁]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ toKaroubiCompN₂IsoN₁ = Γ₂N₁
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
⊢ IsIso f

Tactic:
let F₄ := Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
      (ComplexShape.down ℕ)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
⊢ IsIso f
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:
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.Topology.Homotopy.Product

Goal state before:
pp: I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
⊢ ∀ x ∈ S,
    { toFun := fun x ↦ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x =
      (ContinuousMap.pi f) x

Tactic:
x

Goal state after:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
x : A
⊢ x ∈ S →
    { toFun := fun x ↦ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x =
      (ContinuousMap.pi f) x
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ (F (1, x), G (1, x)) = (f₁.prodMk g₁) x

Tactic:
by simp only [prod_eval, Homotopy.apply_one]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑(σ x.1)

Tactic:
by unit_interval

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑x.1

Tactic:
by unit_interval

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x = 0
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } 0 =
    p.toContinuousMap 0

Tactic:
simp [hf₀]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ =
    (p.reparam (fun t ↦ ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯) x✝

Tactic:
simp only [coe_reparam]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (⇑p ∘ fun t ↦ ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) x✝
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ IsCofibrant ((localizerMorphism C).functor.obj X)

Tactic:
by
  dsimp; infer_instance

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ IsIso (F.map f)

Tactic:
refine ⟨F.map (homMk g'), ?_, ?_⟩

Goal state after:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map f ≫ F.map (homMk g') = 𝟙 (F.obj X)

case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (homMk g') ≫ F.map f = 𝟙 (F.obj Y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
⊢ ∀ (x : ↑(Δ[n + 1].nonDegenerate d)), ↑x ∈ A.obj (op ⦋d⦌) → ↑x ∈ Λ[n + 1, i].obj (op ⦋d⦌)

Tactic:
x

Goal state after:
case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : ↑(Δ[n + 1].nonDegenerate d)
⊢ ↑x ∈ A.obj (op ⦋d⦌) → ↑x ∈ Λ[n + 1, i].obj (op ⦋d⦌)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ V i j = V j i

Tactic:
rw [c.eq_inf, c.eq_inf, inf_comm]

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

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
by_cases! h₃ : m < n

Goal state after:
case pos
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : m < n
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

case neg
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : n ≤ m
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
⊢ ∀ (i_1 : ↑(X.nonDegenerate ↑k)), Subcomplex.ofSimplex ↑i_1 ≤ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
x

Goal state after:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
n : ℕ
⊢ ∀ (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)

Tactic:
x

Goal state after:
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
⊢ ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: 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₁
⊢ horn.faceι 2 0 ι₀._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀

Tactic:
exact (horn.isColimit 2).fac _ (.right ⟨0, by simp⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    hComp (𝟙 (f ≫ g)) η = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ (eqToIso ⋯).inv

Tactic:
simp [← id_hComp_id, hComp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f✝ : a✝ ⟶ b✝
g✝ g : b✝ ⟶ c✝
f : a✝ ⟶ b✝
⊢ ∀ (h1 : f ≫ g✝ = f✝ ≫ g) (h2 : g = g✝) (h3 : f = f✝),
    (eqToIso h1).hom ≫ hComp (𝟙 f✝) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g✝)

Tactic:
rintro _ rfl rfl

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
g : b✝ ⟶ c✝
f : a✝ ⟶ b✝
h1✝ : f ≫ g = f ≫ g
⊢ (eqToIso h1✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (eId (Type v) X ≫ ↾fun f ↦ F.map f) = eId (Type v) (F.obj X)

Tactic:
by ext ⟨⟩; exact F.map_id X

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ x✝.len < (mk (n✝ + 1)).len

Tactic:
e

Goal state after:
case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (σ_mem _ (by lia) _) (hc _ _ _ _ _ (by lia))

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

Goal state before:
pp: X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ (hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom).toFunctor =
    ((iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)).toFunctor

Tactic:
apply mapHomotopyCategory_prod_id_comp_inverse

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val '' s) P

Tactic:
refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
  · obtain ⟨a, ma, rfl⟩ := x
    exact ⟨a.2, fun b x y ↦ by simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]⟩
  · have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
    simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

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

Goal state before:
pp: case mpr.inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y.castSucc ≤ i.castSucc

Tactic:
simp only [Fin.castSucc_le_castSucc_iff]
      by_contra!
      exact (h' i this).not_ge (by simpa using hi)

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

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ x f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) x.simplex = s

Tactic:
refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩

Goal state after:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : { dim := n, simplex := s }.toN.simplex ∈ A.obj (Opposite.op ⦋{ dim := n, simplex := s }.toN.dim⦌)
⊢ s ∈ A.obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
  simpa [type₁_pairing] using h.pairing.isUniquelyCodimOneFace (h.equivII s)

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

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ ∀ (j : Discrete WalkingPair), ((pair X Y).obj j).Finite

Tactic:
rintro ⟨_ | _⟩ <;> dsimp

Goal state after:
case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ X.Finite

case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ Y.Finite
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁴ : HasCoproducts A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
X : C
M : A
inst✝² : IsCardinalPresentable M κ
e : coyoneda.obj (op (freeYoneda X M)) ≅ (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u, v'} :=
  NatIso.ofComponents (fun P ↦ (freeYonedaHomEquiv.trans Equiv.ulift.symm).toIso) ⋯
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J (coyoneda.obj (op M))
⊢ PreservesColimitsOfShape J (coyoneda.obj (op (freeYoneda X M)))

Tactic:
exact preservesColimitsOfShape_of_natIso e.symm

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: C : Type u
inst✝² : SmallCategory C
inst✝¹ : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
e : coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)) ≅
  (evaluation Cᵒᵖ (Type (max u' u))).obj (op X) ⋙ uliftFunctor.{max u u', max u u'} :=
  NatIso.ofComponents (fun P ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯
⊢ PreservesColimitsOfShape J (coyoneda.obj (op (uliftYoneda.{u', u, u}.obj X)))

Tactic:
exact preservesColimitsOfShape_of_natIso e.symm

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
inst✝² : IsLocallyPresentable.{w, v', u'} A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
κ : Cardinal.{w}
w✝ : Fact κ.IsRegular
h✝ : IsCardinalLocallyPresentable A κ
⊢ ∃ κ, ∃ (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Cᵒᵖ ⥤ A) κ

Tactic:
exact ⟨κ, inferInstance, inferInstance⟩

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

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : l.succ ≤ i
⊢ k.succ ≤ (x.cast hd).simplex.1 i

Tactic:
· rw [← hl.simplex_fst_succ]
    exact stdSimplex.monotone_apply _ hi

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

Goal state before:
pp: case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

Tactic:
obtain ⟨i, hi⟩ := mem_range_right x hd j
      dsimp at hi
      obtain rfl | ⟨i, rfl⟩ := Fin.eq_self_or_eq_succAbove l.castSucc i
      · refine ⟨l, ?_⟩
        rw [Fin.succAbove_castSucc_self, ← hi, ← hl.simplex_snd_succ]
        rfl
      · exact ⟨_, hi⟩

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)

Tactic:
x

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.nonDegenerate n → x ∈ (⨆ i, i.subcomplex).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case e_6
⊢ stdSimplex.map (⇑(ConcreteCategory.hom (SimplexCategory.δ 1))) (⦋0⦌.toTopHomeo default) = ⟨Pi.single 0 1, ⋯⟩

Tactic:
rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]

Goal state after:
case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 1)) 0) = ⟨Pi.single 0 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case e_6
⊢ stdSimplex.map (⇑(ConcreteCategory.hom (SimplexCategory.δ 0))) (⦋0⦌.toTopHomeo default) = ⟨Pi.single 1 1, ⋯⟩

Tactic:
rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]

Goal state after:
case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 0)) 0) = ⟨Pi.single 1 1, ⋯⟩
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ ∃ y ∈ U ∩ Set.univ, y ≠ x

Tactic:
refine ⟨x + c^n, by simpa using hn, ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ≠ x