mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 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))
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ ↔
    ∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂

Tactic:
refine ((colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P)).eq_iff' ..).trans ?_

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 : 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))
⊢ (∃ j f,
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
        (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂) ↔
    ∃ Y f y,
      (ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂
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)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
wlog h𝒰 : (∀ i, IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ generalizing R 𝒰

Goal state after:
case inr
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)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

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)
h𝒰 : (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀
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)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ i₁ (IsLocalRing.closedPoint K) ∈ ↑(basicOpen 𝒜 ↑i)

Tactic:
exact hi

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)
⊢ EffectiveEpi f

Tactic:
Sieve.generateSingleton_eq

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ EffectiveEpi f
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)

Tactic:
Sieve.generateSingleton_eq

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case right
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).multicospanShape.L
⊢ (Iso.refl (presheafObjMultifork data G₀ X).pt).hom ≫
      Multifork.ι
        ((Cone.postcompose
              (WalkingMulticospan.functorExt (fun x ↦ presheafObjObjIso data G₀ ((data X).X x))
                  (fun x ↦ presheafObjObjIso data G₀ ((data X).Y x.snd)) ⋯ ⋯).hom).obj
          ((data X).toOneHypercover.multifork (presheaf data G₀)))
        i =
    (presheafObjMultifork data G₀ X).ι i

Tactic:
simp [Multifork.ι, PreOneHypercover.multifork, MulticospanIndex.multicospan]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.uliftYonedaEquiv.symm x ≫ f = J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x)

Tactic:
by
  apply J.uliftYonedaEquiv.injective
  simp [uliftYonedaEquiv_comp]

Goal state after:
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'))
t : F.obj.obj X
⊢ J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) t) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := J.uliftYonedaEquiv.surjective t

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
⊢ J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) (J.uliftYonedaEquiv u)) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv u)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ coconeOfLE (Φ.iter i).F ⋯ ≅ (Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))

Tactic:
refine Cocone.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ ∀ (j : ↑(Set.Iio i)),
    (coconeOfLE (Φ.iter i).F ⋯).ι.app j ≫ (eqToIso ⋯).hom =
      ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))).ι.app j
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ofHoms (fun i ↦ (↑((equivShrink ↑W.toSet).symm i)).hom) f

Tactic:
ofHoms_iff

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) =
    ↑(multiplicity (↑p) c + multiplicity (↑p) q.num) - ↑(multiplicity (↑p) c + multiplicity ↑p ↑q.den)

Tactic:
rw [Nat.cast_add, Nat.cast_add]
    simp_rw [Int.natCast_multiplicity p q.den]
    ring

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
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ (x ^ n).valuation = n * x.valuation

Tactic:
zify; simp [← valuation_coe]

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

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

Tactic:
sub_one_mul_padicValNat_factorial n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ n - (p.digits n).sum < n
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p ↑p = padicValInt p a + 1

Tactic:
simp only [padicValInt.of_nat, padicValNat_self]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
⊢ ∃ W h, h ≫ ⟨f, hf✝⟩ = h ≫ ⟨g, hg⟩

Tactic:
let h := isLimitForkMapOfIsLimit F _ (equalizerIsEqualizer f g)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
⊢ ∃ W h, h ≫ ⟨f, hf✝⟩ = h ≫ ⟨g, hg⟩
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
⊢ Mono f ↔ c.fst = c.snd

Tactic:
constructor
  · intro hf
    simpa only [← cancel_mono f] using c.condition
  · intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h
    rw [hf]

Goal state after:
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
⊢ Nonempty (IsLimit ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op))

Tactic:
exact ⟨{
    lift s := (isSheaf_skyscraperPresheaf_aux R hR s).choose
    fac s j := by
      dsimp
      ext y
      simpa using! (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y
    uniq s m hm := by
      dsimp at hm ⊢
      ext x
      obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
      simpa [← hm (op (Presieve.categoryMk _ _ hg))] using!
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm }⟩

Goal state after:
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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
F : Sheaf J A
M : A
f : Φ.presheafFiber.obj F.obj ⟶ M
⊢ ((Φ.skyscraperSheafAdjunction.homEquiv F M) f).hom = Φ.skyscraperPresheafHomEquiv f

Tactic:
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]

Goal state after:
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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
F : Sheaf J A
M : A
f : F ⟶ Φ.skyscraperSheaf M
⊢ (Φ.skyscraperSheafAdjunction.homEquiv F M).symm f = Φ.skyscraperPresheafHomEquiv.symm f.hom

Tactic:
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑0 = 0

Tactic:
cast_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (x * y).addValuationDef = x.addValuationDef + y.addValuationDef

Tactic:
simp only [addValuationDef]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min x.addValuationDef y.addValuationDef ≤ (x + y).addValuationDef

Tactic:
simp only [addValuationDef]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
⊢ s.d i j ≫ s.d j k = 0

Tactic:
simp only [d, assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n'⦌ ≠ ⦋n⦌

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = PInfty.f n' ≫ X.map i.op

Tactic:
· by_contra h'
      exact h (congr_arg SimplexCategory.len h'.symm)

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = PInfty.f n' ≫ X.map i.op
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk
X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
q₁ : Homotopic.Quotient x₁ y₁
a : Path x₀ y₀
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀)) a) q₁

Tactic:
| mk a =>

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

Tactic:
apply (factorsThroughLocalization C).isLocalizedEquivalence
  apply MorphismProperty.eq_inverseImage_quotientFunctor

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ ∃ X', ∃ (_ : IsCofibrant X'), ∃ p, Fibration p ∧ WeakEquivalence p

Tactic:
by
  have h := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C)
    (initial.to X)
  refine ⟨h.Z, ?_, h.p, inferInstance, inferInstance⟩
  rw [isCofibrant_iff_of_isInitial h.i initialIsInitial]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ toHoCat.map (homMk (resolutionMap (𝟙 X))) = 𝟙 (toHoCat.obj (mk (resolutionObj X)))

Tactic:
← toHoCat.map_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ toHoCat.map (homMk (resolutionMap (𝟙 X))) = toHoCat.map (𝟙 (mk (resolutionObj X)))
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map (homMk (resolutionMap (f ≫ g))) =
    toHoCat.map (homMk (resolutionMap f)) ≫ toHoCat.map (homMk (resolutionMap g))

Tactic:
rw [← toHoCat.map_comp]
    exact resolutionObj_hom_ext (by simpa using .refl _)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence { hom := HoCat.pResolutionObj X.obj }

Tactic:
weakEquivalence_iff_of_objectProperty

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence { hom := HoCat.pResolutionObj X.obj }.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant P.P
⊢ WeakEquivalence (homMk P.ι)

Tactic:
weakEquivalence_iff_of_objectProperty

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant P.P
⊢ WeakEquivalence (homMk P.ι).hom
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (F.map f)

Tactic:
weakEquivalence_iff_of_objectProperty

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
⊢ IsIso (F.map f)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj

Tactic:
weakEquivalence_iff_of_objectProperty

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ c.multispanIndex.left (i₁, i₂)

Tactic:
dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ S = Finset.univ

Tactic:
by
          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)

Goal state after: