mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case left.left.id
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
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
i₁ : data.multicospanShape.L
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁)) ≫
      match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁))

Tactic:
simp [MulticospanIndex.multicospan]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case left.right.fst
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
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.fst j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.fst j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.fst j₂)

Tactic:
simp [MulticospanIndex.multicospan]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case left.right.snd
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
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.snd j₂) ≫
      match WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.left (data.multicospanShape.snd j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.snd j₂)

Tactic:
simp [MulticospanIndex.multicospan]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case right.right.id
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
X : C
data : F.PreOneHypercoverDenseData X
P Q : C₀ᵒᵖ ⥤ A
f : P ⟶ Q
j₁ : data.multicospanShape.R
⊢ ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁)) ≫
      match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) =
    (match WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y j.snd))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁))

Tactic:
simp [MulticospanIndex.multicospan]

Goal state after:
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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
k : ι (pullback (f S i) (f S j))
⊢ F.map (F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j))) ≫ f S i =
    F.map (F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j))) ≫ f S j

Tactic:
by simp [pullback.condition]

Goal state after:
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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ F.map (q ≫ p₁) =
    F.map
      (F.preimage s ≫
        { I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
              Y := fun i j ↦ U (pullback (f S i) (f S j)),
              p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)), w := ⋯ }.p₁
          k)

Tactic:
by simp [fac₁]

Goal state after:
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
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ p ≫ (data X).f i = F.map (𝟙 X₀) ≫ f

Tactic:
simpa using fac

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

Goal state before:
pp: case refine_3.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))
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
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
refine T.affineOneHypercover.isSheafFor_of_pullback hzar ?_ ?_

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 (Sieve.pullback (T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

case refine_3.inr.refine_2
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 j : T.affineOneHypercover.I₀⦄ (k : T.affineOneHypercover.I₁ i j),
    Presieve.IsSeparatedFor F
      (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: ⊢ fpqcTopology.Subcanonical

Tactic:
refine GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun X ↦ ?_

Goal state after:
X : Scheme
⊢ Presieve.IsSheaf fpqcTopology (yoneda.obj X)
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
R : CommRingCat
⊢ ∀ {S : CommRingCat} (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
S

Goal state after:
case refine_2
X : Scheme
R S : CommRingCat
⊢ ∀ (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))
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✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ c₁.ι.app j ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)).hom ≫ colimMap φ =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ (colimit.cocone X₁).ι.app j ≫ colimMap φ = c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_1
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 ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)).hom ≫ colimMap S.f =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,

Goal state after:
case refine_1
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
⊢ (colimit.cocone S.X₁).ι.app j ≫ colimMap S.f =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
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 ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom ≫ colimMap S.g =
    c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,

Goal state after:
case refine_2
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
⊢ (colimit.cocone S.X₂).ι.app j ≫ colimMap S.g =
    c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom
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✝ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : (monomorphisms C).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this✝ : ∀ (j : J), Mono (f.app j)
this : Mono f
⊢ ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j

Tactic:
simp [hφ]

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
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by
  ext X x
  simpa only [uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
    using! congr_arg (J.uliftYonedaEquiv) (h _ (J.uliftYonedaEquiv.symm x))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ arrowMap F k k ⋯ hk = arrowMap G k k ⋯ hk

Tactic:
arrowMap_refl,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ Arrow.mk (𝟙 (F.obj ⟨k, hk⟩)) = arrowMap G k k ⋯ hk
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ Arrow.mk (𝟙 (F.obj ⟨k, hk⟩)) = arrowMap G k k ⋯ hk

Tactic:
arrowMap_refl,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ Arrow.mk (𝟙 (F.obj ⟨k, hk⟩)) = Arrow.mk (𝟙 (G.obj ⟨k, hk⟩))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
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)
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₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
⊢ arrowMap iter₁.F (Order.succ j) (Order.succ j) h₁₂ h₂ = arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂

Tactic:
arrowMap_refl,

Goal state after:
case neg
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)
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₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
⊢ Arrow.mk (𝟙 (iter₁.F.obj ⟨Order.succ j, h₂⟩)) = arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
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)
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₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
⊢ Arrow.mk (𝟙 (iter₁.F.obj ⟨Order.succ j, h₂⟩)) = arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂

Tactic:
arrowMap_refl,

Goal state after:
case neg
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)
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₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
⊢ Arrow.mk (𝟙 (iter₁.F.obj ⟨Order.succ j, h₂⟩)) = Arrow.mk (𝟙 (iter₂.F.obj ⟨Order.succ j, h₂⟩))
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ (∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom) → W f

Tactic:
· rintro ⟨i, hi⟩
      simp only [← W.arrow_mk_mem_toSet_iff, hi, Arrow.mk_eq, Subtype.coe_prop]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) (n₂ * d₁)

Tactic:
hf1.multiplicity_le_multiplicity_iff hf2

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
rw [← zpow_zero (p : ℚ), zpow_right_inj₀]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ -padicValRat p ↑m = 0

case neg.ha₀
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ 0 < ↑p

case neg.ha₁
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ≠ 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · exact iff_of_true (dvd_zero _) (Or.inl rfl)
  · rw [padicValNat_dvd_iff_le_of_ne_one hp ha, or_iff_right ha]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ 0 ≤ max 0 0

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 ≤ max 0 (exp (-padicValRat p y✝))

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ 0 ≤ max (exp (-padicValRat p x✝)) 0

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 ≤ max (exp (-padicValRat p x✝)) (exp (-padicValRat p y✝))

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max 0 0

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max 0 (exp (-padicValRat p y✝))

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max (exp (-padicValRat p x✝)) 0

Tactic:
simp_all [-exp_neg]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max (exp (-padicValRat p x✝)) (exp (-padicValRat p y✝))

Tactic:
simp_all [-exp_neg]

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ padicValRat p x✝ ≤ padicValRat p (x✝ + y✝) ∨ padicValRat p y✝ ≤ padicValRat p (x✝ + y✝)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a.natAbs = 0 ∨ n ≤ padicValNat p a.natAbs

Tactic:
← padicValNat_dvd_iff_of_ne_one hp,

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ p ^ n ∣ a.natAbs