mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
dsimp [restrictFullyFaithful]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.FactorThru

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ (representative.obj P).Factors f → (representative.obj Q).Factors f

Tactic:
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.FactorThru

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ P.Factors f → Q.Factors f

Tactic:
simp only [factors_iff]
  exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
⊢ ∀ (a b : f ⟶ g), a = b

Tactic:
by
    intro h₁ h₂
    apply InducedCategory.hom_ext
    apply Over.OverMorphism.ext
    rw [← cancel_mono g.arrow, Over.w h₁.hom, Over.w h₂.hom]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ QuasiIso φ ↔ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂

Tactic:
have w : φ.τ₂ ≫ S₂.g = 0 := by rw [φ.comm₂₃, hg₁, zero_comp]
  rw [quasiIso_iff_isIso_liftCycles φ hf₁ hg₁ hf₂]
  constructor
  · intro h
    have : Mono φ.τ₂ := by
      rw [← S₂.liftCycles_i φ.τ₂ w]
      apply mono_comp
    refine ⟨?_, this⟩
    apply exact_of_f_is_kernel
    exact IsLimit.ofIsoLimit S₂.cyclesIsKernel
      (Fork.ext (asIso (S₂.liftCycles φ.τ₂ w)).symm (by simp))
  · rintro ⟨h₁, h₂⟩
    refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩
    · rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]
    · rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ 𝟙 ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).X₂ ≫
      (S.map L).g =
    ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).g ≫
      L.map (Abelian.factorThruCoimage S.g)

Tactic:
by
        dsimp
        rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]

Goal state after:
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
F : C ⥤ H
G : D ⥤ H
α : F ⟶ L ⋙ G
⊢ L.lanUnit.app F ≫ L.whiskerLeft (((L.lanAdjunction H).homEquiv F G).symm α) = α

Tactic:
by simp [lanAdjunction]

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

Goal state before:
pp: case mp
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' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' → IsIso φ

Tactic:
intro
    rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]
    infer_instance

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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
⊢ F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂

Tactic:
let eq := LeftExtension.isUniversalEquivOfIso₂ (LeftExtension.mk _ α₁)
    (LeftExtension.mk _ α₂) e e' h

Goal state after:
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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
⊢ HasExactLimitsOfShape J D

Tactic:
by
  have : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
  refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
  refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)
  apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
  exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ F₁.IsLeftKanExtension α.hom

Tactic:
by
  refine ⟨⟨?_⟩⟩
  apply LeftExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
  refine IsInitial.ofUniqueHom
    (fun y ↦ StructuredArrow.homMk <| α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ?_
  intro y m
  ext x
  simpa using α.inv.app x ≫= congr_app m.w x

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
P : { P // ∃ q, q ≫ T.map P.arrow = A.hom }
⊢ ↑((fun P ↦ ⟨projectSubobject P, ⋯⟩) ((fun P ↦ liftSubobject ↑P ⋯) P)) = ↑P

Tactic:
simp only [liftSubobject, homMk_right, projectSubobject_mk,
      Subobject.mk_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
k : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (line k) ≫
      WalkingParallelFamily.casesOn one ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn zero ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (line k)

Tactic:
simp [w (Classical.arbitrary J) k]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ (parallelFamily f).map (line k) ≫ WalkingParallelFamily.casesOn one (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn zero (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (line k)

Tactic:
simp [w (Classical.arbitrary J) k]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan s
hc : IsLimit c
j : Y ⟶ c.pt
h✝ : Mono j
⊢ f = g

Tactic:
rw [← cancel_mono j]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan s
hc : IsLimit c
j : Y ⟶ c.pt
h✝ : Mono j
⊢ f ≫ j = g ≫ j
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v, u'} D
inst✝³ : HasLimits D
inst✝² : WellPowered.{v, v, u'} D
P : ObjectProperty D
inst✝¹ : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : D ⥤ C
inst✝ : PreservesLimits G
this : ∀ (A : C), HasInitial (StructuredArrow A G)
⊢ G.IsRightAdjoint

Tactic:
exact isRightAdjointOfStructuredArrowInitials _

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

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

Tactic:
rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]

Goal state after:
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₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
f : unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X
⊢ (ConcreteCategory.hom
          (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).map g ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₂).snd)).toFun
      (shrinkYonedaObjObjEquiv.symm f) =
    (ConcreteCategory.hom
          ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₁).snd) ≫
            ((const F.Elementsᵒᵖ).obj (F.obj X)).map g)).toFun
      (shrinkYonedaObjObjEquiv.symm f)

Tactic:
simp [shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ * z₂).val = (Additive.toMul au ^ z₂.val) ^ z₁.val

Tactic:
← pow_mul,

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ * z₂).val = Additive.toMul au ^ (z₂.val * z₁.val)
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ (match ofNat a✝ with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      ofNat a✝ =
    a

Tactic:
rw [Int.ofNat_eq_natCast, Nat.cast_ne_zero] at hn

Goal state after:
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : a✝ ≠ 0
⊢ (match ofNat a✝ with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      ofNat a✝ =
    a
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
simpa only [sub_eq_add_neg] using h.neg_nsmul n x

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ (∃ z, a = b + z • p) ↔ ∃ k, k • p = a - b

Tactic:
eq_sub_iff_add_eq',

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ (∃ z, a = b + z • p) ↔ ∃ k, b + k • p = a
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)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    (RingHom.id R) z1 • ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

Tactic:
← (extensionOfMax i f).toLinearPMap.map_smul

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)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap ((RingHom.id R) z1 • ⟨↑z2 • 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 : ↥(supExtensionOfMaxSingleton i f y)
a : ↥(extensionOfMax i f).domain
r : R
eq1 : ↑x = ↑a + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap a + (extendIdealTo i f h y) r

Tactic:
by
  obtain ⟨a, ha⟩ := a
  have eq2 :
    (ExtensionOfMaxAdjoin.fst i x - a : N) = (r - ExtensionOfMaxAdjoin.snd i x) • y := by
    change x = a + r • y at eq1
    rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul]
      at eq1
  have eq3 :=
    ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
      (by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)
  simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3
  unfold ExtensionOfMaxAdjoin.extensionToFun
  rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]
  congr
  ext
  dsimp
  rw [Subtype.coe_mk, add_sub, ← eq1]
  exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm

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

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (Fintype.card (ZMod n)ˣ)

Tactic:
even_iff_two_dvd,

Goal state after:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ 2 ∣ Fintype.card (ZMod n)ˣ
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') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

Tactic:
← pow_mul,

Goal state after:
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') * c ^ d' = c ^ (2 * (c ^ 2 + d' + d + 1))
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
choose c hleft hright using exists_ge_ge (α := α)

Goal state after:
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
by
  simpa using tendsto_iff_seq_tendsto (f := id) (l := 𝓟 {x | p x})

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

Goal state before:
pp: case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
⊢ False

Tactic:
rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'

Goal state after:
case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : 2 = 1
ha' : ¬a = 0
h : 2 * a = b
⊢ False
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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < - -b - -(toIcoDiv hp a (-b) • p)
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
neg_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < b - -(toIcoDiv hp a (-b) • p)
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
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 : α
hc : - -b - -(toIcoDiv hp a (-b) • p) ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
neg_neg,

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

Tactic:
neg_neg,

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

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

Tactic:
neg_neg,

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

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

Tactic:
neg_neg,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (𝓟 {a}).lift' h = 𝓟 (h {a})

Tactic:
lift'_principal hh

Goal state after:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ 𝓟 (h {a}) = 𝓟 (h {a})
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ (𝓟 ∅).lift' h = 𝓟 (h ∅)

Tactic:
lift'_principal hh

Goal state after:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ 𝓟 (h ∅) = 𝓟 (h ∅)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = frontier s

Tactic:
by
  simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

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

Goal state before:
pp: case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False

Tactic:
(modEq_iff_toIcoMod_eq_left hp).1 h

Goal state after:
case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
⊢ ∀ (m : ℕ), x ∈ v m → x ∈ closure[inst✝] (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
intro m xinvm

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
⊢ x ∈ closure[inst✝] (⋃ m' ∈ {m' | m' ≤ m}, u m')
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update pure a₀ l b

Tactic:
by
  refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_
  rcases eq_or_ne a a₀ with (rfl | ha)
  · filter_upwards [hs] with b hb
    rcases eq_or_ne b a with (rfl | hb)
    · exact hs
    · rwa [update_of_ne hb]
  · simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ induced f (induced g inst✝) = induced (g ∘ f) inst✝

Tactic:
induced_compose

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ induced (g ∘ f) inst✝ = induced (g ∘ f) inst✝
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
by rw [nhds_discrete, mem_pure]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
⊢ {x} ∈ 𝓝 x ↔ 𝓝 x = pure x

Tactic:
simp [le_antisymm_iff, pure_le_nhds x]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology α ↔ ∃ x y, ¬Inseparable x y

Tactic:
simpa using indiscrete_iff_forall_inseparable.not

Goal state after: