mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)

Tactic:
cases h

Goal state after:
case rightCompReflexion.left.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.rightCompReflexion.comp (Hom.left.comp Hom.reflexion)

case rightCompReflexion.left.id
⊢ (Hom.rightCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.rightCompReflexion.comp (Hom.left.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)

Tactic:
cases h

Goal state after:
case rightCompReflexion.right.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.right).comp Hom.reflexion =
    Hom.rightCompReflexion.comp (Hom.right.comp Hom.reflexion)

case rightCompReflexion.right.id
⊢ (Hom.rightCompReflexion.comp Hom.right).comp (Hom.id zero) =
    Hom.rightCompReflexion.comp (Hom.right.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case rightCompReflexion.leftCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case rightCompReflexion.leftCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case rightCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case rightCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case rightCompReflexion.leftCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case rightCompReflexion.rightCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case rightCompReflexion.rightCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case rightCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case rightCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case rightCompReflexion.rightCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)

Tactic:
cases h

Goal state after:
case rightCompReflexion.id.left
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.left)

case rightCompReflexion.id.right
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.right)

case rightCompReflexion.id.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case rightCompReflexion.id.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case rightCompReflexion.id.id
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.rightCompReflexion.comp ((Hom.id one).comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)

Tactic:
cases h

Goal state after:
case id.left.reflexion
⊢ ((Hom.id one).comp Hom.left).comp Hom.reflexion = (Hom.id one).comp (Hom.left.comp Hom.reflexion)

case id.left.id
⊢ ((Hom.id one).comp Hom.left).comp (Hom.id zero) = (Hom.id one).comp (Hom.left.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)

Tactic:
cases h

Goal state after:
case id.right.reflexion
⊢ ((Hom.id one).comp Hom.right).comp Hom.reflexion = (Hom.id one).comp (Hom.right.comp Hom.reflexion)

case id.right.id
⊢ ((Hom.id one).comp Hom.right).comp (Hom.id zero) = (Hom.id one).comp (Hom.right.comp (Hom.id zero))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)

Tactic:
cases h

Goal state after:
case id.reflexion.left
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)

case id.reflexion.right
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)

case id.reflexion.leftCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)

case id.reflexion.rightCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)

case id.reflexion.id
⊢ ((Hom.id zero).comp Hom.reflexion).comp (Hom.id one) = (Hom.id zero).comp (Hom.reflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case id.leftCompReflexion.left
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)

case id.leftCompReflexion.right
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)

case id.leftCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case id.leftCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case id.leftCompReflexion.id
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.leftCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h

Goal state after:
case id.rightCompReflexion.left
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)

case id.rightCompReflexion.right
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)

case id.rightCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case id.rightCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case id.rightCompReflexion.id
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.rightCompReflexion.comp (Hom.id one))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id.id
W✝ Z✝ : WalkingReflexivePair
h : W✝.Hom Z✝
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp h = (Hom.id W✝).comp ((Hom.id W✝).comp h)

Tactic:
cases h

Goal state after:
case id.id.left
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)

case id.id.right
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)

case id.id.reflexion
⊢ ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)

case id.id.leftCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)

case id.id.rightCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)

case id.id.id
W✝ : WalkingReflexivePair
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp (Hom.id W✝) = (Hom.id W✝).comp ((Hom.id W✝).comp (Hom.id W✝))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
tauto

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

Goal state before:
pp: case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
tauto

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

Goal state before:
pp: case «2»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨2, ⋯⟩))

Tactic:
tauto

Goal state after:
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 = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h

Tactic:
app'.hom_inv_id,

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.obj' (n + 1) h) = app.hom ≫ app.inv ≫ 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:
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 : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical

Tactic:
split_ifs with hm
  · rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]
  · exact hS.radical_colon_singleton_of_notMem hm

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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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 : ↥p
m : N ⧸ localized' S p f M'
⊢ 1 • m = m

Tactic:
one_smul

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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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 : ↥p
m : N ⧸ localized' S p f M'
⊢ m = m
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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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 : N
⊢ ∃ x, x.2 • Submodule.Quotient.mk y = (Submodule.toLocalizedQuotient' S p f M') x.1

Tactic:
obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y

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✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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 : M
s : ↥p
⊢ ∃ x, x.2 • Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s)) = (Submodule.toLocalizedQuotient' S p f M') x.1
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
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ∀ (x : N), x ∈ localized' S p f g.ker ↔ x ∈ (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g)).ker

Tactic:
by apply SetLike.ext_iff.mp (f.ker_localizedMap_eq_localized₀_ker p f' g).symm

Goal state after:
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
⊢ 1 • 1 = 1

Tactic:
one_smul

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 = 1
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
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (↑(LinearEquiv.restrictScalars R e) ∘ₗ Algebra.idealMap S (ker g))

Tactic:
apply IsLocalizedModule.of_linearEquiv

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

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

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

Tactic:
· rw [mem_localizationLocalizationSubmodule]
      refine ⟨z, c * s, ?_⟩
      rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

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

Tactic:
refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm

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

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

Goal state before:
pp: case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ coeSubmodule S I = coeSubmodule S (R ∙ x)

Tactic:
Ideal.submodule_span_eq,

Goal state after:
case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ coeSubmodule S I = coeSubmodule S (Ideal.span {x})
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ coeSubmodule S (R ∙ x) = R ∙ (algebraMap R S) x

Tactic:
Ideal.submodule_span_eq,

Goal state after:
case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x