mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x✝¹ : Finset ι
x✝ : x✝¹ ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}
hx : x✝¹ ∈ ⋂ K ∈ s, K.faces
hn : x✝¹ ∈ {t | t.Nonempty}
⊢ x✝¹.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x✝¹ → b.Nonempty → b ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
grind [IsRelLowerSet.mem_of_le, PreAbstractSimplicialComplex.isRelLowerSet_faces,
          mem_iInter]

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

Goal state before:
pp: case right
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
⊢ t ∈ {s | ∃ v, s = {v}}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
          | inl h => exact (ht.ne_empty h).elim
          | inr h => exact ⟨v, h⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
⊢ (P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩

Tactic:
let e' := Subcomplex.N.orderIsoOfIso e hA

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
⊢ (P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
this : Nonempty { f // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
⊢ False

Tactic:
obtain ⟨f, hf⟩ := this

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑(P.ofIso e hA).II
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
⊢ False
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)))
⊢ (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 (tensorObjOf y z) <| Fin.cast (by simp +arith) <| i.castAdd (z.len + 1)

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 ⋯)))
      ((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.ProdStdSimplex

Goal state before:
pp: case fst
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).1 = ((objEquiv ↑z₂) i).1

pp: case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2

Tactic:
· exact DFunLike.congr_fun h i

Goal state after:
case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1 = -((-1) ^ (↑x.2 + 1 + ↑x.1) • H.h x.1.castSucc ≫ Y.δ x.2.succ)

Tactic:
simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 hx,
      pow_add, pow_one, mul_neg, mul_one, neg_mul, neg_smul, neg_neg]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ ((-1) ^ ↑x.1 * (-1) ^ ↑x.2) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    ((-1) ^ ↑x.2 * (-1) ^ ↑x.1) • H.h x.1.castSucc ≫ Y.δ x.2.succ
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case none
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)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app none =
    𝟙 (c x✝).pt ≫ (c x✝).π.app none

pp: case some.left
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)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.left) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.left)

pp: case some.right
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)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.right) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.right)

Tactic:
all_goals simp

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
⊢ f.filtration j ≤ f.filtration i

Tactic:
exact f.filtration_monotone hj.le

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

Goal state before:
pp: case none
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)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app none =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app none

pp: case some.left
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)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.left) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.left)

pp: case some.right
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)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.right) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.right)

Tactic:
all_goals simp

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
j : ι
hj : j < m
⊢ f.filtration j ≤ f.filtration m

Tactic:
exact f.filtration_monotone hj.le

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
· obtain rfl := SimplexCategory.eq_id_of_mono g
    exact ⟨x, Or.inl rfl⟩

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}
J : Type u'
inst✝ : Category.{v', u'} J
hJ : HasCardinalLT (Arrow J) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
by
  obtain ⟨S, ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ
  rw [isClosedUnderColimitsOfShape_iff_of_equivalence _ e.symm]
  infer_instance

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : IsCardinalLocallyPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
exact ⟨_, inferInstance, hP.isStrongGenerator, hP.le_isCardinalPresentable⟩

Goal state after:
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) }
this : Nonempty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
⊢ False

Tactic:
obtain ⟨f, hf⟩ := this

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) }
f : ℕ → ↑P.op.II
hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)
⊢ False
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case mpr
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₁₃.π), Nonempty (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)

Tactic:
intro h α

Goal state after:
case mpr
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₃
h : ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty (Arrow.LiftStruct α)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: 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)
⊢ StrictMono (φ x hd)

Tactic:
rw [Fin.strictMono_iff_lt_succ]

Goal state after:
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 + 1)), φ x hd i.castSucc < φ x hd i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.zero
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hd : x.dim = 0
i : Fin (0 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

pp: case neg.succ
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
· fin_cases i
        simp at hx

Goal state after:
case neg.succ
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁
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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₃ : Arrow C₃
⊢ pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj X₃).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj X₃).hom) ≫
      pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
          (adj₂.homEquiv.symm
            (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom) ((G.map (unop (op X₁)).hom.op).app X₃.right)))
          ⋯ ≫
        ((𝟭 (Arrow C₃)).obj X₃).hom =
    pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj X₃).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj X₃).hom) ≫
      ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).obj X₃).hom ≫
        adj₂.homEquiv.symm
          (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom) ((G.map (unop (op X₁)).hom.op).app X₃.right))

Tactic:
· simp [← homEquiv_symm_naturality_one, ← homEquiv_symm_naturality_three,
      pullback.condition]

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

Goal state before:
pp: case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc.castSucc < j.castSucc.succ.succ

Tactic:
Fin.castSucc_lt_succ_iff,

Goal state after:
case snd.h
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ i.castSucc ≤ j.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.op.PtSimplex (n + 1) (opObjEquiv.symm x)
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι

Tactic:
refine boundary.hom_ext (fun i ↦ ?_)

Goal state after:
case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.op.PtSimplex (n + 1) (opObjEquiv.symm x)
i : Fin (n + 2)
⊢ boundary.ι i ≫ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) =
    boundary.ι i ≫ const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
g : X.PtSimplex (n + 1) x
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι

Tactic:
refine boundary.hom_ext (fun i ↦ ?_)

Goal state after:
case succ
X : SSet
x : X _⦋0⦌
n : ℕ
g : X.PtSimplex (n + 1) x
i : Fin (n + 2)
⊢ boundary.ι i ≫ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    boundary.ι i ≫ const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : x ∈ ((fun s ↦ s.map f) a).finset
⊢ x ∈ ((fun s ↦ s.map f) b).finset

Tactic:
simp only [mem_map_iff] at hx ⊢
    obtain ⟨x, hx, rfl⟩ := hx
    exact ⟨x, h hx, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map

Tactic:
by rw [← Fin.castSucc_succ, h.δ_castSucc_map]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.WithAbs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : Field R
T : Type u_3
inst✝² : Field T
v : AbsoluteValue R S
inst✝¹ : Algebra R T
inst✝ : Algebra.IsSeparable R T
⊢ (algebraMap (WithAbs v) T).comp ↑(equiv v).symm = (↑(RingEquiv.refl T)).comp (algebraMap R T)

Tactic:
ext; simp [algebraMap_left_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.WithAbs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
R : Type u_3
T : Type u_4
inst✝⁴ : Semiring R
v : AbsoluteValue R S
P : Type u_5
inst✝³ : SMul P R
inst✝² : SMul P T
inst✝¹ : SMul R T
inst✝ : IsScalarTower P R T
⊢ ∀ (x : P) (y : WithAbs v) (z : T), (x • y) • z = x • y • z

Tactic:
simp [smul_right_def, smul_left_def]

Goal state after:
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
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
⊢ Pairwise (Function.onFun Disjoint fun t ↦ [c + x -[ℝ] c + t • y] ∩ s)

Tactic:
intro t t' htt'

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ᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ Function.onFun Disjoint (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t t'
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
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
⊢ Pairwise (Function.onFun Disjoint fun t ↦ [c - x -[ℝ] c + t • y] ∩ s)

Tactic:
intro t t' htt'

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ᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
⊢ Function.onFun Disjoint (fun t ↦ [c - x -[ℝ] c + t • y] ∩ s) t t'
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
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
⊢ ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
let P (ι : Type _) [Fintype ι] : Prop :=
    ∀ v : ι → AbsoluteValue R S, (∀ i, (v i).IsNontrivial) →
      (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1

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
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
P : (ι : Type ?u.69) → [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
⊢ ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1