mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔ ⟦r⟧ = 0

Tactic:
by

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)
i✝ j✝ k✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯) ≫
      pullback₃.p₁ ⋯ (f j) (f k) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₁ ⋯ (f j) (f k)

Tactic:
by

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)
i✝ j✝ k✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯) ≫
      pullback₃.p₂ ⋯ (f j) (f k) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₂ ⋯ (f j) (f k)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
hf : F.relativelyRepresentable (F.map f)
g : Y ⟶ Z
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.fst' (F.map g) ≫ f) = F.map (hf.snd (F.map g) ≫ g)

Tactic:
by

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)
i✝ j✝ k✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯) ≫
      pullback₃.p₃ ⋯ (f j) (f k) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₃ ⋯ (f j) (f k)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝ : F.Faithful
c : C
a b : c ⟶ hf.pullback g
h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g
h₂ : a ≫ hf.snd g = b ≫ hf.snd g
⊢ F.map a ≫ ⋯.cone.snd = F.map b ≫ ⋯.cone.snd

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
⊢ ∃ N, ∀ i ≥ N, { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Padic.mk f - ↑(↑f i)) < ε

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b✝ : C
f' : F.obj b✝ ⟶ Y
hf' : F.relativelyRepresentable f'
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
c : C
a b : c ⟶ hf'.pullback g
h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g
h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g
⊢ F.map a ≫ hf'.fst g = F.map b ≫ hf'.fst g

Tactic:
by

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, (s i) default = X.hom x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝ : F.Full
⊢ F.map (hf.lift i h hi) ≫ hf.fst g = i

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.lift i h hi ≫ hf.snd g) = F.map h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf'.lift' i h hi ≫ hf'.fst' g) = F.map i

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.lift' i h hi ≫ hf'.snd g = h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.fst' f' = hf'.snd g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
by

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 ∈ ⇑X.hom ⁻¹' {X.hom x}

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.fst' g = 𝟙 (hf'.pullback g) ≫ hf'.fst' g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.snd g = 𝟙 (hf'.pullback g) ≫ hf'.snd g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ IsPullback (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f) (F.map g)

Tactic:
apply F.map_isPullback <| IsPullback.of_hasPullback f g

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : F.obj c ⟶ F.obj b
⊢ ∃ b_1 snd fst, IsPullback fst (F.map snd) (F.map f) g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
inst✝ : IsIso f
a : C
g : F.obj a ⟶ Y
⊢ (g ≫ CategoryTheory.inv f) ≫ f = F.map (𝟙 a) ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : F✝.relativelyRepresentable f
hg : F✝.relativelyRepresentable g
X : C
h : F✝.obj X ⟶ H
⊢ IsPullback (hf.fst (hg.fst h)) (F✝.map (hf.snd (hg.fst h) ≫ hg.snd h)) (f ≫ g) h

Tactic:
by

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)
i j k : ι
⊢ ∀ (i j : (glueData hf).J),
    (ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i)) =
      (ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ hg.fst (h ≫ f) ≫ g = (F.map (hg.snd (h ≫ f)) ≫ h) ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ ∃ b snd fst, IsPullback fst (F.map snd) g' h

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε

Tactic:
by

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
R : Sieve X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : R.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ R ∈ S.smallEtaleTopology X

Tactic:
by

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

Goal state before:
pp: S : Scheme
s : ↥S
⊢ ((SpecToEquivOfField (SeparableClosure ↑(S.residueField s)) S).symm
        ⟨s, CommRingCat.ofHom (algebraMap (↑(S.residueField s)) (SeparableClosure ↑(S.residueField s)))⟩)
      default =
    s

Tactic:
by

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

Goal state before:
pp: S : Scheme
⊢ ⋃ i,
      Set.range
        ⇑((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).invFun
            ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩) =
    Set.univ

Tactic:
by

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)
i : ι
⊢ yoneda.map (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom = f i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ F.map ((F.preimageIso (IsPullback.isoIsPullback X (F.obj a) h BC)).hom ≫ (Arrow.mk g_snd).hom) =
    F.map ((Arrow.mk snd).hom ≫ (Iso.refl (Arrow.mk snd).right).hom)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f

Tactic:
by

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)
i : ι
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op (X i)))) (toGlued hf i) = yonedaEquiv (f i)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
⊢ relative F P (F.map f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ (fst ≫ f) ≫ g = F✝.map snd ≫ ?m.66

Tactic:
by

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

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
⊢ a ≫ toGlued hf i = b ≫ toGlued hf j

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ padicNormE (⟦q'⟧ - ↑(↑q' N)) < ε

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
⊢ relative F✝ P (f ≫ g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : D
P : MorphismProperty C
inst✝³ : F.Faithful
inst✝² : F.Full
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : D
Y : C
g : F.obj Y ⟶ X
⊢ IsPullback g (F.map (𝟙 Y)) (𝟙 X) g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
this : ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b
Z✝ : Cᵒᵖ ⥤ Type v₁
x✝³ x✝² : Z✝ ⟶ F
h : x✝³ ≫ f = x✝² ≫ f
x✝¹ : C
x✝ : yoneda.obj x✝¹ ⟶ Z✝
⊢ (x✝ ≫ x✝³) ≫ f = (x✝ ≫ x✝²) ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ a ≫ f = yoneda.map (𝟙 X) ≫ a ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
⊢ b ≫ f = yoneda.map (𝟙 X) ≫ a ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
h : a ≫ f = b ≫ f
this : ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ monomorphisms (Cᵒᵖ ⥤ Type v₁) f

Tactic:
by

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)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
⊢ 0 < 3

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : MorphismProperty C
G : Cᵒᵖ ⥤ Type v₁
hP : P ≤ monomorphisms C
X : C
f : yoneda.obj X ⟶ G
hf : P.presheaf f
⊢ ⋯.fst' f = ⋯.snd f

Tactic:
by

Goal state after: