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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

Tactic:
have fs_count : (f '' s).Countable := by
    have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) := by
      rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
      wlog hle : u ≤ v generalizing u v
      · exact (this v vs u us huv.symm (le_of_not_ge hle)).symm
      have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
      apply disjoint_iff_forall_ne.2
      rintro a ha b hb rfl
      simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
      exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)
    apply Set.PairwiseDisjoint.countable_of_Ioo A
    rintro _ ⟨y, ys, rfl⟩
    simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
fs_count : (f '' s).Countable
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
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 𝕜
⊢ QuotientAddGroup.mk '' Ioc a (a + p) = univ

Tactic:
by
  rw [image_eq_range]
  exact (equivIoc p a).symm.range_eq_univ

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
      rw [IsInducing.subtypeVal.continuousWithinAt_iff]

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
      rw [IsInducing.subtypeVal.continuousWithinAt_iff]

Goal state after:
case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ (∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0

Tactic:
rintro ⟨A', π, hπ, x, fac⟩
    simp [← cancel_epi π, reassoc_of% fac, condition]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ((f + f').sum fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) =
    (sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) +
      sum f' fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
rw [Finsupp.sum_add_index'] <;> · simp [add_mul]

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

Goal state before:
pp: case e_g
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
⊢ (fun f' s ↦ (g + g').sum fun g' t ↦ single (f' ≫ g') (s * t)) = fun a b ↦
    (sum g fun g' t ↦ single (a ≫ g') (b * t)) + sum g' fun g' t ↦ single (a ≫ g') (b * t)

Tactic:
ext r h

Goal state after:
case e_g
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
⊢ ((g + g').sum fun g' t ↦ single (r ≫ g') (h * t)) a✝ =
    ((sum g fun g' t ↦ single (r ≫ g') (h * t)) + sum g' fun g' t ↦ single (r ≫ g') (h * t)) a✝
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ (sum (f + g) fun f' r ↦ r • F.map f') = (sum f fun f' r ↦ r • F.map f') + sum g fun f' r ↦ r • F.map f'

Tactic:
rw [Finsupp.sum_add_index'] <;> simp [add_smul]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f

Tactic:
induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']

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

Goal state before:
pp: case refine_1
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
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f =
    (ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom

pp: case refine_2
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
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom

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

Goal state after:
case refine_2
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
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
⊢ ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y)

Tactic:
intro Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso ((comparisonAdjunction adj).unit.app Y)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
⊢ m = { f := t.desc (T.forget.mapCocone s), h := ⋯ }

Tactic:
ext1
    apply t.hom_ext
    intro j
    simpa using congr_arg Algebra.Hom.f (J j)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
⊢ ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y)

Tactic:
intro Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso ((comparisonAdjunction adj).unit.app Y)
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✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
⊢ CreatesColimit K R

Tactic:
by
  -- Porting note: It would be nice to have a variant of apply which introduces goals for missing
  -- instances.
  letI A := Monad.comparison (monadicAdjunction R)
  letI B := Monad.forget (Adjunction.toMonad (monadicAdjunction R))
  let i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ Monad.forget _ ≅ K ⋙ R :=
    Functor.associator _ _ _ ≪≫
      isoWhiskerLeft K (Monad.comparisonForget (monadicAdjunction R))
  letI : PreservesColimit ((K ⋙ A) ⋙ Monad.forget
    (Adjunction.toMonad (monadicAdjunction R)))
      (Adjunction.toMonad (monadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesColimit_of_iso_diagram _ i.symm
  letI : PreservesColimit
    (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (monadicAdjunction R))) ⋙
      (Adjunction.toMonad (monadicAdjunction R)).toFunctor)
      (Adjunction.toMonad (monadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesColimit_of_iso_diagram _ (isoWhiskerRight i (monadicLeftAdjoint R ⋙ R)).symm
  letI : CreatesColimit (K ⋙ A) B := CategoryTheory.Monad.forgetCreatesColimit _
  letI : CreatesColimit K (A ⋙ B) := CategoryTheory.compCreatesColimit _ _
  let e := Monad.comparisonForget (monadicAdjunction R)
  apply createsColimitOfNatIso e

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
left✝ : T ≠ ⊤
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon Set.univ).radical
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (T.colon Set.univ).radical
⊢ x✝¹ ∈ S ⊓ T ∨ r✝ ∈ (T.colon Set.univ).radical ⊓ (T.colon Set.univ).radical

Tactic:
inf_idem,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
left✝ : T ≠ ⊤
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon Set.univ).radical
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (T.colon Set.univ).radical
⊢ x✝¹ ∈ S ⊓ T ∨ r✝ ∈ (T.colon Set.univ).radical
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∈ S
⊢ {m} ⊆ ↑S

Tactic:
Set.singleton_subset_iff

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∈ S
⊢ m ∈ ↑S
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
s : Set (Submodule R M)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)

Tactic:
sSup_eq_iSup',

Goal state after:
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
s : Set (Submodule R M)
⊢ localized₀ p f (⨆ a, ↑a) = sSup (localized₀ p f '' s)
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
s : Set (Submodule R M)
⊢ localized' S p f (sSup s) = sSup (localized' S p f '' s)

Tactic:
sSup_eq_iSup',

Goal state after:
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
s : Set (Submodule R M)
⊢ localized' S p f (⨆ a, ↑a) = sSup (localized' S p f '' s)
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
⊢ ∀ (y : ↥(localized₀ p f M')), ∃ x, x.2 • y = (toLocalized₀ p f M') x.1

Tactic:
rintro ⟨y, x, hx, s, rfl⟩

Goal state after:
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
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
| ((toFunBilinear R A) a) p

Tactic:
toFunBilinear_apply_eq_smul,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
| a • Polynomial.map (algebraMap R A) p
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝²⁹ : CommSemiring R✝
inst✝²⁸ : CommSemiring S
inst✝²⁷ : CommSemiring P
inst✝²⁶ : CommSemiring Q
M✝ : Submonoid R✝
T : Submonoid P
inst✝²⁵ : Algebra R✝ S
inst✝²⁴ : Algebra P Q
inst✝²³ : IsLocalization M✝ S
inst✝²² : IsLocalization T Q
g : R✝ →+* P
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (Submonoid.map (↑f) (algebraMapSubmonoid A M)) Bₚ

Tactic:
Submonoid.map_coe_toMonoidHom,

Goal state after:
R✝ : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝²⁹ : CommSemiring R✝
inst✝²⁸ : CommSemiring S
inst✝²⁷ : CommSemiring P
inst✝²⁶ : CommSemiring Q
M✝ : Submonoid R✝
T : Submonoid P
inst✝²⁵ : Algebra R✝ S
inst✝²⁴ : Algebra P Q
inst✝²³ : IsLocalization M✝ S
inst✝²² : IsLocalization T Q
g : R✝ →+* P
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (Submonoid.map f (algebraMapSubmonoid A M)) Bₚ
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ Function.Injective ⇑(lTensor S N.subtype)

Tactic:
have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by
    ext; change _ = (h.equiv _).1; simp [h.equiv_tmul, TensorProduct.smul_tmul']

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
this : lTensor S N.subtype = (Submodule.localized₀ p ((TensorProduct.mk R S P) 1) N.subtype.range).subtype ∘ₗ ↑e
⊢ Function.Injective ⇑(lTensor S N.subtype)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
⊢ ∀ (y : ↥(Submonoid.map (algebraMap R S) N)), IsUnit ((algebraMap S T) ↑y)

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩⟩
    convert! IsLocalization.map_units T ⟨y, hy⟩
    exact (IsScalarTower.algebraMap_apply _ _ _ _).symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (algebraMap R S) x✝¹ = (algebraMap R S) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
rw [IsLocalization.eq_iff_exists M]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
P✝ : Type u_3
inst✝⁹ : CommSemiring P✝
p : Ideal R
inst✝⁸ : p.IsPrime
Rₚ : Type u_4
inst✝⁷ : CommSemiring Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p
inst✝⁴ : IsLocalRing Rₚ
Sₚ : Type u_5
inst✝³ : CommSemiring Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : Algebra Rₚ Sₚ
P : Ideal S
⊢ (maximalIdeal Rₚ).IsMaximal

Tactic:
exact maximalIdeal.isMaximal Rₚ

Goal state after: