mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ (Cone.postcompose
          (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
      (G.mapCone c) ≅
    c.map G

Tactic:
exact Cone.ext (Iso.refl _) (by rintro (_ | _) <;> cat_disch)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
hhp : h ≫ p = 0
s : cokernel g ⟶ cokernel (kernel.ι f)
hs : u ≫ s = p
⊢ p ≫ cokernel.π g ≫ s = p ≫ 𝟙 I

Tactic:
rw [← Category.assoc, hs, Category.comp_id]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
⊢ ∀ (s : Fork prod.snd 0) (m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt),
    m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι → m = s.ι ≫ prod.fst

Tactic:
intro s m h
      have : Mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _)
      apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1
      convert! h
      apply Limits.prod.hom_ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝ : HasImages C
this : HasEqualizers C
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ IsLimit (KernelFork.ofι f ⋯)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝ : HasImages C
this : HasEqualizers C
⊢ IsColimit (CokernelCofork.ofπ f ⋯)

Tactic:
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ IsColimit (CokernelCofork.ofπ f ⋯)
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
by
  congr
  nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm]
  rw [leftCoset_eq_iff, mul_one]
  exact Subgroup.inv_mem _ hb

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
⊢ IsIso (homologyMap φ)

Tactic:
have h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0 := by
    simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality,
      IsIso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
  have ⟨z, hz⟩ := KernelFork.IsLimit.lift' S₁.homologyIsKernel _ h
  dsimp at hz
  refine ⟨⟨z, ?_, ?_⟩⟩
  · rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]
  · rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.snd = g ≫ prod.snd

Tactic:
simp only [prod.lift_snd]

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

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ h.f' = 0

Tactic:
by rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ P.Factors f → Q.Factors f

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ Q.Factors f → P.Factors f

Tactic:
· rintro ⟨i, w⟩
        exact ⟨i ≫ h.hom.hom.left, by rw [Category.assoc, Over.w h.hom.hom, w]⟩

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ Q.Factors f → P.Factors f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ IsZero S.X₂ → S.f = 0 ∧ S.g = 0

Tactic:
intro h
    exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

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

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✝³ : Preadditive C
inst✝² : Preadditive D
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
inst✝ : Epi S.g
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)

Tactic:
by
  have := hS.hasHomology
  have := hS.isIso_fromOpcycles
  exact IsColimit.ofIsoColimit S.opcyclesIsCokernel
    (Cofork.ext (asIso S.fromOpcycles) (by simp))

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
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ (factorThruImage f.hom ≫ Over.Hom.left k.hom) ≫ g.obj.hom = f.hom

Tactic:
rw [assoc, Over.w k.hom]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ factorThruImage f.hom ≫ (image.obj f).obj.hom = f.hom
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobject 0).arrow = 0

Tactic:
rw [← imageSubobject_arrow]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
⊢ (underlyingIso (𝟙 B)).hom = ⊤.arrow

Tactic:
by
  convert! underlyingIso_hom_comp_eq_mk (𝟙 B)
  simp only [comp_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ ((const (StructuredArrow Y L)).obj ((CostructuredArrow.left E).obj Y)).map φ ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    ((CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right) ≫
      (StructuredArrow.proj Y L ⋙ F).map φ

Tactic:
by
        dsimp
        rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]
        congr 1
        apply E.hom.naturality

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
⊢ HasInitial C

Tactic:
let i := wideEqualizer.ι (id : endos → endos)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
⊢ HasInitial C
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 P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso (Hom.right f)).hom) ≫ T.map (Hom.right f) = P.hom ≫ T.map (Hom.right f)

Tactic:
simpa [← T.map_comp] using hq

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ ∀ {a b : Subobject A},
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
apply Subobject.ind₂

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
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
⊢ ∀ {a b : Subobject (op A)},
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
apply Subobject.ind₂

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
⊢ ∀ ⦃A_1 B : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) (g : B ⟶ op A) [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
⊢ Epi (whiskerRight f H)

Tactic:
by
  have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
  apply NatTrans.epi_of_epi_app

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

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

Tactic:
mul_neg,

Goal state after:
n : ℤ
⊢ -(n.negOnePow * 1) = -n.negOnePow
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inl ⟨hcb, hba⟩)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

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

Tactic:
by
  simp +unfoldPartialApp only [Function.onFun]
  simp_rw [Set.disjoint_iff]
  intro m n hmn x hx
  apply hmn
  have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
  have i1 := hx.1.1.trans_le hx.2.2
  have i2 := hx.2.1.trans_le hx.1.2
  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
  exact le_antisymm i1 i2

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

Tactic:
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

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
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
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = (filter (fun x ↦ p x) (range a)).card

Tactic:
←
    multiset_Ico_map_mod n,

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = (filter (fun x ↦ p x) (map (fun x ↦ x % a) (Ico n (n + a)))).card
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: 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 : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
by
    intro a p n hp' hpa hn hPa
    by_cases ha1 : a = 1
    · rw [ha1, mul_one]
      exact prime_pow p n hp' hn
    refine coprime (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) ?_ ?_
      (prime_pow _ _ hp' hn) hPa
    · contrapose! hpa
      simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]
    · simpa [hn, Prime.coprime_iff_not_dvd hp']

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ N (b % n) ≤ b / n

Tactic:
Nat.le_div_iff_mul_le hn.bot_lt,

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ N (b % n) * n ≤ b
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 : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ioc_iff_left, add_right_comm]

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

Tactic:
simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul']

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
ho : ¬IsOpen {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
⊢ False

Tactic:
obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
ho : ¬IsOpen {x}
hU : IsOpen {x}
hne : {x}.Nonempty
hUx : {x} ⊆ {x}
⊢ False
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
refine forall_congr' fun x => ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ closure[inst✝] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : Dense t
hso : IsOpen[inst✝] s
x : X
⊢ x ∈ closure[inst✝] (s ∩ closure[inst✝] t)

Tactic:
by simp [hs.closure_eq, ht.closure_eq]

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

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

Tactic:
simp_rw [btw_coe_iff]

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✝ : α
⊢ toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝ ∨ toIcoMod ⋯ z✝ z✝¹ ≤ toIocMod ⋯ z✝ z✝²
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
m : ℤ
⊢ toIocDiv hp a (b - ↑m * p) = toIocDiv hp a b - m

Tactic:
simpa using toIocDiv_sub_zsmul hp a b m

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

Goal state before:
pp: 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
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ x, IsOpen[inst✝] (q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
← hq.isQuotientMap.isOpen_preimage

Goal state after:
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
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
Module: Mathlib.Topology.Separation.SeparatedNhds

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

Tactic:
suffices sᶜ = (s ∪ t)ᶜ ∪ v from this ▸ hst'.union hv

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
⊢ sᶜ = (s ∪ t)ᶜ ∪ v
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)

Tactic:
rw [induced_generateFrom_eq]
  apply le_generateFrom
  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
  exact h

Goal state after:
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₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[induced f inst✝] s

Tactic:
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩

Goal state after:
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₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ ContinuousOn f univ ↔ Continuous[inst✝¹, inst✝] f

Tactic:
simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
    nhdsWithin_univ]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
rw [← sup_comm, nhdsNE_sup_pure]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
⊢ (s.Nonempty → sᶜ.Finite) → (t.Nonempty → tᶜ.Finite) → (s ∩ t).Nonempty → (s ∩ t)ᶜ.Finite

Tactic:
rintro hs ht ⟨x, hxs, hxt⟩
    rw [compl_inter]
    exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set X
hu : IsClosed[inst✝¹] u
⊢ IsClosed[instTopologicalSpaceSum] (inl '' u)

Tactic:
by
  simpa [isClosed_sum_iff, preimage_image_eq u Sum.inl_injective]

Goal state after: