mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ IsColimit (π₂.mapCocone (CokernelCofork.ofπ p ⋯))

Tactic:
apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ IsColimit (π₃.mapCocone (CokernelCofork.ofπ p ⋯))

Tactic:
apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j

Tactic:
ext
    · apply IsColimit.fac h₁
    · apply IsColimit.fac h₂
    · apply IsColimit.fac h₃

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom =
    (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ)

Tactic:
dsimp only [leftHomologyMap, mapLeftHomologyIso, LeftHomologyData.leftHomologyIso,
    leftHomologyMapIso', Iso.refl]
  simp only [LeftHomologyData.map_leftHomologyMap', Functor.mapShortComplex_obj,
    ← leftHomologyMap'_comp, comp_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (kernel.ι f.op).unop = eqToHom ⋯ ≫ cokernel.π f ≫ (kernelOpUnop f).inv

Tactic:
simp [kernelOpUnop]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ h.g' = 0

Tactic:
← cancel_epi h.p,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ h.p ≫ h.g' = h.p ≫ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
⊢ (AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫
      AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range) =
    0

Tactic:
ext (x : S.X₁)
    dsimp
    rw [QuotientAddGroup.eq_zero_iff, AddMonoidHom.mem_range]
    apply exists_apply_eq_apply

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s = s'

Tactic:
rw [← s'.id, h, add_right_inj, cancel_epi S.g] at eq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : s.s = s'.s
⊢ s = s'
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
⊢ g = h

Tactic:
refine (WithTerminal.isLimitEquiv.invFun p.isLimit).hom_ext (fun j ↦ ?_)
    cases j with
    | of j => have := hp j; rw [← cancel_mono ((p.diag.obj j).hom)]; simpa
    | star => exact e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
i : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj i = (c.inj i).op

Tactic:
simp [opCoproductIsoProduct', Fan.proj]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
    (f'.π.app { as := j }).op

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = (f'.π.app { as := j }).op
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m =
    colimit.desc (liftToFinsetObj F)
      { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } }

Tactic:
apply colimit.hom_ext
        rintro t
        dsimp [liftToFinsetObj]
        apply colimit.hom_ext
        rintro ⟨⟨j, hj⟩⟩
        convert! h j using 1
        · simp [← colimit.w (liftToFinsetObj F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
          rfl
        · simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  (StructuredArrow.hom E ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.Hom.right f₁)).app X.left =
    (StructuredArrow.hom G).app X.left
eq₂ :
  (StructuredArrow.hom E ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.Hom.right f₂)).app X.left =
    (StructuredArrow.hom G).app X.left
⊢ (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y

Tactic:
dsimp at eq₁ eq₂ ⊢

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  (StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₁).app (L.obj X.left) =
    (StructuredArrow.hom G).app X.left
eq₂ :
  (StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₂).app (L.obj X.left) =
    (StructuredArrow.hom G).app X.left
⊢ ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₁).app Y =
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₂).app Y
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).fst = p.fst

Tactic:
by
  simp [map₁]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).snd =
    (ConcreteCategory.hom (G.map (eqToHom ⋯))) ((ConcreteCategory.hom (η.app (op (CostructuredArrow.mk p.fst)))) p.snd)

Tactic:
by
  simp [map₁]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  (((whiskeringLeft C D H).obj L).map f₁.left ≫ CostructuredArrow.hom E).app X.right =
    (CostructuredArrow.hom G).app X.right
eq₂ :
  (((whiskeringLeft C D H).obj L).map f₂.left ≫ CostructuredArrow.hom E).app X.right =
    (CostructuredArrow.hom G).app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

Tactic:
dsimp at eq₁ eq₂ ⊢

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : f₁.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right = (CostructuredArrow.hom G).app X.right
eq₂ : f₂.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right = (CostructuredArrow.hom G).app X.right
⊢ f₁.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right =
    f₂.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case e_7
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))

Tactic:
rw [comp_id, ← StructuredArrow.eq_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
by
  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by
    rw [this]
    infer_instance
  ext X
  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]
  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂

Tactic:
by
  rw [t.app_zero, t.app_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
by rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
by rw [Iso.comp_inv_eq, w]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsSeparator (unop G) ↔ IsCoseparator G

Tactic:
by
  rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (fun x ↦
          match j', x with
          | { as := i }, x => ⟨i, x⟩) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      fun x ↦
      match j, x with
      | { as := i }, x => ⟨i, x⟩

Tactic:
rintro ⟨i⟩ ⟨j⟩ f

Goal state after:
C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ (fun x ↦
        match { as := j }, x with
        | { as := i }, x => ⟨i, x⟩) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    fun x ↦
    match { as := i }, x with
    | { as := i }, x => ⟨i, x⟩
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j' with
        | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
rintro ⟨i⟩ ⟨j⟩ f

Goal state after:
C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := j } with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
    | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (Additive.ofMul u) ^ n = u ^ n

Tactic:
toMul_ofMul

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ n
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (Additive.ofMul u) ^ z = u ^ z

Tactic:
toMul_ofMul

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ u ^ z = u ^ z
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = ↑x - snd i x • y

Tactic:
exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm

Goal state after:
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n

Tactic:
by
  conv_rhs => rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha0)
  · simp [zero_dvd_iff.1 h]
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  have hab' := primeFactors_mono h hb0
  rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
  refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl
  exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsOpen[inst✝] s) fun x ↦ x

Tactic:
by
  convert! nhds_basis_opens x using 2
  exact and_congr_left_iff.2 IsOpen.mem_nhds_iff

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ (¬∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = a

Tactic:
not_imp_comm

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ 𝓟 (s ∪ sᶜ) ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
union_compl_self,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ 𝓟 univ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
rw [toIcoMod_eq_sub, toIocMod_eq_sub _ x₁, add_le_add_iff_right, ← neg_sub x₁ x₃, toIocMod_neg,
    neg_zero, le_sub_iff_add_le]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ (comap Subtype.val (𝓝 x)).NeBot

Tactic:
by
  simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Ioc (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Ioc_add_intCast (0 : α)

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst✝] (s ∪ t)
⊢ IsOpen[inst✝] s

Tactic:
obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsOpen[inst✝] s
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsClosed[inst✝] (s ∪ t)
⊢ IsClosed[inst✝] s

Tactic:
obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsClosed[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsClosed[inst✝] s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY

Goal state after:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : X ⊕ Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) i = (Homeomorph.refl (X ⊕ Y)) i

Tactic:
cases i

Goal state after:
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
val✝ : X
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) (inl val✝) = (Homeomorph.refl (X ⊕ Y)) (inl val✝)

case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
val✝ : Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) (inr val✝) = (Homeomorph.refl (X ⊕ Y)) (inr val✝)