mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inr' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inl' y z)) i)

Tactic:
rw [e₁, e₂, e₃, e₄]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
⊢ Function.Injective ⇑(objEquiv z)

Tactic:
a

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a : Fin (n + 1)
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, (objEquiv z) a = (objEquiv z) a₂ → a = a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ < ⨆ x, P.rank' ⋯ + 1

Tactic:
← Nat.add_one_le_iff

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ + 1 ≤ ⨆ x, P.rank' ⋯ + 1
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ G, ∃ (_ : P G), ∃ f, ¬A.Factors f

Tactic:
by_contra!

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X : C
A : Subobject X
hA : A ≠ ⊤
this : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ False
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst✝ : Mono i
hi : ¬IsIso i
⊢ ∃ G, ∃ (_ : P G), ∃ g, ∀ (f : G ⟶ X), f ≫ i ≠ g

Tactic:
by_contra!

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst✝ : Mono i
hi : ¬IsIso i
this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ f, f ≫ i = g
⊢ False
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms

Tactic:
dsimp [colimitsCardinalClosure]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
⊢ (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ)).IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms

Tactic:
by
  dsimp [colimitsCardinalClosure]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsCardinalClosure κ)

Tactic:
dsimp [colimitsCardinalClosure]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ))
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsCardinalClosure κ)

Tactic:
by
  dsimp [colimitsCardinalClosure]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ S)

Tactic:
dsimp [colimitsCardinalClosure]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ (P.colimitsClosure (SmallCategoryCardinalLT.categoryFamily κ)).IsClosedUnderColimitsOfShape
    (SmallCategoryCardinalLT.categoryFamily κ S)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ S)

Tactic:
by
  dsimp [colimitsCardinalClosure]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts

Tactic:
have := P.isClosedUnderColimitsOfShape_colimitsCardinalClosure κ
    WalkingParallelPair (HasCardinalLT.of_le (by
      simp only [hasCardinalLT_aleph0_iff]
      infer_instance)
    (Cardinal.IsRegular.aleph0_le Fact.out))
  infer_instance

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (f.filtration m)

Tactic:
rw [← f.iSup_filtration_iio m hm]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (⨆ i, f.filtration ↑i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }

Tactic:
by_contra!

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
this : Nonempty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
⊢ False
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
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : k.succ ≤ (x.cast hd).simplex.1 i
⊢ l.succ ≤ i

Tactic:
by_contra!

Goal state after:
case refine_1
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 : k.succ ≤ (x.cast hd).simplex.1 i
this : i < l.succ
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
t : Type₁ k n
ht : min t.x ⋯ = t.index.succ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
isIndex : IsIndex x hd l.succ
h : { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x = t.x
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } = t

Tactic:
obtain ⟨y, d', hd', l', isIndex'⟩ := t

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
isIndex : IsIndex x hd l.succ
hs :
  min { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x ⋯ =
    { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.index.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
isIndex' : IsIndex y hd' l'.succ
ht :
  min { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.x ⋯ =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.index.succ
h :
  { x := x, d := d, hd := hd, index := l, isIndex := isIndex }.x =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }.x
⊢ { x := x, d := d, hd := hd, index := l, isIndex := isIndex } =
    { x := y, d := d', hd := hd', index := l', isIndex := isIndex' }
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 + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
⊢ l ≤ y

Tactic:
by_contra!

Goal state after:
case refine_2
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
this : y < l
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp [Codiscrete.eq_id]

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

Goal state before:
pp: case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp [Codiscrete.eq_id]

Goal state after:
case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ F.map iso.hom = F.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp [Codiscrete.eq_id]

Goal state after:
case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ F.map iso.inv = F.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case one.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp [Codiscrete.eq_id]

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

Goal state before:
pp: 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
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
⊢ x = y

Tactic:
by
  have h₁ := hl.isType₂_δ.type₁_eq_of_δ_eq hl'.type₁ h.symm rfl
  have h₂ := hl.isType₂_δ.type₁_eq_of_δ_eq hl.type₁ rfl rfl
  exact congr_arg Type₁.x (h₂.symm.trans h₁)

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

Goal state before:
pp: X Y Z : SSet
⊢ SSet.evaluation.map (SimplexCategory.δ 1).op ≫ toπ₀NatTrans =
    SSet.evaluation.map (SimplexCategory.δ 0).op ≫ toπ₀NatTrans

Tactic:
by ext X s; exact π₀.sound (Edge.mk' s)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ IsIso ((F.map f₁).app X₂)

pp: case sq
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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
· exact isIso_of_isInitial hX₁ hY₁ _

Goal state after:
case sq
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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ (ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 1 (op ⦋0⦌)) = TopCat.toSSetObj₀Equiv.symm 1

Tactic:
apply yonedaEquiv.symm.injective
  trans stdSimplex.δ 0 ≫ toSSetObjI
  · simp [← yonedaEquiv_symm_comp, stdSimplex.δ_zero_eq_const]
  · simp

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
have hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop := by
    simpa [c] using Tendsto.atTop_mul_const (by linarith) (tendsto_pow_atTop_atTop_of_one_lt ha)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
⊢ IsPathConnected sᶜ

Tactic:
obtain ⟨a, ha⟩ : sᶜ.Nonempty := (hs.dense_compl ℝ).nonempty

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
⊢ IsPathConnected sᶜ
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
by
  classical
  let c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
  have hcᵢ : Tendsto (fun n ↦ v i (c n)) atTop (𝓝 (v i b)) := by
    have : v i a⁻¹ < 1 := map_inv₀ (v i) a ▸ inv_lt_one_of_one_lt₀ ha
    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (v i b)
  have hcⱼ (j : ι) (hj : j ≠ i) : atTop.Tendsto (fun n ↦ v j (c n)) (𝓝 0) := by
    have : 1 < v j a⁻¹ := map_inv₀ (v j) _ ▸
      (one_lt_inv₀ <| (v j).pos fun h ↦ by linarith [map_zero (v _) ▸ h ▸ ha]).2 (haj j hj)
    simpa [c] using (tendsto_div_one_add_pow_nhds_zero this).mul_const _
  have hcₙ : atTop.Tendsto (fun n ↦ w (c n)) (𝓝 (w b)) := by
    have : w a⁻¹ < 1 := map_inv₀ w _ ▸ inv_lt_one_of_one_lt₀ haw
    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (w b)
  simp_rw +instances [OrderTopology.topology_eq_generate_intervals,
    TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_atTop_sets, Set.mem_preimage] at hcⱼ
  choose r₁ hr₁ using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_const_lt hb hcᵢ
  choose rₙ hrₙ using fun j hj ↦ hcⱼ j hj (.Iio 1) (by simpa using ⟨1, .inr rfl⟩) (by simp)
  choose rN hrN using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_lt_const hbw hcₙ
  have := Fintype.ofFinite ι
  let r := max (Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h) rN
  refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
  · exact le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl
  · exact hrₙ j hj _ <| le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _
  · exact hrN _ <| le_max_iff.2 (.inr le_rfl)

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ False

Tactic:
apply this (inv_ne_zero ha₀) (by simpa) hb₀ hb₁ (by simpa)

Goal state after:
case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ 1 < v a⁻¹
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : analyticOrderAt f z₀ = ⊤
⊢ analyticOrderAt (f • g) z₀ = ⊤

Tactic:
by
  rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *
  obtain ⟨t, h₁t, h₂t, h₃t⟩ := hf
  exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑(s + 1)
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x + 1 = ↑(s + 1)

Tactic:
rw [Nat.cast_succ]

Goal state after:
case coe
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑(s + 1)
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x + 1 = ↑s + 1