mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_δ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk n'
j : Fin (n' + 2)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m

Tactic:
obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h

Goal state after:
case comp_δ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ ∃ z_1 e_1 m_1, ∃ (_ : P_σ e_1) (_ : P_δ m_1), (e ≫ m) ≫ δ j = e_1 ≫ m_1
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk (n' + 1)
j : Fin (n' + 1)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m

Tactic:
obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h

Goal state after:
case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
⊢ ∃ z_1 e_1 m_1, ∃ (_ : P_σ e_1) (_ : P_δ m_1), (e ≫ m) ≫ σ j = e_1 ≫ m_1
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (0 + 1)
i✝ : Fin (0 + 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ (e ≫ f ≫ δ i✝) ≫ σ j = e ≫ f

Tactic:
simp [switch_δ_σ₀]

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

Goal state before:
pp: case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk (n' + 1)
j : Fin (n' + 1)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m

Tactic:
| @comp_σ n n' f j h =>

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

Goal state before:
pp: X : SSet
y : X.S
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace y
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm y)

Tactic:
obtain ⟨d', y, rfl⟩ := y.mk_surjective

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm { dim := d', simplex := y })
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace y
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }

Tactic:
obtain ⟨d', y, rfl⟩ := y.mk_surjective

Goal state after:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := { dim := d', simplex := y }.dim,
      simplex :=
        (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y }.dim⦌)))
          { dim := d', simplex := y }.simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := { dim := d + 1, simplex := y }.dim,
      simplex :=
        (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y }.dim⦌)))
          { dim := d + 1, simplex := y }.simplex }

Tactic:
iff

Goal state after:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
⊢ ∃! i,
    (ConcreteCategory.hom (SimplicialObject.δ Y i))
        ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y }.dim⦌)))
          { dim := d + 1, simplex := y }.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
        { dim := d, simplex := x }.simplex
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ Monotone (map' f)

Tactic:
intro x y hxy

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
⊢ map' f x ≤ map' f y
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)
⊢ (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:
have e₂ := inr'_eval x y i

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)
⊢ (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)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ (↑(h.equivII s)).IsUniquelyCodimOneFace (↑(h.pairing.p (h.equivII s))).toS

Tactic:
simpa using h.isUniquelyCodimOneFace s

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
⊢ { app := fun X ↦ (c X).fst, naturality := ⋯ } ≫ f = { app := fun X ↦ (c X).snd, naturality := ⋯ } ≫ g

Tactic:
ext; simp [(c _).condition]

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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i = f.filtration m

Tactic:
apply le_antisymm
  · simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro j hj
    exact f.filtration_monotone hj.le
  · conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]
    exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦
      (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans
        (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.mpr hj⟩))⟩

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 : IsLimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape K (Type w')
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hcX : IsColimit cX
⊢ Nonempty (IsColimit (c.pt.mapCocone cX))

Tactic:
by
    have := fun k ↦ preservesColimitsOfShape_of_isCardinalAccessible (F.obj k) κ J
    exact ⟨Accessible.Limits.isColimitMapCocone c
      (fun Y ↦ isLimitOfPreserves ((evaluation C (Type w')).obj Y) hc) κ hK cX
      (fun k ↦ isColimitOfPreserves (F.obj k) hcX)⟩

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✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
⊢ Set.range ⇑(ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(ConcreteCategory.hom ((f.b j).app d)) = Set.univ

Tactic:
ext ⟨x, hx⟩
  -- generated by `simp? [filtration_def, Subtype.ext_iff] at hx ⊢`
  simp only [filtration_def, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Subfunctor.homOfLe_app,
    TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, Set.sup_eq_union, Set.mem_range, Subtype.ext_iff,
    Subtype.exists, exists_eq_right, Set.mem_univ, iff_true] at hx ⊢
  obtain hx | ⟨i, hi, c, hx⟩ := hx
  · exact Or.inl (Or.inl hx)
  · obtain hi | rfl := hi.lt_or_eq
    · exact Or.inl (Or.inr ⟨i, hi, c, hx⟩)
    · rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx
      obtain ⟨y, hy⟩ := hx
      exact Or.inr ⟨_, hy⟩

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✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₁ f c) = { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

Tactic:
dsimp only [Cell.type₁, mapN]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ { dim := c.dim + 1,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim + 1⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
              (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌)))) } =
    { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : ↑c.s = ↑(P.p c'.s)
⊢ Cell.type₂ f c = Cell.type₁ f c'

Tactic:
exact (P.ne _ _ h.symm).elim

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) } = { down := x ≫ s.ι.app j }

Tactic:
apply ULift.down_injective

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt := ⋯
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) }.down = { down := x ≫ s.ι.app j }.down
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerAnodyneExtensions Λ[n, i].ι

Tactic:
rw [innerAnodyneExtensions_eq_llp_rlp]

Goal state after:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (F.map f₁).app X₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.left β) =
    (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)

Tactic:
by
          have := Arrow.w β =≫ sq₁₃.fst
          dsimp at this
          simp only [Category.assoc, sq₁₃.π_fst] at this
          simp only [← adj₂.homEquiv_symm_naturality_one,
            ← adj₂.homEquiv_symm_naturality_two,
            Arrow.mk_left, Arrow.mk_right, this]

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

Goal state before:
pp: case inl.inr.refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (x.cast hd).simplex.1 i.castSucc ≤ k.castSucc

Tactic:
simplex_fst_le_castSucc_iff

Goal state after:
case inl.inr.refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ i.castSucc < min x hd
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty sq₁₂.ι p

Tactic:
internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty j sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty sq₁₂.ι p

Tactic:
internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty j sq₁₃.π
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
· rcases eq_or_ne (card ι) 2 with (hc | hc)
    · -- If `ι` has two elements this is `exists_one_lt_lt_one_of_not_isEquiv`.
      let ⟨j, hj⟩ := (Nat.card_eq_two_iff' i).1 <| card_eq_nat_card ▸ hc
      let ⟨a, ha⟩ := (v i).exists_one_lt_lt_one_of_not_isEquiv (h i) (h j) (hv hj.1.symm)
      exact ⟨a, ha.1, fun _ h ↦ hj.2 _ h ▸ ha.2⟩
    have hlt : 2 < card ι := Nat.lt_of_le_of_ne (one_lt_card_iff_nontrivial.2 ‹_›) hc.symm
    -- Otherwise, choose another distinguished index `j ≠ i`.
    let ⟨j, hj⟩ := exists_ne i
    -- Apply induction first on the subcollection `v i` for `i ≠ j` to get `a : K`
    let ⟨a, ha⟩ := ih {k : ι // k ≠ j} (card_subtype_lt fun a ↦ a rfl) (restrict _ v)
      (fun i ↦ h _) (hv.comp_of_injective val_injective) ⟨i, hj.symm⟩
    -- Then apply induction next to the subcollection `{v i, v j}` to get `b : K`.
    let ⟨b, hb⟩ := ih {k : ι // k = i ∨ k = j} (by linarith [card_subtype_eq_or_eq_of_ne hj.symm])
      (restrict _ v) (fun _ ↦ h _) (hv.comp_of_injective val_injective) ⟨i, .inl rfl⟩
    rcases eq_or_ne (v j a) 1 with (ha₁ | ha₁)
    · -- If `v j a = 1` then take a large enough value from the sequence `a ^ n * b`.
      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)
    rcases ha₁.lt_or_gt with (ha_lt | ha_gt)
    · -- If `v j a < 1` then `a` works as the divergent point.
      refine ⟨a, ha.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact ha_lt; exact ha.2 ⟨k, h⟩ (by grind)
    · -- If `1 < v j a` then take a large enough value from the sequence `b / (1 + a ^ (-n))`.
      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_one_lt ha.1 ha.2 ha_gt hb.1 (hb.2 ⟨j, .inr rfl⟩
        (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
⊢ ?m.165 ≠ 0

Tactic:
linarith [h.log_div_log_pos ha₀ ha₁]

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

Goal state before:
pp: X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY = ⊤

Tactic:
refine SimplexCategory.Truncated.morphismProperty_eq_top _
    (fun n hn i ↦ ?_) (fun n hn i ↦ ?_)
  · obtain _ | _ | n := n
    · fin_cases i
      · ext; apply hδ₀
      · ext; apply hδ₁
    · fin_cases i
      · ext; apply hδ'₀ f₀ f₁ hδ₁ hδ₀ hY
      · ext; apply hδ'₁ f₀ f₁ hδ₁ hδ₀ H hY
      · ext; apply hδ'₂ f₀ f₁ hδ₁ hδ₀ hY
    · lia
  · obtain _ | _ | n := n
    · fin_cases i
      ext; apply hσ
    · fin_cases i
      · ext; apply hσ'₀ f₀ f₁ hδ₁ hδ₀ hσ hY
      · ext; apply hσ'₁ f₀ f₁ hδ₁ hδ₀ hσ hY
    · lia

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

pp: case neg.ha
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0

Tactic:
· module

Goal state after:
case neg.ha
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℂ → ℂ
s : Set ℂ
f' g' x : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x

Tactic:
by
  simpa using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt

Goal state after: