mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
⊢ x = ↑e.symm y ↔ ↑e x = y

Tactic:
by
  simp [eq_comm, ← symm_apply_eq e hx hy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by
  nontriviality α
  obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
  refine tendsto_atTop_mul_left_of_le' _ C' ?_ hg
  exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
conv in _ * _ => rw [mul_comm]
  exact hg.mul_atBot' hf

Goal state after:
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
hM : Finite ↑M
⊢ Finite ↑N

Tactic:
exact Finite.of_surjective _ hf

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

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Ioi '' s ∪ Iio '' s ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
simp only [union_subset_iff, image_subset_iff]

Goal state after:
case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ s ⊆ Ioi ⁻¹' {s | ∃ a, s = Ioi a ∨ s = Iio a} ∧ s ⊆ Iio ⁻¹' {s | ∃ a, s = Ioi a ∨ s = Iio a}
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ π ≫ a = x₁ ≫ S.f

Tactic:
simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles

Goal state after:
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✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.f))

Tactic:
← Preadditive.mono_iff_injective

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✝ : HasZeroObject C
hS : S.ShortExact
⊢ Mono S.f
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse
    (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))) fun f ↦
    match f.right, f.left, f.hom with
    | x, .(x), Hom.id .(x) => Sum.inl x
    | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
    | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a)

Tactic:
rintro (_ | _ | _)

Goal state after:
case inl
J : MultispanShape
val✝ : WalkingMultispan J
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inl val✝)) =
    Sum.inl val✝

case inr.inl
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inl val✝))) =
    Sum.inr (Sum.inl val✝)

case inr.inr
J : MultispanShape
val✝ : J.L
⊢ (fun f ↦
        match f.right, f.left, f.hom with
        | x, .(x), Hom.id .(x) => Sum.inl x
        | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
        | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
      (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
        (Sum.inr (Sum.inr val✝))) =
    Sum.inr (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
⊢ ∀ (s : Cocone I.multispan) (j : WalkingMultispan J), K.ι.app j ≫ desc s = s.ι.app j

Tactic:
rintro S (a | b)
      · rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]
        congr 1
        apply fac
      · apply fac

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A

Tactic:
Adjunction.unit_naturality_assoc,

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      (reflectorAdjunction R).unit.app (R.obj ((reflector R).obj X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Tactic:
by
  rw [← F.map_comp, reflexion_comp_left, F.map_id]

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)

Tactic:
Adjunction.unit_naturality_assoc,

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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ adj.unit.app (G.obj (F.obj B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ adj.toComonad.Coalgebra ⥤ C

Tactic:
refine
    Adjunction.rightAdjointOfEquiv (F := comparison adj)
      (G_obj := fun A => comparisonRightAdjointObj adj A) (fun A B => ?_) ?_
  · apply comparisonRightAdjointHomEquiv
  · intro A B B' g h
    apply equalizer.hom_ext
    simp [Adjunction.homEquiv_unit]

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✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((comparisonAdjunction adj).counit.app X)

Tactic:
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _

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
X : adj.toComonad.Coalgebra
⊢ IsIso (adj.toComonad.forget.map ((comparisonAdjunction adj).counit.app X))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ f.map' n (n + 1) ⋯ h = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h

Tactic:
app.hom_inv_id_assoc

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ f.map' n (n + 1) ⋯ h = f.map' n (n + 1) ⋯ h
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁶ : Q.LiesOver p
inst✝⁵ : P.LiesOver p
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
E : Type u_7
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ ∀ (r : A ⧸ p), (P.quotientEquiv Q (↑σ) h).toFun ((algebraMap (A ⧸ p) (B ⧸ P)) r) = (algebraMap (A ⧸ p) (C ⧸ Q)) r

Tactic:
by
    rintro ⟨x⟩
    exact congrArg (Ideal.Quotient.mk Q) (AlgHomClass.commutes σ x)

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
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon ↑⊤).radical
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon ↑⊤).radical
⊢ x✝¹ ∈ S ⊓ T ∨ r✝ ∈ ((S ⊓ T).colon ↑⊤).radical

Tactic:
inf_colon,

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
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon ↑⊤).radical
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon ↑⊤).radical
⊢ x✝¹ ∈ S ⊓ T ∨ r✝ ∈ (S.colon ↑⊤ ⊓ T.colon ↑⊤).radical
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' : Submodule R M
⊢ ⇑f '' ↑M' ⊆ ↑(localized' S p f M')

Tactic:
rintro _ ⟨m, hm, rfl⟩; exact ⟨m, hm, 1, by simp⟩

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
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ localized' S p f (comap f (restrictScalars R N'))

Tactic:
refine ⟨m, ?_, 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
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ m ∈ comap f (restrictScalars R N')
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₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) =
    ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))

Tactic:
toFunLinear_mul_tmul_mul_aux_2

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
⊢ Module.IsTorsionFree Rₚ Sₚ

Tactic:
by
  have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
    Submonoid.map_le_of_le_comap _ <| hM.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _))
  have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
    (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  rw [Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]
  intro x hx
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
  simp only [IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    Subtype.exists, exists_prop, this] at hx ⊢
  obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
  simp only [← map_mul,
    (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H
  exact ⟨a, ha, H⟩

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:
by
    rw [IsLocalization.eq_iff_exists M]
    exact fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
x : M
⊢ (quotTensorEquivQuotSMul M I) (1 ⊗ₜ[R] x) = Submodule.Quotient.mk x

Tactic:
by
  rw [← RingHom.map_one (Ideal.Quotient.mk I), TensorProduct.quotTensorEquivQuotSMul_mk_tmul]
  simp

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ t₂ • t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
Algebra.smul_def

Goal state after:
case h.refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (algebraMap S T) t₂ * t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ (map (algebraMap R S) p).IsPrime

Tactic:
have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ (map (algebraMap R S) p).IsPrime
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ under R (map (algebraMap R S) p) = p

Tactic:
have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ under R (map (algebraMap R S) p) = p
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ IsUnit ((algebraMap S T) t₂ * t₁ • y)

Tactic:
Algebra.smul_def

Goal state after:
case h.refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ IsUnit ((algebraMap S T) t₂ * ((algebraMap S T) t₁ * y))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ t₁ • t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
Algebra.smul_def

Goal state after:
case h.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (algebraMap S T) t₁ * t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t