mathlib-initiative/mathlib-tactics huggingface dataset:
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 Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g')
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
⊢ f₁ = f₂

Tactic:
by
  ext Y
  apply (h Y).hom_ext
  intro X
  have eq₁ := congr_app (StructuredArrow.w f₁) X.left
  have eq₂ := congr_app (StructuredArrow.w f₂) X.left
  dsimp at eq₁ eq₂ ⊢
  simp only [assoc, NatTrans.naturality]
  rw [reassoc_of% eq₁, reassoc_of% eq₂]

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 Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g))

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g'))
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
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk q.fst)
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

Tactic:
simpa [unitForward, unitBackward] using congrArg yonedaEquiv.symm p.snd.app_val

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} 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' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
hb_fac_app :
  (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t)) = (StructuredArrow.hom u).app (L.obj t)
hα_fac_app :
  α.app t ≫
      (hα.desc
            (mk (L' ⋙ StructuredArrow.right y)
              (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
        (L.obj t) =
    (StructuredArrow.hom y).app t ≫ 𝟙 ((StructuredArrow.right y).obj (L'.obj (L.obj t)))
a_w_t :
  α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) = (StructuredArrow.hom y).app t
⊢ α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))

Tactic:
simp [← a_w_t, hb_fac_app, u, hα_fac_app]

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
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝² : F'.IsRightKanExtension α
inst✝¹ : HasLimit F
inst✝ : HasLimit F'
i : C
⊢ (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i

Tactic:
by
  simp [limitIsoOfIsRightKanExtension]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
⊢ (∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
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 : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ f (Classical.arbitrary J) ≫ s.ι.app one ≫ k = f (Classical.arbitrary J) ≫ s.ι.app one ≫ l

Tactic:
h

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ f (Classical.arbitrary J) ≫ s.π ≫ l = f (Classical.arbitrary J) ≫ s.ι.app one ≫ l
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
⊢ (∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
f g : X ⟶ Y
⊢ (∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.limitsOfShape J X
X Y : C
f g : X ⟶ Y
⊢ (∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.limitsOfShape J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
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
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ ∀ (j : WalkingParallelFamily J), s.ι.app j ≫ k = t.ι.app j

Tactic:
rintro ⟨_ | _⟩
    · simpa using f (Classical.arbitrary J) ≫= w
    · exact w

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
⊢ ∀ (h : A ⟶ G.obj B), ∃ i g, (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

Tactic:
refine ⟨fun _ _ _ => ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
x✝² : Type w
x✝¹ : Category.{w, w} x✝²
x✝ : IsFiltered x✝²
⊢ HasExactColimitsOfShape x✝² D
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
𝒢 : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v₁, u₁} 𝒢
inst✝ : LocallySmall.{w, v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h : (fun P ↦ {f | P.Factors f.snd}) P = (fun P ↦ {f | P.Factors f.snd}) Q
⊢ ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f

Tactic:
by simpa [Set.ext_iff, Sigma.forall] using h

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : ObjectProperty.singleton G H
h : H ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
      exact hfg h

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : ObjectProperty.singleton G H
h : Y ⟶ H
⊢ f ≫ h = g ≫ h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
      exact hfg h

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
b : ↑(AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })))
i : J
⊢ Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) (fun i ↦ ⋯.choose) i = b i

Tactic:
exact (hf ⟨i⟩ (b i)).choose_spec

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
⊢ (∀ (G : AddCommGrpCat),
      ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g) →
    f = g

Tactic:
h

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h : ∀ (G : AddCommGrpCat), ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g
⊢ f = g
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
x y : (Discrete.functor F).ColimitType
⊢ (Discrete.functor F).descColimitType c x = (Discrete.functor F).descColimitType c y → x = y

Tactic:
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
x y : (Discrete.functor F).ColimitType
h : (Discrete.functor F).descColimitType c x = (Discrete.functor F).descColimitType c y
⊢ x = y
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
⊢ c.inj i y₁ = c.inj i y₂ → y₁ = y₂

Tactic:
h

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
h : c.inj i y₁ = c.inj i y₂
⊢ y₁ = y₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₁ = F i₂

Tactic:
h

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₂ = F i₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
⊢ x✝ = ↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹))

Tactic:
ext ⟨⟩
    exacts [ConcreteCategory.congr_hom (w ⟨left⟩) _, ConcreteCategory.congr_hom (w ⟨right⟩) _]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
      { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ } =
    { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫ ((const F.Elementsᵒᵖ).obj F).map g

Tactic:
by
    ext X x
    obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x
    simp [← shrinkYonedaObjObjEquiv_symm_comp.{w}]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: G H : CommGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q) = (p, q)

Tactic:
apply Prod.ext
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget CommGrpCat.{u}) G H) (p, q)
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)

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
X1 X2 : ExtensionOf i f
x : M
⊢ f x = ↑X2.toLinearPMap ⟨i x, ⋯⟩

Tactic:
← X2.is_extension x

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
X1 X2 : ExtensionOf i f
x : M
⊢ f x = f x
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
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rw [Submodule.coe_sup] at mem1

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
x : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(extensionOfMax i f).domain + ↑(R ∙ y)
⊢ ∃ a b, ↑x = ↑a + b • y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
rcases Nat.mul_eq_zero.1 hmn0 with h | h <;>
      simp only [totient_zero, mul_zero, zero_mul, h]

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

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
⊢ ¬(b < p ^ n ∧ b * p = a)

Tactic:
h

Goal state after:
case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inl
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)

Tactic:
h

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)

Tactic:
h

Goal state after:
case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
calc
      a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
      _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
        congr 1
        exact div_mul_div_comm h1 h2

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
frequently_iff_seq_frequently

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ 𝓟 (g univ) = ⊤

Tactic:
hg',

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ 𝓟 univ = ⊤
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
by
  constructor <;> intro h
  · rintro U U_op ⟨x, x_in⟩
    exact mem_closure_iff.1 (h _) U U_op x_in
  · intro x
    rw [mem_closure_iff]
    intro U U_op x_in
    exact h U U_op ⟨_, x_in⟩

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
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| toIcoMod hp a b + toIcoDiv hp a b • p

Tactic:
h

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
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| a + toIcoDiv hp a b • p
Module: Mathlib.Topology.Neighborhoods

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

Tactic:
by
  rw [nhdsWithin, inf_neBot_iff]
  exact forall₂_congr fun U _ ↦
    ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (frontier s) s ↔ IsOpen s

Tactic:
← isClosed_compl_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (frontier s) s ↔ IsClosed sᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥

Tactic:
ClusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝 x ⊓ F).NeBot ↔ ¬𝓝 x ⊓ F = ⊥
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
ClusterPt,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ (𝓝 x ⊓ f).NeBot
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 : α
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Tactic:
toIcoMod_eq_iff,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (b ∈ Set.Ico a (a + p) ∧ ∃ z, b = b + z • p) ↔ b ∈ Set.Ico a (a + p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: α : Type u_1
F : Filter α
inst✝ : TopologicalSpace α
a : α
⊢ MapClusterPt a F id ↔ ClusterPt a F

Tactic:
MapClusterPt,

Goal state after:
α : Type u_1
F : Filter α
inst✝ : TopologicalSpace α
a : α
⊢ ClusterPt a (map id F) ↔ ClusterPt a F
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i

Tactic:
MapClusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ ClusterPt x (Filter.map u F) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
ClusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot

Tactic:
ClusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝[s \ {x}] x).NeBot
Module: Mathlib.Topology.ClusterPt

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

Tactic:
ClusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), (𝓝 a ⊓ 𝓟 s).NeBot → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ b - ↑(toIocDiv hp a b) * p = toIocMod hp a b

Tactic:
by
  simpa using self_sub_toIocDiv_zsmul hp a b

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

Tactic:
by
  simp only [nhdsSet, image_union, sSup_union]

Goal state after: