mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
⊢ W ((h.ici j).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem i.1 (Set.not_isMax_coe _ hi)
    rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
    have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (coe_succ_of_mem (i.2.trans (Order.le_succ _))) rfl
    replace eq := congr_arg h.F.mapArrow.obj eq
    convert! this using 1

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

Goal state before:
pp: case inr
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬IsMax (Fin.last n)
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
rw [isMax_iff_eq_top] at hj
      exact (hj rfl).elim

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 ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
j✝ j'✝ : { x // x ∈ Set.Iio j }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom ((⋯.functor.op ⋙ F).map f))
      ((fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val)
        j✝) =
    (fun x ↦
        match x with
        | op ⟨i, hi⟩ => (e i hi).val)
      j'✝

Tactic:
dsimp; apply compatibility

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ padicValRat p q = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)

Tactic:
rw [padicValRat.multiplicity_sub_multiplicity hp.1.ne_one hqz]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp.llp = monomorphisms C

Tactic:
by
  refine le_antisymm ?_ (le_llp_rlp _)
  rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]
  trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
  · apply retracts_monotone
    apply transfiniteCompositions_monotone
    apply pushouts_monotone
    apply coproducts_monotone
    apply generatingMonomorphisms_le_monomorphisms
  · simp

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

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

Tactic:
rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]

Goal state after:
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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y)

Tactic:
rw [this, ← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i, Functor.map_comp]

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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom
        (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i) ≫
          Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (Φ.presheafFiber.map f)

Tactic:
isIso_iff_coyoneda_map_bijective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ ∀ (T : A), Function.Bijective fun x ↦ Φ.presheafFiber.map f ≫ x
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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
· let ι' : Type _ := Σ (Φ : P.FullSubcategory), Φ.obj.fiber.obj X
    choose i y hy using fun (j : ι') ↦ hf j.1 j.2
    refine J.superset_covering (S := Sieve.ofArrows _ (fun i' ↦ f (i i'))) ?_ ?_
    · rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]
      exact fun _ ↦ Sieve.ofArrows_mk _ _ _
    · rw [hP.jointly_reflect_ofArrows_mem]
      exact fun Φ x ↦ ⟨_, _, hy ⟨Φ, x⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : HasSheafify J (Type w)
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
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ IsIso f

Tactic:
have : Epi f := by
          rw [← Sheaf.isLocallySurjective_iff_epi]
          exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : HasSheafify J (Type w)
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
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
this : Epi f
⊢ IsIso f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ ↑m = ↑n → m = n

Tactic:
rw [← Rat.cast_natCast]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ ↑↑m = ↑n → m = n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
apply max_le_add_of_nonneg

Goal state after:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ q

case hb
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ r
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
exists max N N2

Goal state after:
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 ≥ max N N2, padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ‖↑q‖ = ↑(padicNorm p q)

Tactic:
by
  dsimp [norm]
  rw [← padicNormE.eq_padic_norm']

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

Goal state before:
pp: case hf.hj₂
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
⊢ n + 2 ≤ ↑((Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)).pred ⋯) + q

Tactic:
dsimp [Fin.cast, Fin.pred]
      rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
      lia

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map ((Q q).f n) = (Q q).f n

Tactic:
← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)),

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map ((P q).f n) + G.map ((Q q).f n) = G.map ((P q).f n) + (Q q).f n
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.ι (unop A.fst).len ≫ S₁.X.map A.e.op) ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A

Tactic:
S₂.s.cofan_inj_eq,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.ι (unop A.fst).len ≫ S₁.X.map A.e.op) ≫ Φ.F.app Δ =
    Φ.f (unop A.fst).len ≫ S₂.s.ι (unop A.fst).len ≫ S₂.X.map A.e.op
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk.mk
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
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f ⦋n'⦌.len ≫ X.map i.op

Tactic:
| _ n'
   => 

Goal state after:
case mk.mk
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
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f ⦋n'⦌.len ≫ X.map i.op
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 (1, x) = f₁ x

Tactic:
F.apply_one

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₁ x = f₁ x
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SimplyConnectedSpace X
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
rw [simply_connected_iff_unique_homotopic] at *

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ (mk γ).cast ⋯ ⋯ = mk γ

Tactic:
| mk γ =>

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

Goal state before:
pp: case mk
X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
γ : Path x y
⊢ ((mk γ).cast hx hy).cast hx' hy' = (mk γ).cast ⋯ ⋯

Tactic:
| mk γ =>

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

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯

Tactic:
dsimp only [prodToProdTopI, uhpath01, hcast]
  refine (@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
    (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_
  simp only [map_eq]
  apply Path.Homotopic.hpath_hext; intro; rfl

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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (refl x₀).trans (mk γ) = mk γ

Tactic:
| mk γ =>

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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).trans (refl x₁) = mk γ

Tactic:
| mk γ =>

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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).trans (mk γ).symm = refl x₀

Tactic:
| mk γ =>

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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).symm.trans (mk γ) = refl x₁

Tactic:
| mk γ =>

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

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩}
⊢ False

Tactic:
simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this

Goal state after:
case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : n + 3 = i
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

Tactic:
have h₀ : Rel f g _ _ := Rel.inl_inr x₀

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
rw [sup_le_iff]
      constructor
      · exact face_le_horn (2 : Fin 3) 1 (by simp)
      · exact face_le_horn (0 : Fin 3) 1 (by simp)

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

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]

pp: case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
· rw [sup_le_iff]
      constructor
      · exact face_le_horn (1 : Fin 3) 2 (by simp)
      · exact face_le_horn (0 : Fin 3) 2 (by simp)

Goal state after:
case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ ∃ c_1 f,
    ∃ (_ : Epi f),
      (ConcreteCategory.hom (c_1.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f) =
        (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s

Tactic:
have hs : s ∉ ∂Δ[d].obj _ :=
    fun hs ↦ hy (⟨c.ιSigmaBoundary.app _ ⟨s, hs⟩, congr($(c.ι_l).app _ ⟨s, _⟩)⟩)

Goal state after:
X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
⊢ ∃ c_1 f,
    ∃ (_ : Epi f),
      (ConcreteCategory.hom (c_1.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f) =
        (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s
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
⊢ (ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl)

Tactic:
apply sx.spineInjective
  dsimp only [spineEquiv, Equiv.coe_fn_mk]
  rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ ((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom =
    (α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y) ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
      (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
        ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)

Tactic:
by
      ext ⟨⟨f, g⟩, h⟩; dsimp at f g h
      dsimp; simp only [Category.assoc, Iso.cancel_iso_inv_left]
      conv_lhs =>
        rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
      conv_rhs => rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ (ρ_ (X ⟶[V] Z)).inv ≫ (X ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Z)).inv ≫ (Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫ eComp V X Y Z'

Tactic:
rw [rightUnitor_inv_naturality_assoc, ← whisker_exchange_assoc]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Z)).inv ≫
      ((X ⟶[V] Y) ⊗ Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ (eComp V X Y Z ▷ Z ⟶[V] Z') ≫ eComp V X Z Z' =
    (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Z)).inv ≫ (Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫ eComp V X Y Z'
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
W X Y Z : C
⊢ (α_ (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom ≫ (W ⟶[V] X) ◁ eComp V X Y Z ≫ eComp V W X Z =
    (eComp V W X Y ▷ Y ⟶[V] Z) ≫ eComp V W Y Z

Tactic:
← e_assoc V W X Y Z,

Goal state after:
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C : Type u₁
inst✝ : EnrichedCategory V C
W X Y Z : C
⊢ (α_ (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom ≫
      (α_ (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv ≫ (eComp V W X Y ▷ Y ⟶[V] Z) ≫ eComp V W Y Z =
    (eComp V W X Y ▷ Y ⟶[V] Z) ≫ eComp V W Y Z
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ((T.unionProd S).preimage (β_ X Y).hom).image (β_ X Y).hom = T.unionProd S

Tactic:
preimage_image_of_isIso

Goal state after:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ T.unionProd S = T.unionProd S
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ (((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝)).toFunctor =
    (Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝).toFunctor

Tactic:
exact adj.homEquiv_naturality_left_symm _ _

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

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

Tactic:
rw [SimplexCategory.mono_iff_injective]
  exact (homEquiv f).injective

Goal state after: