mathlib-initiative/mathlib-tactics huggingface dataset:
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
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
y : M₂
y' : M
s : ↥S₂
e : (y', s).2 • y = f₂ (y', s).1
⊢ (f₁ y', s).2 • y = (liftOfLE S₁ S₂ h f₁ f₂) (f₁ y', s).1

Tactic:
by

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''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
y : M₂
⊢ ∃ x, x.2 • y = (liftOfLE S₁ S₂ h f₁ f₂) x.1

Tactic:
by

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

Goal state before:
pp: X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ 0 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ HasStrictTerminalObjects CommRingCat

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ x✝ = default

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ } = s.ι.app j

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ ∀ (j : J), ((fst L R).mapCocone c).ι.app j ≫ x✝.left = ((fst L R).mapCocone s).ι.app j

Tactic:
by

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

Goal state before:
pp: A B : CommRingCat
c : Cone (pair A B)
j : Discrete WalkingPair
⊢ ofHom ((Hom.hom (c.π.app { as := WalkingPair.left })).prod (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
      (A.prodFan B).π.app j =
    c.π.app j

Tactic:
by

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''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M × ↥S₁
c : ↥S₂
e : ↑c • ↑x₁.2 • x₂.1 = ↑c • ↑x₂.2 • x₁.1
⊢ ↑1 • ↑x₁.2 • ↑c • x₂.1 = ↑1 • ↑x₂.2 • ↑c • x₁.1

Tactic:
by

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''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
⊢ ∀ {x₁ x₂ : M₁}, (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ ∀ (j : J), ((snd L R).mapCocone c).ι.app j ≫ x✝.right = ((snd L R).mapCocone s).ι.app j

Tactic:
by

Goal state after:
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝ = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }

Tactic:
by

Goal state after:
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₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
⊢ HasLimit F

Tactic:
by

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

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
⊢ m = ofHom ((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
s : Cone (Discrete.functor R)
i : Discrete ι
⊢ ofHom (RingHom.pi fun i ↦ Hom.hom (s.π.app { as := i })) ≫ (piFan R).π.app i = s.π.app i

Tactic:
by

Goal state after:
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)
⊢ HasColimit F

Tactic:
by

Goal state after:
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
inst✝ : HasColimitsOfShape J T
⊢ PreservesColimitsOfShape J leftFunc

Tactic:
by

Goal state after:
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
inst✝ : HasColimitsOfShape J T
⊢ PreservesColimitsOfShape J rightFunc

Tactic:
by

Goal state after:
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
X : T
G : A ⥤ T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
⊢ HasLimit F

Tactic:
by

Goal state after:
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
X : T
G : A ⥤ T
F : J✝ ⥤ StructuredArrow X G
inst✝¹ : HasLimitsOfSize.{w, w', v₁, u₁} A
inst✝ : PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G
J : Type w'
hJ : Category.{w, w'} J
⊢ HasLimitsOfShape J (StructuredArrow X G)

Tactic:
by

Goal state after:
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
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit F

Tactic:
by

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
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : g (f (↑n • x)) = g (f (↑m • y))
⊢ a = b

Tactic:
by

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
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
⊢ Function.Injective ⇑g

Tactic:
by

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_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
⊢ Function.Injective ⇑g

Tactic:
by

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''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h₁ h₂ : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (h₁ + h₂)) ⋯ = lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯

Tactic:
by

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''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = (RingHom.id R) r • lift S f (g ∘ₗ h) ⋯

Tactic:
by

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) * inv k = inv k

Tactic:
rw [h, one_mul]

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
⊢ (ConcreteCategory.hom (F.map f)) (inv j) = inv k

Tactic:
by

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
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ ((map S f g) h) (mk' f x s) = mk' g (h x) s

Tactic:
by

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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ (map S f f) LinearMap.id = LinearMap.id

Tactic:
by

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj (of (FreeCommRing PUnit.{u + 1}))).map f ≫
      ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv k) =
    ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f

Tactic:
by

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
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
x : M
s : ↥S
y : M
t : ↥S
c : R
hc : c ∈ S
e : c • s • h y = c • t • h x
⊢ h (c • s • y) = h (c • t • x)

Tactic:
by

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
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
⊢ Function.Injective ⇑((map S f g) h)

Tactic:
by

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
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective ⇑h
s : ↥S
x : M
⊢ ((map S f g) h) (mk' f x s) = Function.uncurry (mk' g) (h x, s)

Tactic:
by

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
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective ⇑h
⊢ Function.Surjective ⇑((map S f g) h)

Tactic:
by

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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l ↦ l ∘ₗ f = f) y → y = e
⊢ (fun l ↦ l ∘ₗ f = f) ↑(LinearEquiv.refl R (LocalizedModule S M))

Tactic:
by

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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
by

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
⊢ IsUnit r ↔ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) r)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) = inv (F.map₂ η)

Tactic:
by

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_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv = inv (F.map₂ η.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Tactic:
by

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsLocalHom (Hom.hom (c.π.app j))

Tactic:
by

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

Goal state before:
pp: J : Type u'
inst✝¹ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
inst✝ : IsLocalRing ↑(F.obj j)
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsLocalRing ↑c.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)

Tactic:
by

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f = ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) ≫ F.map₂ η = 𝟙 (F.map g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map f = F.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂ (eqToHom hfg) = eqToHom ⋯

Tactic:
by

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_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
⊢ (map S f₀ f₁) g ∘ₗ ↑(iso S f₀) = ↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g

Tactic:
by

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ IsLimit (equalizerFork f g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂Iso (eqToIso hfg) = eqToIso ⋯

Tactic:
by

Goal state after: