mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {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 := ⋯ }
a : α
⊢ π a ≫ m = S.ι.app { obj := Over.mk (π a), property := ⋯ }

Tactic:
exact hm ⟨Over.mk (π a), a, 𝟙 _, by simp⟩

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

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

Tactic:
← Sieve.effectiveEpimorphic_singleton,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ (Presieve.singleton f).EffectiveEpimorphic
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:
← Sieve.effectiveEpimorphic_singleton,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ (Presieve.singleton f).EffectiveEpimorphic
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₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ F.map c ≫ F.map b = F.map c ≫ F.map a ≫ f

Tactic:
fac₁

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₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ F.map c ≫ F.map a ≫ f = F.map c ≫ F.map a ≫ 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₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map b) = IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f)

Tactic:
fac₁

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₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f) = IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ F.map a ≫ f)
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r ≫ k = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0

Tactic:
fac₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝² : Small.{u, u_1} α
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : Shrink.{u, u_1} α
⊢ ⊥ ≤ a

Tactic:
by simp [← (orderIsoShrink.{u} α).symm.le_iff_le]

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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u'
inst✝¹² : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝¹¹ : LinearOrder J
inst✝¹⁰ : SuccOrder J
inst✝⁹ : OrderBot J
inst✝⁸ : WellFoundedLT J
J'✝ : Type w'
inst✝⁷ : LinearOrder J'✝
inst✝⁶ : SuccOrder J'✝
inst✝⁵ : OrderBot J'✝
inst✝⁴ : WellFoundedLT J'✝
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : OrderBot J'
inst✝¹ : SuccOrder J'
inst✝ : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (homOfLE ⋯) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((h.ofOrderIso e).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
replace eq := congr_arg h.F.mapArrow.obj eq

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u'
inst✝¹² : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝¹¹ : LinearOrder J
inst✝¹⁰ : SuccOrder J
inst✝⁹ : OrderBot J
inst✝⁸ : WellFoundedLT J
J'✝ : Type w'
inst✝⁷ : LinearOrder J'✝
inst✝⁶ : SuccOrder J'✝
inst✝⁵ : OrderBot J'✝
inst✝⁴ : WellFoundedLT J'✝
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : OrderBot J'
inst✝¹ : SuccOrder J'
inst✝ : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : h.F.mapArrow.obj (Arrow.mk (homOfLE ⋯)) = h.F.mapArrow.obj (Arrow.mk (homOfLE ⋯))
⊢ Arrow.mk ((h.ofOrderIso e).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (⋯.functor.map (homOfLE ⋯)) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((h.iic j).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
replace eq := congr_arg h.F.mapArrow.obj eq

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : h.F.mapArrow.obj (Arrow.mk (⋯.functor.map (homOfLE ⋯))) = h.F.mapArrow.obj (Arrow.mk (homOfLE ⋯))
⊢ Arrow.mk ((h.iic j).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (⋯.functor.map (homOfLE ⋯)) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((h.ici j).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
replace eq := congr_arg h.F.mapArrow.obj eq

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : h.F.mapArrow.obj (Arrow.mk (⋯.functor.map (homOfLE ⋯))) = h.F.mapArrow.obj (Arrow.mk (homOfLE ⋯))
⊢ Arrow.mk ((h.ici j).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ Nonempty (AttachCells g f) → (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
rintro ⟨c⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ MapEq F G i₁ i₃ ⋯ h₃

Tactic:
by
  simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]
  refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩
  rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]
  simp [-homOfLE_comp, m₁₂.w, m₂₃.w]

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
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
⊢ k₂ = ⊥

Tactic:
simpa using h₂

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
⊢ j ≤ i₂

Tactic:
simpa using h₂

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₁ : Order.IsSuccLimit x✝
h₂ : x✝ ≤ ⊥
⊢ IsMin x✝

Tactic:
simpa using h₂

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

Goal state before:
pp: case mp.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f → ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

Tactic:
intro hf

Goal state after:
case mp.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: case isMin
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : IsMin j
⊢ c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂

Tactic:
obtain rfl := hj.eq_bot
    simpa [← cancel_epi c.isoBot.inv] 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) = val₀

Tactic:
by
    simp only [← e.map_zero]
    conv_rhs => rw [← d.map_succ j hj e.val]
    rw [← comp_apply, ← map_comp]
    rfl

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]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ multiplicity p p = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case hmn
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
hqr : ¬q + r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
have : padicValRat p q = min (padicValRat p q) (padicValRat p r) := (min_eq_left h).symm

Goal state after:
case hmn
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
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ padicValRat p q ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ ‖z1 + z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ max ‖z1‖ ‖z2‖
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ max ‖z1‖ ‖z2‖
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = ↑(padicValNat p n !) + ↑n

Tactic:
padicValNat_eq_emultiplicity <| factorial_ne_zero n

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ IsUnit ↑r.den

Tactic:
by
  rw [isUnit_iff]
  apply le_antisymm (r.den : ℤ_[p]).2
  rw [← not_lt, coe_natCast]
  intro norm_denom_lt
  have hr : ‖(r * r.den : ℚ_[p])‖ = ‖(r.num : ℚ_[p])‖ := by
    congr
    rw_mod_cast [@Rat.mul_den_eq_num r]
  rw [padicNormE.mul] at hr
  have key : ‖(r.num : ℚ_[p])‖ < 1 := by
    calc
      _ = _ := hr.symm
      _ < 1 * 1 := mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one
      _ = 1 := mul_one 1
  have : ↑p ∣ r.num ∧ (p : ℤ) ∣ r.den := by
    simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
    exact ⟨key, norm_denom_lt⟩
  apply hp_prime.1.not_dvd_one
  rwa [← r.reduced.gcd_eq_one, Nat.dvd_gcd_iff, ← Int.natCast_dvd, ← Int.natCast_dvd_natCast]

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

Goal state before:
pp: case pos
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 : i ≤ n
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

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:
· exact (hi i le_rfl n hin).le

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 : ∀ j ≥ i, ∀ k ≥ j, ‖↑x' k - ↑(const norm x'.lim) j‖ < ↑p ^ (-↑n)
hin : n < i
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
hj

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f → c.fst = c.snd

Tactic:
intro hf

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : Mono f
⊢ c.fst = c.snd
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → Mono f

Tactic:
intro hf

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPullback (𝟙 X) (𝟙 X) f f → Mono f

Tactic:
intro hf

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPullback (𝟙 X) (𝟙 X) f f
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f → c.inl = c.inr

Tactic:
intro hf

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : Epi f
⊢ c.inl = c.inr
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → Epi f

Tactic:
intro hf

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ Epi f
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Tactic:
intro hf

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

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✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
Z : C
p₁ : Z ⟶ Y₁
p₂ : Z ⟶ Y₂
z : Φ.fiber.obj Z
fac : p₁ ≫ f₁ = p₂ ≫ f₂
hz₁ : (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁
hz₂ : (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂
φ₁ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₁ hf₁ := ObjectProperty.homMk (Over.homMk p₁ ⋯)
⊢ s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫ Pi.π (fun t ↦ M) y₂ =
    s.π.app (op (R.arrows.categoryMk f₁ hf₁)) ≫ Pi.π (fun t ↦ M) y₁

Tactic:
let φ₂ : Presieve.categoryMk _ _ (R.downward_closed hf₁ p₁) ⟶
      Presieve.categoryMk _ _ hf₂ :=
    ObjectProperty.homMk (Over.homMk p₂)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
Z : C
p₁ : Z ⟶ Y₁
p₂ : Z ⟶ Y₂
z : Φ.fiber.obj Z
fac : p₁ ≫ f₁ = p₂ ≫ f₂
hz₁ : (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁
hz₂ : (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂
φ₁ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₁ hf₁ := ObjectProperty.homMk (Over.homMk p₁ ⋯)
φ₂ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₂ hf₂ := ObjectProperty.homMk (Over.homMk p₂ ⋯)
⊢ s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫ Pi.π (fun t ↦ M) y₂ =
    s.π.app (op (R.arrows.categoryMk f₁ hf₁)) ≫ Pi.π (fun t ↦ M) y₁
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

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✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective (⇑Φ.skyscraperPresheafHomEquiv ∘ fun x ↦ Φ.presheafFiber.map f ≫ x)

Tactic:
convert! (hf _ (Φ.isSheaf_skyscraperPresheaf M)).comp Φ.skyscraperPresheafHomEquiv.bijective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ (⇑Φ.skyscraperPresheafHomEquiv ∘ fun x ↦ Φ.presheafFiber.map f ≫ x) = (fun g ↦ f ≫ g) ∘ ⇑Φ.skyscraperPresheafHomEquiv
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε

Tactic:
apply le_add_of_le_of_nonneg

Goal state after:
case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε

case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: j : ℕ
hj : j + 1 = 0
⊢ j + 1 ≤ 0

Tactic:
hj

Goal state after:
j : ℕ
hj : j + 1 = 0
⊢ 0 ≤ 0