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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (pullback.fst i₂ f) ⊤ ≫
        Scheme.Hom.app lft ⊤ ≫
          (Functor.mapIso (Spec (CommRingCat.of K)).presheaf (eqToIso ⋯).op ≪≫ Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)

Tactic:
← Scheme.Hom.comp_app_assoc lft (pullback.fst i₂ f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ : flip (fun x1 x2 ↦ x1 ⤳ x2) x (lft (closedPoint ↑(CommRingCat.of K)))
h₂ : (pullback.fst i₂ f) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (lft ≫ pullback.fst i₂ f) ⊤ ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
← HomogeneousLocalization.isUnit_iff_isUnit_val,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)).val ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case e'_2.e'_3
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ⇑(ConcreteCategory.hom (toSpec 𝒜 f).base) = ProjIsoSpecTopComponent.ToSpec.toFun f

Tactic:
exact funext fun _ => toSpec_base_apply_eq _ _

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)) :=
  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)) ≫
          fst ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)

Tactic:
erw [pullbackDiagonalMapIdIso_inv_snd_fst]

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 ≫ fst ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
let := (awayMap 𝒜 (f := x j) (hxdi i₀) rfl).toAlgebra

Goal state after:
case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
Module: Mathlib.CategoryTheory.Generator.Sheaf

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

Tactic:
intro F G f g hfg

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf J A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf J A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ ∀ (G_1 : Cᵒᵖ ⥤ A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => Presheaf.freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ (sheafToPresheaf J A).obj F), h ≫ (sheafToPresheaf J A).map f = h ≫ (sheafToPresheaf J A).map g

Tactic:
rintro _ ⟨X, i⟩ a

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf J A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (match (X, i) with
    | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
    (sheafToPresheaf J A).obj F
⊢ a ≫ (sheafToPresheaf J A).map f = a ≫ (sheafToPresheaf J A).map g
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
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ (Nonempty.some ⋯).q ≫ (data X).f (Nonempty.some ⋯).i₀ = p ≫ (data X).f i

Tactic:
hg.some.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
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ F.map g ≫ f = p ≫ (data X).f i
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ ⊥ ∈ (propQCTopology P) X

Tactic:
by
  rw [← Sieve.generate_bot]
  exact Precoverage.generate_mem_toGrothendieck (bot_mem_propQCPrecoverage X)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y₁ Y₂ : C
a : α
q : Y₁ ⟶ X a
e : Y₂ ⟶ Y₁
⊢ ∃ a_1 g, g ≫ π a_1 = e ≫ q ≫ π a

Tactic:
exact ⟨a, e ≫ q, by simp⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generateFamily X π).arrows.cocone)

Tactic:
apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₁.ι.app j ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)).hom ≫ colimMap S.f =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom

Tactic:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

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 : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.yonedaEquiv (J.yonedaEquiv.symm x ≫ f) =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x))

Tactic:
simp [yonedaEquiv_comp]

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

Goal state before:
pp: case isMin
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : IsMin j
⊢ W (hf.F.map (homOfLE ⋯))

Tactic:
obtain rfl := hj.eq_bot
    simpa using W.id_mem _

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

Goal state before:
pp: case neg
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:
simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

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

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

Tactic:
obtain h₂ | rfl := h₂₃.lt_or_eq

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₂ < 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

case neg.inr
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
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
by
  dsimp only [functor]
  rw [ofCocone_obj_eq _ _ hi]
  apply congr_obj

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

Goal state before:
pp: case isMin
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : IsMin i
⊢ Nonempty (Φ.Iteration i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi
      exact ⟨mkOfBot Φ J⟩

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
simp [hq]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
k : ℤ
⊢ padicValRat p (q ^ k) = k * padicValRat p q

Tactic:
induction k using Int.negInduction

Goal state after:
case nat
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n✝ : ℕ
⊢ padicValRat p (q ^ ↑n✝) = ↑n✝ * padicValRat p q

case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
a✝ : ∀ (n : ℕ), padicValRat p (q ^ ↑n) = ↑n * padicValRat p q
n✝ : ℕ
⊢ padicValRat p (q ^ (-↑n✝)) = -↑n✝ * padicValRat p q
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [hq]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hq]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ 1 < p

Tactic:
exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)

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

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

Tactic:
| succ d hd =>

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ! < n

Tactic:
apply lt_of_le_of_lt _ (sub_one_mul_padicValNat_factorial_lt_of_ne_zero p hn)
  conv_lhs => rw [← one_mul (padicValNat p n !)]
  gcongr
  exact le_sub_one_of_lt (Nat.Prime.one_lt hp.elim)

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Tactic:
· intro
    exact IsPushout.of_isColimit (PushoutCocone.isColimitMkIdId f)

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))

Tactic:
exact lt_of_le_of_ne hle h

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

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : yoneda.map a ≫ f i = yoneda.map b ≫ f j
⊢ (glueData hf).t i j ≫ (glueData hf).f j i ≫ (glueData hf).ι j = ⋯.snd (f j) ≫ toGlued hf j

Tactic:
by simp [toGlued]

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

Goal state before:
pp: case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) ≤ ?b

pp: case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ?b < ε

pp: case b
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ℚ

Tactic:
· apply padicNormE.add_le

Goal state after:
case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) + padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε