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

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
n : ℕ
hn : (f * g i) ^ n • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t = 0
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0

Tactic:
mul_pow,

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
n : ℕ
hn : (f ^ n * g i ^ n) • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t = 0
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n • t) = 0
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
⊢ (∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂) →
    ∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂

Tactic:
rintro ⟨Y, f, y, hf, hf'⟩
    exact ⟨⟨Y, y⟩, ⟨f, hf⟩, hf'⟩

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

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✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
    (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂

Tactic:
h

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✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType (P.obj (op X))
h : (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
Module: Mathlib.CategoryTheory.Generator.Presheaf

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

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀ (G_1 : Cᵒᵖ ⥤ A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
X Y : Scheme
f : X ⟶ Y
E : PreZeroHypercover Y
⊢ ∀ [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
h

Goal state after:
case refine_2
S : Scheme
X Y : Scheme
f : X ⟶ Y
E : PreZeroHypercover Y
h : ∀ (i : E.I₀), HasPullback f (E.f i)
⊢ qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P Q : MorphismProperty Scheme
⊢ P ≤ Q → propQCPrecoverage P ≤ propQCPrecoverage Q

Tactic:
h

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ propQCPrecoverage P ≤ propQCPrecoverage Q
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
Z : C
g₁ g₂ : Z ⟶ Y
⊢ g₁ ≫ f = g₂ ≫ f → g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }

Tactic:
h

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
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }
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
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
⊢ g₁ ≫ π a₁ = g₂ ≫ π a₂ →
    g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
h

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
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
⊢ Presieve.IsSheafFor F (Presieve.singleton (𝒰.forgetQc.sigma.f default))

Tactic:
let f : Spec _ ⟶ Spec R := (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default

Goal state after:
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
⊢ Presieve.IsSheafFor F (Presieve.singleton (𝒰.forgetQc.sigma.f default))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))

Tactic:
refine ⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩

Goal state after:
case refine_1
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
⊢ (∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
      p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
          (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x) →
    ∃! y, (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x

Tactic:
h

Goal state after:
case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
⊢ ∃! y, (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x
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
⊢ Presheaf.IsSheaf J (presheaf data G₀)

Tactic:
rw [isSheaf_iff data]
  constructor
  · exact (Presheaf.isSheaf_of_iso_iff (compPresheafIso data G₀)).2 G₀.property
  · intro X
    refine ⟨(IsLimit.postcomposeHomEquiv
      (WalkingMulticospan.functorExt
          (fun _ ↦ presheafObjObjIso _ _ _) (fun _ ↦ presheafObjObjIso _ _ _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)
          (fun _ ↦ (compPresheafIso _ _).hom.naturality _)) _).1
      (IsLimit.ofIsoLimit (presheafObjIsLimit data G₀ X)
        (Multifork.ext (Iso.refl _) (fun i ↦ ?_)))⟩
    simp [Multifork.ι, PreOneHypercover.multifork, MulticospanIndex.multicospan]

Goal state after:
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
A₀ : C
⊢ ∀ (g : A₀ ⟶ cokernel t), g ≫ cokernel.map t b l r ⋯ = 0 → g = 0

Tactic:
z

Goal state after:
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
A₀ : C
z : A₀ ⟶ cokernel t
⊢ z ≫ cokernel.map t b l r ⋯ = 0 → z = 0
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 : IsPushout t l r b
A₀ : C
⊢ ∀ (y : A₀ ⟶ kernel b), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ kernel.map t b l r ⋯

Tactic:
z

Goal state after:
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 : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ z = x ≫ kernel.map t b l r ⋯
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yonedaEquiv.symm (J.yonedaEquiv (J.yoneda.map f.unop ≫ u)) =
    J.yoneda.map f.unop ≫ J.yonedaEquiv.symm (J.yonedaEquiv u)

Tactic:
Equiv.symm_apply_apply,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yoneda.map f.unop ≫ u = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm (J.yonedaEquiv u)
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv u)

Tactic:
Equiv.symm_apply_apply,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ (uliftYoneda.{v', v, u} J).map f.unop ≫ u =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv u)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg.isMin
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
i : J
hi : IsMin i
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
subst hi₀
      exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j' ≤ j
h' : m ≤ ⟨j, ⋯⟩
k : J
hk : k ∈ Set.Ici j
hkm : ⟨k, hk⟩ ≤ m
⊢ m ≤ ⟨k, hk⟩

Tactic:
exact h'.trans hk

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Arrow.mk f ∈ Φ.prop.toSet

Tactic:
h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
⊢ W₁ ≤ W₂ → transfiniteCompositions.{w, v, u} W₁ ≤ transfiniteCompositions.{w, v, u} W₂

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
⊢ transfiniteCompositions.{w, v, u} W₁ ≤ transfiniteCompositions.{w, v, u} W₂
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
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ Arrow.mk (𝟙 (F.obj ⟨k, hk⟩)) = Arrow.mk (𝟙 (G.obj ⟨k, hk⟩))

Tactic:
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
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ Arrow.mk (𝟙 (G.obj ⟨k, hk⟩)) = Arrow.mk (𝟙 (G.obj ⟨k, hk⟩))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case isMin
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
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
⊢ iter₁.F = iter₂.F

Tactic:
refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Goal state after:
case isMin
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
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case succ
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
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
⊢ iter₁.F = iter₂.F

Tactic:
refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Goal state after:
case succ
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
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
⊢ Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
      Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

Tactic:
by
  have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)
  dsimp at this ⊢
  rw [← cancel_epi (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right,
    ← reassoc_of% this, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ A', ∃ (h : A < A'), (generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)

Tactic:
induction A using Subobject.ind with | _ f
   =>  _ 

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ¬IsIso f

Tactic:
by simpa only [Subobject.isIso_iff_mk_eq_top] using hA

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
k : ℕ
hq : q ≠ 0
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q

Tactic:
induction k <;>
    simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ', add_mul, add_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r

Tactic:
by
  rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity ↑p ↑q.den + emultiplicity (↑p) (r.num * ↑q.den)

Tactic:
h

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ n.divisors

Tactic:
Nat.mem_divisors

Goal state after:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∈ n.divisors

Tactic:
Nat.mem_divisors

Goal state after:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y x✝ y✝ : ℤ_[p]
h : x✝ = y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y x✝ y✝ : ℤ_[p]
h : x✝ = y✝
⊢ ↑1 * y✝ = ↑1 * y✝
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 : PullbackCone f f
hc : IsLimit c
⊢ Mono f → c.fst = c.snd

Tactic:
intro hf
    simpa only [← cancel_mono f] using c.condition

Goal state after:
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 : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
⊢ g ≫ f = g' ≫ f → g = g'

Tactic:
h

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'