mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: 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₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : ¬i₁ < j
h₁' : i₁ = j
⊢ obj c i₁ = obj c i₂

Tactic:
subst h₁' h₂'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₂ : J
hi : i₂ ≤ i₂
F : ↑(Set.Iio i₂) ⥤ C
c : Cocone F
hi₂ : i₂ ≤ i₂
h₂ h₁ : ¬i₂ < i₂
⊢ obj c i₂ = obj c i₂
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
⊢ t ≫ ι' ≫ eZ.hom ≫ πFunctorObj f πX = f i ≫ b ≫ eS.hom

Tactic:
← commπ,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
⊢ t ≫ ι' ≫ πZ' ≫ eS.hom = f i ≫ b ≫ eS.hom
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
| (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val

Tactic:
← d.map_succ j hj e.val

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
| (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val))
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: case succ.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ ∀ (i : (c.attachCells j hj).ι),
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
      (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
· intro i
      simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : i < Order.succ j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val))

Tactic:
obtain hij | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq
    · rw [← homOfLE_comp ((Order.lt_succ_iff_of_not_isMax hj).mp hi) (Order.le_succ j), op_comp,
        map_comp, comp_apply, d.map_succ, ← e.map_succ i hij,
        ← homOfLE_comp (Order.succ_le_of_lt hij) (Order.le_succ j), op_comp,
        map_comp, comp_apply, d.map_succ]
    · simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom, d.map_succ]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
| (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val

Tactic:
← d.map_succ j hj e.val

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
| (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ Arrow.mk (A.ofLE ⋯.choose ⋯) ≅ Arrow.mk (A.ofLE (largerSubobject hG A) ⋯)
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
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)

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₂)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p (b / p) = padicValNat p b - 1

Tactic:
by
  rw [padicValNat.div_of_dvd dvd, padicValNat_self]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
x✝ : ℝ
hε : x✝ > 0
⊢ ∃ i, ∀ j ≥ i, (fun a ↦ ‖a‖) ((fun n ↦ ↑(↑f n)) j - (fun n ↦ ↑(↑f n)) i) < x✝

Tactic:
simpa [norm, norm_def] using f.cauchy hε

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

Goal state before:
pp: p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
⊢ ↑n ≤ emultiplicity p a ↔ n ≤ padicValNat p a

Tactic:
← padicValNat_eq_emultiplicity_of_ne_one hp ha,

Goal state after:
p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
⊢ ↑n ≤ ↑(padicValNat p a) ↔ n ≤ padicValNat p a
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
⊢ padicValNat p a + p ≤ a

pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
· rcases dvd with ⟨k, hk⟩
    have : padicValNat p k < k := by calc
      _ ≤ log p k := padicValNat_le_nat_log k
      _ < _ := log_lt_self p (by lia)
    rw [hk, padicValNat.mul (by lia) (by lia), padicValNat_self]
    calc
      _ ≤ p + k := by lia
      _ ≤ _ := Nat.add_le_mul hp.out.two_le (by lia)

Goal state after:
case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) = exp 0 ↔ ¬↑p ∣ x

Tactic:
exp_injective.eq_iff

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) = 0 ↔ ¬↑p ∣ x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) = 0 ↔ ¬↑p ∣ x

Tactic:
simp_all [Nat.Prime.ne_one Fact.out]

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k + n - (p.digits n).sum - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
Nat.sub_sub (k + n),

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k + n - ((p.digits n).sum + (p.digits k).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
h : IsLimit (BinaryFan.mk (F.map prod.fst) (F.map prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit F prod.fst prod.snd (prodIsProd X Y)
⊢ ∃ W x x, True

Tactic:
let h' := Types.binaryProductLimit (F.obj X) (F.obj Y)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
h : IsLimit (BinaryFan.mk (F.map prod.fst) (F.map prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit F prod.fst prod.snd (prodIsProd X Y)
h' : IsLimit (Types.binaryProductCone (F.obj X) (F.obj Y)) := Types.binaryProductLimit (F.obj X) (F.obj Y)
⊢ ∃ W x x, True
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ (c.fst ≫ φ) ≫ c.snd = 𝟙 c.pt ≫ c.snd

Tactic:
simp only [assoc, hφ₂, id_comp, comp_id, h]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))

Tactic:
exact norm_eq_of_equiv hf hg hfg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y)

Tactic:
have := ConcreteCategory.congr_hom
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality (f i)) y

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.fiber.map (f i) ≫ Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X)) y =
    (ConcreteCategory.hom
        (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i) ≫
          (shrinkYoneda.{w, v, u} ⋙ Φ.obj.presheafFiber).map (f i)))
      y
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift PadicSeq.norm ⋯ (⟦a✝⟧ + ⟦b✝⟧) ≤
    max (Quotient.lift PadicSeq.norm ⋯ ⟦a✝⟧) (Quotient.lift PadicSeq.norm ⋯ ⟦b✝⟧)

Tactic:
apply PadicSeq.norm_nonarchimedean

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

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
i : ι
hy : (s i) default = X.hom x
⊢ ∃ i, (s i) default = X.hom x

Tactic:
exact ⟨i, hy⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (a b : ℚ_[p]), ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp [Norm.norm, map_mul]

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

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

Tactic:
simp [Norm.norm, map_mul]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q * r‖ = ‖q‖ * ‖r‖

Tactic:
simp [Norm.norm, map_mul]

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

Goal state before:
pp: case mp
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⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ (P q).f (n + 1))

Tactic:
apply HigherFacesVanish.of_comp

Goal state after:
case mp
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⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q ((P q).f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, pf✝³⟩ ≫ X.δ ⟨i, pf✝²⟩ +
      ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0

Tactic:
rw [← Fin.succ_mk (n + 1) a ‹_›, ← Fin.castSucc_mk (n + 2) i ‹_›,
      δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]

Goal state after:
case a
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : ⟨i, hi⟩ ∈ Finset.univ
hia : ⟨i, ⋯⟩ ≤ ⟨a, ⋯⟩.castSucc
pf✝⁴ : IsRightCancelAdd ℕ
pf✝³ : a + 1 < n + 1 + 1
pf✝² : i < n + 1 + 2
pf✝¹ : i < n + 2
pf✝ : a < n + 1
⊢ ((-1) ^ i * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ = -((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

Tactic:
by
  induction x using Quotient.inductionOn with | _ f
  intro hf
  change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)
  rw [PadicSeq.norm_eq_zpow_neg_valuation]
  · rw [Rat.cast_zpow, Rat.cast_natCast]
  · apply CauSeq.not_limZero_of_not_congr_zero
    contrapose hf
    apply Quotient.sound
    simpa using hf

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min ↑x.valuation ↑y.valuation ≤ if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
if_neg hxy,

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
⊢ s.N (unop B.fst).len = s.N (unop A.fst).len

Tactic:
by subst h; rfl

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₁Γ₀.hom.app K =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
by
  change (N₁Γ₀.app K).hom = _
  simp only [N₁Γ₀_app]
  rfl

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
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HigherFacesVanish (n + 1) (((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)))

Tactic:
by
  intro j _
  have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
  rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq; rotate_left
  · intro h
    exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)
  · exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)
  exact eq

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
⊢ IsIso f

Tactic:
let F₂ : SimplicialObject (Karoubi C) ⥤ _ := N₁

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) = 0 ≫ Φ.f j

Tactic:
S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h),

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
⊢ Φ.f (unop A.fst).len ≫ 0 = 0 ≫ Φ.f j
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ Φ.f n ≫ (Y✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ((X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n) ≫ PInfty.f n ≫ Φ.F.app (op ⦋n⦌)

Tactic:
simp only [assoc, PInfty_f_idem_assoc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ Φ.f n ≫ (Y✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n ≫ Φ.F.app (op ⦋n⦌)
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t ∈ {1}
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
· rw [Set.mem_singleton_iff] at ht
      norm_num [ht]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).map f = (Quotient.functor (homRel C)).map g ↔ homRel C f g

Tactic:
rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I

Tactic:
dsimp only [reflTransSymmAux]
  split_ifs
  · constructor
    · apply mul_nonneg <;> grind
    · rw [mul_assoc]
      apply mul_le_one₀ <;> grind
  · constructor
    · apply mul_nonneg <;> grind
    · apply mul_le_one₀ <;> grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject.HoCat C
f g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map f =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map g
⊢ f = g

Tactic:
obtain ⟨Y, rfl⟩ := BifibrantObject.toHoCat_obj_surjective Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ BifibrantObject.toHoCat.obj Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map f =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map g
⊢ f = g