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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (↑q.den * r.num * ↑q.den)

Tactic:
by grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h]

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
exact sum_le hs hF

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ ‖z1 + z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]; apply le_max_right

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ * if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1

Tactic:
dif_pos h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩ = 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔ ⟦r⟧ = 0

Tactic:
rw [Padic.zero_def, Quotient.lift_mk, PadicSeq.norm_zero_iff r]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ r ≈ 0 ↔ ⟦r⟧ = ⟦0⟧
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge :
  ε ≤
    if hf : f - const (padicNorm p) (↑f i) ≈ 0 then 0
    else padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hf))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
dif_pos h

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ 0
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
s : ↥S
⊢ s ∈
      ⋃ i,
        Set.range
          ⇑((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).invFun
              ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩) ↔
    s ∈ Set.univ

Tactic:
simp only [Equiv.invFun_as_coe, Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]

Goal state after:
S : Scheme
s : ↥S
⊢ ∃ i y,
    ((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).symm
          ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩)
        y =
      s
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ (fst ≫ f) ≫ g = F✝.map snd ≫ ?m.66

Tactic:
simpa using h.w

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
⊢ γ ≫ α = γ ≫ β

Tactic:
replace h : (yonedaGluedToSheaf hf).hom.app _ (γ ≫ α) =
        (yonedaGluedToSheaf hf).hom.app _ (γ ≫ β) := by dsimp at h; simp [h]

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
⊢ γ ≫ α = γ ≫ β
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: j : ℕ
hj : j + 1 = 0
⊢ False

Tactic:
apply Nat.not_succ_le_zero j

Goal state after:
j : ℕ
hj : j + 1 = 0
⊢ j.succ ≤ 0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 3) j)) * (-1) ^ (a + 1)) •
        (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) j)) =
      0

pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ i,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i)) * (-1) ^ (a + 1)) •
          (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i)) =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

Tactic:
· rintro ⟨k, hk⟩
    rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
    · intro h
      replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
      lia
    · dsimp [Fin.cast, Fin.pred]
      rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
      lia
    · simp only [Fin.lt_def]
      dsimp [Fin.natAdd, Fin.cast]
      lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ i,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i)) * (-1) ^ (a + 1)) •
          (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i)) =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 → ↑p ∣ k

pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1

Tactic:
· intro h
    contrapose! h
    apply le_of_eq
    rw [eq_comm]
    calc
      ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := eq_padicNorm _
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := ⟨u, ⋯⟩
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ i, ∀ j ≥ i, ‖↑(c - const norm c.lim) j‖ < ε
⊢ s ∈ Filter.map u atTop

Tactic:
simp only [mem_map, mem_atTop_sets]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := ⟨u, ⋯⟩
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ i, ∀ j ≥ i, ‖↑(c - const norm c.lim) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ u ⁻¹' s
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i)

Tactic:
by ext; simp [sup'_apply]

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 ((i : I) → ↑(π.obj (X i)))

Tactic:
apply CategoryTheory.Functor.ext ?_ ?_

Goal state after:
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : (i : I) → ↑(π.obj (X i))),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1

I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
set Fsq : p₁.Homotopy p₂ :=
    Path.Homotopic.prodHomotopy (.trans (.reflTrans _) (.symm <| .transRefl _))
      (.trans (.transRefl _) (.symm <| .reflTrans _))

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
by convert! hp 0 <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
⊢ weakEquivalences C p

Tactic:
by rwa [← weakEquivalence_iff]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y✝ : C
inst✝¹ : IsCofibrant X
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
⊢ weakEquivalences C i

Tactic:
by rwa [← weakEquivalence_iff]

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ ∂Δ[n].obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s

Tactic:
rw [boundary_eq_iSup]

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ (⨆ i, stdSimplex.face {i}ᶜ).obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]

Tactic:
rw [boundary_eq_iSup]

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ⨆ i, stdSimplex.face {i}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ #{i, j.castSucc, j.succ} ≤ n

Tactic:
obtain rfl | hn : n = 2 ∨ 2 < n := by
    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; lia

Goal state after:
case refine_2.inl
i : Fin (2 + 1)
j : Fin 2
h₀ : 0 < ↑i
hₙ : ↑i < 2
⊢ #{i, j.castSucc, j.succ} ≤ 2

case refine_2.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
hn : 2 < n
⊢ #{i, j.castSucc, j.succ} ≤ n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
hn : 2 < n
⊢ #{i, j.castSucc, j.succ} ≤ n

Tactic:
exact Finset.card_le_three.trans hn

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤ ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
by exact le_trans (by rfl) (le_iSup _ hx)

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

Goal state before:
pp: case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 1 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide

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 : (coyoneda.obj (op (𝟙_ C))).obj Z
f : (coyoneda.obj (op (𝟙_ C))).obj X
g : (coyoneda.obj (op (𝟙_ C))).obj Y
⊢ (ConcreteCategory.hom
          (((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom)).toFun
      ((f, g), h) =
    (ConcreteCategory.hom
          ((α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y)
                ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
            (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
              ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2))).toFun
      ((f, g), h)

Tactic:
dsimp at f g h

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
⊢ (ConcreteCategory.hom
          (((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom)).toFun
      ((f, g), h) =
    (ConcreteCategory.hom
          ((α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y)
                ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
            (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
              ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2))).toFun
      ((f, g), h)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
by
  rw [id_eq, ← Functor.map_id]
  exact congr_arg_heq (·.toFunctor.map η) (e_comp_id (V := Cat) a b)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ)

Tactic:
2

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base κ
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
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y') ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] Y) (Y ⟶[V] Y')).inv ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
leftUnitor_tensor_inv_assoc,

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
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        ((λ_ (X' ⟶[V] Y)).inv ▷ Y ⟶[V] Y') ≫
          (α_ (𝟙_ V) (X' ⟶[V] Y) (Y ⟶[V] Y')).hom ≫
            (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y') ≫
              (α_ (X ⟶[V] X') (X' ⟶[V] Y) (Y ⟶[V] Y')).inv ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
hx : faces f✝
⊢ (∃ (h : x✝ = y✝), f✝ = eqToHom h) ∨ x✝.len < y✝.len

Tactic:
cases hx; right; simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
by
  obtain h | rfl | h := lt_trichotomy i.castSucc i'
  · rw [Fin.castSucc_lt_iff_succ_le] at h
    obtain h | rfl := h.lt_or_eq
    · obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
      rw [Fin.succ_lt_succ_iff] at h
      obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
      exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_gt h]⟩
    · exact Or.inl δ_comp_σ_succ
  · exact Or.inl δ_comp_σ_self
  · obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
    rw [Fin.castSucc_lt_castSucc_iff] at h
    obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
    rw [← Fin.le_castSucc_iff] at h
    exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

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

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

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [switch_δ_σ₀]⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
Z✝ : SemiSimplexCategory
g₁ g₂ : Z✝ ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ toSimplexCategory.map g₁ = toSimplexCategory.map g₂

Tactic:
simp only [← cancel_mono (toSimplexCategory.map f), ← Functor.map_comp, h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 0

Tactic:
simpa [toMk₁_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 1

Tactic:
simpa [toMk₁_apply]

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
simp [mem_finset_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsProper
x : B.N
hx : x ∈ (P.ofIso e hA).II
⊢ (↑⟨x, hx⟩).IsUniquelyCodimOneFace (↑((P.ofIso e hA).p ⟨x, hx⟩)).toS

Tactic:
obtain ⟨x, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective x

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsProper
x : A.N
hx : (N.orderIsoOfIso e hA).symm x ∈ (P.ofIso e hA).II
⊢ (↑⟨(N.orderIsoOfIso e hA).symm x, hx⟩).IsUniquelyCodimOneFace
    (↑((P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm x, hx⟩)).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
⊢ StrictMono ⇑(orderHomOfSimplex (↑x) hm)

Tactic:
by
  simpa only [strictMono_orderHomOfSimplex_iff, ← nonDegenerate_iff_strictMono_objEquiv] using x.2

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

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ a = b

Tactic:
← h a,

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ⟨↑(z.1 a) + ↑(z.2 a), ⋯⟩ = b