mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ IsUnit ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) ^ n)

Tactic:
let z : Away 𝒜 x := Away.mk 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) (d + e)
        (g ^ e * f ^ (2 * e + d)) <| by
      convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
      ring

Goal state after:
case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ IsUnit ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) ^ n)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d))) (⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩) = 1

Tactic:
← Localization.mk_one,

Goal state after:
case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d))) (⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩) = Localization.mk 1 1
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
⊢ (ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))).ker =
    (ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))).range

Tactic:
by simp [Finsupp.range_linearCombination, ht]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso (modulesSpecToSheaf.map M.fromTildeΓ)

Tactic:
refine isLocalizing_of_isIso_app_top ?_ (isLocalizing_tilde _) h

Goal state after:
case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso ((modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op ⊤))
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
s : Cone F
m : s.pt ⟶ (liftedCone F).pt
h : ∀ (j : I), m ≫ (liftedCone F).π.app j = s.π.app j
i : I
⊢ ↑m ≫ limit.π (F ⋙ π A) i = ↑⟨limit.lift (F ⋙ π A) ((π A).mapCone s), ⋯⟩ ≫ limit.π (F ⋙ π A) i

Tactic:
simpa using congrArg Subtype.val (h i)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F : Cᵒᵖ ⥤ A
f : freeYoneda X M ⟶ F
⊢ (fun g ↦ { app := fun Y ↦ Sigma.desc fun φ ↦ g ≫ F.map (Quiver.Hom.op φ), naturality := ⋯ })
      ((fun f ↦ Sigma.ι (fun i ↦ M) (𝟙 (unop (op X))) ≫ f.app (op X)) f) =
    f

Tactic:
ext Y
    refine Sigma.hom_ext _ _ (fun φ ↦ ?_)
    simpa using (Sigma.ι _ (𝟙 _) ≫= f.naturality φ.op).symm

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

Goal state before:
pp: case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{v_3, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant J ((sheafEquiv J K G D).inverse.obj F) → IsConstant K F

pp: case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{v_3, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant K F → IsConstant J ((sheafEquiv J K G D).inverse.obj F)

Tactic:
· exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant J D K G hT hT').symm.app _ ≪≫
      (sheafEquiv J K G D).functor.mapIso i ≪≫ (sheafEquiv J K G D).counitIso.app _⟩⟩

Goal state after:
case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{v_3, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant K F → IsConstant J ((sheafEquiv J K G D).inverse.obj F)
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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ res data G₀ h₁ = res data G₀ h₂

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F h₁.q)
      (IsDenseSubsite.imageSieve_mem J₀ J F h₂.q)⟩ _ _ ?_
  rintro ⟨Z₀, a, ⟨b₁, w₁⟩, ⟨b₂, w₂⟩⟩
  refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, (data X).mem₁₀ h₁.i₀ h₂.i₀ b₁ b₂ (by rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac])⟩ _ _ ?_
  rintro ⟨W₀, c, hc⟩
  dsimp [res]
  simp only [assoc, IsDenseSubsite.mapPreimage_comp_map]
  apply presheafObj_mapPreimage_condition
  simp

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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.bind (Sieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀)).arrows fun Y₀ a ha ↦
            Sieve.functorPullback F
              (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                (data Y).toPreOneHypercover.sieve₀),
          ⋯⟩),
    (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map I.f.op =
      restriction data G₀ (f ≫ g) ≫ G₀.obj.map I.f.op

Tactic:
rintro ⟨U₀, _, Y₀, c, d, hd, hc, rfl⟩

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
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : (Sieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀)).arrows d
hc :
  ((fun Y₀ a ha ↦
          Sieve.functorPullback F
            (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
              (data Y).toPreOneHypercover.sieve₀))
        Y₀ d hd).arrows
    c
⊢ (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_1
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (yoneda.obj X)

Tactic:
exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

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

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf TopCat.grothendieckTopology (yoneda.obj (TopCat.of (ULift.{u_1, v} T)))

Tactic:
exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

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
⊢ ∃ j φ, y ≫ Y.map φ = 0

Tactic:
by
  have := isFiltered_of_isCardinalFiltered J κ
  obtain ⟨j, h⟩ := exists_isIso_of_functor_from_monoOver (F y) hXκ _
      (colimit.isColimit (kernel (g y))) (f y) (fun j ↦ by simpa using! hf y j)
      (epi_f hc hy)
  dsimp at h
  refine ⟨j.right, j.hom, ?_⟩
  simpa only [← cancel_epi ((kernel.ι (g y)).app j), comp_zero]
    using! NatTrans.congr_app (kernel.condition (g y)) j

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝ : J
h : x✝ < ⊥
⊢ arrowSucc ((Functor.const ↑(Set.Iic ⊥)).obj Φ.X₀) x✝ h =
    Φ.toSuccArrow (((Functor.const ↑(Set.Iic ⊥)).obj Φ.X₀).obj ⟨x✝, ⋯⟩)

Tactic:
by simp at h

Goal state after:
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 ⋯) ⋯
⊢ IsColimit ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))

Tactic:
refine (IsColimit.precomposeInvEquiv e _).1 ?_

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 ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ IsColimit ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J)))
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
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✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ functorMap f (τ ≫ τ') = functorMap f τ ≫ functorMap f τ'

Tactic:
simp only [functorMap, Arrow.comp_left, Arrow.mk_left]

Goal state after:
case h₁
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✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
      (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ')) (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ =
    pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom)
        (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ ≫
      pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
        (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯
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
⊢ Nonempty (d.Extension val₀ j)

Tactic:
by
  induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩
  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩

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 ?m.86) - ↑(multiplicity ↑p ?m.87) + padicValRat p r

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
⊢ q.num /. ↑q.den = ?m.86 /. ?m.87

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
⊢ ℤ

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
⊢ ℤ

Tactic:
← r.num_divInt_den,

Goal state after:
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 ?m.86) - ↑(multiplicity ↑p ?m.87) + padicValRat p (r.num /. ↑r.den)

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
⊢ q.num /. ↑q.den = ?m.86 /. ?m.87

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
⊢ ℤ

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
⊢ ℤ
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
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (ofHoms (generatingMonomorphisms G).homFamily)).pushouts (hf.F.map (homOfLE ⋯))
⊢ monomorphisms C (hf.F.map (homOfLE ⋯))

Tactic:
simp only [ofHoms_homFamily] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ monomorphisms C (hf.F.map (homOfLE ⋯))
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
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
simpa [hq] using h

Goal state after:
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
hr : r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
simp [hr, max_eq_left hnqp]

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.num /. ↑q.den) ≤ 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:
← r.num_divInt_den,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (r.num /. ↑r.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.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ padicValRat p (↑p ^ r)⁻¹ = -↑r

Tactic:
padicValRat.inv,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ -padicValRat p (↑p ^ r) = -↑r
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p

Tactic:
exact mod_cast hp.1.pos

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
by_cases hx : x = 0
  · subst hx
    simp only [norm_zero, zpow_neg, zpow_natCast, inv_nonneg, iff_true, Submodule.zero_mem]
    exact mod_cast Nat.zero_le _
  rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]

Goal state after:
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
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f (stationaryPoint hf)) < ε

Tactic:
simpa [H] using hε

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

Goal state before:
pp: case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
R : CommRingCat
j : Spec (CommRingCat.of ↑R) ⟶ Y
w✝ : IsOpenImmersion j
y' : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ↑R)
hy : (y' ≫ j) ≫ f = s
⊢ ∃ j_1,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j_1 ∧
      Nonempty (j_1 ⟶ ⟨Etale.mk f, Over.homMk (y' ≫ j) ⋯⟩)

Tactic:
exact ⟨_,
        ⟨Functor.elementsMk _ (AffineEtale.mk (j ≫ f)) (Over.homMk y'), ⟨Iso.refl _⟩⟩,
        ⟨⟨MorphismProperty.Over.homMk j rfl (by simp), by cat_disch⟩⟩⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map t)) v = u

Tactic:
refine (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv.injective ?_
    dsimp [-Functor.comp_obj]
    trans (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w}.obj U)) (shrinkYonedaObjObjEquiv.symm t)
    · rw [← Φ.obj.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app]
      exact Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality_apply t v
    · rw [← hx₁]
      refine Eq.trans (congr_arg _ ht)
        (Φ.obj.toPresheafFiber_naturality_apply f _ v y).symm

Goal state after:
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
⊢ (f + g).norm = max f.norm g.norm

Tactic:
by
      unfold norm at hfgne ⊢; split_ifs at hfgne ⊢
      -- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
      rw [lift_index_left hf, lift_index_right hg] at hfgne
      · rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
        exact padicNorm.add_eq_max_of_ne hfgne

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)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : yoneda.map a ≫ f i = yoneda.map b ≫ f j
| b ≫ toGlued hf j

Tactic:
← (hf i).rep.lift'_snd a b h,

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)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : yoneda.map a ≫ f i = yoneda.map b ≫ f j
| (⋯.lift' a b h ≫ ⋯.snd (f j)) ≫ toGlued hf j
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ hσ' q n m hnm = 0

Tactic:
by
  simp only [hσ', hσ]
  split_ifs
  exact zero_comp

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ X.δ 0 + -𝟙 (X _⦋0⦌) = 0

Tactic:
δ_comp_σ_self' X (Fin.castSucc_zero.symm)

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X _⦋0⦌) + -𝟙 (X _⦋0⦌) = 0