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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
⊢ (if x✝¹ + x✝ = 0 then 0 else exp (-(x✝¹ + x✝).valuation)) ≤
    max (if x✝¹ = 0 then 0 else exp (-x✝¹.valuation)) (if x✝ = 0 then 0 else exp (-x✝.valuation))

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 ≤ max 0 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 ≤ max 0 (exp (-x✝.valuation))

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 ≤ max (exp (-x✝¹.valuation)) 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max 0 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max 0 (exp (-x✝.valuation))

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max (exp (-x✝¹.valuation)) 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))
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
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Tactic:
split_ifs

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ 0 = 0
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₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A

Tactic:
S₁.s.cofan_inj_eq,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.ι (unop A.fst).len ≫ S₁.X.map A.e.op) ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n = PInfty.f n

Tactic:
by
  conv_rhs => rw [← id_comp (PInfty.f n)]
  dsimp only [AlternatingFaceMapComplex.obj_X]
  rw [s.decomposition_id, Preadditive.sum_comp]
  rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]
  rintro A (hA : ¬A.EqId)
  rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

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

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

pp: case pos.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
· intro b _ hb
      rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]

Goal state after:
case pos.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
⊢ (if ↑x.1 ≤ 1 / 2 then (F.extend (2 * ↑x.1)) x.2 else (G.extend (2 * ↑x.1 - 1)) x.2) =
    if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

Tactic:
split_ifs

Goal state after:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.extend (2 * ↑x.1 - 1)) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
⊢ P { toFun := fun x ↦ if ↑t ≤ 1 / 2 then (F.extend (2 * ↑t)) x else (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }

Tactic:
split_ifs

Goal state after:
case pos
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (F.extend (2 * ↑t)) x, continuous_toFun := ⋯ }

case neg
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ if ↑t ≤ 1 / 2 then (F.extend (2 * ↑t)) x else (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }
      x =
    f₀ x

Tactic:
split_ifs

Goal state after:
case pos
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
h✝ : ↑t ≤ 1 / 2
⊢ { toFun := fun x ↦ (F.extend (2 * ↑t)) x, continuous_toFun := ⋯ } x = f₀ x

case neg
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
h✝ : ¬↑t ≤ 1 / 2
⊢ { toFun := fun x ↦ (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ } x = f₀ x
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p

Tactic:
induction p using Path.Homotopic.Quotient.ind
  simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]
  congr

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Nullhomotopic

Tactic:
use default

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Homotopic (const X default)
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then (F.eval x.1).extend (2 * ↑x.2) else (G.eval x.1).extend (2 * ↑x.2 - 1)) =
    if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

Tactic:
split_ifs

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩

case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ (G.eval x.1).extend (2 * ↑x.2 - 1) = (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then ↑x.1 * 2 * ↑x.2 else ↑x.1 * (2 - 2 * ↑x.2)) ∈ I

Tactic:
split_ifs

Goal state after:
case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I

Tactic:
split_ifs

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I

case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I

Tactic:
split_ifs

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I

case pos
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I

case neg
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map (homMk (resolutionMap (f ≫ g))) =
    toHoCat.map (homMk (resolutionMap f)) ≫ toHoCat.map (homMk (resolutionMap g))

Tactic:
by
    rw [← toHoCat.map_comp]
    exact resolutionObj_hom_ext (by simpa using .refl _)

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

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift

Tactic:
by
    let h := factorizationData (cofibrations C) (trivialFibrations C)
      (pushout.desc p g sq.w)
    have sq' : CommSq (𝟙 X) (pushout.inl _ _ ≫ h.i) p h.p := .mk
    have h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p) := by simpa
    have h₂ := comp_mem _ _ _ ((cofibrations C).of_isPushout
      (IsPushout.of_hasPushout f i) (mem_cofibrations i)) h.hi
    rw [← cofibration_iff] at h₂
    have : WeakEquivalence (pushout.inl f i ≫ h.i) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_postcomp _ _ _ h.hp.2 h₁
    exact ⟨⟨{ l := pushout.inr f i ≫ h.i ≫ sq'.lift
              fac_left := by
                simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left }⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ (p.trans q).trans r =
    (p.trans (q.trans r)).reparam (fun t ↦ ⟨transAssocReparamAux t, ⋯⟩) trans_assoc_reparam._proof_1 ⋯ ⋯

Tactic:
ext x
  simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam]
  split_ifs
  iterate 12 grind
  · linarith
  · linarith
  · grind

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ f).trans f = ⟦Path.refl Y.as⟧

Tactic:
by rintro _ _ ⟨f⟩; exact Quotient.sound ⟨(Path.Homotopy.reflSymmTrans f).symm⟩

Goal state after:
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:
intro X₁

Goal state after:
T : Type u'
X₁ : T → Type u
⊢ ∀ (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)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ ∀ {x y z : X₁ ⊕ X₂}, Rel' f g x y → Rel' f g y z → Rel' f g x z

Tactic:
rintro x y z (_ | ⟨_, _, h⟩ | s | _) hyz
    · exact hyz
    · obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
        · exact Rel'.inl_inl _ _ h
        · obtain rfl := (mono_iff_injective f).1 inferInstance h''
          exact Rel'.inl_inl _ _ (h.trans h')
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr
    · obtain z₁ | z₂ := z
      · replace hyz := hyz.symm
        rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s', rfl, hs'⟩ := hyz
        exact Rel'.inl_inl _ _ hs'
      · rw [inr_rel'_inr_iff] at hyz
        subst hyz
        apply Rel'.inl_inr
    · obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
        · apply Rel'.inr_inl
        · obtain rfl := (mono_iff_injective f).1 inferInstance h'
          rw [h]
          apply Rel'.inr_inl
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        apply Rel'.refl

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
⊢ Function.Injective ⇑(ConcreteCategory.hom k)

Tactic:
intro x₃

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₄
⊢ ∀ ⦃a₂ : (fun X ↦ X) X₄⦄, (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) a₂ → x₃ = a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ (skeletonOfMono i) (n + 1) =
    (skeletonOfMono i) n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
by
  dsimp only [skeletonOfMono, OrderHom.coe_mk]
  apply le_antisymm
  · simp only [sup_le_iff, iSup_le_iff, skeleton_succ]
    refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
    by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
    · exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left
    · exact (le_trans (by exact le_trans (by rfl) (le_iSup _ hx))
        (le_iSup _ x)).trans le_sup_right
  · simp only [sup_le_iff, iSup_le_iff]
    exact ⟨⟨le_sup_left, (Y.skeleton.monotone (by simp)).trans le_sup_right⟩,
      fun _ _ ↦ (Y.ofSimplex_le_skeleton _ (by simp)).trans le_sup_right⟩

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

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (f.arrow k) = g.vertex k.castSucc

Tactic:
← g.arrow_src k,

Goal state after:
case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (f.arrow k) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (g.arrow k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ f = X.spine m h (sx.spineToSimplex m h f)

Tactic:
exact sx.spine_spineToSimplex_apply m h f |>.symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| (((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom) ≫ (f ⊗ₘ g ⊗ₘ h)

Tactic:
unitors_inv_equal,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| (((ρ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom) ≫ (f ⊗ₘ g ⊗ₘ h)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      (ρ_ (𝟙_ W)).hom ≫
        Functor.LaxMonoidal.ε F ≫
          (ρ_ (F.obj (𝟙_ V))).inv ≫
            F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
              (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
                Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
unitors_inv_equal,

Goal state after:
V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (ρ_ (𝟙_ W)).inv ≫
      (ρ_ (𝟙_ W)).hom ≫
        Functor.LaxMonoidal.ε F ≫
          (ρ_ (F.obj (𝟙_ V))).inv ≫
            F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
              (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
                Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ (Truncated.Edge.map (𝟙rq x) f).edge =
    (𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)).edge

Tactic:
simp [← NatTrans.naturality_apply, reflQuiver_id]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg Y

Tactic:
simpa using r.degHom_le f (𝟙 Y)

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ mk (n + 1) ⟶ mk n

Tactic:
by
    induction i using Fin.lastCases with
    | last => exact σ (Fin.last n)
    | cast i => exact σ i

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

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi e

Tactic:
exact isSplitEpi_P_σ he |>.exists_splitEpi.some

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

Goal state before:
pp: case cons
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
⊢ standardσ (if j < a then j :: a :: L else a :: simplicialInsert (j + 1) L) ⋯ =
    standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
split_ifs

Goal state after:
case pos
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : j < a
⊢ standardσ (j :: a :: L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)