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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
rw [h.comm₁]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
rw [h.comm₁]

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯

Tactic:
by
    rw [H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl, zero_comp]

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).Exact

Tactic:
by
  have := h.hasHomology
  exact h.map_of_preservesLeftHomologyOf F

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
⊢ i.essImage A

Tactic:
let η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
⊢ i.essImage A
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ Mono (ofMkLE f X h)

Tactic:
dsimp only [ofMkLE]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ Mono ((underlyingIso f).inv ≫ (mk f).ofLE X h)
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject Y
⊢ (map e.hom).obj ((map e.inv).obj g) = g

Tactic:
simp_rw [← map_comp, e.inv_hom_id, map_id]

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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Mono f
S : ShortComplex C := { X₁ := X, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }
⊢ Mono (F.map f)

Tactic:
exact ((S.map F).exact_iff_mono (by simp [S])).1
      (((S.exact_iff_mono rfl).2 hf).map F)

Goal state after:
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.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (L ⋙ L.pointwiseRightKanExtension F).map f ≫
      limit.π (StructuredArrow.proj (L.obj X₂) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f

Tactic:
simp only [comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]
    rw [comp_id]
    let φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) :=
      StructuredArrow.homMk f
    exact (limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

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

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Tactic:
refine ⟨m + 1, ?_⟩

Goal state after:
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ j ≤ sequentialFunctor_obj J (m + 1)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, sequentialFunctor_obj J n ≤ j

Tactic:
refine ⟨m + 1, ?_⟩

Goal state after:
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ sequentialFunctor_obj J (m + 1) ≤ j
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✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ (colimit.ι F j).app d ≫
      (colim ⋙ (evaluation D C).obj d).map η ≫
        (colimitObjIsoColimitCompEvaluation G d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom =
    (colimit.ι F j).app d ≫
      (colimitObjIsoColimitCompEvaluation F d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (colimit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η

Tactic:
by simp [← NatTrans.comp_app_assoc]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ ∀ {X Y : WalkingParallelFamily J} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map f

Tactic:
rintro _ _ (_ | _) <;> cat_disch

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

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

Tactic:
rintro _ _ (_ | _) <;> cat_disch

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

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

Tactic:
rintro _ _ (_ | _) <;> cat_disch

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj (op G)).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
· rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
    exact hf h

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
by
  classical
    constructor
    · rintro ⟨h⟩
      rw [← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,
        ← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]
      dsimp [binaryCoproductCocone]
      refine
        ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩
      rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp]
      dsimp
      rw [Set.range_comp _ Sum.inr, ← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
      simp
    · rintro ⟨h₁, h₂, h₃⟩
      have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
        rw [eq_compl_iff_isCompl.mpr h₃.symm]
        exact fun _ => or_not
      refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩
      · intro T f g
        refine ↾fun x => ?_
        exact
          if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
          else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
      · intro T f g
        ext x
        simp
      · intro T f g
        ext x
        dsimp
        simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff,
          forall_exists_index]
        intro y e
        have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
        rw [disjoint_iff.mp h₃.1] at this
        exact this.elim
      · rintro T _ _ m rfl rfl
        ext x
        simp only [TypeCat.Fun.toFun_apply, Functor.const_obj_obj, pair_obj_left, Set.mem_range,
          comp_apply, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
        split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
⊢ ∃ a, (LinearMap.lcomp R M (Submodule.subtype I)) a = g

Tactic:
use g'

Goal state after:
case h
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
⊢ (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
use g'

Goal state after:
case h
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
⊢ ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)

Tactic:
exact h.periodic.zsmul n

Goal state after:
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 ↦ Ioc (↑n) (↑n + 1))

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

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

Goal state before:
pp: case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)

Tactic:
rw [ha1, mul_one]

Goal state after:
case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
| #({x ∈ Ico k (k + n) | a.Coprime x})

Tactic:
← Nat.mod_add_div n a

Goal state after:
a k n : ℕ
a_ne_zero : a ≠ 0
| #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x})
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

Tactic:
by
  induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
intro N

Goal state after:
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg.refine_2
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ (a * p * d)

Tactic:
exact totient_pos.mpr <| zero_lt_of_ne_zero (by rwa [mul_assoc])

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

Goal state before:
pp: n : ℕ
hn : 0 < n
this : (∏ p ∈ n.primeFactors, p) ^ φ n ∣ n ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
← Finset.prod_pow

Goal state after:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
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 (m • p + b) = m + toIcoDiv hp a b

Tactic:
rw [add_comm, toIcoDiv_add_zsmul, add_comm]

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
inter_eq_self_of_subset_right interior_subset_closure

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = interior s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : Dense t
hso : IsOpen[inst✝] s
x : X
⊢ x ∈ closure[inst✝] (s ∩ closure[inst✝] t)

Tactic:
simp [hs.closure_eq, ht.closure_eq]

Goal state after:
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
m : ℤ
⊢ toIcoDiv hp (a - ↑m * p) b = toIcoDiv hp a b + m

Tactic:
by
  simpa using toIcoDiv_sub_zsmul' hp a b m

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝¹, inst✝²] f
hg : Continuous[inst✝², inst✝] g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝¹

Tactic:
hgf.eq_induced,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝¹, inst✝²] f
hg : Continuous[inst✝², inst✝] g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ induced (g ∘ f) inst✝
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))

Tactic:
rw [mem_nhds_induced, mem_comap]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ Continuous[nhdsAdjoint a l, inst✝] f ↔ Tendsto f l (𝓝 (f a))

Tactic:
by
  simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = ⨅ i, comap (fun x ↦ x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Tactic:
by
  simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
    iInf_principal_finite hI, ← iInf_inf_eq]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s

Tactic:
intro x xs
  rcases h x xs with ⟨t, open_t, xt, ct⟩
  have := ct x ⟨xs, xt⟩
  rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
by
  ext; simp +contextual [mem_nhdsWithin_iff_eventually, hf.nhds_eq_comap, forall_comm (α := _ ∈ _)]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
refine mem_nhdsSetWithin.2 ⟨w, hw.1, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' t ⊆ w

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)

Tactic:
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, a ∈ U i

pp: case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u

Tactic:
· exact fun i hi ↦ (hU i hi).2

Goal state after:
case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)

Tactic:
by
  simp only [isEmbedding_iff, isInducing_sigmaMap h, forall_and,
    h.sigma_map_iff]

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✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : SigmaCompactSpace X
inst✝ : SigmaCompactSpace Y
⊢ ⋃ n, (fun n ↦ compactCovering X n ×ˢ compactCovering Y n) n = univ

Tactic:
simp only [iUnion_prod_of_monotone (compactCovering_subset X) (compactCovering_subset Y),
        iUnion_compactCovering, univ_prod_univ]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : SigmaCompactSpace X
inst✝ : SigmaCompactSpace Y
⊢ ⋃ n, (fun n ↦ Sum.inl '' compactCovering X n ∪ Sum.inr '' compactCovering Y n) n = univ

Tactic:
simp only [iUnion_union_distrib, ← image_iUnion, iUnion_compactCovering, image_univ,
        range_inl_union_range_inr]

Goal state after: