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 F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ (unitForward η X ∘ unitBackward η X) x = id x

Tactic:
by simp [unitForward, unitBackward]

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₀
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)

Tactic:
by
    let u : L'.LeftExtension F₁ :=
      mk y.right <|
        hα.desc <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom
    refine
      ⟨⟨StructuredArrow.homMk (hb.desc u) <| by
          ext x
          have hb_fac_app := congr_app (hb.fac u) (L.obj x)
          have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]⟩, fun a => ?_⟩
    dsimp
    ext1
    apply hb.hom_ext
    apply hα.hom_ext
    ext t
    dsimp
    have a_w_t := congr_app a.w t
    have hb_fac_app := congr_app (hb.fac u) (L.obj t)
    have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t
    dsimp at hb_fac_app hα_fac_app
    simp only [whiskeringLeft_obj_obj, comp_obj,
      precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app,
      precomp₂_obj_hom_app, whiskerLeft_app, assoc] at a_w_t
    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
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
by
    have := hm (L.obj j)
    nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)]
    dsimp at this ⊢
    rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default

Tactic:
rw [← cancel_epi e]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ e ≫ a = e ≫ default
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ Subobject A → Subobject A.right

Tactic:
refine Subobject.lift (fun P f hf => Subobject.mk f.right) ?_
  intro P Q f g hf hg i hi
  refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) ?_
  exact congr_arg CommaMorphism.right hi

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
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
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (p ≫ presheafHom φ P ≫ F.op.whiskerLeft (G.map f)) = uliftYonedaEquiv ((p ≫ f) ≫ presheafHom φ Q)

Tactic:
uliftYonedaEquiv_ι_presheafHom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
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
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (p ≫ presheafHom φ P ≫ F.op.whiskerLeft (G.map f)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
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
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ (hom ((F.op.whiskerLeft (G.map f)).app (op X))) (uliftYonedaEquiv (p ≫ presheafHom φ P)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })

Tactic:
uliftYonedaEquiv_ι_presheafHom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
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
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ (hom ((F.op.whiskerLeft (G.map f)).app (op X)))
      ((hom ((G.map p).app (op (F.obj X))))
        ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Tactic:
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCoseparator (op G) ↔ IsSeparator G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))

Tactic:
apply IsTerminal.ofIso Over.mkIdTerminal

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
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 ((2 * n) • c)

Tactic:
mul_comm,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((n * 2) • c)
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total b c with hbc | hcb

Goal state after:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total b c with hbc | hcb

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

Tactic:
simp [Nat.zero_dvd.1 hm]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n

Tactic:
exact (card_filter_le _ _).trans_eq (card_range _)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k ↦ p (k + b)) a + count p b

Tactic:
rw [add_comm, count_add, add_comm]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k ↦ p (b + k)) a + count p b = count (fun k ↦ p (k + b)) a + count p b
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a + a * (n / a))

Tactic:
mul_comm,

Goal state after:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a + n / a * a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ (p - 1) * p ^ n = 1 * p ^ n * (p - 1)

Tactic:
one_mul,

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ (p - 1) * p ^ n = p ^ n * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
mul_comm,

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p * (p ^ (n.factorization p - 1) * (p - 1)) = p ^ n.factorization p * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ (n * ∏ p ∈ n.primeFactors, (p - 1)) / ∏ p ∈ n.primeFactors, p =
    (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

pp: n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p

Tactic:
mul_comm,

Goal state after:
n : ℕ
⊢ (∏ p ∈ n.primeFactors, (p - 1)) * n / ∏ p ∈ n.primeFactors, p =
    (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = 1 * ↑p - (↑p)⁻¹ * ↑p

Tactic:
one_mul,

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - (↑p)⁻¹ * ↑p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - (↑p)⁻¹ * ↑p

Tactic:
mul_comm,

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - ↑p * (↑p)⁻¹
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 * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))

Tactic:
mul_comm,

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.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d

Tactic:
mul_comm,

Goal state after:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d
Module: Mathlib.Data.Nat.Totient

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

Tactic:
refine lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))

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

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)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
mul_comm,

Goal state after:
case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (p * a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * (p * k - 1 * k - 1))

Tactic:
one_mul,

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * (p * k - k - 1))
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 : α
⊢ toIocMod hp a a = a + p

Tactic:
by
  rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]
  exact ⟨lt_add_of_pos_right _ hp, -1, by simp⟩

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 : α
⊢ toIcoDiv hp a b • p = toIocDiv hp a b • p + p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
← add_one_zsmul,

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

Tactic:
← add_one_zsmul,

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

Tactic:
convert! sub_le_iff_le_add.mp hr using 1

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
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p
Module: Mathlib.Topology.Order

Goal state before:
pp: case inl
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen[generateFrom s] t

pp: case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t

Tactic:
· exact ht

Goal state after:
case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t
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 X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsEmbedding g
⊢ IsInducing f ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f

Tactic:
hg.injective.of_comp_iff f

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)

Tactic:
by
  rw [h.nhds_eq_comap, h.apply_symm_apply]

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
haveI := ta2

Goal state after:
X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
⊢ Sort ?u.37
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure[inst✝] (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[≠] z, x ∈ s

Tactic:
simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty Z
inst✝ : Nonempty W
f : Z → X
g : W → Y
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g) ↔
    Continuous[inst✝³, inst✝⁵] f ∧ Continuous[inst✝², inst✝⁴] g

Tactic:
by
  simp [continuous_iff_continuousAt, forall_and]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (s.domRestrict f) (𝓝 ⟨a, h⟩) l

Tactic:
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 ⟨a, h⟩) l ↔ Tendsto (s.domRestrict f) (𝓝 ⟨a, h⟩) l
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
← x.eta

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 ↦ f ((x.1, x.2).1, x_1)) {b | ((x.1, x.2).1, b) ∈ s} (x.1, x.2).2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
← x.eta

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 ↦ f (x_1, (x.1, x.2).2)) {a | (a, (x.1, x.2).2) ∈ s} (x.1, x.2).1
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
y : β
⊢ y ∈ sβ → f a y = g y

Tactic:
simp [g]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
y : α
⊢ y ∈ sα → f y b = g y

Tactic:
simp [g]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
← continuousOn_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ ContinuousOn f univ
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
⊢ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Goal state after:
case inl
α : Type u_2
x✝ : Bornology α
h : ∀ x ∈ ∅, IsBounded ∅
⊢ IsBounded ∅

case inr
α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
x : α
hx : x ∈ s
⊢ IsBounded s
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 : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)

Tactic:
rw [subset_compl_comm, ← preimage_compl] at hts

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)