mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (∃ ι A B f, W = ofHoms f) → IsSmall.{w, v, u} W

Tactic:
· rintro ⟨_, _, _, _, rfl⟩
    infer_instance

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

Tactic:
obtain hij | rfl := hij.lt_or_eq

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

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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.succ j hj e.val) =
    d.lift (Order.succ j) hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: 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
⊢ W.rlp ≤ ((coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).rlp

Tactic:
← le_llp_iff_le_rlp

Goal state after:
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
⊢ (coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

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

Tactic:
← le_llp_iff_le_rlp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Small.{w, max u v} (Subobject G)
⊢ MorphismProperty.IsSmall.{w, v, u} (generatingMonomorphisms G)

Tactic:
dsimp [generatingMonomorphisms]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Small.{w, max u v} (Subobject G)
⊢ MorphismProperty.IsSmall.{w, v, u} (MorphismProperty.ofHoms fun X ↦ X.arrow)
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:
by
  refine le_antisymm ?_
    (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.ord.ToType)
  intro X Y f hf
  have sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 _) := ⟨by simp⟩
  have := hf _ (rlp_πObj I κ f)
  refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩
  exact
    { i := Arrow.homMk (𝟙 _) sq.lift
      r := Arrow.homMk (𝟙 _) (πObj I κ f) }

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
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
h3 : min (padicValRat p (r + q)) (padicValRat p q) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
rw [add_comm] at h3

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
h3 : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < padicNorm p ↑m

Tactic:
rw [h, inv_lt_one₀] <;> norm_cast

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p

case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ‖↑x‖ ≤ 1
⊢ 0 ≤ (↑x).valuation

Tactic:
rwa [Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx, zpow_le_one_iff_right₀, neg_nonpos]
    at this

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ↑p ^ (-(↑x).valuation) ≤ 1
⊢ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0

Tactic:
hx,

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * 0 = 0
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ : C
x : F.obj X✝
X : (fromOverFunctor F x).Elements
⊢ { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.map
        ((Iso.refl (𝟭 (fromOverFunctor F x).Elements)).hom.app X) ≫
      (Iso.refl
              ({ obj := fun u ↦ (fromOverFunctor F x).elementsMk (Over.mk ↑u.hom) ⟨u.left.snd, ⋯⟩,
                  map := fun {X Y} f ↦
                    homMk ((fromOverFunctor F x).elementsMk (Over.mk ↑X.hom) ⟨X.left.snd, ⋯⟩)
                      ((fromOverFunctor F x).elementsMk (Over.mk ↑Y.hom) ⟨Y.left.snd, ⋯⟩)
                      (Over.homMk ↑(Over.Hom.left f) ⋯) ⋯,
                  map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
                  map := fun {X Y} f ↦
                    Over.homMk
                      (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                        (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                        (Over.Hom.left ↑f) ⋯)
                      ⋯,
                  map_id := ⋯, map_comp := ⋯ })).hom.app
        ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
              map := fun {X Y} f ↦
                Over.homMk
                  (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                    (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                    (Over.Hom.left ↑f) ⋯)
                  ⋯,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
by simp_all; rfl

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

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

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
⊢ f.norm = g.norm

Tactic:
have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.norm = g.norm
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: 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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
Φ : P.FullSubcategory
hf : Epi (Φ.obj.presheafFiber.map f)
⊢ Epi (Φ.obj.presheafFiber.map f')

Tactic:
exact (MorphismProperty.epimorphisms _).of_isPullback
        ((IsPullback.of_hasPullback f (shrinkYonedaEquiv.{w}.symm s)).map
          Φ.obj.presheafFiber) (.infer_property _)

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

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
x : ↥X
hx : f x = s default
⊢ ∃ l, l ≫ f = s ∧ l default = x

Tactic:
by
  obtain ⟨⟨s, a⟩, rfl⟩ := (SpecToEquivOfField Ω S).symm.surjective s
  obtain rfl : f x = s := by simp [hx, SpecToEquivOfField]
  let m := (f.residueFieldMap x).hom
  dsimp at m
  algebraize [m, a.hom]
  let b : X.residueField x →ₐ[S.residueField (f x)] Ω :=
    IsSepClosed.lift
  have : f.residueFieldMap x ≫ CommRingCat.ofHom b.toRingHom = a := by
    ext1; exact b.comp_algebraMap
  refine ⟨Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x, ?_, ?_⟩
  · simp [SpecToEquivOfField, ← this]
    rfl
  · dsimp
    apply fromSpecResidueField_apply

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ P snd

Tactic:
refine (P.arrow_mk_iso_iff ?_).2 H
    exact Arrow.isoMk (F.preimageIso (h.isoIsPullback X (F.obj a) BC)) (Iso.refl _)
      (F.map_injective (by simp))

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

Goal state before:
pp: 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
this : padicNormE (↑(limSeq f j) - ↑(limSeq f (max N N2))) < ε
⊢ padicNormE ↑(limSeq f j - limSeq f (max N N2)) < ε

Tactic:
exact mod_cast this

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩ =
    0

Tactic:
rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
      X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
    simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
      add_neg_cancel]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ (↑q).valuation = padicValRat p q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

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

case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ (↑q).valuation = padicValRat p q
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Tactic:
simp only [hσ'_eq (show n + 1 = 0 + q by lia) (c_mk (n + 2) (n + 1) rfl), pow_zero,
      Fin.mk_zero, one_zsmul, eqToHom_refl, comp_id, comp_sum,
      AlternatingFaceMapComplex.obj_d_eq]
    -- All terms of the sum but the first two are zeros
    rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
    · simp only [Fin.val_zero, Fin.val_succ, Fin.val_castSucc, zero_add, pow_zero, one_smul,
        pow_one, neg_smul, comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ,
        add_neg_cancel]
    · intro j
      rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
      · simp [Fin.succ_ne_zero]
      · dsimp
        lia
      · simp only [Fin.succ_lt_succ_iff, j.succ_pos]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else ↑(x * y).valuation) =
    (if x = 0 then ⊤ else ↑x.valuation) + if y = 0 then ⊤ else ↑y.valuation

Tactic:
hx,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if 0 * y = 0 then ⊤ else ↑(0 * y).valuation) =
    (if 0 = 0 then ⊤ else ↑(valuation 0)) + if y = 0 then ⊤ else ↑y.valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
hx,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if 0 = 0 then ⊤ else ↑(valuation 0)) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if 0 + y = 0 then ⊤ else ↑(0 + y).valuation
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
rw [iff] at hi

Goal state after:
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
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 Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ φ.f.f i✝ ≫ Q.p.f i✝ = P.p.f i✝ ≫ φ.f.f i✝

Tactic:
simp only [HomologicalComplex.comp_p_d, HomologicalComplex.p_comp_d]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ (N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

Tactic:
rw [N₁Γ₀_hom_app]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: α : Type u_1
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p

Tactic:
induction p with
  | nil => rfl
  | cons _ _ ih => dsimp [pathToList] at *; rw [ih]

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), F (0, x) = g₀ x

Tactic:
by simp [← h₀]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant P.P
⊢ weakEquivalences (BifibrantObject C) (homMk P.ι)

Tactic:
by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (⨆ j, stdSimplex.face {↑j}ᶜ).toSSet.HasDimensionLT n

Tactic:
hasDimensionLT_iSup_iff

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ ∀ (i_1 : ↑{i}ᶜ), (stdSimplex.face {↑i_1}ᶜ).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A

Tactic:
refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : stdSimplex.face {i}ᶜ ≤ A
⊢ False

case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ (⨆ i, stdSimplex.face {i}ᶜ).toSSet.HasDimensionLT n

Tactic:
hasDimensionLT_iSup_iff

Goal state after:
n : ℕ
⊢ ∀ (i : Fin (n + 1)), (stdSimplex.face {i}ᶜ).toSSet.HasDimensionLT n
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), monomorphisms (Type u) (f j)
⊢ monomorphisms (Type u) (Limits.Sigma.map f)

Tactic:
simp only [monomorphisms.iff, mono_iff_injective] at h ⊢

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
⊢ Function.Injective ⇑(hom (Limits.Sigma.map f))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case pos
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∈ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
obtain ⟨x₁, rfl⟩ := h₂

Goal state after:
case pos
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₁ : X₁
hx₃ : (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁) = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1)
⊢ f.arrow j = g.arrow j

Tactic:
· exact h j

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))

Tactic:
← types_comp_apply (σ.app _) (Y.map _),

Goal state after:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }) ≫ Y.map (tr (mkOfSucc k) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (Y.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))

Tactic:
← types_comp_apply (σ.app _) (Y.map _),

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌) ≫ Y.map (mkOfSucc k).op)) (sx.spineToSimplex f)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.hom, map_id := h_id } ≫ { toPrefunctor := e.inv, map_id := ⋯ } = 𝟙 (of V)

Tactic:
apply forgetToQuiv.map_injective
    exact e.hom_inv_id

Goal state after: