mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε

Tactic:
by

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✝¹ : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ F.map (p₂ hf₁ f₂ f₃) ≫ f₂ = π hf₁ f₂ f₃

Tactic:
by

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✝¹ : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ F.map (p₃ hf₁ f₂ f₃) ≫ f₃ = π hf₁ f₂ f₃

Tactic:
by

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

Goal state before:
pp: j : ℕ
⊢ ¬c.Rel 0 j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ hσ' q n m hnm = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩

Tactic:
by

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✝ F : C ⥤ D
inst✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift' x₁ x₂ h₁₂ ≫ hf₁.fst' f₂ = hf₁.lift' x₁ x₃ h₁₃ ≫ hf₁.fst' f₃

Tactic:
by

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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ≫ pullback₃.p₁ hf₁ f₂ f₃ = x₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
this : X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0
⊢ (((-1) ^ 0 • X.σ ⟨0, ⋯⟩) ≫ eqToHom ⋯) ≫ K[X].d 1 0 = 0

Tactic:
by

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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ≫ pullback₃.p₂ hf₁ f₂ f₃ = x₂

Tactic:
by

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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ≫ pullback₃.p₃ hf₁ f₂ f₃ = x₃

Tactic:
by

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

Goal state before:
pp: 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
this : padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (Hσ q).f 0 = 0

Tactic:
by

Goal state after:
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 : ι
⊢ ∀ {X_1 : Schemeᵒᵖ} (x y : ToType ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj X_1)),
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) x =
        (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) y →
      Presheaf.equalizerSieve x y ∈ zariskiTopology (unop X_1)

Tactic:
by

Goal state after:
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 : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ IsIso (yonedaGluedToSheaf hf)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ Hσ q = Hσ q ≫ (alternatingFaceMapComplex C).map f

Tactic:
by

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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ = φ'

Tactic:
by

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
h : F.relativelyRepresentable (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
⊢ hσ' q n m hnm = G.map (hσ' q n m hnm)

Tactic:
by

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

Goal state before:
pp: 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
this : padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) < ε / 3 + ε / 3
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (Hσ q).f n = G.map ((Hσ q).f n)

Tactic:
by

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
⊢ (limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
        (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
          (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯) ≫
      (prodIsoPullback X X).inv =
    (pullback.congrHom ⋯ ⋯ ≪≫
          (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
            (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom ≫
      prodMap

Tactic:
by

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ (pbRepr.hom ≫ pullback.fst g g') ≫ g = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g')) ≫ g'

Tactic:
simp [pullback.condition]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
by

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ (pbRepr.hom ≫ pullback.fst g g') ≫ g = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g')) ≫ g'

Tactic:
by

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ pbRepr.hom ≫ pullback.fst g g' = pbRepr.hom ≫ pullback.fst g g'

Tactic:
by

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ pbRepr.hom ≫ pullback.snd g g' = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g'))

Tactic:
by

Goal state after:
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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ ↑j + q
⊢ φ ≫ X.δ j = 0

Tactic:
by

Goal state after:
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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ n + 1 ≤ ↑j + (q + 1)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ (f ≫ φ) ≫ X.δ j.succ = 0

Tactic:
by

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
h : F.relativelyRepresentable (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g

Tactic:
by

Goal state after:
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
⊢ a + 1 < n + 2

Tactic:
by

Goal state after:
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
⊢ a < n + 1

Tactic:
by

Goal state after:
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
d : ℕ
⊢ n + d = a + d + q

Tactic:
by

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✝ 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)
⊢ 𝟙 (F.obj a) ≫ (g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X =
    𝟙 (F.obj a) ≫ (g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x : ℚ_[p]), dist x x = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = dist y x

Tactic:
by

Goal state after: