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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => Exists.choose hT ≫ e,
          naturality := ⋯ } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ Exists.choose ⋯ ≫ e = e

Tactic:
← Category.id_comp e

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => Exists.choose hT ≫ e,
          naturality := ⋯ } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ Exists.choose ⋯ ≫ e = 𝟙 Y ≫ e
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Sieve.pullback (V.affineOneHypercover.f i)
        (Sieve.generate
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).X
            (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f))).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
            ← Presieve.isSheafFor_iff_generate]

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows
      (fun i_1 ↦ pullback ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f i_1) (V.affineOneHypercover.f i)) fun x ↦
      pullback.snd ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f x) (V.affineOneHypercover.f i))
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
I : Type u_2
x✝ : Category.{u_1, u_2} I
this : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))
⊢ PreservesLimitsOfShape I J.yoneda

Tactic:
exact preservesLimitsOfShape_of_reflects_of_preserves _ (sheafToPresheaf J _)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))

Tactic:
refine Cofan.IsColimit.mk _ (fun s ↦ ⟨?_⟩) (fun s j ↦ ?_) fun s m hm ↦ ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt.obj ⟶ s.pt.obj

case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ { hom := ?refine_1 } = s.inj j

case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m = { hom := ?refine_1 }
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x✝² x✝¹ : ↑(Iic j)
x✝ : (fun j_1 ↦ ↑j_1) x✝² = (fun j_1 ↦ ↑j_1) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ {a b : ↑(Iic j)}, { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } a < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } b ↔ a < b

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x✝² x✝¹ : ↑(Iio j)
x✝ : (fun j_1 ↦ ↑j_1) x✝² = (fun j_1 ↦ ↑j_1) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ {a b : ↑(Iio j)}, { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } a < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } b ↔ a < b

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ (b : α), b ∈ range ⇑{ toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ } ↔ b < j

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
x✝² x✝¹ : ↑(Iic i)
x✝ : (fun k ↦ ⟨↑k, ⋯⟩) x✝² = (fun k ↦ ⟨↑k, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : ↑(Iic i)}, { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } a < { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } b ↔ a < b

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
x✝² x✝¹ : ↑(Iio i)
x✝ : (fun k ↦ ⟨↑k, ⋯⟩) x✝² = (fun k ↦ ⟨↑k, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : ↑(Iio i)}, { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } a < { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } b ↔ a < b

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ (b : ↑(Iic j)), b ∈ range ⇑{ toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ } ↔ b < ⟨i, h⟩

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ Φ.succ X = Y

Tactic:
cases hf
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (colimit.ι (restrictionLT iter.F hij) ⟨k, hk⟩ ≫ eqToHom ⋯) = Arrow.mk (iter.F.map (homOfLE ⋯))

Tactic:
← arrowMap

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (colimit.ι (restrictionLT iter.F hij) ⟨k, hk⟩ ≫ eqToHom ⋯) =
    arrowMap iter.F ↑((Set.principalSegIioIicOfLE hij).toRelEmbedding ⟨k, hk⟩) ↑(Set.principalSegIioIicOfLE hij).top ⋯
      hij
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter₁ iter₂ : Φ.Iteration j
this : iter₁.F = iter₂.F
⊢ iter₁ = iter₂

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ i = ⊥

Tactic:
by simpa using hij

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯) ≫ F.map α ≫ sq'.f' = f

Tactic:
← F.map_comp_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯ ≫ α) ≫ sq'.f' = f
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
| F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯) ≫ ⋯.lift

Tactic:
← F.map_comp_assoc

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
| F.map (homOfLE ⋯ ≫ homOfLE ⋯) ≫ ⋯.lift
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
l : J
hl : l ∈ Set.Iio i
⊢ (e ↑(op ⟨l, hl⟩).1 ⋯).val = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩)

Tactic:
rw [d.map_lift _ _ _ _ hl]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ (ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) a = f

Tactic:
simpa using ha =≫ pushout.desc p f pullback.condition

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp ≤ (monomorphisms C).rlp

pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp

Tactic:
· intro X Y p hp A B i (_ : Mono i)
    obtain ⟨J, _, _, _, _, ⟨h⟩⟩ :=
      generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i
    exact transfiniteCompositionsOfShape_le_llp_rlp _ _ _ h.mem _ (by simpa)

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ -padicValRat p ↑z ≤ -↑n

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
neg_le_neg_iff,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ padicValRat p ↑z

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
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.PadicVal.Basic

Goal state before:
pp: case inr
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p k = padicValNat p (k * b) - padicValNat p b

Tactic:
padicValNat.mul hk hb,

Goal state after:
case inr
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p k = padicValNat p k + padicValNat p b - padicValNat p b
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε

Tactic:
← inv_lt_inv₀ hε (zpow_pos _ _)

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ -↑x.valuation ≤ -↑n ↔ n ≤ x.valuation

pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 1 < ↑p

Tactic:
neg_le_neg_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ ↑x.valuation ↔ n ≤ x.valuation

p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 1 < ↑p
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (ConcreteCategory.hom (f.hom.app (op T))) ((equiv₀ F hT) x) = (equiv₀ G hT) ((map f 0) x)

Tactic:
simp only [equiv₀, AddEquiv.trans_apply, addEquiv₀_map f x]
  rfl

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ max v1 (max v2 (stationaryPoint hf))

Tactic:
apply le_trans
    · apply le_max_right v2
    · apply le_max_right

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ IsIso c.inl → c.inl = c.inr

Tactic:
· intro
    obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
    have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by
      rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩
    rw [← cancel_mono φ, hφ₁, hφ₂]

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 : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩

Tactic:
rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ (Q q).f n = (Q q).f n ≫ f.app (op ⦋n⦌)

Tactic:
by
  simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality,
    sub_comp, sub_left_inj]
  dsimp
  simp only [comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ Δ ≠ Δ''

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
· by_contra h
    simp only [left_eq_add, h, add_eq_zero, and_false, reduceCtorEq] at eq

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ (homotopyPToId X (q + 1)).hom n (n + 1) = (homotopyPToId X q).hom n (n + 1)

Tactic:
simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Homotopy.trans_hom,
    Homotopy.ofEq_hom, Pi.zero_apply, Homotopy.add_hom, Homotopy.compLeft_hom, add_zero,
    Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel, hσ'_eq_zero hqn (c_mk (n + 1) n rfl),
    dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PartialOrder β
f g : C(α, β)
x✝ : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by aesop

Goal state after: