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
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
⊢ ↑⋯.unit⁻¹ ((g ∘ₗ h) x) = mk' g (h x) s

Tactic:
]

Goal state after:
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
⊢ ↑⋯.unit⁻¹ ((g ∘ₗ h) x) = mk' g (h x) s
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case h
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
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1

Tactic:
]

Goal state after:
case h
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
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1
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
⊢ e = ↑(LinearEquiv.refl R (LocalizedModule S M))

Tactic:
]

Goal state after:
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
⊢ e = ↑(LinearEquiv.refl R (LocalizedModule S M))
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
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j

Tactic:
]

Goal state after:
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
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j
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
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
]

Goal state after:
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
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
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)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)

Tactic:
]

Goal state after:
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)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)
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₂ η.inv

Tactic:
]

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

Goal state before:
pp: case h
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₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s)

Tactic:
| _ m s
   => 

Goal state after:
case h
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₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s)
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 f) = 𝟙 (F.map f)

Tactic:
]

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 g) = 𝟙 (F.map g)

Tactic:
]

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 f

Tactic:
]

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

Goal state before:
pp: case h
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₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)

Tactic:
]

Goal state after:
case h
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₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
intro m hm
    ext x
    exact Subtype.ext <| RingHom.congr_fun (congrArg Hom.hom hm) x

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

Goal state before:
pp: R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0

Tactic:
]

Goal state after:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Bijective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
]

Goal state after:
case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Bijective ⇑((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ a = a

Tactic:
]

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

Goal state before:
pp: case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ (∃ m, m • (x - y) = 0) → ∃ c, c • x = c • y

Tactic:
]

Goal state after:
case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ (∃ m, m • (x - y) = 0) → ∃ c, c • x = c • y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ g.ker

Tactic:
]

Goal state after:
R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ g.ker
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S g
inst✝ : Subsingleton M
⊢ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
]

Goal state after:
R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S g
inst✝ : Subsingleton M
⊢ ∀ (m : M), ∃ r ∈ S, r • m = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
S : Submonoid R
⊢ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
S : Submonoid R
⊢ ∀ (m : M), ∃ r ∈ S, r • m = 0
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) =
    ((Hom.hom
          (m ≫
            ofHom
              ((RingHom.fst ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x,
      (Hom.hom
          (m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x)

Tactic:
]

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) =
    ((Hom.hom
          (m ≫
            ofHom
              ((RingHom.fst ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x,
      (Hom.hom
          (m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₂, t₂))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)

Tactic:
]

Goal state after:
case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₂, t₂))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

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 ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h

Tactic:
]

Goal state after:
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 ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ F.map₂ (λ_ f).hom = F.map₂ (λ_ f).hom

Tactic:
]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b) ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b) ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ F.map₂ (ρ_ f).hom = F.map₂ (ρ_ f).hom

Tactic:
]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵒᵖᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b

Tactic:
]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = fg

Tactic:
]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝) =
    G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)

Tactic:
]

Goal state after:
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:
]

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