mathlib-initiative/mathlib-tactics huggingface dataset:
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
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → IsIso c.inl

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

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → IsIso c.inl
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt

pp: case mp.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt

Tactic:
·

Goal state after:
case mp.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt

Tactic:
·

Goal state after:
case mp.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inr ≫ φ ≫ c.inl = c.inr ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.EpiMono

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

Tactic:
·

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
⊢ IsIso c.inl → c.inl = c.inr
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:
·

Goal state after:
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)
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
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Tactic:
·

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.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J 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
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = 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:
refine ⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
    fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩

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
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
⊢ s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫ Pi.π (fun t ↦ M) y₂ =
    s.π.app (op (R.arrows.categoryMk f₁ hf₁)) ≫ Pi.π (fun t ↦ M) y₁
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = 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
inst✝¹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝ : HasWeakSheafify J A
⊢ ∀ {X Y : Cᵒᵖ ⥤ A} (f : X ⟶ Y),
    Φ.presheafFiber.map f ≫ (asIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J Y))).hom =
      (asIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J X))).hom ≫ (presheafToSheaf J A ⋙ Φ.sheafFiber).map f

Tactic:
by simp [sheafFiber, ← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ≤ Sieve.ofArrows U f

pp: case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ∈ J X

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ≤ Sieve.ofArrows U f
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ∈ J X

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ∈ J X
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f

pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
hF₂ : ∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f

Tactic:
·

Goal state after:
case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
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 : ℕ := ⋯
⊢ stationaryPoint ?hf ≤ i

pp: case a
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 : ℕ := ⋯
⊢ stationaryPoint ?hf ≤ stationaryPoint hf

pp: case hf
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 : ℕ := ⋯
⊢ ¬f ≈ 0

Tactic:
·

Goal state after:
case a
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 : ℕ := ⋯
⊢ stationaryPoint ?hf ≤ i
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
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 : ℕ := ⋯
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
·

Goal state after:
case a
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 : ℕ := ⋯
⊢ stationaryPoint hf ≤ stationaryPoint hf
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ i

pp: case a
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ stationaryPoint hg

pp: case hf
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ ¬g ≈ 0

Tactic:
·

Goal state after:
case a
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ i
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg

Tactic:
·

Goal state after:
case a
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 : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: case refine_1
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x) ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩

pp: case refine_2
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x) default = x

Tactic:
·

Goal state after:
case refine_1
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x) ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩