mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ EffectiveEpi f

Tactic:
rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ ∀ (Y_1 : Scheme), Presieve.IsSheafFor (yoneda.obj Y_1) (Presieve.singleton f)
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ EffectiveEpi f

Tactic:
rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]
  intro Z
  exact (GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor _
    (Precoverage.generate_mem_toGrothendieck f.singleton_mem_fppfPrecoverage)

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
⊢ (Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S)

Tactic:
rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
  apply Precoverage.locallyCoverDense_of_map_functorPullback_mem
  intro X R hR
  obtain ⟨R, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve _ H hR
  simpa

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

Goal state before:
pp: S : Scheme
⊢ (ProEt.forget S).LocallyCoverDense (proetaleTopology.over S)

Tactic:
apply MorphismProperty.locallyCoverDense_forget_of_le

Goal state after:
S : Scheme
⊢ proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ φ.app j ≫ c₂.ι.app j ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂

Tactic:
← reassoc_of% hf,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ c₁.ι.app j ≫ f ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x : ↑(Iic j)
k : α
h : k < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ } x
⊢ k ∈ range ⇑{ toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
by simpa using h.le.trans x.2

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 : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)

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 : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
this : (iter₁.trunc ⋯).F = (iter₂.trunc ⋯).F
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
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 : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ j ≤ k₂

Tactic:
by simpa using h₄

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 ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
e' : d.Extension val₀ i
h : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) e.val = e'.val

Tactic:
obtain rfl : e' = e.ofLE h := Subsingleton.elim _ _

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 ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
h : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) e.val = (e.ofLE h).val
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
x✝ : ↑(Set.Iio j)
i : J
hij : i ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone F).ι.app ⟨i, hij⟩ ≫ liftHom hj s ≫ p =
    ((Set.principalSegIio j).cocone F).ι.app ⟨i, hij⟩ ≫ c.ι.app (Opposite.unop (Opposite.op j)) ≫ g

Tactic:
have := (s.1 ⟨i, hij⟩).w₂
    dsimp at this ⊢
    rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
⊢ sq.HasLift

Tactic:
by
  obtain ⟨s, hs⟩ := (wellOrderInductionData c f g hF).surjective { w₂ := sq.w, .. }
  replace hs := congr_arg SqStruct.f' hs
  dsimp at hs
  let t : Cocone F := Cocone.mk X
    { app j := (s.1 ⟨j⟩).f'
      naturality j j' g := by simpa using congr_arg SqStruct.f' (s.2 g.op) }
  let l := hc.desc t
  have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j
  exact ⟨⟨{
    l := l
    fac_left := by rw [hl, hs]
    fac_right := hc.hom_ext (fun j ↦ by rw [reassoc_of% (hl j), SqStruct.w₂])}⟩⟩

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
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ ⋯.choose = largerSubobject hG A

Tactic:
simp [largerSubobject, dif_neg hA]

Goal state after:
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
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) d₁ + multiplicity (↑p) n₂

Tactic:
add_comm,

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₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) n₂ + multiplicity (↑p) d₁
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
padicNorm.eq_zpow_of_nonzero hq

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : q = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
by simp [hq, max_eq_right hnrp]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
add_comm,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p q) (padicNorm p r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)
h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p (r + q + -q)
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
add_neg_cancel_right,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p q
h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n

Tactic:
by_contra h
  rw [padicValNat.eq_zero_of_not_dvd h] at hp
  exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
by
  zify; simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy

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

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!

Tactic:
add_succ,

Goal state after:
case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1

Tactic:
by
  simp [norm_le_one z, nonunits, isUnit_iff]

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

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den = 1
⊢ (Int.padicValuation p) x.num ≤ (Int.padicValuation p) ↑x.den ↔ (Int.padicValuation p) ↑x.den = 1

Tactic:
simp [h, Int.padicValuation_le_one]

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 - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
add_comm,

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

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

Tactic:
sub_add_cancel

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ < ↑p ^ n
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
n : ℕ
x : F.H n
⊢ (map (𝟙 F) n) x = x

Tactic:
simp [H.map_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
n : ℕ
G' : Sheaf J AddCommGrpCat
g : G ⟶ G'
x : F.H n
⊢ (map (f ≫ g) n) x = (map g n) ((map f n) x)

Tactic:
simp [H.map_apply]

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

Goal state before:
pp: case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0

Tactic:
intro H

Goal state after:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ False
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_1
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.fst = 𝟙 c.pt ≫ c.fst

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]

Goal state after:
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
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
rw [h1, h2, max_eq_left (norm_nonneg _)]

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 i : ι
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (i, i) with
      | (i, j) => ⋯.pullback (f j))

Tactic:
apply (hf i).rep.hom_ext' <;>
    simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
⊢ False

Tactic:
have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := fun h ↦ by
    rw [PadicSeq.norm, dif_pos h] at hge
    exact not_lt_of_ge hge hε

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
← add_thirds ε

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

Goal state before:
pp: case neg
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✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)

Tactic:
simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
    rfl

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

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

Tactic:
add_comm,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = ‖y + -x‖
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

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

Tactic:
· simp only [Fin.lt_def]
      dsimp [Fin.natAdd, Fin.cast]
      lia

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

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 = ‖↑k‖

Tactic:
eq_comm

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = 1
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 : ℕ
⊢ P q ≫ P q = P q

Tactic:
by
  ext n
  exact P_f_idem q n

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
eq_comm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z2‖ = ‖z1‖
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]

Tactic:
simp only [add_sub_cancel]

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

Goal state before:
pp: case neg.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X _⦋0 + 1⦌
v : HigherFacesVanish q φ
j : Fin (0 + 1)
hj₁ : 0 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ 0
ha : q + a = 0
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ

pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ

Tactic:
· simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero,
      δ_comp_σ_succ, comp_id]
    rfl

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
⊢ (Q (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
· obtain ⟨a, ha⟩ := Nat.le.dest hqn
      rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
      symm
      conv_rhs => rw [sub_eq_add_neg, add_comm]
      let q' : Fin (n + 1) := ⟨q, Nat.lt_succ_of_le hqn⟩
      rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]
      congr
      · have hnaq' : n = a + q := by lia
        simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]
        rfl
      · ext ⟨i, hi⟩
        simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
        lia

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

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

Tactic:
sub_add_cancel

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ < ↑p ^ n
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ (𝟙 (X _⦋n + 1⦌) ≫ X.σ i) ≫ (P (q + 1)).f (n + 1 + 1) = 0

Tactic:
← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)),

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ (((P q).f n.succ + (Q q).f n.succ) ≫ X.σ i) ≫ (P (q + 1)).f (n + 1 + 1) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → A.fst = Δ

Tactic:
intro h
    dsimp at h
    rw [h]
    rfl

Goal state after: