mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y

Tactic:
congr 2

Goal state after:
case e_a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) = R'.map (iD.map f) ≫ comm2.hom.app Y
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 → Mono S.g

Tactic:
exact hS.mono_g

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

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)

Tactic:
← F.map_comp,

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (S.f ≫ s.r) = 𝟙 (F.obj S.X₁)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
by rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ (pullback X✝.arrow ⋙ map X✝.arrow).obj g ⟶ (pullback Y✝.arrow ⋙ map Y✝.arrow).obj g

Tactic:
apply homMk _ _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ((pullback X✝.arrow ⋙ map X✝.arrow).obj g).obj.left ⟶ ((pullback Y✝.arrow ⋙ map Y✝.arrow).obj g).obj.left

C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ?m.65 ≫ ((pullback Y✝.arrow ⋙ map Y✝.arrow).obj g).arrow = ((pullback X✝.arrow ⋙ map X✝.arrow).obj g).arrow
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)
S : ShortComplex C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
⊢ F.map S.g = F.map (cokernel.π (kernel.ι S.g)) ≫ F.map (Abelian.factorThruCoimage S.g)

Tactic:
← F.map_comp,

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)
S : ShortComplex C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
⊢ F.map S.g = F.map (cokernel.π (kernel.ι S.g) ≫ Abelian.factorThruCoimage S.g)
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)
S : ShortComplex C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex C := { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
⊢ F.map (Abelian.factorThruImage S.f) ≫ F.map (kernel.ι (cokernel.π S.f)) = F.map S.f ≫ 𝟙 (F.obj S.X₂)

Tactic:
← F.map_comp,

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)
S : ShortComplex C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex C := { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
⊢ F.map (Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)) = F.map S.f ≫ 𝟙 (F.obj S.X₂)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
⊢ F.map (kernel.ι S.g) ≫ F.map S.g = 0

Tactic:
by simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero]

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

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Tactic:
dsimp [ran, ranCounit]

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: 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.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }

Tactic:
by
    dsimp
    simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]
    congr 1
    apply CostructuredArrow.map_comp

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
let eq : (RightExtension.mk _ α).IsUniversal ≃
    (RightExtension.mk _
      ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))

Goal state after:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)
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
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ op s = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val))

Tactic:
simp [← CostructuredArrow.eq_mk]

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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ s = op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ (unop t).hom))

Tactic:
simp [← CostructuredArrow.eq_mk]

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
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ op (CostructuredArrow.mk (YonedaCollection.fst p.val)) = op s

Tactic:
simp [← CostructuredArrow.eq_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasLimitsOfShape K C
inst✝ : PreservesColimitsOfShape J lim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ ((lim ⋙ (evaluation D C).obj d).map η ≫
        (limitObjIsoLimitCompEvaluation G d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G =
    ((limitObjIsoLimitCompEvaluation F d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (limit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G

Tactic:
by simp [← NatTrans.comp_app]

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

Goal state before:
pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
simp only [monoLift_comp]

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 : D
T : C ⥤ 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:
suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
    rw [this]
    infer_instance

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
⊢ P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ L.IsLeftKanExtension e.hom

Tactic:
rw [isLeftKanExtension_along_uliftYoneda_iff]
  exact ⟨inferInstance, ⟨inferInstance⟩⟩

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

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
i : C
x : (Discrete.functor F).obj { as := i }
j : C
y : (Discrete.functor F).obj { as := j }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := j } y)
⊢ (Discrete.functor F).ιColimitType { as := i } x = (Discrete.functor F).ιColimitType { as := j } y

Tactic:
obtain rfl := h₃ _ _ _ _ h

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
i : C
x y : (Discrete.functor F).obj { as := i }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } y)
⊢ (Discrete.functor F).ιColimitType { as := i } x = (Discrete.functor F).ιColimitType { as := i } y
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
· exact negOnePow_odd n

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: 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)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap ((RingHom.id R) z1 • ⟨↑z2 • y, ⋯⟩)

Tactic:
congr 2

Goal state after:
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)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(z1 • z2) • y = (RingHom.id R) z1 • ↑⟨↑z2 • y, ⋯⟩
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 = toIcoDiv hp a b - m

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a b + -m = toIcoDiv hp a b + -m
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 : ℤ
⊢ toIocDiv hp a b + -m = toIocDiv hp a b - m

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a b + -m = toIocDiv hp a b + -m
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 c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp (a + -c) b

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp (a + -c) b = toIcoDiv hp (a + -c) b
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 c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp (a + -c) b

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp (a + -c) b = toIocDiv hp (a + -c) b
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 : α
⊢ toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

Tactic:
by
  simpa only [neg_neg] using toIocDiv_neg hp (-a) (-b)

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ DirectedOn (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) f.sets

Tactic:
intro t₁ ht₁ t₂ ht₂

Goal state after:
case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₂ z
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g h : Set α → Filter β
⊢ (f.lift fun x ↦ g x ⊓ h x) = f.lift g ⊓ f.lift h

Tactic:
by simp only [Filter.lift, iInf_inf_eq]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (pure a).lift' h = 𝓟 (h {a})

Tactic:
by
  rw [← principal_singleton, lift'_principal hh]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, Tendsto g f (𝓝 x)
⊢ f.limUnder g = Classical.choice hX

Tactic:
simp_rw [Tendsto] at h
  simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, Tendsto g f (𝓝 x)
⊢ f.limUnder g = Classical.choice hX

Tactic:
by
  simp_rw [Tendsto] at h
  simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
simp only [subset_def, mem_interior]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ False

Tactic:
exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

Goal state after:
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ⋃ y ∈ S, f ⁻¹' g y = ⋃ i ∈ S, i

Tactic:
exact iUnion₂_congr hfg

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)

Tactic:
← mem_closure_iff_clusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ x ∉ closure[inst✝] sᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Sort w
x : X
t : Set X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ (i : ι), p i → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i

Tactic:
by
    simp only [Set.Nonempty, mem_inter_iff, and_comm]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ x ∈ closure[inst✝] i'

Tactic:
true_and,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, x ∈ closure[inst✝] i'
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²

Tactic:
simp_rw [← modEq_iff_eq_mod_zmultiples]

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ z✝² ≡ z✝¹ [PMOD p] ∨ z✝¹ ≡ z✝ [PMOD p] ∨ z✝ ≡ z✝² [PMOD p]
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = a + Int.fract ((b - a) / p) * p

Tactic:
rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - ↑⌊(b - a) / p⌋) * p
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
simp only [nhds_generateFrom, @forall_comm (b ∈ _), tendsto_iInf, mem_ofPred_eq, and_imp,
    tendsto_principal]

Goal state after:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ (∀ i ∈ g, b ∈ i → ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f