mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
j : R.arrows.categoryᵒᵖ
⊢ ⋯.choose ≫ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).π.app j = s.π.app j

Tactic:
by
      dsimp
      ext y
      simpa using! (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
y : Spec (CommRingCat.of Ω) ⟶ Y
hy : y ≫ f = s
⊢ ∃ R j, ∃ (_ : IsOpenImmersion j), ∃ y', y' ≫ j = y

Tactic:
obtain ⟨R, j, _, hj, _⟩ := exists_affine_mem_range_and_range_subset
          (x := y.base default) (U := ⊤) (by simp)
        refine ⟨R, j, inferInstance, _, IsOpenImmersion.lift_fac j y ?_⟩
        rintro _ ⟨a, rfl⟩
        rwa [Subsingleton.elim a default]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
⊢ (f + g).norm = max f.norm g.norm

Tactic:
by
  classical
  have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
  exact if hf : f ≈ 0 then by
    have : LimZero (f - 0) := hf
    have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
    have h1 : (f + g).norm = g.norm := norm_equiv this
    have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
    rw [h1, h2, max_eq_right (norm_nonneg _)]
  else
    if hg : g ≈ 0 then by
      have : LimZero (g - 0) := hg
      have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
      have h1 : (f + g).norm = f.norm := norm_equiv this
      have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
      rw [h1, h2, max_eq_left (norm_nonneg _)]
    else by
      unfold norm at hfgne ⊢; split_ifs at hfgne ⊢
      -- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
      rw [lift_index_left hf, lift_index_right hg] at hfgne
      · rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
        exact padicNorm.add_eq_max_of_ne hfgne

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind [hσ', hσ]` -/

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < (↑p)⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ‖(↑p)⁻¹‖

Tactic:
rw [norm_inv, norm_p, inv_inv]
        exact mod_cast hp.1.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑n‖ < 1 ↔ p ∣ n

Tactic:
simpa [Int.natCast_dvd_natCast] using norm_intCast_lt_one_iff (p := p) (k := n)

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

Goal state before:
pp: j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0

Tactic:
constructor
  · rintro ⟨_, h₂⟩
    by_contra h
    exact h₂ (Fin.succAbove_ne_zero_zero h)
  · rintro rfl
    exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩

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)
⊢ n + 1 ≤ ↑i + (n + 1)

Tactic:
simp only [le_add_iff_nonneg_left, zero_le]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : c.Rel i j
⊢ P.p.f i ≫ P.p.f i ≫ P.X.d i j = P.X.d i j ≫ P.p.f j

Tactic:
simp only [HomologicalComplex.Hom.comm, HomologicalComplex.Hom.comm_assoc,
                  HomologicalComplex.p_idem]

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 ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop

Tactic:
fac

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ θ.unop ≫ A.e = (A.e.op ≫ θ).unop
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ f ≫ QInfty.f (n + 1) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
QInfty_f,

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ f ≫ (Q (n + 1)).f (n + 1) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F G : U ⥤rq V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e
  simp

Goal state after:
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)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ PInfty.f n ≫
      P.p.app (op ⦋n⦌) ≫
        (PInfty.f (unop (Splitting.IndexSet.id (op ⦋n⦌)).fst).len ≫
            ((Γ₀.splitting K[P.X]).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))) ≫
          ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫ P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
simp [Splitting.IndexSet.e]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ : C
⊢ f X✝ * (f X✝)⁻¹ = 𝟙 ()

Tactic:
simp only [SingleObj.id_as_one, mul_inv_cancel]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ {X Y Z : C} (f_1 : X ⟶ Y) (g : Y ⟶ Z), f Z * (f X)⁻¹ = (f Y * (f X)⁻¹) ≫ (f Z * (f Y)⁻¹)

Tactic:
intros

Goal state after:
M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ * (f X✝)⁻¹ = (f Y✝ * (f X✝)⁻¹) ≫ (f Z✝ * (f Y✝)⁻¹)
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ ∀ {W X Y Z : Grpd} (f : ↑W ⥤ ↑X) (g : ↑X ⥤ ↑Y) (h : ↑Y ⥤ ↑Z), (f ⋙ g) ⋙ h = f ⋙ g ⋙ h

Tactic:
intros

Goal state after:
W✝ X✝ Y✝ Z✝ : Grpd
f✝ : ↑W✝ ⥤ ↑X✝
g✝ : ↑X✝ ⥤ ↑Y✝
h✝ : ↑Y✝ ⥤ ↑Z✝
⊢ (f✝ ⋙ g✝) ⋙ h✝ = f✝ ⋙ g✝ ⋙ h✝
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (j : J), (Functor.pi' fun j ↦ s.proj j) ≫ (piLimitFan F).proj j = s.proj j

Tactic:
intros

Goal state after:
J : Type u
F : J → Grpd
s✝ : Limits.Fan F
j✝ : J
⊢ (Functor.pi' fun j ↦ s✝.proj j) ≫ (piLimitFan F).proj j✝ = s✝.proj j✝
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ (prod (Quotient.mk a✝) (Quotient.mk b✝)).map { toFun := Prod.fst, continuous_toFun := ⋯ } = Quotient.mk a✝

Tactic:
prod_lift,

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ (Quotient.mk (a✝.prod b✝)).map { toFun := Prod.fst, continuous_toFun := ⋯ } = Quotient.mk a✝
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ (prod (Quotient.mk a✝) (Quotient.mk b✝)).map { toFun := Prod.snd, continuous_toFun := ⋯ } = Quotient.mk b✝

Tactic:
prod_lift,

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ (Quotient.mk (a✝.prod b✝)).map { toFun := Prod.snd, continuous_toFun := ⋯ } = Quotient.mk b✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: 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

Tactic:
intros

Goal state after:
I : Type u
X : I → TopCat
X✝ : (i : I) → ↑(π.obj (X i))
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: 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 ⋯

Tactic:
intros

Goal state after:
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ 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.Product

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

Tactic:
intros

Goal state after:
case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X

Tactic:
intros

Goal state after:
case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝ = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))),
    ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X

Tactic:
intros

Goal state after:
case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝ = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
⊢ ContractibleSpace (X × Y)

Tactic:
obtain ⟨hX⟩ := hequiv_unit' (X := X)
  obtain ⟨hY⟩ := hequiv_unit' (X := Y)
  refine ⟨⟨(hX.prodCongr hY).trans ?_⟩⟩
  exact (Homeomorph.prodUnique Unit Unit).toHomotopyEquiv

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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ ∀ (a : X),
    (∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
      ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
intros

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
a✝ : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
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
⊢ ∀ (t : ↑I), f (p' t) = H.uliftMap (((Path.refl { down := 0 }).prod p') t)

Tactic:
intros

Goal state after:
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
t✝ : ↑I
⊢ f (p' t✝) = H.uliftMap (((Path.refl { down := 0 }).prod p') t✝)
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
⊢ ∀ (t : ↑I), g (p' t) = H.uliftMap (((Path.refl { down := 1 }).prod p') t)

Tactic:
intros

Goal state after:
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
t✝ : ↑I
⊢ g (p' t✝) = H.uliftMap (((Path.refl { down := 1 }).prod p') t✝)
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
convert! hp 1

Goal state after:
case e'_2
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₁ = p₁ 1

case e'_3
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₃ = p₂ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSimplyConnected s ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

Tactic:
rw [IsSimplyConnected, simply_connected_iff_loops_nullhomotopic,
    ← isPathConnected_iff_pathConnectedSpace]
  refine .and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩
  · lift x to s using by simpa using hp 0
    rcases h x {
      toFun := fun t ↦ ⟨p t, hp t⟩
      source' := by simp
      target' := by simp
    } with ⟨F⟩
    exact ⟨F.map (.restrict s (.id _)), fun t ↦ (F t).2⟩
  · rcases h x (p.map continuous_subtype_val) (fun t ↦ (p t).2) with ⟨F, hF⟩
    exact ⟨{
      toFun t := ⟨F t, hF t⟩
      map_zero_left := by simp
      map_one_left := by simp
      prop' := by simp
    }⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (toHoCat.map { hom := HoCat.pResolutionObj X.obj })

Tactic:
rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence { hom := HoCat.pResolutionObj X.obj }.hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ n = 2 ∨ 2 < n

Tactic:
rw [eq_comm, or_comm, ← le_iff_lt_or_eq]

Goal state after:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 ≤ n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ Λ[n, i].toSSet _⦋1⦌

Tactic:
refine edge n i j.castSucc j.succ ?_ ?_
  · simp only [← Fin.val_fin_le, Fin.val_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]
  simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
  obtain rfl | hn : n = 2 ∨ 2 < n := by
    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; lia
  · revert i j; decide
  · exact Finset.card_le_three.trans hn

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

Goal state before:
pp: case zero
X : SSet
i : Fin (0 + 2)
f : (j : Fin (0 + 2)) → j ≠ i → (Δ[0] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
rintro ⟨⟨a, b⟩, hab⟩
      grind

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ∀ {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g

Tactic:
intros

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Center C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ tensorHom f✝ g✝ = whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case comp_homMk
V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x✝ y✝ : FreeRefl V
x y : V
f✝ : mk x ⟶ mk y
h : f✝ = homMk default
g : y ⟶ y
⊢ f✝ ≫ homMk g = homMk default

Tactic:
obtain rfl := Subsingleton.elim g (𝟙rq _)

Goal state after:
case comp_homMk
V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x✝ y✝ : FreeRefl V
x y : V
f✝ : mk x ⟶ mk y
h : f✝ = homMk default
⊢ f✝ ≫ homMk (𝟙rq y) = homMk default
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ Function.Surjective mk

Tactic:
rintro ⟨⟨x⟩⟩

Goal state after:
V : Truncated 2
x : Paths (OneTruncation₂ V)
⊢ ∃ a, mk a = { as := { as := x } }
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ r.degHom (f ≫ g) ≤ r.degHom g

Tactic:
have ⟨_, g₁, g₂, _, _, h_fac, h_deg⟩ := r.exists_fac g

Goal state after:
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
w✝ : C
g₁ : Y ⟶ w✝
g₂ : w✝ ⟶ Z
left✝¹ : W₁ g₁
left✝ : W₂ g₂
h_fac : g₁ ≫ g₂ = g
h_deg : r.degHom g = r.deg w✝
⊢ r.degHom (f ≫ g) ≤ r.degHom g
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (n + 1)
hf : P_δ f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
induction n generalizing x with

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))

Tactic:
dsimp [← Edge.id_tensor_id]

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

Goal state before:
pp: 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)
i : Fin (a + 1)
g' : { len := a } ⟶ { obj := { len := b }, property := hb }.obj
hf' : f.hom = SimplexCategory.σ i ≫ g'
⊢ W f

Tactic:
replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'

Goal state after:
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)
i : Fin (a + 1)
g' : { len := a } ⟶ { obj := { len := b }, property := hb }.obj
hf' : f = Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
⊢ ∃ a, toMk₁ a = f

Tactic:
let S : Finset (Fin (n + 1)) := { i | f i = 1}

Goal state after:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
⊢ ∃ a, toMk₁ a = f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : c ≤ x✝ ∧ x✝ ≤ a
⊢ ∀ ⦃b : α⦄, b ≤ x✝ → c ≤ b → b ≤ a

Tactic:
exact fun _ x _ ↦ x.trans b.2

Goal state after: