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

Goal state before:
pp: case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j) =
    0

Tactic:
← homOfLE_comp hfgigi (hfgi i),

Goal state after:
case refine_1
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigi ≫ homOfLE ⋯).op)) (t i) -
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j) =
    0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (toSpec 𝒜 f)

Tactic:
have : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm
  have _ (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
    rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
  have : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding
  exact LocallyRingedSpace.IsOpenImmersion.to_iso _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ IsCompact (basicOpen 𝒜 ↑i).carrier

Tactic:
← Proj.opensRange_awayι _ _ (hxd _ i.2) (hd _ i.2).bot_lt

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ IsCompact (Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯)).carrier
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType =
    ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

Tactic:
IsSeparated.eq_valuativeCriterion,

Goal state after:
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType =
    ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
this : Cover.Over X V := { over := fun w ↦ { hom := (Z (i w)).hom }, isOver_map := ⋯ }
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows

Tactic:
have (w : W.left) : Etale (V.X w ↘ X) := (Z (i w)).prop

Goal state after:
case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
this✝ : Cover.Over X V := { over := fun w ↦ { hom := (Z (i w)).hom }, isOver_map := ⋯ }
this : ∀ (w : ↥W.left), Etale (V.X w ↘ X)
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (Opposite.op T)
F : Sheaf J D
⊢ IsConstant J F ↔ L.essImage F

Tactic:
essImage_eq_of_natIso (adj.leftAdjointUniq (constantSheafAdj J D hT))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : HasWeakSheafify J D
L : D ⥤ Sheaf J D
T : C
hT : IsTerminal T
adj : L ⊣ (sheafSections J D).obj (Opposite.op T)
F : Sheaf J D
⊢ IsConstant J F ↔ (constantSheaf J D).essImage F
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 : C
i : (data X).I₀
⊢ restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i

Tactic:
id_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 : C
i : (data X).I₀
⊢ restriction data G₀ ((data X).f i) = presheafObjπ data G₀ X i
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: 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)
h𝒰 : (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
obtain ⟨_, _⟩ := h𝒰

Goal state after:
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)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
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₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ presheafObjObjIso.hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i

Tactic:
id_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₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ presheafObjObjIso.hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) =
    presheafObjπ data G₀ (unop (op (F.obj X₀))) i
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (uliftYoneda.{v', v, u} J).map f ≫ J.uliftYonedaEquiv.symm x =
    J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

Tactic:
apply J.uliftYonedaEquiv.injective
  simp only [uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
  rw [uliftYonedaEquiv_uliftYoneda_map]
  rfl

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

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ ((Functor.const (Under j₀)).obj X).map f ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ (Under.forget j₀ ⋙ Y).map f

Tactic:
dsimp
    simp only [Category.id_comp, Category.assoc, ← Functor.map_comp, Under.w]

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

Goal state before:
pp: case pos
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 : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (objIso F X ⟨i, ⋯⟩).hom ≫ 𝟙 (F.obj ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv = 𝟙 (obj F X ⟨i, ⋯⟩)

Tactic:
id_comp,

Goal state after:
case pos
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 : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (objIso F X ⟨i, ⋯⟩).hom ≫ (objIso F X ⟨i, h₁⟩).inv = 𝟙 (obj F X ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 Φ.X₀ ≫ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    ((Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯)) ≫ (Φ.iterationFunctor J).map f

Tactic:
id_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    ((Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯)) ≫ (Φ.iterationFunctor J).map f
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Φ.prop ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯))
⊢ Φ.prop ((Φ.iterationFunctor J).map (homOfLE ⋯))

Tactic:
rw [prop_iff] at this ⊢

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Arrow.mk ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iter (Order.succ j)).F.obj ⟨j, ⋯⟩)
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iterationFunctor J).obj j)
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
⊢ W = ofHoms fun i ↦ (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
ext A B f

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ofHoms (fun i ↦ (↑((equivShrink ↑W.toSet).symm i)).hom) f
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)

Tactic:
by
  have := locallySmall I κ
  have := isSmall I κ
  have := hasColimitsOfShape_discrete I κ
  have := hasPushouts I κ
  intro _ _ _ ⟨F⟩ f
  constructor
  · nth_rw 1 [← I.ofHoms_homFamily]
    apply pushouts_mk _ (functorObj_isPushout I.homFamily (F.obj f).hom)
    exact coproducts_of_small _ _ (colimitsOfShape_colimMap _ (by rintro ⟨j⟩; constructor))
  · rw [MorphismProperty.isomorphisms.iff]
    dsimp [succStruct]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ 𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f) ≫
      Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
        (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f

Tactic:
id_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
      (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : C
⊢ generatingMonomorphisms G ≤ MorphismProperty.monomorphisms C

Tactic:
rintro _ _ _ ⟨X⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G X✝ Y : C
X : Subobject G
⊢ MorphismProperty.monomorphisms C X.arrow
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p

Tactic:
exact Nat.Prime.one_lt Fact.out

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (k + n - ((p.digits n).sum + (p.digits k).sum) + (p.digits (n + k)).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
sub_add_eq,

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case refine_2
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, ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)

Tactic:
refine ⟨x'.lim, fun n => ?_⟩
      have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _
      obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this
      by_cases! hin : i ≤ n
      · exact (hi i le_rfl n hin).le
      · specialize hi i le_rfl i le_rfl
        specialize hx hin.le
        have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
        rw [sub_add_sub_cancel] at this
        exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
have hn_coe : (n : ℤ) = -x.valuation := by
        rw [hn, Int.toNat_of_nonneg]
        rw [Right.nonneg_neg_iff]
        rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
        exact hx.le

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ ≫ c.fst = c.fst
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesColimit (span f f) (F i)
inst✝ : HasPushout f f
⊢ Epi f

Tactic:
have hc := pushoutIsPushout f f
  rw [epi_iff_isIso_inl hc, h.isIso_iff]
  intro i
  exact (epi_iff_isIso_inl ((isColimitMapCoconePushoutCoconeEquiv (F i) pushout.condition).1
    (isColimitOfPreserves (F i) hc))).1 (hf i)

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

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
i : ι
hi : (s i) default = X.hom x
x' : (pointSmallEtale (s i)).fiber.obj X
hx' : pointSmallEtaleFiberObjToPreimage (s i) hi x' = ⟨x, ⋯⟩
⊢ ∃ i y, (f i).left y = x

Tactic:
rw [Subtype.ext_iff] at hx'

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
i : ι
hi : (s i) default = X.hom x
x' : (pointSmallEtale (s i)).fiber.obj X
hx' : ↑(pointSmallEtaleFiberObjToPreimage (s i) hi x') = ↑⟨x, ⋯⟩
⊢ ∃ i y, (f i).left y = x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
rw [← not_iff_not]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬‖↑z‖ = 1 ↔ ¬IsCoprime z ↑p
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
by
  rw [← not_iff_not]
  simp [Nat.coprime_comm, ← norm_natCast_lt_one_iff, -norm_intCast_lt_one_iff,
    Int.isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, Int.gcd,
    ← hp.out.dvd_iff_not_coprime, norm_natAbs, -cast_natAbs, norm_int_le_one]

Goal state after: