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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ =
    Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t', b := b', w := ⋯ }

Tactic:
by
  subst hb' ht'
  simp [functorMapSrc]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

Tactic:
obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j k₁ : J
h₁ : Order.IsSuccLimit k₁
h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration k₁
this✝ : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁), k₂ < k₁ → MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃
h₁₂ h₃ : k₁ ≤ k₁
h₄ : ¬k₁ < k₁
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < k₁
⊢ MapEq iter₁.F iter₂.F k₁ k₁ h₁₂ h₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).symm.hom =
    ((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).ι.app ⟨i, hi⟩

Tactic:
by
        dsimp
        rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case isMin
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : IsMin i
⊢ Nonempty (Φ.Iteration i)

Tactic:
| isMin i hi =>

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

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val = d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val)

Tactic:
e.map_succ k (lt_of_lt_of_le hk hij)

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val) =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isMin
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 : IsMin i
⊢ Subsingleton (d.Extension val₀ i)

Tactic:
| isMin i hi =>

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

Goal state before:
pp: case succ
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.incl.app (Order.succ j) ≫ φ₁ = c.incl.app (Order.succ j) ≫ φ₂

Tactic:
apply (c.attachCells j hj).hom_ext

Goal state after:
case succ.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₁ = c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₂

case succ.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ ∀ (i : (c.attachCells j hj).ι),
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
      (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isMin
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 : IsMin i
⊢ Nonempty (d.Extension val₀ i)

Tactic:
| isMin i hi =>

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 : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
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
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)

Tactic:
calc
        _ ≤ min (emultiplicity ↑p (q.num * r.den * q.den))
                (emultiplicity ↑p (q.den * r.num * q.den)) :=
          le_min
            (by rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm])
            (by grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h])
        _ ≤ _ := min_le_emultiplicity_add

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ ↑p < 0 → 0 = 1

Tactic:
← Nat.cast_zero,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ ↑p < ↑0 → ↑0 = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
← int_eq_one_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
← int_eq_one_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ padicNorm p ↑↑m = 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
s : Finset α
f : α → ℤ_[p]
⊢ ↑(∑ z ∈ s, f z) = ∑ z ∈ s, ↑(f z)

Tactic:
simp [← Coe.ringHom_apply, map_sum PadicInt.Coe.ringHom f s]

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

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

Tactic:
← zpow_natCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * (↑p ^ (-↑x.valuation) * ↑p ^ ↑x.valuation)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ False

Tactic:
have : ↑p ∣ r.num ∧ (p : ℤ) ∣ r.den := by
    simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
    exact ⟨key, norm_denom_lt⟩

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
by_cases hx : ‖x‖ ≤ 1

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev = (Q (n + 1)).f (n + 1)

Tactic:
exact Eq.trans (by simp) (decomposition_Q n (n + 1)).symm

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

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

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors (PInfty.f (n + 1))

Tactic:
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]

Goal state after:
case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ i ∈ Finset.univ, (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ PInfty.f n = 0

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ PInfty.f n = 0
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
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      NormalizedMooreComplex.objD X n ≫ (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n

Tactic:
← normalizedMooreComplex_objD,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      ((normalizedMooreComplex A).obj X).d (n + 1) n ≫ (inclusionOfMooreComplexMap X).f n =
    K[X].d (n + 1) n ≫ PInfty.f n
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
X : ChainComplex C ℕ
⊢ (N₂.map (isoΓ₀.hom.app X)).f = PInfty

Tactic:
ext
  apply comp_id

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as

Tactic:
apply Prod.ext

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.1 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.2 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.2
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adj.unit.app X)

Tactic:
obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
  dsimp [HoCat.adj]
  infer_instance

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
⊢ ⟨a, ha⟩ ∈ A.toSSet.degenerate i ↔ ⟨a, ha⟩ ∈ ⊤

Tactic:
rw [A.mem_degenerate_iff]

Goal state after:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
⊢ ↑⟨a, ha⟩ ∈ Δ[n].degenerate i ↔ ⟨a, ha⟩ ∈ ⊤
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_2
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx : x ∈ c.multicofork.pt
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx⟩

Tactic:
simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq,
      Set.iSup_eq_iUnion, Set.mem_iUnion] at hx
    obtain ⟨i, hi⟩ := hx
    exact ⟨i, ⟨x, hi⟩, rfl⟩

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)

Tactic:
exact Or.inl h₁

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

Goal state before:
pp: case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝

Tactic:
· simp only [iSup_iff, ofHoms_iff] at h
    obtain ⟨n, ⟨i, h0, hn⟩, _, _⟩ := h
    exact horn_ι_mem_innerHornInclusions h0 hn

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

Goal state before:
pp: X : SSet
⊢ X.skeleton 0 = ⊥

Tactic:
simp [skeleton]

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

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

Tactic:
conv_lhs => dsimp [skeleton]

Goal state after:
case a
X : SSet
n : ℕ
⊢ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

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

Tactic:
revert h1 h2 h3 h4

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom =
      (eqToIso h4).hom ≫ (eqToIso pf✝).hom
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝⁴ : C
x✝³ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝⁴
x✝² : C
x✝¹ : (coyoneda.obj (Opposite.op x✝⁴)).obj x✝²
x✝ : F.obj x✝²
⊢ (ConcreteCategory.hom
          (((ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝⁴)) x✝³).app x✝²
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((ConcreteCategory.hom (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝⁴))
                x✝³).app
            x✝² x✝¹)).toFun
      x✝

Tactic:
apply Prod.ext

Goal state after:
case fst
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝⁴ : C
x✝³ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝⁴
x✝² : C
x✝¹ : (coyoneda.obj (Opposite.op x✝⁴)).obj x✝²
x✝ : F.obj x✝²
⊢ ((ConcreteCategory.hom
            (((ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝⁴)) x✝³).app x✝²
              x✝¹)).toFun
        x✝).1 =
    ((ConcreteCategory.hom
            (((ConcreteCategory.hom
                    (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝⁴))
                  x✝³).app
              x✝² x✝¹)).toFun
        x✝).1

case snd
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝⁴ : C
x✝³ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝⁴
x✝² : C
x✝¹ : (coyoneda.obj (Opposite.op x✝⁴)).obj x✝²
x✝ : F.obj x✝²
⊢ ((ConcreteCategory.hom
            (((ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝⁴)) x✝³).app x✝²
              x✝¹)).toFun
        x✝).2 =
    ((ConcreteCategory.hom
            (((ConcreteCategory.hom
                    (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝⁴))
                  x✝³).app
              x✝² x✝¹)).toFun
        x✝).2
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯ =
    mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯

Tactic:
by
      ext y
      obtain ⟨y, rfl⟩ := mk_surjective y
      simpa using homMk_comp_homMk (h.tensor (.idCompId y))

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
⊢ Mono (toSimplexCategory.map f)

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f))
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: case inl
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ i.as ≤ l

pp: case inr
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ g.I
⊢ i.as ≤ l

Tactic:
exacts [(f.left_le l h), (Path.le f).trans (g.left_le l h)]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
k : K
⊢ (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) (↑y₁ k) =
    (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) (↑y₂ k)

Tactic:
simp only [y₁, y₂, Types.isLimitEquivSections_apply]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
k : K
⊢ (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j))
      ((ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj j)).mapCone c).π.app k)) x₁) =
    (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j))
      ((ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj j)).mapCone c).π.app k)) x₂)
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
⊢ ∃ h, Nonempty (categoryFamily Ω h ≌ C)

Tactic:
by
  let f₁ := (Cardinal.lift_mk_le'.1 h₁).some
  let f₂ (X Y) := (Cardinal.lift_mk_le'.1 (h₂ X Y)).some
  let e := Equiv.ofInjective _ f₁.injective
  let h : CoreSmallCategoryOfSet Ω C :=
    { obj := Set.range f₁
      hom X Y := Set.range (f₂ (e.symm X) (e.symm Y))
      objEquiv := e.symm
      homEquiv {_ _} := by simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm }
  exact ⟨h.smallCategoryOfSet, ⟨h.equivalence⟩⟩

Goal state after: