mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (WalkingParallelPairHom.id X✝) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          zero) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          zero) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj zero)

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          one) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          one) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj one)

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one

Tactic:
cat_disch

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)

Tactic:
cat_disch

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

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map (line a✝)

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
cat_disch

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X✝ : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one

Tactic:
cat_disch

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X✝ : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
a✝ : J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
P : ObjectProperty C
X : C
inst✝ : HasProduct (P.productToFamily X)
Y : C
f : X ⟶ Y
hY : P Y
⊢ ∏ᶜ P.productToFamily X ⟶ Y

Tactic:
by
  exact Pi.π (P.productToFamily X) (StructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))

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

Goal state before:
pp: G : GrpCat
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
  · ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]
  · ext
    subsingleton

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

Goal state before:
pp: G : CommGrpCat
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
  · ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]
  · ext
    subsingleton

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

Goal state before:
pp: G H : GrpCat
⊢ ∀ {T : GrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
cat_disch

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

Goal state before:
pp: G H : AddGrpCat
⊢ ∀ {T : AddGrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
cat_disch

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

Goal state before:
pp: G H : CommGrpCat
⊢ ∀ {T : CommGrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
cat_disch

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
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ ∀ (j : F.Elementsᵒᵖ),
    colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        (shrinkYoneda.{w, v₁, u₁} ⋙
                (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op ⋙ colim).map
            f ≫
          ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₂)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₂)).hom =
      colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₁)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₁)).hom ≫
          F.map f

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
⊢ ∃ h, ∀ (x : X), h (f x) = g x
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow * negOnePow 1 = -n.negOnePow

Tactic:
negOnePow_one,

Goal state after:
n : ℤ
⊢ n.negOnePow * -1 = -n.negOnePow
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:
Submodule.coe_sup

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.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
r : R
eq1 : r • y = 0
⊢ r • y ∈ (extensionOfMax i f).domain

Tactic:
rw [eq1]

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
r : R
eq1 : r • y = 0
⊢ 0 ∈ (extensionOfMax i f).domain
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
h : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
by
    obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
    exact ⟨h, DFunLike.congr_fun H⟩

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case basic.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ = A
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

pp: case basic.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

Tactic:
· exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩

Goal state after:
case basic.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop

Tactic:
cases isEmpty_or_nonempty α
  · subsingleton
  cases isEmpty_or_nonempty β
  · subsingleton
  simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

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

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ((a.gcd b / ∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a.gcd b).primeFactors, (p - 1)) *
      ((a * b / ∏ p ∈ (a * b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) *
        ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
shuffle,

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) *
        ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s \ frontier s = interior s

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s \ (closure s \ interior s) = interior s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ frontier s = interior s

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ (closure s \ interior s) = interior s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s = closure s ∩ (interior s)ᶜ

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s \ interior s = closure s ∩ (interior s)ᶜ
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s ⊆ s ↔ IsClosed s

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s \ interior s ⊆ s ↔ IsClosed s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ frontier s = s \ interior s

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ closure s \ interior s = s \ interior s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ frontier s = closure s \ s

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ closure s \ interior s = closure s \ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure[inst✝¹] s
⊢ ContinuousWithinAt f s x

Tactic:
by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
  rw [ContinuousWithinAt, hx]
  exact tendsto_bot

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousWithinAt f {x}ᶜ x

Tactic:
exact continuousWithinAt_of_not_accPt h

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[instTopologicalSpaceSum] Z
⊢ IsClosed[inst✝] (f '' Z)

Tactic:
isClosed_sum_iff

Goal state after:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
⊢ IsClosed[inst✝] (f '' Z)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
simp only [Dense, hb.mem_closure_iff]

Goal state after:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u

Tactic:
rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩

Goal state after:
case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
i : ι
hi : a ∈ U i
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) ⊆ s

Tactic:
· exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ (f ⁻¹' t)ᶜ
⊢ IsBounded (f '' s)

Tactic:
← preimage_compl

Goal state after:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ L ≤ generate (powerset '' l.sets)

Tactic:
le_generate_iff,

Goal state after:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ powerset '' l.sets ⊆ L.sets
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
by
  simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

Goal state after:
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
h : IsLocallyClosed (range f)
⊢ LocallyCompactSpace X

Tactic:
by
  rcases h with ⟨U, Z, hU, hZ, hUZ⟩
  have (x : X) : (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U)
      (fun s ↦ f ⁻¹' (s ∩ Z)) := by
    have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
    rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]
    exact (nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _
  refine .of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_
  rw [hf.isCompact_preimage_iff]
  exacts [hs.inter_right hZ, hUZ ▸ by gcongr]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
    · exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)
    · exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)
  · rintro (x | x) u hxu u_open
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
      exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
      exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Goal state after: