mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((Hom.hom ((μIso R X Y).hom ▷ (free R).obj Z))
          ((ConcreteCategory.hom (μIso R X Y).inv) (freeMk ((x, y), z).1) ⊗ₜ[R] freeMk ((x, y), z).2))) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          ((ConcreteCategory.hom (μIso R X Y).inv) (freeMk ((x, y), z).1) ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
μIso_inv_freeMk,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom))
      ((Hom.hom (μIso R (X ⊗ Y) Z).hom)
        ((Hom.hom ((μIso R X Y).hom ▷ (free R).obj Z))
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2))) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δlast.Exact

Tactic:
rw [exact_iff_δlast] at hS

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ (hom (Pi.π F j)) ((productEquiv F).symm x) = x j

Tactic:
by
  rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.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
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType (X₁ ⨯ X₂)
⊢ ((prodEquiv X₁ X₂) x).2 = (hom prod.snd) x

Tactic:
by
  simpa using! congr_hom (prodComparison_snd (forget C) X₁ X₂) x

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 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₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
have := (forget₂ C Ab).preservesFiniteLimits_of_preservesHomology
  have : PreservesFiniteLimits (forget C) := by
    have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp
    simpa only [← this] using comp_preservesFiniteLimits _ _
  have eq := CategoryTheory.congr_fun (D.snd_δ)
    (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
  have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
  have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
  rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at eq
  rw [eq₂] at eq
  refine eq.trans (CategoryTheory.congr_arg (D.v₂₃.τ₁) ?_)
  apply (Preadditive.mono_iff_injective' D.L₂.f).1 inferInstance
  rw [← ConcreteCategory.comp_apply, φ₁_L₂_f]
  dsimp [φ₂]
  rw [ConcreteCategory.comp_apply, eq₁]
  exact h₁.symm

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
b : J.R
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
← app_right_eq_ι_comp_fst,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))

Tactic:
· dsimp; rw [a.condition_assoc]; simp

Goal state after:
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
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
this : PreservesLimit
  (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_2 R K
⊢ CreatesLimit K R

Tactic:
letI : CreatesLimit (K ⋙ A) B := CategoryTheory.Comonad.forgetCreatesLimit _

Goal state after:
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
this✝ : PreservesLimit
  (((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) ⋙ (comonadicAdjunction R).toComonad.toFunctor)
  (comonadicAdjunction R).toComonad.toFunctor :=
  comonadicCreatesLimitOfPreservesLimit._proof_2 R K
this : CreatesLimit (K ⋙ A) B := Comonad.forgetCreatesLimit (K ⋙ A)
⊢ CreatesLimit K R
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm n • x = n • x

Tactic:
rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]

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
hS : S.IsPrimary
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
⊢ (S ⊓ T).IsPrimary

Tactic:
by
  obtain ⟨_, hS⟩ := hS
  obtain ⟨_, hT⟩ := hT
  refine ⟨by grind, fun ⟨hS', hT'⟩ ↦ ?_⟩
  simp_rw [← mem_colon_iff_le, ← Ideal.mem_radical_iff, inf_colon, Ideal.radical_inf,
    top_coe, h, inf_idem, mem_inf, and_or_right] at hS hT ⊢
  exact ⟨hS hS', hT hT'⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ span {x} * I + span {x * y} ≤ I ∨ y ∈ I.radical

Tactic:
add_le_iff,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ span {x} * I ≤ I ∧ span {x * y} ≤ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I + span {y} ≤ m
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
add_le_iff,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I ≤ m ∧ span {y} ≤ m
⊢ x ∈ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes ⊆ {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro I

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I✝ I : Ideal R
⊢ I ∈ I✝.minimalPrimes → I ∈ {J | I✝ ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
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 P.primeCompl (f P)
m m' : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m'
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
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 P.primeCompl (f P)
m m' : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m'
⊢ 1 • m = 1 • m'
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
⊢ Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)

Tactic:
intro s

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
s : S ⧸ I
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = s
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
z : S
r : R
s : ↥M
e : z * (algebraMap R S) ↑(r, s).2 = (algebraMap R S) (r, s).1
⊢ ∃ x, g z * (algebraMap R' S') ↑x.2 = (algebraMap R' S') x.1

Tactic:
refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
z : S
r : R
s : ↥M
e : z * (algebraMap R S) ↑(r, s).2 = (algebraMap R S) (r, s).1
⊢ g z * (algebraMap R' S') ↑(f r, ⟨f ↑s, ⋯⟩).2 = (algebraMap R' S') (f r, ⟨f ↑s, ⋯⟩).1
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
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)

Tactic:
simpa [this] using! e.injective

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
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:
by
    rintro ⟨_, ⟨y, hy, rfl⟩⟩
    convert! IsLocalization.map_units T ⟨y, hy⟩
    exact (IsScalarTower.algebraMap_apply _ _ _ _).symm

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
intro s

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s : S
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case surj
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 ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Tactic:
intro s

Goal state after:
case surj
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 ↑σ
s : S
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Tactic:
intro s

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (r : S), ∃ s ∈ σ, IsUnit s ∧ s • (algebraMap S T) r ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
intro s

Goal state after:
case 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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
s : S
⊢ ∃ s_1 ∈ σ, IsUnit s_1 ∧ s_1 • (algebraMap S T) s ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
⊢ ∀ (m : S) (x : S ⧸ Ideal.map (algebraMap R S) I),
    (↑(tensorQuotEquivQuotSMul S I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I)).symm).toFun
        (m • x) =
      (RingHom.id S) m •
        (↑(tensorQuotEquivQuotSMul S I ≪≫ₗ
                    (I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯ ≪≫ₗ
                  Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I)).symm).toFun
          x

Tactic:
rintro _ ⟨_⟩
    congr

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_4
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx * sy) • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]

Goal state after:
case refine_4
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
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sx • x * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (s : T ⊗[R] S),
    ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
      IsUnit t ∧ s * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
intro s

Goal state after:
case h
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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s : T ⊗[R] S
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ s * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a b : ℤ
a✝ : b ∈ p.coeff.support
hb : b ≠ a
⊢ (Finsupp.single b (p.coeff b)) a = 0

Tactic:
single_eq_of_ne' hb

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a b : ℤ
a✝ : b ∈ p.coeff.support
hb : b ≠ a
⊢ 0 = 0