mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = 𝟙 S.opcycles

Tactic:
rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.g ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = S.pOpcycles
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯

Tactic:
simp only [ofMkLE, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
    assoc, Iso.hom_inv_id_assoc]
  congr 1

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso f

Tactic:
← ofMkLEMk_comp h.le,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) ⋯ ≫ 𝟙 Y)
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F, PreservesFiniteLimits F].TFAE

Tactic:
tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_
    apply (KernelFork.isLimitMapConeEquiv _ F).2
    let S := ShortComplex.mk _ _ (kernel.condition f)
    let hS := hF S ⟨exact_kernel f, inferInstance⟩
    have : Mono (S.map F).f := hS.2
    exact hS.1.fIsKernel

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F, PreservesFiniteLimits F].TFAE
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨c⟩ := h F
    exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ (equivShrink (Subobject A)) f ∈ ⇑(equivShrink (Subobject A)) '' s

Tactic:
simpa [Set.mem_image] using hf

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op

Tactic:
by
  rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]

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

Goal state before:
pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (j ⟶ i)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A

pp: case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)

pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_1 ≫ ?refine_2.refine_2 = 𝟙 (kernel (cokernel.π f))

pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_2 ≫ ?refine_2.refine_1 = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := ?refine_2.refine_1, inv := ?refine_2.refine_2, hom_inv_id := ?refine_2.refine_3,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
· exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))

Goal state after:
case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)

case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ ?refine_2.refine_2 = 𝟙 (kernel (cokernel.π f))

case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_2 ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := ?refine_2.refine_2, hom_inv_id := ?refine_2.refine_3,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
⊢ ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
      ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g

Tactic:
intro p

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

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
inst✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (CostructuredArrow S T)

Tactic:
by
  rw [← essentiallySmall_congr
    (CostructuredArrow.pre (equivSmallModel.{w} C).inverse S T).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

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 : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (Subobject.mk f.unop.left.op).arrow.unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ (unop P).hom =
    A.hom

Tactic:
rw [← Category.assoc, ← S.map_comp, ← unop_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : S.Exact
⊢ (S.map colim).Exact

Tactic:
replace hS := fun j => hS.map ((evaluation _ _).obj j)
    simp only [ShortComplex.ab_exact_iff_ker_le_range] at hS ⊢
    intro x (hx : _ = _)
    dsimp at hx
    rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩
    rw [← ConcreteCategory.comp_apply, colimMap_eq, colimit.ι_map, ConcreteCategory.comp_apply,
      ← map_zero (colimit.ι S.X₃ j).hom] at hx
    rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx with ⟨k, e₁, e₂, hk⟩
    rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply]
      at hk
    rcases hS k hk with ⟨t, ht⟩
    use colimit.ι S.X₁ k t
    erw [← ConcreteCategory.comp_apply, colimit.ι_map, ConcreteCategory.comp_apply, ht]
    exact colimit.w_apply S.X₂ e₁ y

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
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map v)) u.snd = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)

Tactic:
← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map v)) u.snd = x
⊢ G.ιColimitType (op u)
      ((ConcreteCategory.hom
          (G.map
            (have this := ⟨v, h⟩;
              this).op))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : GrpCat} (f : X' ⟶ X) (g : X ⟶ (forget GrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
by
        intros
        ext : 1
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't apply this theorem anymore
        apply FreeGroup.ext_hom
        intros
        rfl

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

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

Tactic:
rcases n with n | n
  · simpa only [Int.ofNat_eq_natCast, natCast_zsmul] using h.nsmul n
  · simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

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

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

Tactic:
by
  rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯ + Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)

Tactic:
map_add

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)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) + f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)
Module: Mathlib.Algebra.Group.Nat.Range

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

Tactic:
apply disjoint_range_addLeftEmbedding

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
map_add

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)

pp: case neg
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ motive (p ^ n * a)

Tactic:
· rw [ha1, mul_one]
      exact prime_pow p n hp' hn

Goal state after:
case neg
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ motive (p ^ n * a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).gcd (1 % (n + 1)) = 1

Tactic:
gcd_comm,

Goal state after:
n : ℕ
⊢ (1 % (n + 1)).gcd (n + 1) = 1
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case hf
ι : Type u_1
ι' : Type u_2
⊢ Monotone fun p ↦ p.1 ×ˢ p.2

Tactic:
intro p

Goal state after:
case hf
ι : Type u_1
ι' : Type u_2
p : Finset ι × Finset ι'
⊢ ∀ ⦃b : Finset ι × Finset ι'⦄, p ≤ b → (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∀ x ∈ n.factorization.support, φ (x ^ n.factorization x) = x ^ (n.factorization x - 1) * (x - 1)

Tactic:
intro p

Goal state after:
n : ℕ
hn : n ≠ 0
p : ℕ
⊢ p ∈ n.factorization.support → φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: case refine_2
α : 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 : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)

Tactic:
apply hright

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 : α
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p

Tactic:
by
  rw [toIcoMod, sub_sub_cancel]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed[inst✝] s₁
h₂ : IsClosed[inst✝] s₂
⊢ IsClosed[inst✝] (s₁ ∩ s₂)

Tactic:
← isOpen_compl_iff

Goal state after:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁ᶜ
h₂ : IsOpen[inst✝] s₂ᶜ
⊢ IsOpen[inst✝] (s₁ ∩ s₂)ᶜ
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 : ℤ
⊢ toIcoMod hp (a + -m • p) b = toIcoMod hp a b + -m • p

Tactic:
toIcoMod_add_zsmul'

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝 x ⊓ F).NeBot ↔ ¬𝓝 x ⊓ F = ⊥

Tactic:
neBot_iff

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ 𝓝 x ⊓ F ≠ ⊥ ↔ ¬𝓝 x ⊓ F = ⊥
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C

Tactic:
have : (∃ᶠ z in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ z in 𝓝 x, z ∈ C ∧ z ∈ ({x} : Set X)ᶜ :=
    frequently_inf_principal.trans <| by simp only [and_comm]
  rw [accPt_iff_frequently, this]
  congr! 2
  tauto

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 : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p

Tactic:
exact this

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ ↑(toIocDiv hp a b) * p - b = -toIocMod hp a b

Tactic:
simpa using toIocDiv_zsmul_sub_self hp a b

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
rw [sInf_eq_iInf', sInf_image', induced_iInf]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen[TopologicalSpace.induced (⇑e.symm) t] U ↔ IsOpen[TopologicalSpace.coinduced (⇑e) t] U

Tactic:
rw [isOpen_induced_iff, isOpen_coinduced]

Goal state after:
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen[t] t_1 ∧ ⇑e.symm ⁻¹' t_1 = U) ↔ IsOpen[t] (⇑e ⁻¹' U)
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsClosed[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsClosed[inst✝] s

Tactic:
← isOpen_compl_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsOpen[inst✝] sᶜ
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
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsClosed[induced f t] (f ⁻¹' s)

Tactic:
← isOpen_compl_iff

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)ᶜ
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
    and_true]
  exact fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
by
  refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
  simp only [eventually_nhdsWithin_iff] at h ⊢
  exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}] a = pure a

Tactic:
by
  rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

Goal state after: