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

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

Tactic:
rw [← Sieve.generate_bot]

Goal state after:
P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ Sieve.generate ⊥ ∈ (propQCTopology P) X
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
⊢ ∀ (s : Cocone (Sieve.generateSingleton f).arrows.diagram) (m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ s.pt),
    (∀ (j : (Sieve.generateSingleton f).arrows.category),
        (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = s.ι.app j) →
      m = Hf.desc (s.ι.app { obj := Over.mk f, property := ⋯ }) ⋯

Tactic:
intro S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
⊢ ∀ (m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt),
    (∀ (j : (Sieve.generateSingleton f).arrows.category),
        (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
      m = Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯
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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)

Tactic:
have := J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hc))
    (J₀.pullback_stable c (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hd)))

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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)
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
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (s : Cocone (Sieve.generateFamily X π).arrows.diagram) (j : (Sieve.generateFamily X π).arrows.category),
    (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫
        H.desc (fun a ↦ s.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯ =
      s.ι.app j

Tactic:
intro S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (j : (Sieve.generateFamily X π).arrows.category),
    (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫
        H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯ =
      S.ι.app j
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
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (s : Cocone (Sieve.generateFamily X π).arrows.diagram) (m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ s.pt),
    (∀ (j : (Sieve.generateFamily X π).arrows.category),
        (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = s.ι.app j) →
      m = H.desc (fun a ↦ s.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯

Tactic:
intro S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt),
    (∀ (j : (Sieve.generateFamily X π).arrows.category),
        (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
      m = H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯
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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve a, ⋯⟩),
    (hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj.map I.f.op =
      (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫ G₀.obj.map I.f.op

Tactic:
rintro ⟨T₀, b, ⟨c, hc⟩⟩

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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ (hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj.map { Y := T₀, f := b, hf := ⋯ }.f.op =
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
      G₀.obj.map { Y := T₀, f := b, hf := ⋯ }.f.op
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
⊢ (Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S)

Tactic:
over_toGrothendieck_eq_toGrothendieck_comap_forget

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
⊢ (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)).toGrothendieck =
    (Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)

Tactic:
over_toGrothendieck_eq_toGrothendieck_comap_forget

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)).toGrothendieck =
    (Over.forget P ⊤ S).restrictedTopology (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫
      (presheafObjObjIso data G₀ ((data X).X i)).inv ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j

Tactic:
presheafObjObjIso,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫
      { hom := presheafObjObjIso.hom data G₀ ((data X).X i), inv := presheafObjObjIso.inv data G₀ ((data X).X i),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
        presheafObjπ data G₀ (F.obj ((data X).X i)) j
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
⊢ Mono (cokernel.map t b l r ⋯)

Tactic:
by
  rw [Preadditive.mono_iff_cancel_zero]
  intro A₀ z hz
  obtain ⟨A₁, π₁, _, x₂, hx₂⟩ :=
    surjective_up_to_refinements_of_epi (cokernel.π t) z
  have : (ShortComplex.mk _ _ (cokernel.condition b)).Exact :=
    ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel b)
  obtain ⟨A₂, π₂, _, x₃, hx₃⟩ := this.exact_up_to_refinements (x₂ ≫ r) (by
    simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w)
  obtain ⟨x₁, hx₁, rfl⟩ := sq.exists_lift (π₂ ≫ x₂) x₃ (by simpa)
  simp [← cancel_epi π₁, ← cancel_epi π₂, hx₂, ← reassoc_of% hx₁]

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

Goal state before:
pp: case he
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ ∀ ⦃X Y_1 : C⦄ (f : X ⟶ Y_1) (x : (CategoryTheory.yoneda.obj Y).obj (op Y_1)),
    Equiv.ulift.symm ((ConcreteCategory.hom ((CategoryTheory.yoneda.obj Y).map f.op)) x) =
      (ConcreteCategory.hom ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).map f.op)) (Equiv.ulift.symm x)

Tactic:
intros

Goal state after:
case he
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x✝ : (CategoryTheory.yoneda.obj Y).obj (op Y✝)
⊢ Equiv.ulift.symm ((ConcreteCategory.hom ((CategoryTheory.yoneda.obj Y).map f✝.op)) x✝) =
    (ConcreteCategory.hom ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).map f✝.op)) (Equiv.ulift.symm x✝)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
⊢ ∀ {X Y : ↑(Set.Iio j)} (f : X ⟶ Y),
    (restrictionLT (ofCocone c) ⋯).map f ≫
        (match Y with
          | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom =
      (match X with
          | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom ≫
        F.map f

Tactic:
intros

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
X✝ Y✝ : ↑(Set.Iio j)
f✝ : X✝ ⟶ Y✝
⊢ (restrictionLT (ofCocone c) ⋯).map f✝ ≫
      (match Y✝ with
        | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom =
    (match X✝ with
        | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom ≫
      F.map f✝
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
⊢ Small.{w, max u v} ↑(iSup W).toSet

Tactic:
toSet_iSup

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
⊢ Small.{w, max u v} ↑(⋃ i, (W i).toSet)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val

Tactic:
d.map_lift _ _ _ _ hi

Goal state after:
case e_x
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ ↑⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩
      (op ⟨i, hi⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
have hqd : (q.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
by
      have hqn : q.num ≠ 0 := Rat.num_ne_zero.2 hq
      have hqd : (q.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
      have hrn : r.num ≠ 0 := Rat.num_ne_zero.2 hr
      have hrd : (r.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
      have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
      have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
      conv_lhs => rw [← q.num_divInt_den]
      rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
        emultiplicity_le_emultiplicity_iff, mul_left_comm,
        emultiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]
      rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h
      calc
        _ ≤ min (emultiplicity ↑p (q.num * r.den * q.den))
                (emultiplicity ↑p (q.den * r.num * q.den)) :=
          le_min
            (by rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm])
            (by grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h])
        _ ≤ _ := min_le_emultiplicity_add

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

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
padicValNat_dvd_iff_le_of_ne_one hp ha,

Goal state after:
case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ n ≤ padicValNat p a ↔ a = 0 ∨ n ≤ padicValNat p a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
simpa [norm_intCast_eq_padic_norm]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  intro t ht
  simp only [Finset.mem_image, Finset.mem_range] at ht
  obtain ⟨k, hk, rfl⟩ := ht
  rw [Finset.mem_erase, Nat.mem_divisors]
  refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
  exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ),
    (if x * y = 0 then 0 else exp (-padicValRat p (x * y))) =
      (if x = 0 then 0 else exp (-padicValRat p x)) * if y = 0 then 0 else exp (-padicValRat p y)

Tactic:
intros

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
⊢ (if x✝ * y✝ = 0 then 0 else exp (-padicValRat p (x✝ * y✝))) =
    (if x✝ = 0 then 0 else exp (-padicValRat p x✝)) * if y✝ = 0 then 0 else exp (-padicValRat p y✝)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ),
    (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
      max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))

Tactic:
intros

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
⊢ (if x✝ + y✝ = 0 then 0 else exp (-padicValRat p (x✝ + y✝))) ≤
    max (if x✝ = 0 then 0 else exp (-padicValRat p x✝)) (if y✝ = 0 then 0 else exp (-padicValRat p y✝))
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ ↑↑⟨x, hx⟩ ≠ 0

Tactic:
PadicInt.coe_ne_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ ↑⟨x, hx⟩ ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
by simp [hf, norm]

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
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ = 𝟙 c.pt

Tactic:
← cancel_mono c.fst,

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst✝ : HasPullback f f
hc : IsLimit (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯)
⊢ Mono f

Tactic:
mono_iff_isIso_fst hc,

Goal state after:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyReflectIsomorphisms F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst✝¹ : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst✝ : HasPullback f f
hc : IsLimit (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯)
⊢ IsIso (PullbackCone.mk (pullback.fst f f) (pullback.snd f f) ⋯).fst
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)
l : Φ.fiber.obj X → (s.pt ⟶ M)
hl :
  ∀ (x : Φ.fiber.obj X) ⦃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 x
j : R.arrows.category
y : Φ.fiber.obj j.obj.left
⊢ Pi.lift l ≫ Pi.π (fun x ↦ M) ((ConcreteCategory.hom (Φ.fiber.map j.obj.hom)) y) = s.π.app (op j) ≫ Pi.π (fun t ↦ M) y

Tactic:
by simpa using! (hl _ j.obj.hom  j.property y rfl).symm

Goal state after: