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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
⊢ Over.Hom.left q ≫ ⋯.choose ≫ e ⋯.choose = (⋯.choose ≫ e ⋯.choose) ≫ 𝟙 W

Tactic:
rw [Category.comp_id, ← Category.assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ ⋯.choose) ≫ e ⋯.choose = ⋯.choose ≫ e ⋯.choose
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case refine_2
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
⊢ (Spec.map (CommRingCat.ofHom φ'') ≫ awayι 𝒜 ↑i₀ ⋯ ⋯) ≫ toSpecZero 𝒜 =
    { R := O, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K, field := field✝,
        algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂, commSq := w }.i₂

Tactic:
· simp only [Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]
    conv_rhs => rw [← Spec.map_preimage i₂]
    congr 1
    ext x
    apply IsFractionRing.injective O K
    refine (DFunLike.congr_fun hφ'' (fromZeroRingHom 𝒜 _ _)).trans ?_
    simp only [RingHom.coe_comp, Function.comp_apply]
    rw [awayMap_fromZeroRingHom, ← awayMap_fromZeroRingHom 𝒜 (hxd i₀ i₀.2) rfl,
      ← RingHom.comp_apply, hφ]
    exact congr($(H.symm) x)

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
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) = presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv

Tactic:
apply presheafObj_hom_ext

Goal state after:
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
i : (data X).I₀
⊢ ∀ (i_1 : (data (F.obj ((data X).X i))).I₀),
    presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) i_1 =
      (presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv) ≫
        presheafObjπ data G₀ (F.obj ((data X).X i)) i_1
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₀ Y₀ : C₀
f : X₀ ⟶ Y₀
⊢ G₀.obj.map f.op ≫ (presheafObjObjIso data G₀ X₀).inv =
    (presheafObjObjIso data G₀ Y₀).inv ≫ presheafMap data G₀ (F.map f)

Tactic:
apply presheafObj_hom_ext

Goal state after:
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₀ Y₀ : C₀
f : X₀ ⟶ Y₀
⊢ ∀ (i : (data (unop (op (F.obj X₀)))).I₀),
    (G₀.obj.map f.op ≫ (presheafObjObjIso data G₀ X₀).inv) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i =
      ((presheafObjObjIso data G₀ Y₀).inv ≫ presheafMap data G₀ (F.map f)) ≫
        presheafObjπ data G₀ (unop (op (F.obj X₀))) i
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
⊢ (x₂ ≫ r) ≫ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.g = 0

Tactic:
by
    simpa [hz] using hx₂.symm =≫ cokernel.map _ _ _ _ sq.w

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
⊢ j < i ↔ j ≤ cases 0 castSucc i

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (by simpa using! hi)

Goal state after:
n : ℕ
j : Fin (n + 1)
i : Fin n
hi : ¬IsMin i.succ
⊢ j < i.succ ↔ j ≤ cases 0 castSucc i.succ
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
by
    rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
      (orderIsoShrink.{w'} J)]
    infer_instance

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

Goal state before:
pp: 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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
k : J
hk : k ∈ Set.Iio i
⊢ (colimit.cocone (restrictionLT iter.F hij)).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom = (coconeOfLE iter.F hij).ι.app ⟨k, hk⟩

Tactic:
apply Arrow.mk_injective

Goal state after:
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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk ((colimit.cocone (restrictionLT iter.F hij)).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom) =
    Arrow.mk ((coconeOfLE iter.F hij).ι.app ⟨k, hk⟩)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ (⋯.functor ⋙ Φ.iterationFunctor J).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (restrictionLT (Φ.iter i).F ⋯).map f

Tactic:
apply Arrow.mk_injective

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ Arrow.mk ((⋯.functor ⋙ Φ.iterationFunctor J).map f ≫ (eqToIso ⋯).hom) =
    Arrow.mk ((eqToIso ⋯).hom ≫ (restrictionLT (Φ.iter i).F ⋯).map f)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ (coconeOfLE (Φ.iter i).F ⋯).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom =
    ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))).ι.app ⟨k, hk⟩

Tactic:
apply Arrow.mk_injective

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk ((coconeOfLE (Φ.iter i).F ⋯).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom) =
    Arrow.mk (((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))).ι.app ⟨k, hk⟩)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
⊢ Subsingleton (d.Extension val₀ i)

Tactic:
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
    have h₁ := e₁.map_limit i hi (by rfl)
    have h₂ := e₂.map_limit i hi (by rfl)
    simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂
    rw [h₁, h₂]
    congr
    ext ⟨⟨l, hl⟩⟩
    have := hi' l hl
    exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (monomorphisms C).HasFunctorialFactorization (monomorphisms C).rlp

Tactic:
have hG := isSeparator_separator C

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator (separator C)
⊢ (monomorphisms C).HasFunctorialFactorization (monomorphisms C).rlp
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)

Tactic:
exact hF _ (lt_trans hi (lt_add_one _))

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

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

Tactic:
by_cases dvd : p ∣ a
  · 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)
  · rw [padicValNat.eq_zero_of_not_dvd dvd]
    lia

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
t : ℕ
⊢ t ∈ Finset.image (fun x ↦ p ^ x) (Finset.range (padicValNat p n + 1)) → t ∈ n.divisors

Tactic:
ht

Goal state after:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x ↦ p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ n.divisors
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
⊢ t ∈ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) → t ∈ n.divisors.erase 1

Tactic:
ht

Goal state after:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ n.divisors.erase 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]

Tactic:
Ideal.span_le,

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ {↑p} ⊆ ↑(maximalIdeal ℤ_[p])
Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology

Goal state before:
pp: X : Scheme
ℓ : ℕ
inst✝¹ : Fact (Nat.Prime ℓ)
inst✝ : IsEmpty ↥X
n : ℕ
⊢ Subsingleton (X.EllAdicCohomology ℓ n)

Tactic:
by
  apply Sheaf.subsingleton_H_of_isZero
  exact Functor.map_isZero _ (isZero_ellAdicSheaf_of_isEmpty _ _)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ f.norm = g.norm

Tactic:
rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]

Goal state after:
case ha₀
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ 0 < ↑p

case ha₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ↑p ≠ 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f i + -↑g i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False

Tactic:
add_eq_max_of_ne hpne,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  max (padicNorm p (↑f i)) (padicNorm p (-↑g i)) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)

Tactic:
· simpa only [sub_zero, add_sub_cancel_right] using 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
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
pbIso : Limits.pullback ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit (pair a a)) :=
  pullback.congrHom ⋯ ⋯ ≪≫
    (prodIsoPullback (F.obj a) (F.obj a)).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp a a F)).symm ≪≫ (preservesLimitIso F (pair a a)).symm
⊢ F.relativelyRepresentable (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯)

Tactic:
← comp_id (pullback.lift _ _),

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

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

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]

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

Goal state before:
pp: case hf.hj₁
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
⊢ (Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)).pred ⋯ ≠ 0

Tactic:
intro h
      replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
      lia

Goal state after:
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:
← Fin.succ_mk (n + 1) a ‹_›,

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.σ ⟨a, pf✝⟩.succ ≫ X.δ ⟨i, pf✝²⟩ +
      ((-1) ^ a * (-1) ^ i) • φ ≫ X.δ ⟨i, pf✝¹⟩ ≫ X.σ ⟨a, pf✝⟩ =
    0
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, ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ +
      ∑ i, ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ =
    0

Tactic:
rw [← Finset.sum_add_distrib]
    apply Finset.sum_eq_zero
    rintro ⟨i, hi⟩ _
    simp only
    have hia : (⟨i, by lia⟩ : Fin (n + 2)) ≤
        Fin.castSucc (⟨a, by lia⟩ : Fin (n + 1)) := by
      rw [Fin.le_iff_val_le_val]
      dsimp
      lia
    generalize_proofs
    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]
    congr 2
    ring

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

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

Tactic:
Fin.sum_univ_succ,

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ X.σ 0 ≫ ((-1) ^ ↑0 • X.δ 0) + ∑ i, φ ≫ X.σ 0 ≫ ((-1) ^ ↑i.succ • X.δ i.succ) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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

Tactic:
Fin.sum_univ_succ,

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