mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i ∈ s, (P i).Factors f) → (s.sup P).Factors f

Tactic:
induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
h : ∃ i ∈ s, (P i).Factors f
⊢ (s.sup P).Factors f

Tactic:
by
  classical
  revert h
  induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
⊢ x ∈ ⇑e '' s → e.symm x ∈ s

Tactic:
rintro ⟨a, m, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ e.symm (e a) ∈ s
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.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ f.app X ≫ α.app X =
    ((L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)

Tactic:
have h := congr_app (L.lanUnit.naturality f) X

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.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
h :
  ((𝟭 (C ⥤ H)).map f ≫ L.lanUnit.app F₂).app X = (L.lanUnit.app F₁ ≫ (L.lan ⋙ (whiskeringLeft C D H).obj L).map f).app X
⊢ f.app X ≫ α.app X =
    ((L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)
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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseRightKanExtensionAt F' Y

Tactic:
rw [hasPointwiseRightKanExtensionAt_iff_of_natIso_left _ e₁.symm]
  let e : StructuredArrow.proj Y L ⋙ F' ≅ StructuredArrow.proj Y L ⋙ F :=
    NatIso.ofComponents fun X ↦ (e₂.app _).symm
  rw [HasPointwiseRightKanExtensionAt, hasLimit_iff_of_iso e]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (((evaluation C D).obj Y).mapCocone (((whiskeringLeft C E D).obj F).mapCocone c))

Tactic:
change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)
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
⊢ a = StructuredArrow.homMk (hb.desc u) ⋯

Tactic:
ext1

Goal state after:
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₁ := ⋯
a : (precomp₂ L' α).obj b ⟶ y
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
⊢ a = default

Tactic:
ext1

Goal state after:
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := ⋯
a : b ⟶ y
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right default
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ (functorToRepresentables P).map f ≫ uliftYonedaEquiv.symm (unop x₂).snd =
    uliftYonedaEquiv.symm (unop x₁).snd ≫ ((Functor.const P.Elementsᵒᵖ).obj P).map f

Tactic:
dsimp
        rw [comp_id, ← uliftYonedaEquiv_symm_map, f.unop.2]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ φ = StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right (StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft (F.op.lan.map f) ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    presheafHom φ P ≫ F.op.whiskerLeft (G.map f)

Tactic:
← reassoc_of% eq,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ f ≫
      F.op.lanUnit.app Q ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    presheafHom φ P ≫ F.op.whiskerLeft (G.map f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ (ObjectProperty.singleton (op G)).IsSeparating ↔ (ObjectProperty.singleton G).IsCoseparating

Tactic:
← isSeparating_op_iff,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ (ObjectProperty.singleton (op G)).IsSeparating ↔ (ObjectProperty.singleton G).op.IsSeparating
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) 1 = (Hom.hom default) 1

Tactic:
map_one,

Goal state after:
case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ 1 = (Hom.hom default) 1
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))

Tactic:
intro u₁

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
⊢ ∀ ⦃a₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType⦄,
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
          (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
            (coconeπOpCompShrinkYonedaObj F X))
          u₁ =
        ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
          (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
            (coconeπOpCompShrinkYonedaObj F X))
          a₂ →
      u₁ = a₂
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) 1 = (Hom.hom default) 1

Tactic:
map_one,

Goal state after:
case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ 1 = (Hom.hom default) 1
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₂
x✝ : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
⊢ c.inj i₁ y₁ = c.inj i₂ y₂

Tactic:
subst h₁ h₂

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₂ : F i₁
x✝ : ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂
⊢ c.inj i₁ y₂ = c.inj i₁ y₂
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
Int.not_even_iff_odd

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (↑n) (↑n + 1))

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

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)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ↑(ExtensionOfMaxAdjoin.fst i a) + ExtensionOfMaxAdjoin.snd i a • y +
      (↑(ExtensionOfMaxAdjoin.fst i b) + ExtensionOfMaxAdjoin.snd i b • y) =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y

Tactic:
add_smul,

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)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ↑(ExtensionOfMaxAdjoin.fst i a) + ExtensionOfMaxAdjoin.snd i a • y +
      (↑(ExtensionOfMaxAdjoin.fst i b) + ExtensionOfMaxAdjoin.snd i b • y) =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a • y + ExtensionOfMaxAdjoin.snd i b • y)
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ n

Tactic:
rw [count_eq_card_filter_range]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ count p n ≤ #hp.toFinset

Tactic:
rw [count_eq_card_filter_range]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #hp.toFinset
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = 0 ↔ ∀ m < n, ¬p m

Tactic:
simp [count_eq_card_filter_range]

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)
h : Baer R Q
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun y => ?_
  rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin,
    Submodule.mem_sup]
  exact ⟨0, Submodule.zero_mem _, y, Submodule.mem_span_singleton_self _, zero_add _⟩

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 ≠ 0 → f 1 = (factorization 1).prod fun p k ↦ f (p ^ k)

Tactic:
rintro -
    rw [factorization_one, hf]
    simp

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).gcd (1 % (n + 1)) = 1

Tactic:
by rw [gcd_comm, ← gcd_rec, gcd_one_right]

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ N (b % n) ≤ b / n

Tactic:
rw [Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ n * N (b % n) ≤ b
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ (⋃₀ s)ᶜ ∈ T

Tactic:
by
    simp only [Set.compl_sUnion]
    exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

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 | toIcoMod hp a b = toIocMod hp a b} = ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
ext1

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ a, ↑a ∈ t

Tactic:
Set.inter_nonempty_iff_exists_right,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ a, ↑a ∈ t
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p

Tactic:
add_smul,

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b • p + 1 • p)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p

Tactic:
add_smul,

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b • p + 1 • p)
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' g ⁻¹' q '' V

Tactic:
refine ⟨_, hV, ?_⟩

Goal state after:
case mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s = ∅
⊢ IsClosed[inst✝] (f '' ∅)

Tactic:
image_empty,

Goal state after:
case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s = ∅
⊢ IsClosed[inst✝] ∅
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s = ∅
⊢ IsClosed[inst✝] (f '' s)

pp: case inr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s.Nonempty
⊢ IsClosed[inst✝] (f '' s)

Tactic:
· simp_rw [h2s, image_empty, isClosed_empty]

Goal state after:
case inr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s.Nonempty
⊢ IsClosed[inst✝] (f '' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a

Tactic:
← nhdsWithin_univ

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)

Tactic:
rw [ContinuousOn, continuous_iff_continuousAt]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : s ×ˢ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [h, prod_eq_empty_iff.1 h]

Goal state after: