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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
X : C
R : Presieve X
⊢ R ∈ ((fun P ↦ P.precoverage) ((fun K ↦ K.preZeroHypercoverFamily) K)).coverings X ↔ R ∈ K.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ ((fun P ↦ P.precoverage) ((fun K ↦ K.preZeroHypercoverFamily) K)).coverings X ↔
    E.presieve₀ ∈ K.coverings X
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
R S : Presieve X
hR : R ∈ P.precoverage.coverings X
hS : S ∈ P.precoverage.coverings X
⊢ R ⊔ S ∈ P.precoverage.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
S : Presieve X
hS : S ∈ P.precoverage.coverings X
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ S ∈ P.precoverage.coverings X
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone transfiniteCompositions.{w, v, u}

Tactic:
intro W₁ W₂ h X Y f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨J, _, _, _, _, hf⟩ := hf
  exact transfiniteCompositionsOfShape_le_transfiniteCompositions _ _ _
    (transfiniteCompositionsOfShape_monotone J h _ hf)

Goal state after:
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)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
⊢ e₁.val = e₂.val

Tactic:
have h₂ := e₂.map_limit i hi (by rfl)

Goal state after:
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)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
h₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val,
        ⋯⟩
⊢ e₁.val = e₂.val
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
z : ℤ
⊢ p = 1 ∨ z = 0 ∨ ¬p ∣ z.natAbs ↔ p = 1 ∨ z = 0 ∨ ¬↑p ∣ z

Tactic:
← Int.ofNat_dvd_left

Goal state after:
p : ℕ
z : ℤ
⊢ p = 1 ∨ z = 0 ∨ ¬↑p ∣ z ↔ p = 1 ∨ z = 0 ∨ ¬↑p ∣ z
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
⊢ ∀ (f : X ⟶ Y), (generatingMonomorphisms G).rlp f → (monomorphisms C).rlp f

Tactic:
p

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
⊢ (generatingMonomorphisms G).rlp p → (monomorphisms C).rlp p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
ne : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-padicValRat p✝ ↑q)) = 1

Tactic:
p

Goal state after:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
ne : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case coe.ofAdd
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯, map_one' := ⋯,
          map_mul' := ⋯ }
        a =
      ↑(Multiplicative.ofAdd x)

Tactic:
MonoidWithZeroHom.coe_mk

Goal state after:
case coe.ofAdd
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)

Tactic:
have : padicNorm p (f n - f m) < ε := hN2 _ (max_le_iff.1 hn).2 _ (max_le_iff.1 hm).2
    have : padicNorm p (f n - f m) < padicNorm p (f n) :=
      lt_of_lt_of_le this <| hN1 _ (max_le_iff.1 hn).1
    have : padicNorm p (f n - f m) < max (padicNorm p (f n)) (padicNorm p (f m)) :=
      lt_max_iff.2 (Or.inl this)
    by_contra hne
    rw [← padicNorm.neg (f m)] at hne
    have hnam := add_eq_max_of_ne hne
    rw [padicNorm.neg, max_comm] at hnam
    rw [← hnam, sub_eq_add_neg, add_comm] at this
    apply _root_.lt_irrefl _ this

Goal state after:
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
f : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hg : (ConcreteCategory.hom (F.map g)) x = y
⊢ ∃ W h, h ≫ ⟨f, hf⟩ = h ≫ ⟨g, hg⟩

Tactic:
← hg

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
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
⊢ ∃ W h, h ≫ ⟨f, hf✝⟩ = h ≫ ⟨g, hg⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑f j) < ε

Tactic:
intro n

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
⊢ n ≥ stationaryPoint hf → padicNorm p (↑f n) < ε
Module: Mathlib.CategoryTheory.Limits.EpiMono

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

Tactic:
rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id]

Goal state after:
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 (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 (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 - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) - padicNorm p (↑g (stationaryPoint hg))
⊢ False

Tactic:
lift_index_right hg N (stationaryPoint hf)

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' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ False
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
φ : c.pt ⟶ Z
h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ
⊢ c.inl ≫ φ = c.inr ≫ φ
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: case refine_2
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
⊢ (TopCat.Hom.hom (X.fromSpecResidueField x).base) ((TopCat.Hom.hom (Spec.map (CommRingCat.ofHom ↑b)).base) default) = x

Tactic:
apply fromSpecResidueField_apply

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
⊢ ∀ (i : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).Elements),
    ∃ j,
      (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
        Nonempty (j ⟶ i)

Tactic:
rintro ⟨X, x⟩

Goal state after:
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
x : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ j,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
      Nonempty (j ⟶ ⟨X, 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.fst' f' = hf'.snd g

Tactic:
simp [symmetry]

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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g

Tactic:
simp [symmetry]

Goal state after:
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
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Tactic:
ext Y'
  simp [equivalence₂, equivalence₁CounitIso_eq]

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

Goal state before:
pp: case refine_2
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
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ Arrow.mk snd ≅ Arrow.mk g_snd

Tactic:
exact Arrow.isoMk (F.preimageIso (h.isoIsPullback X (F.obj a) BC)) (Iso.refl _)
      (F.map_injective (by simp))

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 : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (a ≫ (glueData hf).openCover.f i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
⊢ a ≫ (glueData hf).openCover.f i = γ ≫ β

Tactic:
← fac₂

Goal state after:
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 : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (a ≫ (glueData hf).openCover.f i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (b ≫ (glueData hf).openCover.f j)
⊢ a ≫ (glueData hf).openCover.f i = b ≫ (glueData hf).openCover.f j
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
  unfold Hσ
  have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
  simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
  rw [eq]
  let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm
  congr

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:
have hε3 : 0 < ε / 3 := div_pos hε (by simp)
  let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
  let ⟨N2, hN2⟩ := f.cauchy₂ hε3
  exists max N N2
  intro j hj
  suffices
    padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
    ring_nf at this
    rw [← padicNormE.eq_padic_norm']
    exact mod_cast this
  apply lt_of_le_of_lt
  · apply padicNormE.add_le
  · rw [← add_thirds ε]
    apply _root_.add_lt_add
    · 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 _ _)
    · apply mod_cast hN (max N N2)
      apply le_max_left

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ padicNorm p { num := n, den := d, den_nz := hn, reduced := hd } ≤ 1

Tactic:
rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
        padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ (↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num)⁻¹ ≤ 1
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ ((-1) ^ ↑0 • X.δ 0 + (-1) ^ ↑1 • X.δ 1) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ((-1) ^ ↑0 • X.δ 0 + ∑ i, (-1) ^ ↑i.succ • X.δ i.succ)) =
    0

Tactic:
Fin.sum_univ_two

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ ((-1) ^ ↑0 • X.δ 0 + (-1) ^ ↑1 • X.δ 1) ≫ (1 • X.σ 0) +
        X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            (-1 • X.σ 1) ≫
              ((-1) ^ ↑0 • X.δ 0 +
                ((-1) ^ ↑(Fin.succ 0) • X.δ (Fin.succ 0) + (-1) ^ ↑(Fin.succ 1) • X.δ (Fin.succ 1)))) =
    0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
r✝ : ℚ
⊢ (Valuation.comap (Rat.castHom ℚ_[p]) mulValuation) r✝ = (Rat.padicValuation p) r✝

Tactic:
simp [Rat.padicValuation]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
⊢ ∀ (n : ℕ), S₁.s.φ F₁ n = S₁.s.φ F₂ n

Tactic:
intro n

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
n : ℕ
⊢ S₁.s.φ F₁ n = S₁.s.φ F₂ n
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
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty

Tactic:
ext n
  dsimp [N₂Γ₂ToKaroubiIso]
  simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]
  convert! comp_id _
  apply (Γ₀.splitting X).hom_ext'
  intro A
  rw [Splitting.ι_desc]
  erw [comp_id, id_comp]

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
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
⊢ ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))

Tactic:
intro n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
n : ℕ
⊢ IsIso (f.app (op ⦋n⦌))
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✝ : Preadditive C
n : ℕ
⊢ (𝟙 (X _⦋n⦌) - PInfty.f n) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0

Tactic:
← comp_PInfty_eq_zero_iff,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ (𝟙 (X _⦋n⦌) - PInfty.f n) ≫ PInfty.f n = 0
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = G

Tactic:
obtain ⟨Gpre, Gid⟩ := G

Goal state after:
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
Fpre : V ⥤q W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : V ⥤q W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid }.obj X = { toPrefunctor := Gpre, map_id := Gid }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid }.map f = Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid }.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid } = { toPrefunctor := Gpre, map_id := Gid }
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : ReflQuiver U
inst✝ : ReflQuiver V
F G : U ⥤rq V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
by
  subst e
  simp

Goal state after: