mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op zero))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

Tactic:
·

Goal state after:
case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op zero))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
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), IsUnit ((algebraMap R (End R S')) ↑x)

pp: case surj
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
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1

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₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • 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), IsUnit ((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

Tactic:
·

Goal state after:
case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.left
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.Injective ⇑((algebraMap R (End R S')) ↑x)

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
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
·

Goal state after:
case map_units.left
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.Injective ⇑((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case lift
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ (s : PullbackCone f g) →
    s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))

pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ?lift s ≫
        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

pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ?lift s ≫
        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

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)))),
    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 →
      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 →
        m = ?lift s

Tactic:
·

Goal state after:
case lift
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ (s : PullbackCone f g) →
    s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
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
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
·

Goal state after:
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
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        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

pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        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

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)))),
    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 →
      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 →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)

Tactic:
·

Goal state after:
case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        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
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        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

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)))),
    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 →
      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 →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)

Tactic:
·

Goal state after:
case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        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
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case surj
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
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1

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₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
·

Goal state after:
case surj
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
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1
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₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂

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₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂
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)))),
    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 →
      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 →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)

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)))),
    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 →
      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 →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case pos
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
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
⊢ x = y

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
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∉ S
⊢ x = y

Tactic:
·

Goal state after:
case pos
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
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
⊢ x = y
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case none
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app none)) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

pp: case some.left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.left))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

pp: case some.right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.right))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
·

Goal state after:
case none
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app none)) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case some.left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.left))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

pp: case some.right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.right))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
·

Goal state after:
case some.left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.left))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case some.right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.right))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
·

Goal state after:
case some.right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ ∃ k f_1 g_1,
    IsLocalHom (Hom.hom ((cospan f g).map f_1)) ∧
      (ConcreteCategory.hom ((cospan f g).map f_1))
          ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.right))) x) =
        (ConcreteCategory.hom ((cospan f g).map g_1)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
⊢ (ofObj X).op = ofObj fun i ↦ op (X i)

Tactic:
ext Z

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (ofObj X).op Z ↔ ofObj (fun i ↦ op (X i)) Z
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) → ∃ i, op (X i) = Z

pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) → ∃ i, op (X i) = Z
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h.inl
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I

pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
·

Goal state after:
case h.inl
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I