mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ f.rank (g (n₀ + (n + 1))) < f.rank (g (n₀ + n))

Tactic:
rw [← add_assoc]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ f.rank (g (n₀ + n + 1)) < f.rank (g (n₀ + n))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y z : X.N
h : x ≤ y
h' : y ≤ z
⊢ monoOfLE h ≫ monoOfLE h' = monoOfLE ⋯

Tactic:
symm
  simp [monoOfLE_eq_iff]

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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ ∃ s, x = h.type₁ s ∨ x = h.type₂ s

Tactic:
exact ⟨s, Or.inl (by rwa [N.ext_iff, SSet.N.ext_iff])⟩

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

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i } ≫ f) ≤ Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
by rfl

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

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
i : ι
⊢ Subcomplex.range (Sigma.ι X i ≫ f) ≤ Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := i } ≫ f)

Tactic:
by rfl

Goal state after:
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
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x ∈ Finset.univ ×ˢ Finset.univ, α x + -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • H.h x_1 ≫ Y.δ x + H.h 0 ≫ Y.δ 0

Tactic:
← Finset.sum_product .univ .univ β,

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
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x ∈ Finset.univ ×ˢ Finset.univ, α x + -∑ x ∈ Finset.univ ×ˢ Finset.univ, β x + H.h 0 ≫ Y.δ 0
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
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0

Tactic:
have hγ₂ : Function.Injective γ₂ := fun _ _ ↦ by aesop

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
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
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 ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ (↑(P.p c.s)).subcomplex

Tactic:
by rfl

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✝ : SuccOrder ι
j : ι
c : f.Cell j
hi : ¬IsMax j
hj : j ≤ j
⊢ (↑(P.p c.s)).subcomplex ≤ (↑(P.p c.s)).subcomplex

Tactic:
by rfl

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
⊢ f.filtration ⊥ ≤ f.filtration ↑⟨⊥, ⋯⟩

Tactic:
by rfl

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
j : ι
hj : j < m
c : f.Cell j
⊢ f.filtration (Order.succ j) ≤ f.filtration ↑⟨Order.succ j, ⋯⟩

Tactic:
by rfl

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

Goal state before:
pp: case mem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : X.N
a✝ : s.subcomplex ≤ ⊤
hs : s.subcomplex ≤ A
⊢ s.subcomplex ≤ ⨆ i, f.filtration i

Tactic:
| mem s hs =>

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

Goal state before:
pp: case a.mem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
hs' : s.subcomplex ≤ A
⊢ s.subcomplex ≤ f.filtration j

Tactic:
exact hs'.trans (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.isoClosure.IsCardinalFilteredGenerator κ
⊢ P.isoClosure ≤ P.isoClosure

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
by
  let e := ShrinkHoms.equivalence.{w} C
  have (k : K) : IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ := by
    dsimp; infer_instance
  rw [← isCardinalPresentable_iff_of_isEquivalence c.pt κ e.functor]
  exact isCardinalPresentable_of_isColimit' _
    (isColimitOfPreserves e.functor hc) κ hK

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ Cardinal.aleph0 ≤ Cardinal.aleph0

Tactic:
by rfl

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ Cardinal.aleph0 ≤ Cardinal.aleph0

Tactic:
by rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: m : ℕ
k : Fin (m + 2)
h0 : 0 < k
hn : k < Fin.last (m + 1)
n : ℕ
⊢ innerAnodyneExtensions (Λ[m + 1, k].unionProd ∂Δ[n]).ι

Tactic:
obtain ⟨k, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hn)
  obtain ⟨k, rfl⟩ := Fin.eq_succ_of_ne_zero
    (Fin.ne_zero_of_lt (show 0 < k from Fin.val_pos_iff.mp h0))
  exact (pairing k.castSucc.succ n).innerAnodyneExtensions

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

Goal state before:
pp: case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ False

Tactic:
apply hx _ hd i.succ

Goal state after:
case inl.inr.refine_3
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ IsIndex x hd i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ J.rlp sq₁₃.π

Tactic:
intro _ _ _ h

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
h : J g✝
⊢ HasLiftingProperty g✝ sq₁₃.π
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left) (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      pushout.desc
          ((α_ X₁.right X₂.right X₃.left).hom ≫
            X₁.right ◁
                pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
          (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
            pushout.desc
              (X₁.right ◁
                  pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              ⋯)
          ⋯ ≫
        pushout.desc
          (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
            pushout.desc
              (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯)
          ((α_ X₁.left X₂.right X₃.right).inv ≫
            pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
          ⋯ =
    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp

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

Goal state before:
pp: case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤

Tactic:
have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
    subsingleton

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

Goal state before:
pp: case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False

Tactic:
· exact (lt_self_iff_false _).1 (X.dim_lt_of_nonDegenerate ⟨x, by simp⟩ 0)

Goal state after:
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✝² x✝¹ : Arrow C₂
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.right
      ((𝟭 (Arrow C₂)).map x✝ ≫
        Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝¹).right))) ⋯)
          ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝²).right))) ⋯)
          ⋯ ≫
        (F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).map x✝)

Tactic:
· apply pullback.hom_ext <;> simp [← homEquiv_naturality_two, ← homEquiv_naturality_three]

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

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₃ : Arrow C₃
⊢ 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 =
    ((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:
apply pushout.hom_ext

Goal state after:
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.inl ((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.inl ((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))

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))
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 m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
⊢ s.index = 0

Tactic:
rwa [← Fin.castSucc_eq_zero_iff]

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 m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
⊢ False

Tactic:
obtain ⟨i, hi⟩ := mem_range_left s.x s.hd 0 (fun h ↦ by simp [Fin.ext_iff] at h)

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
i : Fin ((s.x.cast ⋯).dim + 1)
hi : (s.x.cast ⋯).simplex.1 i = 0
⊢ False
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 : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.succ.castSucc
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
rw [← Fin.succ_castSucc] at hj

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
⊢ stdSimplex.δ j ≫ h.map = const x
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case inl
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
⊢ #↑t ≤ ↑n

Tactic:
apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)

Goal state after:
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case inr
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
⊢ JoinedIn sᶜ a b

Tactic:
let c := (2 : ℝ)⁻¹ • (a + b)

Goal state after:
case inr
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)
⊢ JoinedIn sᶜ a b
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
c : ℕ → R := fun n ↦ 1 / (1 + 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 (𝓝 (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)

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 : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.LinearAlgebra.Complex.Determinant

Goal state before:
pp: ⊢ LinearMap.det ↑↑conjAe = -1

Tactic:
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]
  simp

Goal state after: