mathlib-initiative/mathlib-tactics huggingface dataset:
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 : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop

Tactic:
conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op f.unop.left]
  rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : x✝² ⟶ c.pt), x✝¹ ≫ h = x✝ ≫ h
b : β
g : x✝² ⟶ f b
⊢ x✝¹ ≫ g = x✝ ≫ g

Tactic:
classical simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b

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
⊢ f = default

Tactic:
ext x

Goal state after:
case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
⊢ (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
⊢ f = default

Tactic:
ext x

Goal state after:
case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
⊢ (Hom.hom f) x = (Hom.hom default) x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₁ = F i₂

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : Cocone (Functor.empty (Type u))
x✝¹ :
  { pt := PEmpty.{u + 1},
        ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt ⟶
    x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    { pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        x✝¹ =
      x✝².ι.app j
⊢ x✝¹ = ↾fun x ↦ PEmpty.elim x

Tactic:
ext x

Goal state after:
C : Type u
F : C → Type v
x✝² : Cocone (Functor.empty (Type u))
x✝¹ :
  { pt := PEmpty.{u + 1},
        ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt ⟶
    x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    { pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        x✝¹ =
      x✝².ι.app j
x :
  { pt := PEmpty.{u + 1},
      ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt
⊢ (ConcreteCategory.hom x✝¹).toFun x = (ConcreteCategory.hom (↾fun x ↦ PEmpty.elim x)).toFun x
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
⊢ (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
      (coconeπOpCompShrinkYonedaObj F Y).ι.app u =
    (coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).obj X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
            (coconeπOpCompShrinkYonedaObj F Y).ι.app u)).toFun
      x =
    (ConcreteCategory.hom
          ((coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f)).toFun
      x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
⊢ (c.inl ≫
      ↾fun x ↦
        if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
          (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
        else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
    f

Tactic:
ext x

Goal state after:
case mpr.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := left }
⊢ (ConcreteCategory.hom
          (c.inl ≫
            ↾fun x ↦
              if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))).toFun
      x =
    (ConcreteCategory.hom f).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
⊢ (c.inr ≫
      ↾fun x ↦
        if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
          (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
        else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
    g

Tactic:
ext x

Goal state after:
case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ (ConcreteCategory.hom
          (c.inr ≫
            ↾fun x ↦
              if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))).toFun
      x =
    (ConcreteCategory.hom g).toFun x
Module: Mathlib.Algebra.Category.ModuleCat.Injective

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
ext x

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
⊢ m =
    ↾fun x ↦
      if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
      else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)

Tactic:
ext x

Goal state after:
case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ (ConcreteCategory.hom m).toFun x =
    (ConcreteCategory.hom
          (↾fun x ↦
            if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
              (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
            else
              (ConcreteCategory.hom (c.inr ≫ m))
                ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))).toFun
      x
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ a + ↑(b - a).toNat = b

Tactic:
toNat_sub_of_le h,

Goal state after:
a b : ℤ
h : a ≤ b
⊢ a + (b - a) = b
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ b - ↑(b - a).toNat = a

Tactic:
toNat_sub_of_le h,

Goal state after:
a b : ℤ
h : a ≤ b
⊢ b - (b - a) = a
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: 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

Tactic:
ext x

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⟩
x : ↥I
⊢ ((LinearMap.lcomp R M (Submodule.subtype I)) g') x = g x
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))

Tactic:
Set.disjoint_iff

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Disjoint (Ico (a * b ^ x) (a * b ^ (x + 1))) (Ico (a * b ^ y) (a * b ^ (y + 1)))

Tactic:
Set.disjoint_iff

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)

Tactic:
simp only [← Set.inter_assoc, Set.inter_comm _ A]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)

Tactic:
ext x

Goal state after:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
m n : ℕ
⊢ φ m = 1 ∨ φ n = 1 → (φ m).Coprime (φ n)

Tactic:
rintro (h | h) <;> rw [h]

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)

case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ atTop.IsCountablyGenerated

Tactic:
rw [← prod_atTop_atTop_eq]
  infer_instance

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

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

Tactic:
intro a1

Goal state after:
a b a1 : ℕ
⊢ ∀ (a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
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

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) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * 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 : α
⊢ a - 0 • p ∈ Set.Ico a (a + p)

Tactic:
simp [hp]

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 : α
⊢ a - -1 • p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]

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 : α
⊢ a + p - 1 • p ∈ Set.Ico a (a + p)

Tactic:
simp [hp]

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 : α
⊢ a + p - 0 • p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]

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 : α
m : ℤ
⊢ toIcoDiv hp a b - -m = toIcoDiv hp a b + m

Tactic:
sub_neg_eq_add

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

Tactic:
sub_neg_eq_add

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

Tactic:
← sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-a - p) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ DirectedOn (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) f.sets

Tactic:
intro t₁ ht₁ t₂ ht₂
    exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩

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 : α
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n, c - b = n • p

Tactic:
by
  refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩
  · conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]
    rw [h, sub_smul]
    abel
  · rcases h with ⟨z, hz⟩
    rw [sub_eq_iff_eq_add] at hz
    rw [hz, toIcoMod_zsmul_add]

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
  · rintro U U_op ⟨x, x_in⟩
    exact mem_closure_iff.1 (h _) U U_op x_in
  · intro x
    rw [mem_closure_iff]
    intro U U_op x_in
    exact h U U_op ⟨_, x_in⟩

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: α : Type u_1
F : Filter α
inst✝ : TopologicalSpace α
a : α
⊢ MapClusterPt a F id ↔ ClusterPt a F

Tactic:
by
  rw [MapClusterPt, map_id]

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 : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
exact h.2.1 ((toIcoMod_inj _).1 <| h₁₃₂.antisymm h₁₂₃)

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

Goal state before:
pp: case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h : btw (↑z✝¹) (↑z✝) x₃
⊢ btw (↑z✝) x₃ ↑z✝¹

Tactic:
induction x₃ using QuotientAddGroup.induction_on

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h : btw ↑z✝² ↑z✝¹ ↑z✝
⊢ btw ↑z✝¹ ↑z✝ ↑z✝²
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ x₄ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h₂₃₄ : btw (↑z✝) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝
h₁₂₃ : btw (↑z✝¹) (↑z✝) x₃ ∧ ¬btw x₃ ↑z✝ ↑z✝¹
⊢ btw (↑z✝¹) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝¹

Tactic:
induction x₃ using QuotientAddGroup.induction_on

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₄ : α ⧸ AddSubgroup.zmultiples p
z✝² z✝¹ z✝ : α
h₂₃₄ : btw (↑z✝¹) x₄ ↑z✝ ∧ ¬btw (↑z✝) x₄ ↑z✝¹
h₁₂₃ : btw ↑z✝² ↑z✝¹ ↑z✝ ∧ ¬btw ↑z✝ ↑z✝¹ ↑z✝²
⊢ btw (↑z✝²) x₄ ↑z✝ ∧ ¬btw (↑z✝) x₄ ↑z✝²
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
h₁₂₃ : btw (↑z✝¹) (↑z✝) x₃
h₃₂₁ : btw x₃ ↑z✝ ↑z✝¹
⊢ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = x₃ ∨ x₃ = ↑z✝¹

Tactic:
induction x₃ using QuotientAddGroup.induction_on

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : btw ↑z✝² ↑z✝¹ ↑z✝
h₃₂₁ : btw ↑z✝ ↑z✝¹ ↑z✝²
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : α ⧸ AddSubgroup.zmultiples p
z✝¹ z✝ : α
⊢ btw (↑z✝¹) (↑z✝) x₃ ∨ btw x₃ ↑z✝ ↑z✝¹

Tactic:
induction x₃ using QuotientAddGroup.induction_on

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
⊢ btw ↑z✝² ↑z✝¹ ↑z✝ ∨ btw ↑z✝ ↑z✝¹ ↑z✝²
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
⊢ g ⁻¹' q '' V = U

Tactic:
ext x

Goal state after:
case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : C
⊢ x ∈ g ⁻¹' q '' V ↔ x ∈ U
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ closure[inst✝] s = f ⁻¹' closure[inst✝¹] (f '' s)

Tactic:
ext x

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst✝] s ↔ x ∈ f ⁻¹' closure[inst✝¹] (f '' s)
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
⊢ Continuous[t₂, t₃] f

Tactic:
rw [continuous_iff_le_induced] at h₂ ⊢

Goal state after:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (id '' s)

Tactic:
rwa [image_id]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] (id '' s)

Tactic:
rwa [image_id]

Goal state after: