mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom)
        ((ConcreteCategory.hom a) (f ^ n) •
          (AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op)) t))) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) 0
⊢ f ^ n • t = 0

Tactic:
Scheme.Modules.restrictAppIso_smul_Spec,

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ℕ
hn : (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom iso.inv) t = 0
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      (f ^ n •
        (ConcreteCategory.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom)
          ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯).op)) t))) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) 0
⊢ f ^ n • t = 0
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_1.refine_1
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f

Tactic:
rw [w₁, assoc, assoc, assoc, assoc, hp']

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
R S : Presieve X
hR : R ∈ P.precoverage.coverings X
hS : S ∈ P.precoverage.coverings X
⊢ R ⊔ S ∈ P.precoverage.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover
    obtain ⟨F, rfl⟩ := S.exists_eq_preZeroHypercover
    rw [← PreZeroHypercover.presieve₀_sum]
    rw [PreZeroHypercover.presieve₀_mem_precoverage_iff] at hR hS ⊢
    exact h hR hS

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ Precoverage.ZeroHypercover.Small 𝒰

Tactic:
refine ⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀,
      ⟨?_, ?_⟩⟩
    · rw [Scheme.presieve₀_mem_qcPrecoverage_iff]
      exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩
    · rw [Scheme.presieve₀_mem_precoverage_iff]
      exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩

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 : 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₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
A₂ : D := { obj := Over.mk (π a₂), property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ π a₁), property := ⋯ }
i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂ ⋯)
⊢ g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
change F.map i₁ ≫ _ = F.map i₂ ≫ _

Goal state after:
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₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D := { obj := Over.mk (π a₁), property := ⋯ }
A₂ : D := { obj := Over.mk (π a₂), property := ⋯ }
Z' : D := { obj := Over.mk (g₁ ≫ π a₁), property := ⋯ }
i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂ ⋯)
⊢ F.map i₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } =
    F.map i₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
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) ≫ π ⋯.choose = ⋯.choose ≫ π ⋯.choose

Tactic:
rw [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 ≫ π ⋯.choose = ⋯.choose ≫ π ⋯.choose
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (continuousMapPresheafIsoUlift T)]

Goal state after:
T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology
    (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ yoneda.obj (TopCat.of (ULift.{u_1, v} T)))
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₄
sq : IsPullback t l r b
⊢ Mono (cokernel.map t b l r ⋯)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

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₄
sq : IsPullback t l r b
⊢ ∀ (P : C) (g : P ⟶ cokernel t), g ≫ cokernel.map t b l r ⋯ = 0 → g = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
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
inst✝ : IsFiltered J
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 : Mono f
s : Subobject X
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ s
⊢ Subobject.mk f ≤ s

Tactic:
induction s using Subobject.ind with

Goal state after:
case a.h
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
inst✝¹ : IsFiltered J
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 : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
⊢ Subobject.mk f ≤ Subobject.mk g
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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ 𝟙 X ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ Y.map (Under.Hom.right f)

Tactic:
simp only [Category.id_comp, Category.assoc, ← Functor.map_comp, Under.w]

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'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
j : Fin (n + 1)
hj : ¬IsMax j
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
obtain ⟨j, rfl⟩ | rfl := j.eq_castSucc_or_eq_last
    · replace hF := hF j
      rw [← W.arrow_mk_mem_toSet_iff] at hF ⊢
      have eq : Arrow.mk (homOfLE (Order.le_succ j.castSucc)) =
        Arrow.mk (homOfLE j.castSucc_le_succ) :=
          Arrow.ext rfl j.orderSucc_castSucc rfl
      replace eq := congr_arg F.mapArrow.obj eq
      convert! hF using 1
    · rw [isMax_iff_eq_top] at hj
      exact (hj rfl).elim

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} W ≤ W

Tactic:
intro _ _ f hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : ¬k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
· 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]

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : ¬k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
by
  wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
  · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]
  rw [Subsingleton.elim iter₁ (iter₂.trunc hj)]
  rfl

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

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

Tactic:
by
          have := congr_arg SqStruct.f' (s.2 g.op)
          dsimp at this ⊢
          rw [this, comp_id]

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

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

Tactic:
by
        dsimp
        simp only [← sq'.w₁]
        conv_rhs => rw [← sq'.sq.fac_left, ← F.map_comp_assoc]
        rfl

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

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    val₀

Tactic:
rw [d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)]

Goal state after:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ↑⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩
      (op ⟨⊥, ⋯⟩) =
    val₀
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} W ≤ W.rlp.llp

Tactic:
intro _ _ f hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W.rlp.llp f
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) ≤ ↑(multiplicity (↑p) d₁) + ↑(multiplicity (↑p) n₂) - ↑(multiplicity (↑p) d₂)

Tactic:
le_sub_iff_add_le

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) + ↑(multiplicity (↑p) d₂) ≤ ↑(multiplicity (↑p) d₁) + ↑(multiplicity (↑p) n₂)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 0 ≤ (↑x).valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ (↑0).valuation

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ 0 ≤ (↑x).valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))

Tactic:
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.NumberTheory.Padics.PadicNumbers

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

Tactic:
apply _root_.add_lt_add

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

case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
apply _root_.add_lt_add

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

case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f j - ↑f (max N N2)) < ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: 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)) + padicNormE (↑(↑(lim' f) i) - ↑f i) < ε / 2 + ε / 2

Tactic:
apply _root_.add_lt_add

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

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) i) - ↑f i) < ε / 2
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x⁻¹.valuation = -x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0⁻¹.valuation = -valuation 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (0 ^ (n + 1)).valuation = ↑(n + 1) * valuation 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation