mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1.refine_2
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
this :
  ∃! s, ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) s = f ^ K • t i
⊢ ∃ t, (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = f ^ (N + K) • s

Tactic:
obtain ⟨a, ha, -⟩ := this
      use a
      refine TopCat.Sheaf.eq_of_locally_eq' ⟨_, M.isSheaf⟩ (fun i ↦ basicOpen (f * g i)) _
          (fun i ↦ homOfLE (basicOpen_mul_le_left f (g i))) ?_ _ _ ?_
      · rw [left_eq_inf.mpr hf, hg, inf_iSup_eq]
        simp_rw [basicOpen_mul]
        exact le_rfl
      · intro i
        rw [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp,
          ← homOfLE_comp (basicOpen_mul_le_right _ _) (hgle i), op_comp, M.presheaf.map_comp_apply,
          M.map_smul_Spec, ha, M.map_smul_Spec, pow_add, mul_smul, smul_comm, ht i]

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

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
intro x

Goal state after:
case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this : n i ≤ ⨆ i, n i
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

Tactic:
have : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by lia

Goal state after:
case h.h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) ((f ^ ⨆ i, n i) • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))),
    ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y

Tactic:
intro x

Goal state after:
case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))
⊢ ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0

Tactic:
intro x

Goal state after:
case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
⊢ (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0
Module: Mathlib.CategoryTheory.Sites.Point.Basic

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
B : Type u''
inst✝⁴ : Category.{v'', u''} B
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory A FC
⊢ ∀ {J_1 : Type w} [inst : Category.{w, w} J_1], PreservesColimitsOfShape J_1 Φ.presheafFiber

Tactic:
by
    dsimp [presheafFiber]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
R : CommRingCat
⊢ (tilde.functor R).essImage ≤ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf

Tactic:
intro M ⟨N, ⟨e⟩⟩
    exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso e
      (by dsimp; infer_instance)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property E.shrink

Tactic:
PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ heq

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E F : PreZeroHypercover X
h : P.property F.shrink
heq : E.presieve₀ = F.presieve₀
⊢ P.property F.shrink
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) ≫ IsDenseSubsite.mapPreimage J F G₀ d =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map (c ≫ a).op

Tactic:
← IsDenseSubsite.mapPreimage_comp,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ IsDenseSubsite.mapPreimage J F G₀ (d ≫ (data (F.obj X₀)).f i) =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map (c ≫ a).op
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
j : J
t : ↑(Set.range s) := ⟨s j, ⋯⟩
⊢ Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom

Tactic:
trans Subobject.mk (F.obj (σ t)).obj.hom

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := ⋯
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
j : J
t : ↑(Set.range s) := ⋯
⊢ Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (σ t)).obj.hom

C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := ⋯
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
j : J
t : ↑(Set.range s) := ⋯
⊢ Subobject.mk (F.obj (σ t)).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

Tactic:
· let s := f.toPrincipalSeg hf
    obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩
    induction i using SuccOrder.limitRecOn with
    | isMin i hi =>
      subst hi₀
      exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
    | succ i hi _ =>
      obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
      have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
      infer_instance
    | isSuccLimit i hi =>
      subst hi₀
      exact hasColimitsOfShape_of_isSuccLimit' C s hi

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : ¬i₁ ≤ j
⊢ obj F X ⟨i₁, ⋯⟩ = obj F X ⟨i₂, hi₂⟩

Tactic:
congr
        rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))]

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 j (Order.succ j) h₀ h₂

Tactic:
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 ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    val₀

Tactic:
rw [d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)]
    simpa using (e ⊥ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)).map_zero

Goal state after:
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩)

Tactic:
rw [map_lift _ _ _ _ _ (hl.trans hij')]

Goal state after:
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val = ↑⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩ (op ⟨l, ⋯⟩)
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X Y : D
f g : X ⟶ Y
⊢ (adj.homEquiv (G.obj X) Y).symm (G.map (f + g)) = (adj.homEquiv (G.obj X) Y).symm (G.map f + G.map g)

Tactic:
by simp [homEquiv_counit]

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 : C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this✝ : Nonempty κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ Order.succ (Cardinal.lift.{w, max u v} (Cardinal.mk (Subobject X))) ≤
    Cardinal.lift.{max u v, w} (Cardinal.mk κ.ord.ToType)

Tactic:
by simp [κ]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpenEmbedding Subtype.val

Tactic:
refine (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1}).isOpenEmbedding_subtypeVal

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpen {y | ‖y‖ ≤ 1}
Module: Mathlib.NumberTheory.Padics.PadicIntegers

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

Tactic:
Padic.norm_intCast_lt_one_iff

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ↑p ∣ z ↔ ↑p ∣ z
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:

Tactic:
_ = _ := hr.symm
      _ < 1 * 1 := mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one
      _ = 1 := mul_one 1

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Function.Surjective ⇑(padicValuation p)

Tactic:
intro x

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : WithZero (Multiplicative ℤ)
⊢ ∃ a, (padicValuation p) a = x
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}

Tactic:
intro x

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → x ∈ Ideal.span {↑p}
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ IsCauSeq norm x

Tactic:
intro ε hε

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, ‖x j - x i‖ < ε
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x n - x m‖ ≤ ↑p ^ (-↑m)

Tactic:
← neg_sub,

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖-(x m - x n)‖ ≤ ↑p ^ (-↑m)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
hi : ‖↑x' i - ↑(const norm x'.lim) i‖ < ↑p ^ (-↑n)
hin : n < i
this : ‖x n - x i + (x i - x'.lim)‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

Tactic:
rw [sub_add_sub_cancel] at this

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
hi : ‖↑x' i - ↑(const norm x'.lim) i‖ < ↑p ^ (-↑n)
hin : n < i
this : ‖x n - x'.lim‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
⊢ f ≈ 0

Tactic:
intro ε hε

Goal state after:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ LimZero f

Tactic:
intro ε hε

Goal state after:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑f j) < ε
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 : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Tactic:
intro Z g g' h

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'
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
hf : c.inl = c.inr
⊢ ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Tactic:
intro Z g g' h

Goal state after:
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
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'
Module: Mathlib.CategoryTheory.Types.Epimorphisms

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
⊢ Function.Surjective ⇑(ConcreteCategory.hom l)

Tactic:
intro x

Goal state after:
x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
x : x✝³
⊢ ∃ a, (ConcreteCategory.hom l) a = x
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)
⊢ ∀ (x : Φ.fiber.obj X),
    ∃ l,
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
        (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l

Tactic:
intro x

Goal state after:
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)
x : Φ.fiber.obj X
⊢ ∃ l,
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
      (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l