mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : 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)
this : i₁ (IsLocalRing.closedPoint K) ∈ ⊤
⊢ ⋯.HasLift

Tactic:
rw [← Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx),
    TopologicalSpace.Opens.mem_iSup] at this

Goal state after:
σ : 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)
this : ∃ i, i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
⊢ ⋯.HasLift
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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
intro Z a₁ a₂ g₁ g₂ h
      let A₁ : D := ⟨Over.mk (π a₁), a₁, 𝟙 _, by simp⟩
      let A₂ : D := ⟨Over.mk (π a₂), a₂, 𝟙 _, by simp⟩
      let Z' : D := ⟨Over.mk (g₁ ≫ π a₁), a₁, g₁, rfl⟩
      let i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁)
      let i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂)
      change F.map i₁ ≫ _ = F.map i₂ ≫ _
      simp only [F, A₁, A₂, S.w]

Goal state after:
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

Tactic:
← 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.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₀
⊢ ∀ (b : (data (unop (op (F.obj X₀)))).multicospanShape.R),
    IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f ((data (unop (op (F.obj X₀)))).multicospanShape.fst b)) ≫
        ((data (unop (op (F.obj X₀)))).multicospanIndex G₀.obj).fst b =
      IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f ((data (unop (op (F.obj X₀)))).multicospanShape.snd b)) ≫
        ((data (unop (op (F.obj X₀)))).multicospanIndex G₀.obj).snd b

Tactic:
by
      intro ⟨⟨i, i'⟩, j⟩
      simp [IsDenseSubsite.mapPreimage_comp_map, (data (F.obj X₀)).w j]

Goal state after:
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.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
X : S.ProEt
inst✝ : IsEmpty ↥X.left
⊢ ⊥ ∈ (topology S) X

Tactic:
by
  rw [topology, ← Sieve.generate_bot]
  refine Precoverage.generate_mem_toGrothendieck ?_
  simp [precoverage, proetalePrecoverage, bot_mem_propQCPrecoverage]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
obtain ⟨h⟩ := hdisj h a b hab
      have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
      exact Subsingleton.elim _ _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso ((kernel.ι (g y)).app j)
⊢ ∃ j φ, y ≫ Y.map φ = 0

Tactic:
refine ⟨j.right, j.hom, ?_⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso ((kernel.ι (g y)).app j)
⊢ y ≫ Y.map j.hom = 0
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f → Arrow.mk f = Φ.toSuccArrow X

Tactic:
rintro ⟨_⟩
    rfl

Goal state after:
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)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
φ : FunctorObjIndex f πX →
  (i : Shrink.{t, w} I) × Shrink.{t, v} ((A ((equivShrink I).symm i) ⟶ X) × (B ((equivShrink I).symm i) ⟶ S)) :=
  fun x ↦
    ⟨(equivShrink I) x.i,
      (equivShrink
          ((A ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ X) × (B ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b)⟩
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w✝¹ : t₁ ≫ πX = f i₁ ≫ b₁
i₂ : I
t₂ : A i₂ ⟶ X
b₂ : B i₂ ⟶ S
w✝ : t₂ ≫ πX = f i₂ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w✝¹ } = φ { i := i₂, t := t₂, b := b₂, w := w✝ }
⊢ i₁ = i₂

Tactic:
by simpa [φ] using congr_arg Sigma.fst h

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₁ iter₂ : Φ.Iteration j
⊢ iter₁ = iter₂

Tactic:
by
    suffices iter₁.F = iter₂.F by aesop
    revert iter₁ iter₂
    induction j using SuccOrder.limitRecOn with
    | isMin j h =>
      obtain rfl := h.eq_bot
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      obtain rfl : k₂ = ⊥ := by simpa using h₂
      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
      apply mapEq_refl _ _ (by simp only [obj_bot])
    | succ j hj₁ hj₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      have h₀ := Order.le_succ j
      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
      dsimp at hj₂ hsucc
      wlog h : k₂ ≤ j generalizing k₁ k₂
      · obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
    | isSuccLimit j h₁ h₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ padicValNat p p = 1

Tactic:
rw [padicValNat_def (@Fact.out p.Prime).ne_zero]
  simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) =
    ↑(multiplicity (↑p) c) + ↑(multiplicity (↑p) q.num) - (↑(multiplicity (↑p) c) + ↑(multiplicity p q.den))

Tactic:
ring

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

Tactic:
ring

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False

Tactic:
if_neg hq

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

Tactic:
norm_cast at hz

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ n ≤ padicValNat p a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
or_iff_right ha

Goal state after:
case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ n ≤ padicValNat p a ↔ n ≤ padicValNat p a
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.add_sub_assoc <|
      digit_sum_le p 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.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, ‖↑x' k - ↑(const norm x'.lim) j‖ < ↑p ^ (-↑n)
hin : n < i
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

Tactic:
specialize hi i le_rfl i le_rfl

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ‖↑x' i - ↑(const norm x'.lim) i‖ < ↑p ^ (-↑n)
hin : n < i
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)
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
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.lift' i h hi ≫ hf'.snd g = h

Tactic:
by
  simp [lift']

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
i : ι
W Y : S.Etale
a : α
p : W ⟶ T a
y : { obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.obj W
hi :
  (s i) default =
    X.hom
      ((Over.Hom.left
          ((ConcreteCategory.hom ({ obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.map (p ≫ f a))) y))
        default)
⊢ ∃ i_1 y_1,
    (f i_1).left y_1 =
      (Over.Hom.left
          ((ConcreteCategory.hom ({ obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.map (p ≫ f a))) y))
        default

Tactic:
exact ⟨a, (pointSmallEtaleFiberObjToPreimage (s i) hi (y ≫ p.hom)).1, rfl⟩

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

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

Tactic:
refine (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ ?_

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
⊢ padicNormE (↑f i - ↑(limSeq f i)) < ε
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 : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij ↦ hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
rw [eq]

Goal state after:
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 : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij ↦ hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij ↦ hσ' q i j hij).f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (lim f - ↑(↑(lim' f) i)) < ε / 2

Tactic:
apply hN2 _ (le_of_max_le_right hi)

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)) ⋯ ≫ pbIso.hom ≫ pbIso.inv)

Tactic:
← Category.assoc

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)) ⋯ ≫ pbIso.hom) ≫ pbIso.inv)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
ring

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n + 1 ≤ q
⊢ (P (q + 1)).f (n + 1) = (P q).f (n + 1)

Tactic:
simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      add_eq_left]
    exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

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

Goal state before:
pp: case a.e_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) = -((-1) ^ a * (-1) ^ i)

Tactic:
ring

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
PadicSeq.val_eq_iff_norm_eq hf hg

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.norm f = PadicSeq.norm g
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.σ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ (P (q + 1)).f (0 + 1) = 0

Tactic:
rw [show q = 0 by lia]

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.σ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ (P (0 + 1)).f (0 + 1) = 0