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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
this : { num := n, den := d, den_nz := hn, reduced := hd } = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 ≫ (P q).f 0 = (P q).f 0

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)

Tactic:
· rw [P_f_0_eq q, comp_id]

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map ((Q q).f n) = (Q q).f n

Tactic:
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f,
    P_add_Q_f]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 (((whiskering C D).obj G).obj X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n + 1 ≤ q
⊢ (P (q + 1)).f (n + 1) = (P q).f (n + 1)

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0⁻¹.valuation = -valuation 0

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation

Tactic:
· simp

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (0 ^ (n + 1)).valuation = ↑(n + 1) * valuation 0

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation

Tactic:
· simp

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a = g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a

pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ ∑ x, (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev

Tactic:
· simp

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ ∑ x, (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T U : C
g : T ⟶ U
f : X _⦋0⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T U : C
g : T ⟶ U
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
· simp

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T U : C
g : T ⟶ U
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ DegeneraciesVanish (PInfty.f 0)

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f (n + 1))

Tactic:
· simp

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
f : X _⦋0⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f 0 ≫ f = 0

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f (n + 1) ≫ f = 0

Tactic:
· simp

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f (n + 1) ≫ f = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0

Tactic:
· simp

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧

Tactic:
by grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
by grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1

Tactic:
by grind

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

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

Tactic:
split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)

Tactic:
by grind

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)

Tactic:
by grind

Goal state after:
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 <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq.HasLift

Tactic:
exact ⟨⟨{
    l := Over.homMk sq'.lift
      (by rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r])
  }⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) (bifibrantResolutionMap f)

Tactic:
change weakEquivalences _ (CofibrantObject.homMk (bifibrantResolutionMap f).hom)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ weakEquivalences (CofibrantObject C) (homMk (bifibrantResolutionMap f).hom)
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (fibrations (Over S)).IsStableUnderRetracts

Tactic:
rw [fibrations_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₂

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₃

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₂ ≤ x₄

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
x₁ x₂ x₃ x₄ : T
inst✝ : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₃ ≤ x₄

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x✝ : (MultispanShape.prod ι).L
⊢ (match x✝ with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).fst x✝)

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x✝ : (MultispanShape.prod ι).L
⊢ (match x✝ with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).snd x✝)

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
i j : Bool
⊢ (bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂) = (bif i then x₃ else x₂) ⊓ bif j then x₃ else x₂

Tactic:
by grind

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

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n + 1].obj (op ⦋m⦌)

Tactic:
· obtain ⟨i, q, rfl⟩ := SimplexCategory.eq_comp_δ_of_not_surjective f (fun hf ↦ by
      rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia)
    apply face_singleton_compl_le_boundary i
    rw [stdSimplex.face_singleton_compl, stdSimplex.objEquiv_symm_comp,
      ← Subcomplex.ofSimplex_le_iff]
    apply Subcomplex.ofSimplex_map_le

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

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
⊢ j ∈ (∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv).obj (op ⦋d⦌) ↔ j ∈ ∂Δ[n].obj (op ⦋d⦌)

Tactic:
simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_boundary_iff_notMem_range, Set.mem_range,
    stdSimplex.opObjEquiv_opObjEquiv_symm_apply, not_exists]

Goal state after:
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) ↔ ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i.rev
h₂ : ∀ (x : Fin (d + 1)), ¬j x = k
⊢ ¬k.rev = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k.rev

Tactic:
by grind

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
⊢ m =
    ↾Quot.lift
        (fun x ↦
          match x with
          | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
          | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
        ⋯

Tactic:
ext ⟨x₁ | x₂⟩

Goal state after:
case mk.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₁ : X₁
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inl x₁)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inl x₁))

case mk.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inr x₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (cofibrations SSet).IsMultiplicative

Tactic:
rw [cofibrations_eq]
  infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (cofibrations SSet).IsStableUnderRetracts

Tactic:
rw [cofibrations_eq]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (terminal.from X)

Tactic:
Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y),

Goal state after:
X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ InnerFibration (p ≫ terminal.from Y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case zero
X : SSet
i : Fin (0 + 2)
g : Λ[0 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

Tactic:
· simp

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ j ≤ k

Tactic:
by grind

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

Goal state before:
pp: n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.succ

Tactic:
fin_cases i
    · exact p.arrow_tgt 0
    · exact q.arrow_tgt 0

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl)

Tactic:
by
  apply sx.spineInjective
  dsimp only [spineEquiv, Equiv.coe_fn_mk]
  rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ ↑k < n + 2

Tactic:
by grind

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑k + 2 ≤ n + 1 + 2

Tactic:
by grind

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + n ≤ n + 1

Tactic:
by grind

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + ↑i = ↑i.succ

Tactic:
by grind

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑triangle)) z =
    (stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))) z

Tactic:
rw [SSet.yonedaEquiv_map]

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑triangle)) z =
    (stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (stdSimplex.objEquiv.symm (SimplexCategory.δ j)))) z
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: case snd
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝⁴ : C
x✝³ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝⁴
x✝² : C
x✝¹ : (coyoneda.obj (Opposite.op x✝⁴)).obj x✝²
x✝ : F.obj x✝²
⊢ ((ConcreteCategory.hom
            (((ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝⁴)) x✝³).app x✝²
              x✝¹)).toFun
        x✝).2 =
    ((ConcreteCategory.hom
            (((ConcreteCategory.hom
                    (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝⁴))
                  x✝³).app
              x✝² x✝¹)).toFun
        x✝).2

Tactic:
· simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
Y : ↑(of W)
⊢ (Quiv.homEquivOfIso e) (e.inv.map (𝟙rq Y)) = (Quiv.homEquivOfIso e) (𝟙rq (e.inv.obj Y))

Tactic:
by simp [Quiv.hom_map_inv_map_of_iso, h_id]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (Cat.FreeRefl.quotientFunctor C ⋙ (adj.counit.app (Cat.of C)).toFunctor).map f.toPath =
    eqToHom ⋯ ≫ (pathComposition C).map f.toPath ≫ eqToHom ⋯

Tactic:
dsimp
    simp only [adj_counit_app, composePath_toPath, comp_id, id_comp]
    apply Cat.FreeRefl.lift_map

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

Goal state before:
pp: case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) (Fin.last (n + 1)) = 𝟙 (mk n)

Tactic:
simp only [Fin.lastCases_last]
      exact δ_comp_σ_succ

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

Goal state before:
pp: case succ
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
| succ n =>

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

Goal state before:
pp: case comp_σ.comp_of.succ
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
n : ℕ
j : Fin (n + 1 + 1)
g : y✝ ⟶ mk (n + 1 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
| succ n =>

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

Goal state before:
pp: m a b : ℕ
L : List ℕ
⊢ a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m → IsAdmissible m (a :: b :: L)

Tactic:
by grind

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

Goal state before:
pp: 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✝¹ : x✝² < y✝
x✝ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : 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

Tactic:
by grind

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

Goal state before:
pp: 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✝¹ : x✝² < y✝
x✝ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝² :: y✝ :: xs✝)[k] ≤ m + k
⊢ 0 < xs✝.length + 1 + 1

Tactic:
by grind

Goal state after: