mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l

Tactic:
refine ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩
  obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s :=
    mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
  refine ⟨t, htl, fun p hp => ?_⟩
  rcases le_total p.1 p.2 with h | h
  · rw [mem_preimage, uIcc_of_le h]
    exact hts p hp
  · rw [mem_preimage, uIcc_of_ge h]
    exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 * p.2

Tactic:
simp only [continuous_iff_continuousAt, Prod.forall, ContinuousAt,
      LinearOrderedCommGroup.tendsto_nhds]
    intro a b ε hε
    rcases dense_or_discrete 1 ε with ⟨δ, hδ₁, hδε⟩ | ⟨-, hε_min⟩
    · filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]
      rintro ⟨c, d⟩ ⟨hc, hd⟩
      calc
        |c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
        _ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul_le ..
        _ < δ * (ε / δ) := mul_lt_mul_of_lt_of_lt hc hd
        _ = ε := mul_div_cancel ..
    · have (x : G) : ∀ᶠ y in 𝓝 x, y = x :=
        (eventually_mabs_div_lt _ hε).mono fun y hy ↦ mabs_div_le_one.mp <| hε_min _ hy
      filter_upwards [(this _).prod_nhds (this _)]
      simp [hε]

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 α
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Ioc_eq_nhdsGT hab]

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 ∈ 𝓝[Ioc a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : 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 : α
hx : x ∈ t
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_ofPred_eq, t] at hx

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 : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ x_1, x < x_1
⊢ ∃ y > x, s ∩ Ioo x y = ∅
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
f1 : α → Set α := fun a ↦ Ioi a
f2 : α → Set α := fun a ↦ Iio a
⊢ {s | ∃ a, s = Ioi a ∨ s = Iio a}.Countable

Tactic:
exact Countable.mono (fun s hs => by grind) ((countable_range f1).union (countable_range f2))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : CommMonCat
⊢ (β_ (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X
          (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X).hom ≫
      μ =
    μ

Tactic:
ext ⟨x : A, y : A⟩

Goal state after:
A : CommMonCat
x y : ↑A
⊢ (hom
          ((β_ (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X
                (MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)).X).hom ≫
            μ)).toFun
      (x, y) =
    (hom μ).toFun (x, y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
⊢ atTop.IsCountablyGenerated

Tactic:
obtain ⟨s, s_count, hs⟩ := exists_countable_dense α

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ atTop.IsCountablyGenerated
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: A : CommGrpCat
⊢ (β_ (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X
          (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X).hom ≫
      μ =
    μ

Tactic:
ext ⟨x : A, y : A⟩

Goal state after:
A : CommGrpCat
x y : ↑A
⊢ (hom
          ((β_ (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X
                (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X).hom ≫
            μ)).toFun
      (x, y) =
    (hom μ).toFun (x, y)
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 : X ⟶ Y
g g' : Y ⟶ Z
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
dsimp +instances [CategoryTheory.categoryFree]
    rw [← Finsupp.sum_add]
    congr; ext r h
    rw [Finsupp.sum_add_index'] <;> · simp [mul_add]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀.X₂), x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀'.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀'.X₂), x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₁'.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.δ ≫ f.f₃.τ₁ = f.f₀.τ₃ ≫ S₂.δ

Tactic:
rw [← cancel_epi (pullback.snd _ _ : S₁.P ⟶ _), S₁.snd_δ_assoc, ← comp_τ₁, ← f.comm₂₃,
    comp_τ₁, naturality_φ₁_assoc, ← S₂.snd_δ, functorP_map, pullback.lift_snd_assoc, assoc]

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

Goal state before:
pp: case pos
J : MultispanShape
a b : J.L
h : a = b
⊢ Subsingleton (left a ⟶ left b)

Tactic:
subst h
    infer_instance

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

Goal state before:
pp: case pos
J : MultispanShape
a b : J.R
h : a = b
⊢ Subsingleton (right a ⟶ right b)

Tactic:
subst h
    infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : S.Exact
⊢ (S.map (restrictScalars f)).Exact

Tactic:
CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact

Goal state after:
R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (S.map (restrictScalars f)).f)
    ⇑(ConcreteCategory.hom (S.map (restrictScalars f)).g)
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
        rfl

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
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
⊢ ∀ (s : Cone I.multicospan) (m : s.pt ⟶ K.pt), (∀ (j : WalkingMulticospan J), m ≫ K.π.app j = s.π.app j) → m = lift s

Tactic:
rintro E m hm
      apply uniq
      intro i
      apply hm

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

Goal state before:
pp: ⊢ ∀ {X Y Z : WalkingParallelPair} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match Z, X, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y, X, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z, Y, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)

Tactic:
intro _ _ _ f g; cases f <;> cases g <;> rfl

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) N.subtype)

Tactic:
← EquivLike.injective_comp (cancelBaseChange R S S _ _),

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 (⇑((AlgebraTensorModule.lTensor S M) N.subtype) ∘ ⇑(cancelBaseChange R S S M ↥N))
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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ (T.mapCone c).π.app j =
    (t.lift (T.forget.mapCone s) ≫ (liftedCone c t).pt.a) ≫ (T.mapCone c).π.app j

Tactic:
by
          dsimp
          rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting, ← assoc, ← assoc, t.fac,
            assoc, ← Functor.map_comp, t.fac]
          exact (s.π.app j).h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t

Tactic:
refine ⟨?_, zero_mem_smul_set⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁴ : CommSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsPrime
⊢ p.IsPrime

Tactic:
rw [over_def P p]
  exact IsPrime.under A P

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
hp : p ≠ ⊥
P : Ideal B
inst✝ : P.LiesOver p
⊢ P ≠ ⊥

Tactic:
contrapose hp
  rw [over_def P p, hp, under_bot]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = I.radical

Tactic:
by
  rw [I.radical_eq_sInf]
  apply le_antisymm
  · intro x hx
    rw [Ideal.mem_sInf] at hx ⊢
    rintro J ⟨e, hJ⟩
    obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
    exact hp' (hx hp)
  · apply sInf_le_sInf _
    intro I hI
    exact hI.1.symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ (Ideal.map (algebraMap R S) I).radical ≤ Ideal.map (algebraMap R S) I.radical

Tactic:
rintro x ⟨n, hn⟩

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : S
n : ℕ
hn : x ^ n ∈ Ideal.map (algebraMap R S) I
⊢ x ∈ Ideal.map (algebraMap R S) I.radical
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ (Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)

Tactic:
by
  suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
      Ideal.map (algebraMap R R') p from ⟨by rw [← h, IsLocalization.map_under (M := M)]⟩
  rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
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ₚ
inst✝ : p.IsMaximal
n : ℕ
⊢ under R (maximalIdeal Rₚ ^ n) = p ^ n

Tactic:
ext
  rw [mem_comap, ← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
    algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]
  refine ⟨fun ⟨m, hm, h⟩ ↦ ?_, fun h ↦ ⟨1, by simp, by simp [h]⟩⟩
  exact (IsMaximal.mul_mem_pow _ h).resolve_left (mem_primeCompl_iff.mp hm)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) r).toAlgebra
r : R
hr : r ∈ s
this :
  algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
    (↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
      (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r)))
⊢ P
    ((↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
      (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r))))

Tactic:
exact hP.1 _ _ (hf ⟨r, hr⟩)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P

Tactic:
· introv _ _ hf
    exact hPc _ _ hf (hPl T s)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝³ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝² : IsLocalization.Away 1 R
this✝¹ : IsLocalization.Away (f 1) T
this✝ : RingHomInvPair ↑e ↑e.symm
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
⊢ (IsLocalization.Away.map R T f 1).comp (e.symm.toRingHom.comp e.toRingHom) = IsLocalization.Away.map R T f 1

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
⊢ P (Localization.awayMap f ↑r)

Tactic:
let e₁ := (Localization.algEquiv (.powers r.val) Rᵣ).toRingEquiv

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
⊢ P (Localization.awayMap f ↑r)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
R : Type u_5
inst✝² : Monoid R
inst✝¹ : MulAction R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A).IsSymm
⊢ (⅟k • k • A).IsSymm

Tactic:
exact h.smul ⅟k

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
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✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ α * β - 1 ∈ p

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
          map_mul, hβ, mul_inv_cancel₀, sub_self]
        rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

case inr
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)