mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

Tactic:
induction x using Quotient.inductionOn with | _ f
  intro hf
  change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)
  rw [PadicSeq.norm_eq_zpow_neg_valuation]
  · rw [Rat.cast_zpow, Rat.cast_natCast]
  · apply CauSeq.not_limZero_of_not_congr_zero
    contrapose hf
    apply Quotient.sound
    simpa using hf

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

Goal state before:
pp: case neg.h.hj₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ j.succ.succ.pred ⋯ ≠ 0

pp: case neg.h.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ ↑(j.succ.succ.pred ⋯) + q

pp: case neg.h.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < j.succ.succ

Tactic:
· simp [Fin.succ_ne_zero]

Goal state after:
case neg.h.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ ↑(j.succ.succ.pred ⋯) + q

case neg.h.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < j.succ.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ

Tactic:
rw [h]

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ (unop A.fst).len = (unop Δ).len

Tactic:
rw [h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop A.fst).len

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len

Tactic:
by
    simp only [dif_neg this, dif_pos hi]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f

Tactic:
rw [h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₁.f n = Φ₂.f n

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ (P (n + 1)).f (n + 1) = 0

Tactic:
σ_comp_P_eq_zero X i

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ 0 = 0

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ

Tactic:
←
      image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)),

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))) ≫
      image.ι (θ'.unop ≫ A.e) =
    (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i : Δ' ⟶ ⦋n⦌
hi : Mono i
h₁ : Δ'.len ≠ n
h₂ : ¬Isδ₀ i
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
induction Δ' using SimplexCategory.rec with

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
⊢ PInfty.f n ≫ X.map i.op = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ∀ [IsIso (N₁.map f)], IsIso f

Tactic:
by
    intro
    -- restating the result in a way that allows induction on the degree n
    suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌)) by
      have : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
      apply NatIso.isIso_of_isIso_app
    -- restating the assumption in a more practical form
    have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
    have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
    have h₃ := fun n =>
      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
    simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃
    -- we have to construct an inverse to f in degree n, by induction on n
    intro n
    induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ isoN₁ = Γ₂N₁

Tactic:
dsimp only [isoN₁]
  ext1
  rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
  ext X : 2
  rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
    Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
  dsimp only [Functor.comp_obj, Preadditive.DoldKan.equivalence_inverse, Preadditive.DoldKan.Γ.eq_1,
    toKaroubiEquivalence, Functor.asEquivalence_functor, Preadditive.DoldKan.N.eq_1,
    NatTrans.id_app]
  rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]

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

Goal state before:
pp: case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op

Tactic:
induction Δ' using SimplexCategory.rec with

Goal state after:
case mk.mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f ⦋n'⦌.len ≫ X.map i.op
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (Γ₂N₂.natTrans.app P) = inv (N₂Γ₂.inv.app (N₂.obj P))
⊢ IsIso (N₂.map (Γ₂N₂.natTrans.app P))

Tactic:
rw [h]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (Γ₂N₂.natTrans.app P) = inv (N₂Γ₂.inv.app (N₂.obj P))
⊢ IsIso (inv (N₂Γ₂.inv.app (N₂.obj P)))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ ≍ ⟦p₂⟧

Tactic:
heq_iff_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ = ⟦p₂⟧
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R : (localizerMorphism C).LeftResolution X
⊢ WeakEquivalence R.w

Tactic:
simpa only [weakEquivalence_iff] using R.hw

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y x' y' : X
p : Path.Homotopic.Quotient x y
hx : x' = x
hy : y' = y
⊢ eqToHom ⋯ ≫ p ≫ eqToHom ⋯ = p.cast hx hy

Tactic:
by
  subst hx hy; simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ Subfunctor.equalizer f g

Tactic:
rw [h]

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

Goal state before:
pp: case pos
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : m < n
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
simp [boundary_obj_eq_univ m n h₃]

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ x₂ : X₁ i₁
hx : (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₂)
⊢ (hom (Sigma.ι X₁ i₁)) x₁ = (hom (Sigma.ι X₁ i₁)) x₂

Tactic:
obtain rfl := h _ (Cofan.inj_injective_of_isColimit (coproductIsCoproduct X₂) i₁ hx)

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
hx : (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁)
⊢ (hom (Sigma.ι X₁ i₁)) x₁ = (hom (Sigma.ι X₁ i₁)) x₁
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
⊢ ∀ (X₁ X₂ : T → Type u) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) → monomorphisms (Type u) (Limits.Sigma.map f)

Tactic:
by
    intro X₁ X₂ _ _ f h
    simp only [monomorphisms.iff, mono_iff_injective] at h ⊢
    intro x₁ x₂ hx
    obtain ⟨i₁, x₁, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₁
    obtain ⟨i₂, x₂, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₂
    simp only [cofan_mk_inj] at hx ⊢
    replace hx : Sigma.ι X₂ i₁ (f i₁ x₁) = Sigma.ι X₂ i₂ (f i₂ x₂) := by
      have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
      have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
      simp only [comp_apply] at h₁ h₂ hx
      simpa [← h₁, ← h₂]
    obtain rfl := Cofan.eq_of_inj_apply_eq_of_isColimit (coproductIsCoproduct X₂) _ _ hx
    obtain rfl := h _ (Cofan.inj_injective_of_isColimit (coproductIsCoproduct X₂) i₁ hx)
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : (ConcreteCategory.hom g) s✝ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
rw [h]

Goal state after:
case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : (ConcreteCategory.hom g) s✝ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) w✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ IsPullback t l r b

Tactic:
rw [isPullback_iff]
  refine ⟨h.w, fun x₁ y₁ ⟨h₂, _⟩ ↦ ht h₂, fun x₂ x₃ hx ↦ ?_⟩
  have := (pushoutCocone_inl_eq_inr_iff_of_isColimit h.isColimit ht x₂ x₃).1 hx
  grind

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin (n + 1)
⊢ f.vertex i = g.vertex i

Tactic:
rw [h]

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin n
⊢ f.arrow i = g.arrow i

Tactic:
rw [h]

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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨j, by omega⟩ hij)

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: ⊢ generators.multiplicativeClosure = ⊤

Tactic:
by
  apply le_antisymm (by simp)
  rintro x y f -
  induction f using CategoryTheory.Quotient.induction with | _ f
  induction f using Paths.induction with
  | id => exact generators.multiplicativeClosure.id_mem _
  | comp _ k h =>
    cases k
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

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

Goal state before:
pp: case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ →
    List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) →
      ((∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧ x✝ ≤ m ↔
        ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k)

Tactic:
and_comm

Goal state after:
case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ →
    List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) →
      ((x✝ ≤ m ∧ ∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ↔
        ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case neg
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
obtain _ | a := a

Goal state after:
case neg.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : 0 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : x = y
⊢ x.len = y.len

Tactic:
rw [h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
· rw [Eq.comm, hx, map'_last]
      rw [map'_eq_last_iff] at hx ⊢
      intro i
      apply hx

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

Goal state before:
pp: case refine_1
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) ≤ ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
simp only [iSup_le_iff, Discrete.forall]
    intro i
    exact le_trans (by rfl) (le_iSup _ i)

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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ c.horn.image c.map ≤ (↑(P.p c.s)).subcomplex

Tactic:
simpa using! image_le_range c.horn c.map

Goal state after: