mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.left
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
·

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.right
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ t • t' • mk m s = t' • t • mk m s

Tactic:
simp_rw [smul_def, smul_smul, mul_left_comm, mul_comm]

Goal state after:
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
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Nonempty (IsLimit (BinaryFan.mk fst snd))

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : Nonempty (IsLimit (BinaryFan.mk fst snd))
⊢ IsPullback fst snd f g

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Nonempty (IsLimit (BinaryFan.mk fst snd))
Module: Mathlib.RingTheory.FreeCommRing

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

pp: case refine_2
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (-1) = ↑n

pp: case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) (z * n) = ↑n_1

pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
·

Goal state after:
case refine_1
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) 1 = ↑n
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : Nonempty (IsLimit (BinaryFan.mk fst snd))
⊢ IsPullback fst snd f g

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : Nonempty (IsLimit (BinaryFan.mk fst snd))
⊢ IsPullback fst snd f g
Module: Mathlib.RingTheory.FreeCommRing

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

pp: case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) (z * n) = ↑n_1

pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
·

Goal state after:
case refine_2
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (-1) = ↑n
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:
·

Goal state after:
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))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
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:
·

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_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) (z * n) = ↑n_1

pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
·

Goal state after:
case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) n = ↑n_1) →
        ∃ n_1, (lift fun a ↦ if a ∈ s then 0 else X) (z * n) = ↑n_1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
·

Goal state after:
case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case pos
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s

pp: case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
this : ∃ n, X = ↑n
⊢ p ∈ s

Tactic:
·

Goal state after:
case pos
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s
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

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

pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

pp: case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y

Tactic:
·

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) ((restriction s) 1) = 1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ IsPullback p q f g → ∃ e, q = Over.Hom.left e.hom ≫ pullback.snd f g

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ (∃ e, q = Over.Hom.left e.hom ≫ pullback.snd f g) → IsPullback p q f g

Tactic:
·

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ IsPullback p q f g → ∃ e, q = Over.Hom.left e.hom ≫ pullback.snd f g
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

pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

pp: case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y

Tactic:
·

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) ((restriction s) (-1)) = -1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

pp: case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y

Tactic:
·

Goal state after:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.e_m
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
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n

pp: case e_s
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
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)

Tactic:
·

Goal state after:
case h.h.e_m
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
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ (∃ e, q = Over.Hom.left e.hom ≫ pullback.snd f g) → IsPullback p q f g

Tactic:
·

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ (∃ e, q = Over.Hom.left e.hom ≫ pullback.snd f g) → IsPullback p q f g
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y

Tactic:
·

Goal state after:
case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_s
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
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)

Tactic:
·

Goal state after:
case e_s
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
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 + y) • mk m s =
    IsLocalization.mk' T ?m.109 ?m.110 • ?m.112

Tactic:
← IsLocalization.mk'_sec (M := S) T y,

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
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 +
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T ?m.109 ?m.110 • ?m.112
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.e_m
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 y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
        ↑s) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m

pp: case e_s
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)

Tactic:
·

Goal state after:
case h.e_m
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 y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
        ↑s) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_s
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)

Tactic:
·

Goal state after:
case e_s
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)