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

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
use i₀, φ', IsLocalization.Away.lift_comp ..

Goal state after:
case right
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := ⋯
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := ⋯
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := ⋯
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
⊢ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallySurjective J f
X : C
z : ToType (Q.obj (op X))
Y : C
g : Y ⟶ unop (op X)
t : ToType (P.obj (op Y))
ht : (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (Q.map g.op)) z
y : Φ.fiber.obj Y
⊢ (ConcreteCategory.hom (Φ.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.toPresheafFiber Y y P)) t) =
    (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) Q)) z

Tactic:
by simp [← toPresheafFiber_w, ← ht]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₁.op = restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₂.op

Tactic:
restriction.res_eq_res data G₀ _ h₁,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op = restriction.res data G₀ ⋯.some ≫ G₀.obj.map p₂.op
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
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
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₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
h1 : ∃ a g, g ≫ π a = T.hom
h2 : ∃ g, g ≫ π h1.choose = T.hom
⊢ g ≫ π a = h2.choose ≫ π h1.choose

Tactic:
h2.choose_spec

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
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
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₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
h1 : ∃ a g, g ≫ π a = T.hom
h2 : ∃ g, g ≫ π h1.choose = T.hom
⊢ g ≫ π a = T.hom
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := g }

Tactic:
by
  rw [uliftYonedaEquiv_naturality, uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]

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

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ∃ j, IsIso (F.obj j).obj.hom

Tactic:
refine ⟨IsCardinalFiltered.max σ hs, ?_⟩

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ IsIso (F.obj (IsCardinalFiltered.max σ hs)).obj.hom
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯ ≫ homOfLE ⋯))

Tactic:
hf.F.map_comp

Goal state after:
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯) ≫ hf.F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

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

Tactic:
← Φ.prop.arrow_mk_mem_toSet_iff,

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Arrow.mk f ∈ Φ.prop.toSet
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
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
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift j hj
              ⟨fun x ↦
                match x with
                | op ⟨i, hi⟩ => (e i hi).val,
                ⋯⟩),
        ⋯⟩

pp: case inr
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 hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift i hj
        ⟨fun x ↦
          match x with
          | op ⟨i_1, hi⟩ => (e i_1 hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift i hj
              ⟨fun x ↦
                match x with
                | op ⟨i_1, hi⟩ => (e i_1 hi).val,
                ⋯⟩),
        ⋯⟩

Tactic:
· have := (e i hij').map_limit i hi (by rfl)
      dsimp at this ⊢
      rw [map_id, id_apply] at this
      rw [d.map_lift _ _ _ _ hij']
      dsimp
      rw [this]
      congr
      ext ⟨⟨l, hl⟩⟩
      rw [map_lift _ _ _ _ _ (hl.trans hij')]
      apply compatibility

Goal state after:
case inr
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 hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift i hj
        ⟨fun x ↦
          match x with
          | op ⟨i_1, hi⟩ => (e i_1 hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift i hj
              ⟨fun x ↦
                match x with
                | op ⟨i_1, hi⟩ => (e i_1 hi).val,
                ⋯⟩),
        ⋯⟩
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
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1

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
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts

Tactic:
refine le_antisymm ?_
    (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.ord.ToType)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p < 1

Tactic:
padicNorm_p hp,

Goal state after:
p : ℕ
hp : 1 < p
⊢ (↑p)⁻¹ < 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ ↑p ∣ ↑m

Tactic:
← int_lt_one_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ padicNorm p ↑↑m < 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

Tactic:
· rw [padicValNat_dvd_iff_le_of_ne_one hp ha, or_iff_right ha]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ 0 = 0 * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 = 0 * exp (-padicValRat p y✝)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ 0 = exp (-padicValRat p x✝) * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 = exp (-padicValRat p x✝) * exp (-padicValRat p y✝)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = 0 * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = 0 * exp (-padicValRat p y✝)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = exp (-padicValRat p x✝) * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = exp (-padicValRat p x✝) * exp (-padicValRat p y✝)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ p ∣ 1

Tactic:
← r.reduced.gcd_eq_one,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den
⊢ p ∣ r.num.natAbs.gcd r.den
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f.norm = 0 → f ≈ 0

Tactic:
intro h
    by_contra hf
    unfold norm at h
    split_ifs at h
    apply hf
    intro ε hε
    exists stationaryPoint hf
    intro j hj
    have heq := stationaryPoint_spec hf le_rfl hj
    simpa [h, heq]

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
set a := x * (p : ℚ_[p]) ^ n with ha

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1
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
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
⊢ ∃ W h, h ≫ ⟨f, hf✝⟩ = h ≫ ⟨g, hg⟩

Tactic:
let h' := (Types.equalizerLimit (g := F.map f) (h := F.map g)).isLimit

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
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
h' : IsLimit Types.equalizerLimit.cone := Types.equalizerLimit.isLimit
⊢ ∃ W h, h ≫ ⟨f, hf✝⟩ = h ≫ ⟨g, hg⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f * g).norm = f.norm * g.norm

Tactic:
exact if hf : f ≈ 0 then by
    have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
    simp only [hf, hg, norm, dif_pos, zero_mul]
  else
    if hg : g ≈ 0 then by
      have hf : f * g ≈ 0 := mul_equiv_zero _ hg
      simp only [hf, hg, norm, dif_pos, mul_zero]
    else by
      unfold norm
      have hfg := mul_not_equiv_zero hf hg
      simp only [hfg, hf, hg, dite_false]
      -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
      rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
      apply padicNorm.mul

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
h : F.relativelyRepresentable (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)] at h

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
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)

Tactic:
← norm_p_zpow,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ‖↑p ^ ↑n‖
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
a✝ : Mono A.e
⊢ A.EqId

Tactic:
rw [eqId_iff_len_le]

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
a✝ : Mono A.e
⊢ (unop Δ).len ≤ (unop A.fst).len
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : c.Rel i j
⊢ P.p.f i ≫ P.X.d i j = (P.p.f i ≫ P.X.d i j) ≫ P.p.f j

Tactic:
simp only [HomologicalComplex.Hom.comm, assoc, HomologicalComplex.p_idem]

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False

Tactic:
replace h := congr_arg SimplexCategory.len h

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌.len = ⦋n⦌.len
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

Tactic:
intro B _ h₂
    rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ h₂, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False

Tactic:
rw [← h] at h₁

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋n⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False