mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))

Tactic:
rw [Proj.opensRange_awayι]

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)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ Set.range ⇑i₁ ⊆ ↑(basicOpen 𝒜 ↑i)
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram := ⋯
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
⊢ ∀ (j : (Sieve.generateSingleton f).arrows.category),
    (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = (aux e ⋯).ι.app j

Tactic:
rintro ⟨A, g, hA⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => Exists.choose hT ≫ e,
          naturality := ⋯ } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
⊢ (Sieve.generateSingleton f).arrows.cocone.ι.app { obj := A, property := ⋯ } ≫ m =
    (aux e ⋯).ι.app { obj := A, property := ⋯ }
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)
Y : C
⊢ ∀ ⦃Y_1 : Cᵒᵖ⦄ (f : op Y ⟶ Y_1),
    ((Sieve.ofArrows X c.inj).functor.map f ≫
        ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y_1)) (Sieve.ofArrows.h ⋯)) =
      (↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Y))) (Sieve.ofArrows.h ⋯)) ≫
        s.pt.obj.map f

Tactic:
⟨Z⟩

Goal state after:
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)
Y Z : C
⊢ ∀ (f : op Y ⟶ op Z),
    ((Sieve.ofArrows X c.inj).functor.map f ≫
        ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Z))) (Sieve.ofArrows.h ⋯)) =
      (↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Y))) (Sieve.ofArrows.h ⋯)) ≫
        s.pt.obj.map f
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : J.Subcanonical
ι : Type u_1
inst✝² : CoproductsOfShapeDisjoint C ι
inst✝¹ : HasPullbacks C
inst✝ : HasStrictInitialObjects C
hcov : ∀ {X : ι → C} {c : Cofan X} (x : IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt
htriv : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
X : ι → C
c : Cofan X
hc : IsColimit c
this : ∀ (i : ι), Mono (c.inj i)
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))

Tactic:
refine isColimitCofanMkYoneda _ _ (hcov hc) htriv fun hij Y a b hab ↦ ⟨?_⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : J.Subcanonical
ι : Type u_1
inst✝² : CoproductsOfShapeDisjoint C ι
inst✝¹ : HasPullbacks C
inst✝ : HasStrictInitialObjects C
hcov : ∀ {X : ι → C} {c : Cofan X} (x : IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt
htriv : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
X : ι → C
c : Cofan X
hc : IsColimit c
this : ∀ (i : ι), Mono (c.inj i)
i✝ j✝ : ι
hij : i✝ ≠ j✝
Y : C
a : Y ⟶ X i✝
b : Y ⟶ X j✝
hab : a ≫ c.inj i✝ = b ≫ c.inj j✝
⊢ IsInitial Y
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case succ.inr.inl
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
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂✝ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h : ¬k₂ ≤ j
h₂ : k₂ < Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂✝

pp: case succ.inr.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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
· exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)

Goal state after:
case succ.inr.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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

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

Tactic:
by
  intro _ _ f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨_, _, _, _, _, hf⟩ := hf
  exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

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₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))

Tactic:
have : Mono c.pt.hom := by dsimp [c]; infer_instance

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₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑n‖ = 1 ↔ p.Coprime n

Tactic:
norm_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑↑n‖ = 1 ↔ p.Coprime n
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑n‖ < 1 ↔ p ∣ n

Tactic:
norm_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑↑n‖ < 1 ↔ p ∣ n
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = 1 ↔ IsCoprime z ↑p

Tactic:
norm_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑↑z‖ = 1 ↔ IsCoprime z ↑p
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ < 1 ↔ ↑p ∣ z

Tactic:
norm_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑↑z‖ < 1 ↔ ↑p ∣ z
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 : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ c.inl = c.inr

Tactic:
constructor
  · intro hf
    simpa only [← cancel_epi f] using c.condition
  · intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
    rw [hf]

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

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x

Tactic:
refine ⟨Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x, ?_, ?_⟩

Goal state after:
case refine_1
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x) ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩

case refine_2
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
this : Hom.residueFieldMap f x ≫ CommRingCat.ofHom b.toRingHom = a
⊢ (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x) default = x
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ IsPullback fst (F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ F✝.map (⋯.snd p)) (f ≫ g) p

Tactic:
rw [← Functor.map_comp, lift_snd]

Goal state after:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ IsPullback fst (F✝.map snd) (f ≫ g) p
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (a ≫ (glueData hf).openCover.f i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (b ≫ (glueData hf).openCover.f j)
⊢ yoneda.map a ≫ f i = yoneda.map b ≫ f j

Tactic:
simpa [Scheme.GlueData.openCover_X, yonedaEquiv_naturality] using h

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable
    (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫
      𝟙
        (Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X)))

Tactic:
← pbIso.hom_inv_id,

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom ≫ pbIso.inv)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
hi : i ≥ N
h : padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
⊢ ‖↑f i - q‖ < ε

Tactic:
refine lt_trans ?_ hε'.2

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
hi : i ≥ N
h : padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
⊢ ‖↑f i - q‖ < ↑ε'
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ X.σ 0 ≫ ((-1) ^ ↑j.succ.succ • X.δ j.succ.succ) = 0

Tactic:
rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]

Goal state after:
case neg.h.hj₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ j.succ.succ.pred ⋯ ≠ 0

case neg.h.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ ↑(j.succ.succ.pred ⋯) + q

case neg.h.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < j.succ.succ
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 + (X.σ 0 + -X.σ 0 + (-X.σ 0 + (X.σ 0 + -X.σ 0))) = 0

Tactic:
simp only [add_neg_cancel, add_zero, zero_add]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((functor ⋙ inverse).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n
            dsimp
            simp only [HomologicalComplex.p_idem]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ ((functor ⋙ inverse).obj P).p ≫
      { f := fun n ↦ P.p.f n, comm' := ⋯ } ≫ ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p =
    { f := fun n ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n
            dsimp
            simp only [HomologicalComplex.p_idem]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Tactic:
apply id_comp

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
apply id_comp

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
⊢ N.map (Γ₂N₂.hom.app P) ≫ N₂Γ₂.hom.app (N.obj P) = 𝟙 (N.obj P)

Tactic:
let β := N₂Γ₂.app (N.obj P)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ N.map (Γ₂N₂.hom.app P) ≫ N₂Γ₂.hom.app (N.obj P) = 𝟙 (N.obj P)
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
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
⊢ f ≫ PInfty.f n = 0 ↔ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0

Tactic:
constructor
  · intro h
    rcases n with _ | n
    · dsimp at h
      rw [comp_id] at h
      rw [h, zero_comp]
    · have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
      dsimp at h'
      rw [comp_id, comp_add, h, zero_add] at h'
      rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
        Finset.sum_eq_zero]
      intro i _
      simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]
  · intro h
    rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_zero]
    intro A
    by_cases hA : A.EqId
    · dsimp at hA
      subst hA
      rw [assoc, reassoc_of% h, zero_comp]
    · simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

Goal state after: