mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseRightKanExtensionAt F' Y

Tactic:
hasPointwiseRightKanExtensionAt_iff_of_natIso_left _ e₁.symm

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L.HasPointwiseRightKanExtensionAt F' Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : StructuredArrow.proj Y L ⋙ F' ≅ StructuredArrow.proj Y L ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((StructuredArrow.proj Y L).obj X)).symm) ⋯
⊢ HasLimit (StructuredArrow.proj Y L ⋙ F')

Tactic:
hasLimit_iff_of_iso e

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : StructuredArrow.proj Y L ⋙ F' ≅ StructuredArrow.proj Y L ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((StructuredArrow.proj Y L).obj X)).symm) ⋯
⊢ HasLimit (StructuredArrow.proj Y L ⋙ F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ (L.lanAdjunction H).unit = L.lanUnit

Tactic:
ext F : 2

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.lanAdjunction H).unit.app F = L.lanUnit.app F
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ (L.ranAdjunction H).counit = L.ranCounit

Tactic:
ext F : 2

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.ranAdjunction H).counit.app F = L.ranCounit.app F
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case e_7
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.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ j = CostructuredArrow.mk j.hom

Tactic:
← CostructuredArrow.eq_mk

Goal state after:
case e_7
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.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ j = j
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 ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ IsIso e.hom ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L

Tactic:
exact ⟨inferInstance, ⟨inferInstance⟩⟩

Goal state after:
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
⊢ ∀ {a b : Subobject A},
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by
    apply Subobject.ind₂
    intro P Q f g hf hg
    refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩
    · exact homMk (Subobject.ofMkLEMk _ _ h)
        ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))
    · simp
    · refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
      exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
hH : ObjectProperty.singleton G G
h : G ⟶ Y
⊢ ∃! h', h' ≫ f = h

Tactic:
exact hf h

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
hH : ObjectProperty.singleton G G
h : X ⟶ G
⊢ ∃! h', f ≫ h' = h

Tactic:
exact hf h

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (coyoneda.obj (op G)).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : G ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : (coyoneda.obj (op G)).obj x✝⁴
⊢ (hom ((coyoneda.obj (op G)).map x✝²)).toFun x✝ = (hom ((coyoneda.obj (op G)).map x✝¹)).toFun x✝

Tactic:
apply hfg

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (yoneda.obj G).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : x✝³ ⟶ G), x✝² ≫ h = x✝¹ ≫ h
x✝ : (yoneda.obj G).obj (op x✝³)
⊢ (hom ((yoneda.obj G).map x✝².op)).toFun x✝ = (hom ((yoneda.obj G).map x✝¹.op)).toFun x✝

Tactic:
apply hfg

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ HasExactLimitsOfShape (Discrete J) AddCommGrpCat

Tactic:
apply +allowSynthFailures hasExactLimitsOfShape_of_preservesEpi

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ lim.PreservesEpimorphisms
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 : ∀ (b : (fun X ↦ X) ((coyoneda.obj (op G)).obj B✝)), ∃! a, (hom ((coyoneda.obj (op G)).map f)) a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Tactic:
exact hf h

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

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

Tactic:
have : x = 1 := Subsingleton.elim _ _

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

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

Tactic:
have : x = 1 := Subsingleton.elim _ _

Goal state after:
case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x
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:
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.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f y = x

Tactic:
hy

Goal state after:
A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ x = x
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
exact negOnePow_odd n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * -c) = 0

Tactic:
h.neg.nat_mul_eq_of_eq_zero hi

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n

Tactic:
have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
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
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
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] (i : ι) → M i
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
choose l hl using fun i ↦ extension_property R _ _ _ f hf ((LinearMap.proj i).comp g)

Goal state after:
R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
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] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
⊢ ∃ h, ∀ (x : X), h (f x) = g x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a

Tactic:
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]

Goal state after:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x} ∪
        {x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) +
      #({x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
intro hap b h

Goal state after:
case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
⊢ p ≤ q → (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) q

Tactic:
hpq

Goal state after:
case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
hpq : p ≤ q
⊢ (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) q
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inl
d d' : ℕ
hn : 2 * (0 ^ 2 + d + 1) ≤ 2 * (0 ^ 2 + d + 1) + d'
⊢ 0 ^ (2 * (0 ^ 2 + d + 1) + d') < (2 * (0 ^ 2 + d + 1) + d' - d)!

Tactic:
simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]

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

Tactic:
toIocMod_add_right

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp a b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ ⊥.lift' closure = ⊥

Tactic:
rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
constructor <;> intro h

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
have not_h₃₂ := (h.trans hIoc₁₃.le).not_gt

Goal state after:
case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
not_h₃₂ : ¬x₃' - p < x₂'
⊢ x₃' ≤ toIocMod hp x₂' x₁
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap (⇑h.symm ∘ ⇑h ∘ f)

Tactic:
exact h.symm.isOpenMap.comp hf

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
mem_comap

Goal state after:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ ∃ t ∈ 𝓝 (f a), f ⁻¹' t ⊆ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ (∃ i, ((x ∈ i.1 ∧ IsOpen[inst✝¹] i.1) ∧ y ∈ i.2 ∧ IsOpen[inst✝] i.2) ∧ i.1 ×ˢ i.2 ⊆ s) ↔
    ∃ u v, IsOpen[inst✝¹] u ∧ x ∈ u ∧ IsOpen[inst✝] v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
by
    simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s✝ s : Set α
⊢ (∃ v ∈ 𝓝ˢ (f '' s✝), f ⁻¹' v ⊆ s) ↔ s ∈ comap f (𝓝ˢ (f '' s✝))

Tactic:
mem_comap

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s✝ s : Set α
⊢ (∃ v ∈ 𝓝ˢ (f '' s✝), f ⁻¹' v ⊆ s) ↔ ∃ t_1 ∈ 𝓝ˢ (f '' s✝), f ⁻¹' t_1 ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ s_1 ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen[generateFrom s] s_1

pp: case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Tactic:
· rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
    exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

Goal state after:
case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

Tactic:
by
  simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ t ≤ generateFrom (range (uncurry b))

Tactic:
rw [le_generateFrom_iff_subset_isOpen]

Goal state after:
case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ range (uncurry b) ⊆ {s | IsOpen[t] s}
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
⊢ y ∈ f ⁻¹' U → y ∈ range (Sigma.mk i)

Tactic:
hy

Goal state after:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst✝] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ y ∈ range (Sigma.mk i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ (fun x ↦ a ↑x) '' T ⊆ t

Tactic:
simp only [image_subset_iff]
    rintro ⟨x, xu⟩ -
    exact hat x xu

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb

Tactic:
refine forall₂_congr fun u hu ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la

Tactic:
rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la