mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ (coyoneda.obj (op G)).map x✝¹ = (coyoneda.obj (op G)).map x✝

Tactic:
ext

Goal state after:
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✝
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
⊢ (yoneda.obj G).map x✝¹.op = (yoneda.obj G).map x✝.op

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ G = X ∨ H = X ↔ ∃ i, WalkingPair.rec G H i = X

Tactic:
constructor

Goal state after:
case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

case e'_2.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ (∃ i, WalkingPair.rec G H i = X) → G = X ∨ H = X
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ G = X ∨ H = X ↔ ∃ i, WalkingPair.rec G H i = X

Tactic:
constructor

Goal state after:
case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

case e'_2.mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ (∃ i, WalkingPair.rec G H i = X) → G = X ∨ H = X
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
⊢ Function.Surjective (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i })))

Tactic:
refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
b : ↑(AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })))
⊢ (Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) fun i ↦ ⋯.choose) = b
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_2
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : X ⟶ G
⊢ f = default

Tactic:
ext

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

Goal state before:
pp: case refine_2
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : X ⟶ G
⊢ f = default

Tactic:
ext

Goal state after:
case refine_2
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : X ⟶ G
x✝ : ↑X
⊢ (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
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Bijective ((Discrete.functor F).descColimitType c)

Tactic:
constructor

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Injective ((Discrete.functor F).descColimitType c)

case right
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Surjective ((Discrete.functor F).descColimitType c)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝

Tactic:
ext

Goal state after:
X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝)))
      x✝ =
    (Hom.hom
        (free.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝))
      x✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
⊢ Mono (free.map f)

Tactic:
constructor

Goal state after:
case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
⊢ ∀ {Z : AddCommGrpCat} (g h : Z ⟶ free.obj X), g ≫ free.map f = h ≫ free.map f → g = h
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X : Type u
⊢ Nonempty (IsInitial X) ↔ IsEmpty X

Tactic:
constructor

Goal state after:
case mp
X : Type u
⊢ Nonempty (IsInitial X) → IsEmpty X

case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial 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:
constructor

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

case mpr
X Y : Type u
c : BinaryCofan X Y
⊢ Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr)) →
    Nonempty (IsColimit c)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
⊢ ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm (f✝ ≫ g✝) =
    abelianize.map f✝ ≫
      ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝

Tactic:
ext

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝ =
    (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      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
X : C
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
m : ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).fst ⟶ u.fst
hm :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map m))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd
⊢ ⟨m, hm⟩ = ⟨shrinkYonedaObjObjEquiv u.snd, ⋯⟩

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
m : ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).fst ⟶ u.fst
hm :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map m))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd
⊢ ↑⟨m, hm⟩ = ↑⟨shrinkYonedaObjObjEquiv u.snd, ⋯⟩
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
constructor

Goal state after:
case mp
n : ℤ
⊢ n.negOnePow = 1 → Even n

case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
constructor

Goal state after:
case mp
n : ℤ
⊢ n.negOnePow = -1 → Odd n

case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIcc a b)ᶜ = cIoo b a

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ x✝ ∈ cIcc b a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d

case inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d

case inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d

case inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d

case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c ∧ c < a

Tactic:
constructor

Goal state after:
case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c

case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d

case inr.inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d

case inr.inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d

case inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d

case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)

Tactic:
simpa only [sub_eq_add_neg, Periodic] using h.sub_eq

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c ∧ c < a

Tactic:
constructor

Goal state after:
case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c

case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
constructor

Goal state after:
case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d

case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c ∧ c < a

Tactic:
constructor

Goal state after:
case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c

case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a ∧ a < d

Tactic:
constructor

Goal state after:
case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a

case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
by
  rcases a with ⟨_, m, rfl⟩
  simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ -f (x + ↑n * (2 * c)) = -f x

Tactic:
h.nat_even_mul_periodic

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ -f x = -f x
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
x✝² x✝¹ : ExtensionOf i f
x✝ : x✝².toLinearPMap = x✝¹.toLinearPMap
⊢ x✝² = x✝¹

Tactic:
ext

Goal state after:
case domain_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
⊢ x✝ ∈ x✝³.domain ↔ x✝ ∈ x✝².domain

case to_fun_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
ha✝ : x✝ ∈ x✝³.domain
hb✝ : x✝ ∈ x✝².domain
⊢ ↑x✝³.toLinearPMap ⟨x✝, ha✝⟩ = ↑x✝².toLinearPMap ⟨x✝, hb✝⟩
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case e_a
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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ fst i x = ⟨a + (r • y - snd i x • y), ⋯⟩

Tactic:
ext

Goal state after:
case e_a
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 : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = ↑⟨a + (r • y - snd i x • y), ⋯⟩
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
disjoint_left,

Goal state after:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → a_1 ∉ map (addLeftEmbedding a) s
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
this : ∃ x < n + 1, (n + 1).gcd x = 1
⊢ φ (n + 1) = 0 ↔ n + 1 = 0

Tactic:
simpa [totient, filter_eq_empty_iff]

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
have : NeZero (m * n) := ⟨hmn0⟩

Goal state after:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
Module: Mathlib.Data.Nat.Totient

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

Tactic:
constructor

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

case mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
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)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)

Tactic:
constructor

Goal state after:
case mp
α : 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)

case mpr
α : 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 ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: m n : ℕ
⊢ (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
constructor

Goal state after:
case mp
m n : ℕ
⊢ (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
⊢ ∃ x, Tendsto x atTop f

Tactic:
by
  obtain ⟨B, h⟩ := f.exists_antitone_basis
  choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
  exact ⟨x, h.tendsto hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
rw [tendsto_inf, tendsto_principal] at hx

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l