mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
φ : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x)) ⟶ CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))) } =
    { down := A.map g.unop ≫ f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }

Tactic:
congr 1

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
φ : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x)) ⟶ CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))) =
    A.map g.unop ≫ f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ PreservesFiniteLimits colim

Tactic:
apply +allowSynthFailures preservesFiniteLimits_of_preservesHomology
    · exact preservesHomology_of_preservesMonos_and_cokernels _
    · exact additive_of_preservesBinaryBiproducts _

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝² : F'.IsRightKanExtension α
inst✝¹ : HasLimit F
inst✝ : HasLimit F'
i : C
⊢ (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i

Tactic:
by
  rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]

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 : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  α.app p.left ≫
      L.map p.hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
          ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)).app p
hg :
  α.app p.left ≫
      L.map (p.hom ≫ f) ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g) =
    ((restrictedULiftYonedaHomEquiv' A Q X).symm g).app ((CostructuredArrow.map f).obj p)
⊢ ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g

Tactic:
dsimp [restrictedULiftYonedaHomEquiv]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  α.app p.left ≫
      L.map p.hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
          ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)).app p
hg :
  α.app p.left ≫
      L.map (p.hom ≫ f) ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g) =
    ((restrictedULiftYonedaHomEquiv' A Q X).symm g).app ((CostructuredArrow.map f).obj p)
⊢ (α.app p.left ≫ L.map p.hom) ≫
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    (α.app p.left ≫ L.map p.hom) ≫
      L.map f ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g)
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 : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
eq₁ : uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd = uliftYonedaEquiv.symm y.snd
eq₂ :
  (hom
        ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op ≫
          (G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) }) =
    (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) })
⊢ uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y

Tactic:
have eq₃ := ConcreteCategory.congr_hom (CC := fun X ↦ X)
    (congr_app (φ.naturality f.1.unop) _) (ULift.up (𝟙 _))

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 : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
eq₁ : uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd = uliftYonedaEquiv.symm y.snd
eq₂ :
  (hom
        ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).map (F.map (↑f).unop).op ≫
          (G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop y.fst)))))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) }) =
    (hom ((G.map (uliftYonedaEquiv.symm x.snd)).app (op (F.obj (unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op))
      ((hom ((φ.app (unop x.fst)).app (op (F.1 (unop x.fst))))) { down := 𝟙 (unop (op (F.1 (unop x.fst)))) })
eq₃ :
  (hom (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map (↑f).unop ≫ φ.app (unop x.fst)).app (op (F.1 (unop y.fst)))))
      { down := 𝟙 (unop (op (F.1 (unop y.fst)))) } =
    (hom ((φ.app (unop y.fst) ≫ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).map (↑f).unop).app (op (F.1 (unop y.fst)))))
      { down := 𝟙 (unop (op (F.1 (unop y.fst)))) }
⊢ uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ IsIso f ↔ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

Tactic:
constructor
  · intro h
    rw [isIso_iff_yoneda_map_bijective] at h
    intro A _
    exact (h A).2
  · intro hf
    refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
    · exact hf A hA g
    · intro l₁ l₂ h₁ h₂
      rw [← cancel_mono f, h₁, h₂]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
⊢ P.IsCoseparating → P.IsCodetecting

Tactic:
by
  simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x

Tactic:
add_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f x = f x
Module: Mathlib.Order.Circular

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

Tactic:
exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)

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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ = ↑(extensionOfMax i f).toLinearPMap ⟨i m, ?m.544⟩ + 0

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
m : M
⊢ i m ∈ (extensionOfMax i f).domain

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
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ?m.544⟩ + 0 • y

Tactic:
add_zero

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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ = ↑(extensionOfMax i f).toLinearPMap ⟨i m, ?m.544⟩

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
m : M
⊢ i m ∈ (extensionOfMax i f).domain

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
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ?m.544⟩ + 0 • 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
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x + 0 = ↑(extensionOfMax i f).toLinearPMap x

Tactic:
add_zero

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
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x = ↑(extensionOfMax i f).toLinearPMap x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p

Tactic:
succ_le_iff

Goal state after:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 0 < p
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d' + d') = c ^ (2 * (c ^ 2 + d' + d + 1))

Tactic:
congr 1

Goal state after:
case e'_3.e_a
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' + d' = 2 * (c ^ 2 + d' + d + 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
congr 1

Goal state after:
case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' - d = c ^ 2 + (c ^ 2 + d' + d + 1) + 1
Module: Mathlib.Data.Nat.Totient

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

Tactic:
congr 1

Goal state after:
case e_a
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
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 ^ (p ^ (k - 1) * (p - 1) / (p - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
Nat.mul_div_left _ (Nat.sub_pos_of_lt hp.one_lt),

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 ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
have h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1)) := by
    rw [mul_left_comm]
    refine le_mul_of_one_le_right (Nat.zero_le _) ?_
    exact Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt
  simp_rw [Nat.totient_prime_pow hp hk, Nat.primeFactors_prime_pow hk.ne' hp, Finset.prod_singleton,
    Nat.mul_div_left _ (Nat.sub_pos_of_lt hp.one_lt), ← pow_mul]
  rw [Nat.pow_div h hp.pos]
  simp_rw [Nat.sub_mul, one_mul, Nat.mul_sub, mul_one]
  ring_nf

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 c : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b + 1) • p

Tactic:
· rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p + 0

Tactic:
add_zero

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst✝] s
⊢ s ⊆ closure[inst✝] (f '' f ⁻¹' s)

Tactic:
rw [image_preimage_eq_inter_range]
  exact hf.open_subset_closure_inter hs

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
⊢ ↑(toIcoDiv hp a b) * p + toIcoMod hp a b = b

Tactic:
rw [add_comm, toIcoMod_add_toIcoDiv_mul]

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

Tactic:
rw [add_comm, toIcoMod_add_intCast_mul', add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a ≤ b - ↑⌊(b - a) / p⌋ * p ∧ b - ↑⌊(b - a) / p⌋ * p < a + p

Tactic:
← sub_nonneg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - ↑⌊(b - a) / p⌋ * p - a ∧ b - ↑⌊(b - a) / p⌋ * p < a + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ b + ↑⌊(a + p - b) / p⌋ * p ≤ a + p

Tactic:
← sub_nonneg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - (b + ↑⌊(a + p - b) / p⌋ * p)
Module: Mathlib.Topology.Order

Goal state before:
pp: case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y

Tactic:
filter_upwards [hs] with b hb

Goal state after:
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ DenseRange f ↔ Surjective f

Tactic:
rw [DenseRange, dense_discrete, range_eq_univ]

Goal state after:
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

Tactic:
exact ht

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ F.lift' (closure[inst✝] ∘ image f) = F.lift' (image f ∘ closure[inst✝¹])

Tactic:
congr 1

Goal state after:
case e_h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ closure[inst✝] ∘ image f = image f ∘ closure[inst✝¹]
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
⊢ Continuous[inst✝, instTopologicalSpaceProd] fun y ↦ (x, y)

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ Continuous[inst✝¹, instTopologicalSpaceProd] fun x ↦ (x, y)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim inl (inr ∘ inl))

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[inst✝, instTopologicalSpaceSum] (inr ∘ inr)

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[inst✝², instTopologicalSpaceSum] (inl ∘ inl)

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim (inl ∘ inr) inr)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
s : Set α
hs : IsOpen[t] s
⊢ P s

Tactic:
obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs; exact sUnion _ fun b hb ↦ basis _ <| hS hb

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 β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ ContinuousOn (fun b ↦ (a, b)) sβ

Tactic:
by fun_prop

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)
⊢ ContinuousOn (fun a ↦ (a, b)) sα

Tactic:
by fun_prop

Goal state after: