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

Goal state before:
pp: case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
⊢ ∃ c, ↑c * HomogeneousLocalization.mk y = ↑c * HomogeneousLocalization.mk z

Tactic:
obtain ⟨i, c, hc, hc', e⟩ : ∃ i, ∃ c ∈ 𝒜 i, c ∉ x.1.asHomogeneousIdeal ∧
        c * (z.den.1 * y.num.1) = c * (y.den.1 * z.num.1) := by
      apply_fun HomogeneousLocalization.val at e
      simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mk, mk_eq_mk',
        IsLocalization.mk'_eq_iff_eq] at e
      obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e
      obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)
      refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩
      apply_fun fun x ↦ (decompose 𝒜 x (i + z.deg + y.deg)).1 at hc
      conv_rhs at hc => rw [add_right_comm]
      rwa [← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        ← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        mul_assoc, mul_assoc] at hc
      exacts [y.den.2, z.num.2, z.den.2, y.num.2]

Goal state after:
case exists_of_eq
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ ∃ c, ↑c * HomogeneousLocalization.mk y = ↑c * HomogeneousLocalization.mk z
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq.e_6.e_a
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ c ^ (m - 1) * (c * (↑z.den * ↑y.num)) = c ^ (m - 1) * (c * (↑y.den * ↑z.num))

Tactic:
e

Goal state after:
case exists_of_eq.e_6.e_a
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ c ^ (m - 1) * (c * (↑y.den * ↑z.num)) = c ^ (m - 1) * (c * (↑y.den * ↑z.num))
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:
x

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))),
    (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.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ IsIso M.fromTildeΓ

Tactic:
rw [isIso_fromTildeΓ_iff_isLocalizing, isLocalizing_iff_aux]

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ Aux M ⊤
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
⊢ ∀ ⦃X Y : Cᵒᵖ ⥤ D⦄ (f : X ⟶ Y),
    ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f ≫
        {
          app := fun x ↦
            match x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := ⋯ } =
      {
          app := fun x ↦
            match x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := ⋯ } ≫
        (𝟭 (Cᵒᵖ ⥤ D)).map f

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun i ↦ { I₀ := σ i, X := Y i, f := g i }
i : E.I₀
⊢ P.property (F i)

Tactic:
rw [← (F i).presieve₀_mem_precoverage_iff]
      exact hg i

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover

Tactic:
by
  dsimp; infer_instance

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

Goal state before:
pp: case refine_3.inr.refine_1
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F (Sieve.pullback (T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
          ← Presieve.isSheafFor_iff_generate]

Goal state after:
case refine_3.inr.refine_1
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (fun i_1 ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.f i)) fun x ↦
      pullback.snd (𝒰.f x) (T.affineOneHypercover.f i))
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:
a₁

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₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: ⊢ fppfPrecoverage = precoverage @Flat ⊓ precoverage @LocallyOfFinitePresentation

Tactic:
by
  grind [fppfPrecoverage, precoverage, precoverage, MorphismProperty.precoverage_inf]

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

Goal state before:
pp: ⊢ fpqcTopology.Subcanonical

Tactic:
by
  refine GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun X ↦ ?_
  rw [fpqcTopology_eq_propQCTopology, isSheaf_type_propQCTopology_iff]
  refine ⟨?_, ?_⟩
  · exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _
  · intro R S f hf₁ hf₂
    have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _
    exact .singleton_of_isRepresentable_of_effectiveEpi _ _

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
i : 𝒰.I₀
⊢ P (𝒰.X i).hom

Tactic:
rw [← CategoryTheory.Over.w (𝒰.f i)]
    exact P.comp_mem _ _ (H _ 𝒰.mem₀ ⟨⟨i⟩⟩) X.prop

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
⊢ Mono (c.ι.app j₀)

Tactic:
by
  let f : (Functor.const _).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
    { app j := X.map j.hom
      naturality _ _ g := by
        dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w] }
  have := NatTrans.mono_of_mono_app f
  exact colim.map_mono' f (isColimitConstCocone _ _)
    ((Functor.Final.isColimitWhiskerEquiv _ _).symm hc) (c.ι.app j₀) (by cat_disch)

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

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

Tactic:
by
    rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
h : Epi f
this✝ : IsFiltered J
this : Mono f
⊢ ∃ j, IsIso (F.obj j).obj.hom

Tactic:
rw [Subobject.epi_iff_mk_eq_top f,
    subobjectMk_of_isColimit_eq_iSup F hc f hf] at h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
⊢ ∃ j, IsIso (F.obj j).obj.hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := ⋯
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
j : J
t : ↑(Set.range s) := ⋯
⊢ Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (σ t)).obj.hom

Tactic:
exact (hσ t).symm.le

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ Φ.succ X = Y

Tactic:
by
  cases hf
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
⊢ f i ≫ l ≫ eZ.inv = t ≫ ι'

Tactic:
rw [reassoc_of% hl₁, ← reassoc_of% commι, eZ.hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
e.map_limit k hk (hki.trans hij)

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩ =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

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

Tactic:
exfalso
      exact hj hi.isMax

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

Goal state before:
pp: case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ insert s S', F i)

Tactic:
Finset.sum_insert Hnot

Goal state after:
case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
h' : (Int.padicValuation p) x.num = 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num

pp: case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
h' : (Int.padicValuation p) x.num < 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num

Tactic:
· simp [h, h']

Goal state after:
case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
h' : (Int.padicValuation p) x.num < 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε

Tactic:
stationaryPoint_spec hf le_rfl hn

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f (stationaryPoint hf)) < ε
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : LocallySmall.{w, v, u} C
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
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
K L : Sheaf J A
f : K ⟶ L
x✝ : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ IsIso ((sheafCompose J (forget A)).map f)

Tactic:
hP.jointlyReflectIsomorphisms_type.isIso_iff

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : LocallySmall.{w, v, u} C
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
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
K L : Sheaf J A
f : K ⟶ L
x✝ : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map ((sheafCompose J (forget A)).map f))
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
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
rw [this, hcfg]

Goal state after:
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
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : max f.norm g.norm = f.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
rw [this, hcfg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
⊢ (f + g).norm = max f.norm g.norm

Tactic:
have h1 : (f + g).norm = f.norm := norm_equiv this

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
⊢ (f + g).norm = max f.norm g.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
exact Quotient.eq.symm

Goal state after: