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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂.τ₂ - φ₄.τ₂)

Tactic:
comp_sub,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂.τ₂ - φ₄.τ₂)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ S₁.g ≫ h.h₃ = 0

Tactic:
h.g_h₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ 0 = 0
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
S : ShortComplex C
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapHomologyIso' F = S.mapHomologyIso F

Tactic:
ext
  rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]
  dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso,
    leftHomologyIso, LeftHomologyData.leftHomologyIso]
  simp only [RightHomologyData.map_H, rightHomologyMapIso'_inv, rightHomologyMapIso'_hom, assoc,
    Functor.map_comp, RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
    Functor.map_id, LeftHomologyData.map_H, leftHomologyMapIso'_inv, leftHomologyMapIso'_hom,
    LeftHomologyData.map_leftHomologyMap', ← rightHomologyMap'_comp_assoc, ← leftHomologyMap'_comp,
    id_comp]
  have γ : HomologyMapData (𝟙 (S.map F)) (map S F).homologyData (S.homologyData.map F) := default
  have eq := γ.comm
  rw [← γ.left.leftHomologyMap'_eq, ← γ.right.rightHomologyMap'_eq] at eq
  dsimp at eq
  simp only [← reassoc_of% eq, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]

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

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : (ConcreteCategory.hom f) y ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ (ConcreteCategory.hom g) (Classical.choose h) = (ConcreteCategory.hom g).toFun y

Tactic:
rw [mono_iff_injective] at mono
        simp [mono (Classical.choose_spec h)]

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✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ x₂ = 0

Tactic:
rw [← hx₁, this, zero_comp]

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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f ≫ (𝟙 S.X₂ - S.g ≫ s) = 𝟙 S.X₁ ≫ S.f

Tactic:
comp_sub,

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f ≫ 𝟙 S.X₂ - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)

Tactic:
exact ⟨MonoOver.leInf _ _ _ k l⟩

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

Goal state before:
pp: case insert.inl
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
s✝ : Finset I
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
a✝ : j ∉ s✝
⊢ (P j ⊔ s✝.sup P).Factors f

Tactic:
exact sup_factors_of_factors_left h

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
f : Fan Z
hf : IsLimit f
e : (Discrete.functor fun x ↦ Opposite.op (Z x)) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
  Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Opposite.op (Z x)).obj x)
⊢ IsColimit f.op

Tactic:
refine IsColimit.ofIsoColimit ((IsColimit.precomposeHomEquiv e _).2
    (IsColimit.whiskerEquivalence hf.op (Discrete.opposite α).symm))
    (Cocone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
f : Fan Z
hf : IsLimit f
e : (Discrete.functor fun x ↦ Opposite.op (Z x)) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
  Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Opposite.op (Z x)).obj x)
x✝ : Discrete α
a : α
⊢ ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).ι.app { as := a } ≫
      (Iso.refl
          ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).pt).hom =
    f.op.ι.app { as := a }
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
L' : C ⥤ D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
revert L L' e
  suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y],
      HasPointwiseLeftKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
  intro L L' e _
  let Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso _ e.symm
  let e' : CostructuredArrow.proj L' Y ⋙ F ≅
    Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F := Iso.refl _
  exact hasColimit_of_iso e'

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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso_left F eL,
    hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]

Goal state after:
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j

Tactic:
simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
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
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j

Tactic:
simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
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
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case w
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
⊢ (isoMk (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)) ⋯).hom ≫ f =
    homMk (projectSubobject (Subobject.mk f)).arrow hq

Tactic:
· exact ext _ _ (by simp)

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h

Tactic:
ht (i ≫ g) (Category.assoc _ _ _),

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ t = i ≫ h
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
⊢ Subobject (op A) → Subobject (op A.left)

Tactic:
refine Subobject.lift (fun P f hf => Subobject.mk f.unop.left.op) ?_

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] (i : A_1 ≅ B),
    i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ ∀ (j : WalkingParallelFamily J), s.ι.app j ≫ k = t.ι.app j

Tactic:
by
    rintro ⟨_ | _⟩
    · simpa using f (Classical.arbitrary J) ≫= w
    · exact w

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

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✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsSeparating
⊢ HasTerminal C

Tactic:
have : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating (P.isCoseparating_op_iff.2 hP)
  exact hasTerminal_of_hasInitial_op

Goal state after:
Module: Mathlib.GroupTheory.Divisible

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

Tactic:
simp [RootableBy.root_cancel _ hn]

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

Goal state before:
pp: case mp
n : ℤ
h' : Odd n
h : -1 = 1
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False

Tactic:
contradiction

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

Goal state after:
case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)
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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) '' c)

Tactic:
by
  rintro _ ⟨a, a_mem, rfl⟩ _ ⟨b, b_mem, rfl⟩ ne
  exact hchain a_mem b_mem (ne_of_apply_ne _ ne)

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case neg.refine_2
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
⊢ (p ^ n).Coprime a

Tactic:
· simpa [hn, Prime.coprime_iff_not_dvd hp']

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX)

Tactic:
exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a

Tactic:
by grw [← mul_add_one, ih]

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 (φ n)

Tactic:
by
    rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
x : α
hx : x ∈ ⋂ i, Ici ↑i
y : α
hy : x ≤ y
⊢ p y

Tactic:
simp only [mem_iInter] at hS hx

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ i ∈ S, x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p)) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))

Tactic:
← Nat.mul_div_assoc

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))

case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p ∣ a * b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
⊢ a = b

Tactic:
rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'
    rw [h', ha']

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

Tactic:
neg_smul

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

Tactic:
neg_smul

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

Tactic:
by
  rw [toIcoMod, sub_add_cancel]

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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
neg_add,

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

Tactic:
neg_add,

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
⊢ -a = -a + -p + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ z, b = a + z • p) → toIocMod hp a b = a + p

Tactic:
rintro ⟨z, rfl⟩
    rw [toIocMod_add_zsmul, toIocMod_apply_left]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ interior s ↔ x ∈ {x | s ∈ 𝓝 x}

Tactic:
by simp only [mem_interior, mem_nhds_iff, mem_ofPred_eq]

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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| b

Tactic:
rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
| a + toIcoDiv hp a b • p
Module: Mathlib.Topology.Closure

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

Tactic:
frontier_eq_inter_compl_interior

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ toIocMod hp a z✝ - z✝ ∈ AddSubgroup.zmultiples p

Tactic:
toIocMod_sub_self

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ -toIocDiv hp a z✝ • p ∈ AddSubgroup.zmultiples 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
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp 0 (x₁ - x₃) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
le_sub_iff_add_le

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
not_h₃₂ : ¬x₃' - p < x₂'
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
contradiction

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t

Tactic:
simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

Goal state after: