mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
let t := { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬ IsTop x}

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ 0 < x

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

Tactic:
tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) = 0

Tactic:
have := F'.m_mono

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) = 0
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
have := F'.m_mono

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ ↑a = ↑0

Tactic:
QuotientAddGroup.mk_zero

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ ↑a = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ : ShortComplex C
⊢ mapToComposableArrows (𝟙 S₁) = 𝟙 S₁.toComposableArrows

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
ψ : S₂ ⟶ S₃
⊢ mapToComposableArrows (φ ≫ ψ) = mapToComposableArrows φ ≫ mapToComposableArrows ψ

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0

Tactic:
· simp [mul_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)

Tactic:
· simp [mul_add]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ

Tactic:
obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ hy₂

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂

Tactic:
S.exact_iff_exact_map_forget₂,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.map (forget₂ C Ab)).Exact ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker

Tactic:
hfg

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (ModuleCat.Hom.hom g).ker ≤ (ModuleCat.Hom.hom g).ker
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ (ConcreteCategory.hom (e.hom.app D.L₀.X₃ ≫ (forget C).map D.δ)) x₃ =
    (ConcreteCategory.hom (e.hom.app D.L₂.X₁ ≫ (forget C).map D.v₂₃.τ₁)) x₁

Tactic:
exact D.δ_apply _ _ _
    (((ConcreteCategory.congr_hom (e.hom.naturality D.L₁.g) x₂).symm.trans (by simp_all)).trans
      (ConcreteCategory.congr_hom (e.hom.naturality D.v₀₁.τ₃) x₃))
    (((ConcreteCategory.congr_hom (e.hom.naturality D.L₂.f) x₁).symm.trans (by simp_all)).trans
      (ConcreteCategory.congr_hom (e.hom.naturality D.v₁₂.τ₂) x₂))

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one

Tactic:
apply Fan.IsLimit.hom_ext hd
          simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
⊢ Multifork (ofParallelHoms J f g) ≌ Fork f g

Tactic:
refine (multiforkEquivPiForkOfIsLimit _
      (Fan.isLimitMkOfUnique (Iso.refl X) _) (Fan.isLimitMkOfUnique (Iso.refl Y) _)).trans
      (Fork.equivOfIsos (.refl _) (.refl _) ?_ ?_)
  · refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_
    rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, fstPiMapOfIsLimit_proj]
    simp
  · refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_
    rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, sndPiMapOfIsLimit_proj]
    simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀' X₀ X₁ : C
h : X₀' = X₀
f : X₀ ⟶ X₁
⊢ mk₁ (eqToHom h ≫ f) = mk₁ f

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ X₁' : C
f : X₀ ⟶ X₁
h : X₁ = X₁'
⊢ mk₁ (f ≫ eqToHom h) = mk₁ f

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)

Tactic:
simp [show PreservesFiniteColimits (tensorLeft M) from inferInstance]

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))

Tactic:
iterate 2 apply Flat.lTensor_preserves_injective_linearMap

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑N.subtype
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this : PreservesLimit ((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_1 R K
⊢ PreservesLimit (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
    (comonadicAdjunction R).toComonad.toFunctor

Tactic:
dsimp
    exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
I : Ideal R
H : I.IsPrime
g : M
⊢ (g • I).IsPrime

Tactic:
rw [I.pointwise_smul_eq_comap]
  apply H.comap

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ -s • t = -(s • t)

Tactic:
by
  simp_rw [← image_neg_eq_neg]
  exact image2_image_left_comm neg_smul

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ ∃ x_1, x_1.2 • ⟨IsLocalizedModule.mk' f x s, ⋯⟩ = (toLocalized₀ p f M') x_1.1

Tactic:
exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ (algebraMap R S) z' * (algebraMap R S) ↑t = ↑s * (algebraMap R S) ↑(t * t')

Tactic:
← eq₃,

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ ↑s * (algebraMap R S) ↑t' * (algebraMap R S) ↑t = ↑s * (algebraMap R S) ↑(t * t')
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    Function.Exact ⇑((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
      ⇑((IsLocalizedModule.map J.primeCompl (g J) (h J)) G)
⊢ Function.Exact ⇑F ⇑G

Tactic:
simp only [LinearMap.exact_iff] at H ⊢

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
⊢ G.ker = F.range
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
      ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)
⊢ Function.Exact ⇑F ⇑G

Tactic:
simp only [LinearMap.exact_iff] at H ⊢

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
⊢ G.ker = F.range
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
· intro x y e
      exact ⟨1, by simpa using Subtype.ext e⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Tactic:
let S := Submodule.span A {(a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) | (a : A) (m : M) (n : N)}
    let F : M ⊗[A] N →ₗ[A] (M ⊗[R] N) ⧸ S := TensorProduct.lift ({
      toFun m := {
        toFun n := S.mkQ (m ⊗ₜ[R] n)
        map_add' _ _ := by simp [tmul_add]
        map_smul' a n := by
          rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]
          exact Submodule.subset_span ⟨a, m, n, rfl⟩ }
      map_add' _ _ := by ext _; simp [add_tmul]
      map_smul' _ _ := by simp; rfl })
    have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ := by ext; simp [S, F]
    change (mapOfCompatibleSMul A R A M N).ker ≤ S
    rw [← Submodule.ker_mkQ S, ← h]
    exact (mapOfCompatibleSMul A R A M N).ker_le_ker_comp F

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (T n).degree = ↑n

Tactic:
rw [← one_mul (T n), ← map_one C]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n