mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : f (m, s).1 = ⋯.unit • x
⊢ x ∈ span Rₛ (⇑f '' v)

Tactic:
← inv_smul_eq_iff

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ x ∈ span Rₛ (⇑f '' v)
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = Finsupp.single i ((algebraMap R Rₛ) 1)

Tactic:
map_one

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = Finsupp.single i 1
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm = LinearMap.id

Tactic:
ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f = LinearMap.id

Tactic:
ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[R] N
⊢ (fun e ↦ restrictScalars R e) ((fun e ↦ extendScalarsOfIsLocalization S A e) e) = e

Tactic:
ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[A] N
⊢ (fun e ↦ extendScalarsOfIsLocalization S A e) ((fun e ↦ restrictScalars R e) e) = e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ snd = e₁.hom ≫ snd' ≫ e₃.inv

Tactic:
rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂

Tactic:
reassoc_of% hm₁,

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ s.fst ≫ g₁ = l₂ ≫ t₂.fst

Tactic:
hl₂

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ s.fst ≫ g₁ = s.fst ≫ g₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂

Tactic:
by rw [s.w, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
by rw [s.w, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₁.inl ≫ l₁ = t₁.inl ≫ t₂.inl ≫ l₂

Tactic:
hl₂

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ t₁.inl ≫ l₁ = t₁.inl ≫ l₁
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 = (algebraMap R T) 1

Tactic:
map_one

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 = 1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ (lift fun a ↦ if a ∈ s then 0 else X) 1 = ↑1

Tactic:
map_one

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ 1 = ↑1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ Nonempty (IsColimit (BinaryCofan.mk inl inr))

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : Nonempty (IsColimit (BinaryCofan.mk inl inr))
⊢ IsPushout f g inl inr

Tactic:
· exact ⟨BinaryCofan.IsColimit.mk _ (fun u v ↦ h.desc u v (by subsingleton))
      (by subsingleton) (by subsingleton) (by subsingleton)⟩

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : Nonempty (IsColimit (BinaryCofan.mk inl inr))
⊢ IsPushout f g inl inr
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) 1) = 1

Tactic:
map_one

Goal state after:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) 1 = 1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) (-(restriction s) 1) = -1

Tactic:
map_one

Goal state after:
case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) (-1) = -1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
⊢ x • 0 = 0

Tactic:
conv => lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = y * x

Tactic:
rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
⊢ (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of).comp
      (FreeCommRing.lift fun a ↦ MvPolynomial.X a) =
    RingHom.id (FreeCommRing α)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ (algebraMap R (End R M'')) ↑s = ↑e ∘ₗ (algebraMap R (End R M')) ↑s ∘ₗ ↑e.symm

Tactic:
ext; simp

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

Goal state before:
pp: case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X

Tactic:
simp only [← Category.assoc, NatIso.cancel_natIso_hom_right]

Goal state after:
case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X = (T.μ.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.μ.app X
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
⊢ ∀ (p p' : M × ↥S), p ≈ p' → ↑⋯.unit⁻¹ (f p.1) = ↑⋯.unit⁻¹ (f p'.1)

Tactic:
by
      rintro ⟨a, b⟩ ⟨a', b'⟩ ⟨c, eq1⟩
      dsimp
      rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, ← map_smul,
        Module.End.algebraMap_isUnit_inv_apply_eq_iff', ← map_smul]
      exact (IsLocalizedModule.eq_iff_exists S f).mpr ⟨c, eq1.symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPushoutsAlong f
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
this : ∀ (Z : Under X), Mono ((mapPushoutAdj f).unit.app Z)
⊢ (pushout f).Faithful

Tactic:
exact (mapPushoutAdj f).faithful_L_of_mono_unit_app

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ ({ hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft,
      (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight) =
    ↑(Algebra.TensorProduct.liftEquiv.symm
        (Hom.hom
            (ofHom
              (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                  ⋯).toRingHom)).toIntAlgHom)

Tactic:
Prod.mk.injEq

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft =
      (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.1 ∧
    (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
      (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.2
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasColimit F

Tactic:
have : HasColimit (F ⋙ Comma.snd _ _) := i₂

Goal state after:
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this✝ : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasColimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)

Tactic:
simp only [Iso.hom_inv_id, PrelaxFunctor.map₂_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.isoClosure.op = P.op.isoClosure

Tactic:
by
  ext ⟨X⟩
  exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩,
    fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯) = f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ ⊤
⊢ x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
rw [← ht''] at this

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ((𝟭 F.Elementsᵒᵖ).map (op f) ≫
        (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst) ⋯).op.hom).unop =
    ((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : C
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫ (colimitFiberwiseColimitIso G).hom =
    colimit.ι G { base := X, fiber := d }

Tactic:
by
  simp [colimitFiberwiseColimitIso]

Goal state after: