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

Goal state before:
pp: case 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
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := ⋯
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
m : ℕ
hm :
  (f * (g i * g j)) ^ m •
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
⊢ (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t i)) =
    (fun x ↦ (g i * g j) ^ m • x) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ m • t j))

Tactic:
simpa [M.map_smul_Spec _ (f ^ m), ← mul_smul, ← mul_smul, ← mul_pow, ← mul_comm f,
            smul_sub, sub_eq_zero] using hm

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Function.Bijective ⇑(g.rangeRestrict.comp f)

Tactic:
refine ⟨?_, ?_⟩
  · exact .of_comp (f := Subtype.val) (by convert! (IsFractionRing.injective R K); rw [← h]; rfl)
  · let V : ValuationSubring K :=
      ⟨(algebraMap R K).range, ValuationRing.isInteger_or_isInteger R⟩
    suffices LocalSubring.range g ≤ V.toLocalSubring by
      rintro ⟨_, x, rfl⟩
      obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
      exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩
    apply V.isMax_toLocalSubring
    have H : (algebraMap R K).range ≤ g.range := fun x ⟨a, ha⟩ ↦ ⟨f a, by simp [← ha, ← h]⟩
    refine ⟨H, ⟨?_⟩⟩
    rintro ⟨_, a, rfl⟩ (ha : IsUnit (M := g.range) ⟨algebraMap R K a, _⟩)
    suffices IsUnit a from this.map (algebraMap R K).rangeRestrict
    apply IsUnit.of_map f
    apply (IsLocalHom.of_surjective g.rangeRestrict g.rangeRestrict_surjective).1
    convert! ha
    simp [← h]

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

Goal state before:
pp: case h₁
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) := ⋯
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅
  Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) := ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) := ⋯
this : Function.Surjective ⇑F
⊢ ((e₂.inv ≫
          ((pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f (i, j).1)
                  ((affineOpenCover 𝒜).openCover.f (i, j).2) (toSpecZero 𝒜)).inv ≫
              snd (diagonal (toSpecZero 𝒜))
                ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover
                      (toSpecZero 𝒜) (toSpecZero 𝒜)).f
                  (i, j))) ≫
            e₁.hom) ≫
        (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv) ≫
      snd (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))) =
    (Spec.map (CommRingCat.ofHom F) ≫ (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)).inv) ≫
      snd (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd))))

Tactic:
simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id,
      limit.lift_π, PullbackCone.mk_π_app, pullbackSpecIso_inv_snd,
      ← Spec.map_comp, e₂, e₁]

Goal state after:
case h₁
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ (pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯).inv ≫
      (pullbackDiagonalMapIdIso ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j)
            (toSpecZero 𝒜)).inv ≫
        snd (diagonal (toSpecZero 𝒜))
            ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
                  (toSpecZero 𝒜)).f
              (i, j)) ≫
          snd ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) =
    Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight ≫ CommRingCat.ofHom F)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
⊢ ∃ n, f ^ n • t = 0

Tactic:
obtain ⟨n, hn⟩ := h.uniqueness (a f) le_top (iso.inv t) <| by
      simpa [M', iso, ← M.presheaf.map_comp_apply, homOfLE_op_comp_eqToHom, e] using
        congr((e _ hf).inv $ht)

Goal state after:
case refine_2
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
⊢ ∃ n, f ^ n • t = 0
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
X✝ : C
data✝ : F.OneHypercoverDenseData J₀ J X✝
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ F.map p ≫ h.q ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f

Tactic:
h.fac,

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
X✝ : C
data✝ : F.OneHypercoverDenseData J₀ J X✝
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ F.map p ≫ F.map g ≫ f = F.map (p ≫ g) ≫ f
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
hR : R ∈ etaleTopology S
f : Spec (CommRingCat.of Ω) ⟶ S
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1),
      ∃ y, (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map f_1)) y = f

Tactic:
by
    obtain ⟨⟨x, a⟩, rfl⟩ := (Scheme.SpecToEquivOfField Ω S).symm.surjective f
    rw [mem_grothendieckTopology_iff] at hR
    obtain ⟨𝒰, hle⟩ := hR
    obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
    refine ⟨𝒰.X i, 𝒰.f i, hle _ _ ⟨i⟩, ?_⟩
    let k := (𝒰.X i).residueField y
    let m : S.residueField (𝒰.f i y) ⟶ (𝒰.X i).residueField y :=
      (𝒰.f i).residueFieldMap y
    algebraize [((𝒰.f i).residueFieldMap y).hom, a.hom]
    let b : (𝒰.X i).residueField y →ₐ[S.residueField (𝒰.f i y)] Ω :=
      IsSepClosed.lift
    have hfac : (𝒰.f i).residueFieldMap y ≫ CommRingCat.ofHom b.toRingHom = a := by
      ext1; exact b.comp_algebraMap
    use Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y
    simp [SpecToEquivOfField, ← hfac]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
⊢ (ObjectProperty.ofObj fun x ↦
      match x with
      | (X, i) => freeYoneda X (S i)).IsSeparating

Tactic:
intro F G f g h
  ext ⟨X⟩
  refine hS _ _ ?_
  rintro _ ⟨i⟩ α
  apply freeYonedaHomEquiv.symm.injective
  simpa only [freeYonedaHomEquiv_symm_comp] using
    h _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α)

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

Goal state before:
pp: P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

Tactic:
refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩

Goal state after:
P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Presieve.singleton f ∈ (precoverage P).coverings Y
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor F R

Tactic:
rw [← isSheafFor_comp_uliftFunctor_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (F ⋙ uliftFunctor.{?u.29, w}) R
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
inst✝¹ : IsFiltered J
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 : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A✝, ι := { app := fun j ↦ Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
j : J
⊢ c.ι.app j ≫ hc.desc c' ≫ g = c.ι.app j ≫ f

Tactic:
by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]

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
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Tactic:
rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone transfiniteCompositions.{w, v, u}

Tactic:
intro W₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ : MorphismProperty C
⊢ ∀ ⦃b : MorphismProperty C⦄, W₁ ≤ b → transfiniteCompositions.{w, v, u} W₁ ≤ transfiniteCompositions.{w, v, u} b
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 ⟨Order.succ j, ⋯⟩ = obj F X ⟨i₂, hi₂⟩

Tactic:
by
          congr
          exact le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂

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

Goal state before:
pp: case neg.inl
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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ < Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h

Tactic:
rw [Order.lt_succ_iff_of_not_isMax hj] at h₂

Goal state after:
case neg.inl
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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
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
i : J
hi : Order.IsSuccLimit i
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ Arrow.mk ((⋯.functor ⋙ Φ.iterationFunctor J).map f ≫ (eqToIso ⋯).hom) =
    Arrow.mk ((eqToIso ⋯).hom ≫ (restrictionLT (Φ.iter i).F ⋯).map f)

Tactic:
simpa using! Φ.arrowMk_iterationFunctor_map k₁ k₂ (leOfHom f) (Φ.iter i) h₂.le

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
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ (generatingMonomorphisms G).pushouts ((⋯.functor ⋙ functor hG A₀ J).map (homOfLE ⋯))

Tactic:
dsimp [MonoOver.forget]

Goal state after:
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
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ (generatingMonomorphisms G).pushouts
    ((transfiniteIterate (largerSubobject hG) (↑k) A₀).ofLE
      (transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀) ⋯)
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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ ((transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).isoOfEq (Subobject.mk f) ⋯ ≪≫
          Subobject.underlyingIso f).hom ≫
      (Arrow.mk f).hom =
    (Arrow.mk ((functor hG (Subobject.mk f) J).map (homOfLE ⋯))).hom ≫ (asIso t.arrow).hom

Tactic:
dsimp [MonoOver.forget]

Goal state after:
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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ ((transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
        (Subobject.underlyingIso f).hom) ≫
      f =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
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 : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this : Nonempty o.ToType
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
have : OrderBot o.ToType := WellFoundedLT.toOrderBot _

Goal state after:
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 : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this✝ : Nonempty o.ToType
this : OrderBot o.ToType
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)
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
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
⊢ (monomorphisms C).rlp p

Tactic:
A

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
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A : C
⊢ ∀ ⦃Y_1 : C⦄ (g : A ⟶ Y_1), monomorphisms C g → HasLiftingProperty g p
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ i < n, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range n, F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range n, F i)

Tactic:
induction n with

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
⊢ ↑(if hf : ⟨fun n ↦ ↑(seq n), h⟩ ≈ 0 then 0 else padicNorm p (↑⟨fun n ↦ ↑(seq n), h⟩ (PadicSeq.stationaryPoint hf))) ≤
    1

Tactic:
split_ifs with hne

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑0 ≤ 1

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ¬⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑(padicNorm p (↑⟨fun n ↦ ↑(seq n), h⟩ (PadicSeq.stationaryPoint hne))) ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

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

Tactic:
by
  obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹
  use k
  rw [← inv_lt_inv₀ hε (zpow_pos _ _)]
  · rw [zpow_neg, inv_inv, zpow_natCast]
    apply lt_of_lt_of_le hk
    norm_cast
    apply le_of_lt
    convert! Nat.lt_pow_self _ using 1
    exact hp.1.one_lt
  · exact mod_cast hp.1.pos

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ min ↑x.valuation ↑y.valuation ≤ ↑(x + y).valuation

Tactic:
simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy

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

Goal state before:
pp: p n m : ℕ
hp : Fact (Nat.Prime p)
h : n < p
⊢ padicValNat p (p * m + n)! = padicValNat p (p * m)!

Tactic:
induction n with

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

Goal state before:
pp: p n k b : ℕ
hp : Fact (Nat.Prime p)
hkn : k ≤ n
hnb : log p n < b
⊢ padicValNat p (n.choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| (choose_ne_zero hkn)) ▸
    Prime.emultiplicity_choose hp.out hkn hnb

Goal state after:
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)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Ext.addEquiv₀ ((map f 0) x) = Ext.addEquiv₀ x ≫ f

Tactic:
by
  delta Ext.addEquiv₀
  apply (Ext.mk₀_bijective _ G).injective
  simp only [AddEquiv.coe_mk, Ext.mk₀_homEquiv₀_apply, Ext.mk₀_homEquiv₀_apply, ← Ext.mk₀_comp_mk₀]
  rfl

Goal state after:
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
⊢ Mono f ↔ IsIso c.fst

Tactic:
rw [mono_iff_fst_eq_snd hc]
  constructor
  · intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
    · simp only [assoc, hφ₁, id_comp, comp_id]
    · simp only [assoc, hφ₂, id_comp, comp_id, h]
  · intro
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    have : IsSplitEpi φ := IsSplitEpi.mk ⟨SplitEpi.mk c.fst (by
      rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id])⟩
    rw [← cancel_epi φ, hφ₁, hφ₂]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
hpg : padicNorm p (↑g (stationaryPoint hg)) = padicNorm p (↑g i)
⊢ padicNorm p (↑f i) = padicNorm p (↑g (stationaryPoint ⋯))

Tactic:
hpg,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
hpg : padicNorm p (↑g (stationaryPoint hg)) = padicNorm p (↑g i)
⊢ padicNorm p (↑f i) = padicNorm p (↑g i)