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

Goal state before:
pp: case h.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
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op))
      (f ^ ((⨆ i, n i) - n i) • f ^ n i • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

Tactic:
Scheme.Modules.map_smul_Spec,

Goal state after:
case h.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
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ f ^ ((⨆ i, n i) - n i) • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ (ConcreteCategory.hom (Φ.presheafFiber.map (shrinkYoneda.{w, v, u}.map f)))
      ((ConcreteCategory.hom (Φ.toPresheafFiber X x (shrinkYoneda.{w, v, u}.obj X)))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    (ConcreteCategory.hom (Φ.toPresheafFiber X x (shrinkYoneda.{w, v, u}.obj Y))) (shrinkYonedaObjObjEquiv.symm f)

Tactic:
refine (Φ.toPresheafFiber_naturality_apply (shrinkYoneda.{w}.map f) _ x
    (shrinkYonedaObjObjEquiv.symm (𝟙 X))).trans (congr_arg _ ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map f).app (op X))) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    shrinkYonedaObjObjEquiv.symm f
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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op = restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₂.op

Tactic:
restriction.res_eq_res data G₀ _ h₂

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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op = restriction.res data G₀ h₂ ≫ G₀.obj.map p₂.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: 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)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ P.precoverage.coverings S

Tactic:
let E : PreZeroHypercover S := ⟨_, _, f⟩
    let F (i : ι) : PreZeroHypercover (E.X i) := ⟨_, _, g i⟩
    refine (E.bind F).presieve₀_mem_precoverage_iff.mpr (h _ _ ?_ fun i ↦ ?_)
    · rwa [← E.presieve₀_mem_precoverage_iff]
    · rw [← (F i).presieve₀_mem_precoverage_iff]
      exact hg i

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this : i₁ (IsLocalRing.closedPoint K) ∈ ⨆ i, basicOpen 𝒜 ↑i
⊢ ⋯.HasLift

Tactic:
TopologicalSpace.Opens.mem_iSup

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this : ∃ i, i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ ⋯.HasLift
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₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
let A₂ : D := ⟨Over.mk (π a₂), a₂, 𝟙 _, by simp⟩

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₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
A₂ : D := { obj := Over.mk (π a₂), property := ⋯ }
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), 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₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
A₂ : D := { obj := Over.mk (π a₂), property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ π a₁), property := ⋯ }
i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁ ⋯)
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
let i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂)

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₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
A₂ : D := { obj := Over.mk (π a₂), property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ π a₁), property := ⋯ }
i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂ ⋯)
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
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₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r

Tactic:
eq,

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₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₂ ≫ r + x₃ ≫ b = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ gj ≫ (T j).hom = gi ≫ (T i).hom

Tactic:
← Over.w (g i),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ gj ≫ (T j).hom = gi ≫ Over.Hom.left (g i) ≫ Z✝.hom
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt.obj ⟶ s.pt.obj

Tactic:
refine (s.pt.2.isSheafFor _ H).extend ?_
    refine ⟨fun Y ↦ ↾fun g ↦ ((s.inj (Sieve.ofArrows.i g.2)).hom.app Y)
      (Sieve.ofArrows.h g.2), ?_⟩
    intro ⟨Y⟩ ⟨Z⟩ ⟨(g : Z ⟶ Y)⟩
    ext u
    simp only [Sieve.functor_obj, Sieve.generate_apply, Sieve.functor_map, Quiver.Hom.unop_op',
      TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
      ← heq s (g ≫ Sieve.ofArrows.h u.2)
      (Sieve.ofArrows.h <| Sieve.downward_closed _ u.2 g) (by simp)]
    exact ConcreteCategory.congr_hom ((s.inj _).hom.naturality g.op) _

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
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 (σ t)).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom

Tactic:
exact MonoOver.subobjectMk_le_mk_of_hom
      (F.map (IsCardinalFiltered.toMax σ hs t))

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

Goal state before:
pp: 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
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

Tactic:
wlog h : j₁ ≤ j₂ generalizing j₁ j₂

Goal state after:
case inr
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
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂),
    j₁ ≤ j₂ → iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
h : ¬j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

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
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

Tactic:
· simp [functorMap,
      ι_functorMapTgt_assoc f (𝟙 (Arrow.mk πX)) i t b w b (by simp) t (by simp)]

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

Goal state before:
pp: 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)
⊢ functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 (functorObj f πX)

Tactic:
by
  ext ⟨i, t, b, w⟩
  · simp [functorMap]
  · simp [functorMap,
      ι_functorMapTgt_assoc f (𝟙 (Arrow.mk πX)) i t b w b (by simp) t (by simp)]

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

Goal state before:
pp: 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
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom

Tactic:
by
      rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.llp.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.llp.transfiniteCompositionsOfShape J ≤ W.llp
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
⊢ W.llp f

Tactic:
have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
      (hc := h.isColimit) (fun j hj ↦ h.map_mem j hj _ hp)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
this : W.llp (h.incl.app ⊥)
⊢ W.llp f
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
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
      (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f ≫
        ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f

Tactic:
Iso.inv_hom_id_app,

Goal state after:
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
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
      (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      𝟙 (((succStruct I κ).succ (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).obj f)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ Arrow.mk (A.ofLE ⋯.choose ⋯) ≅ Arrow.mk (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
exact Arrow.isoMk (Iso.refl _)
      (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
rw [h, zero_add]

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ! < n

Tactic:
by
  apply lt_of_le_of_lt _ (sub_one_mul_padicValNat_factorial_lt_of_ne_zero p hn)
  conv_lhs => rw [← one_mul (padicValNat p n !)]
  gcongr
  exact le_sub_one_of_lt (Nat.Prime.one_lt hp.elim)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False

Tactic:
have hpn : 0 < padicNorm p (f (stationaryPoint hf)) - padicNorm p (g (stationaryPoint hg)) :=
    sub_pos_of_lt hlt

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
⊢ False