mathlib-initiative/mathlib-tactics huggingface dataset:
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 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

Tactic:
⟨(g : Z ⟶ Y)⟩

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
g : Z ⟶ Y
⊢ ((Sieve.ofArrows X c.inj).functor.map (op g) ≫
      ↾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 (op g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f✝ : α <i β
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : β ⥤ C
i j : α
f : i ⟶ j
⊢ (⋯.functor ⋙ F).map f ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ ((Functor.const α).obj (F.obj f✝.top)).map f

Tactic:
dsimp
        rw [← F.map_comp, comp_id]
        rfl

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.Sites.Subcanonical

Goal state before:
pp: case e
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
X✝ : C
⊢ (CategoryTheory.yoneda.obj Y).obj (op X✝) ≃ (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X✝)

Tactic:
exact Equiv.ulift.symm

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
⊢ W ((h.ici j).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem i.1 (Set.not_isMax_coe _ hi)

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
this : W (h.F.map (homOfLE ⋯))
⊢ W ((h.ici j).F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

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
A : C
⊢ ∀ ⦃Y : C⦄ (f : A ⟶ Y), W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f

Tactic:
B

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
A B : C
⊢ ∀ (f : A ⟶ B), W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

pp: case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃

Tactic:
· obtain hi₂₃ | rfl := hi'.lt_or_eq
    · dsimp [map]
      obtain hi₃' | rfl := hi₃.lt_or_eq
      · rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
      · rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]
    · rw [map_id, comp_id]

Goal state after:
case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowMap (functor hj iter) k i ⋯ hij✝ = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk

Tactic:
rw [arrowMap_functor _ _ _ _ _ hij, arrow_mk_mapObj,
        arrowMap_limit _ _ hi _ _ hk]
      congr 1
      apply Arrow.functor_ext
      rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
      dsimp
      generalize_proofs
      rw [← arrowMap, ← arrowMap, arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij),
        arrow_mk_mapObj]
      apply congr_arrowMap

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

Goal state before:
pp: p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ ↑(padicValInt p q.num) - ↑(padicValNat p q.den) = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)

Tactic:
padicValInt.of_ne_one_ne_zero hp (Rat.num_ne_zero.2 hq),

Goal state after:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ ↑(multiplicity (↑p) q.num) - ↑(padicValNat p q.den) = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A✝ ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)

Tactic:
refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
    (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A✝ ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ Arrow.mk ((Subobject.mk f).ofLE (Subobject.mk p') ⋯) ≅ Arrow.mk i
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A : C
⊢ ∀ ⦃Y_1 : C⦄ (g : A ⟶ Y_1), monomorphisms C g → HasLiftingProperty g p

Tactic:
B

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
⊢ ∀ (g : A ⟶ B), monomorphisms C g → HasLiftingProperty g p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q ≠ 0

Tactic:
by
  rw [padicNorm.eq_zpow_of_nonzero hq]
  apply zpow_ne_zero
  exact mod_cast ne_of_gt hp.1.pos

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
⊢ n * padicValNat p q = 0

Tactic:
padicValNat_primes ne,

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
⊢ n * 0 = 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
rw [norm_def]; exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ : C
x : F.obj X✝
X : (fromOverFunctor F x).Elements
⊢ { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.map
        ((Iso.refl (𝟭 (fromOverFunctor F x).Elements)).hom.app X) ≫
      (Iso.refl
              ({ obj := fun u ↦ (fromOverFunctor F x).elementsMk (Over.mk ↑u.hom) ⟨u.left.snd, ⋯⟩,
                  map := fun {X Y} f ↦
                    homMk ((fromOverFunctor F x).elementsMk (Over.mk ↑X.hom) ⟨X.left.snd, ⋯⟩)
                      ((fromOverFunctor F x).elementsMk (Over.mk ↑Y.hom) ⟨Y.left.snd, ⋯⟩)
                      (Over.homMk ↑(Over.Hom.left f) ⋯) ⋯,
                  map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
                  map := fun {X Y} f ↦
                    Over.homMk
                      (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                        (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                        (Over.Hom.left ↑f) ⋯)
                      ⋯,
                  map_id := ⋯, map_comp := ⋯ })).hom.app
        ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
              map := fun {X Y} f ↦
                Over.homMk
                  (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                    (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                    (Over.Hom.left ↑f) ⋯)
                  ⋯,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
simp_all; rfl

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
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x

Tactic:
have : f.residueFieldMap x ≫ CommRingCat.ofHom b.toRingHom = a := by
    ext1; exact b.comp_algebraMap

Goal state after:
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
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
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f

Tactic:
by
  refine ⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩
  all_goals obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
  · refine ⟨c, g_snd, g_fst, BC⟩
  · refine (P.arrow_mk_iso_iff ?_).2 H
    exact Arrow.isoMk (F.preimageIso (h.isoIsPullback X (F.obj a) BC)) (Iso.refl _)
      (F.map_injective (by simp))

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
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
⊢ relative F P (F.map f)

Tactic:
apply relative.of_exists
  intro Y' g
  obtain ⟨g, rfl⟩ := F.map_surjective g
  exact ⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩

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
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
⊢ P snd

Tactic:
← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)

Goal state after:
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
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hbc.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3

Tactic:
suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]
      apply lt_of_le_of_lt
      · apply padicNormE.add_le
      · apply _root_.add_lt_add
        · rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj
        · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε

Tactic:
refine ⟨x, fun ε hε => ?_⟩

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
this : φ ≫ X.δ ⟨a + 2 + k, ⋯⟩ = 0
⊢ ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) ⟨k, hk⟩))) •
      (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) ⟨k, hk⟩))) ≫ X.σ ⟨a, ⋯⟩ =
    0

Tactic:
by
      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)

Tactic:
by
  rw [← norm_p_zpow, zpow_natCast]

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

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑(↑p * x)‖ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ ↑(x * y).valuation = ↑x.valuation + ↑y.valuation

Tactic:
← WithTop.coe_add,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ ↑(x * y).valuation = ↑(x.valuation + y.valuation)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (K.X Δ.len)

Tactic:
unfold mapMono
  simp only [eqToHom_refl, dite_eq_ite, if_true]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e

Tactic:
unop_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ.unop ≫ θ'.unop) ≫ A.e
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ

Tactic:
← image.fac (θ'.unop ≫ A.e),

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ factorThruImage (θ'.unop ≫ A.e) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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 : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ PInfty.f n ≫
      P.p.app (op ⦋n⦌) ≫
        ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).cofan (op ⦋n⦌)).inj
            (Splitting.IndexSet.id (op ⦋n⦌)) ≫
          ((Γ₀.splitting (N₂.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ }).X).desc (op ⦋n⦌) fun A ↦
              PInfty.f (unop A.fst).len ≫ ((Γ₀.splitting K[P.X]).cofan (op ⦋n⦌)).inj A) ≫
            ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫
              P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
rw [Splitting.ι_desc_assoc]

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 : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ PInfty.f n ≫
      P.p.app (op ⦋n⦌) ≫
        (PInfty.f (unop (Splitting.IndexSet.id (op ⦋n⦌)).fst).len ≫
            ((Γ₀.splitting K[P.X]).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))) ≫
          ((Γ₀.splitting K[P.X]).desc (op ⦋n⦌) fun A ↦ PInfty.f (unop A.fst).len ≫ P.X.map A.e.op) ≫ P.p.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ∈ I
x : X
⊢ (F.extend t) x = F (⟨t, ht⟩, x)

Tactic:
by
  simp [ht]

Goal state after: