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

Goal state before:
pp: α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f (Multiplicative.toAdd (x * y))).prod = (Multiset.map f x + Multiset.map f y).prod

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ (lift (⇑f ∘ of)) (-1) = f (-1)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
⊢ PreservesColimit (span f g) F ↔ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) (x + y) = f (x + y)

Tactic:
by

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1

Tactic:
by

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1

Tactic:
by

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
by

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
⊢ ∀ (p p' : M × ↥S), p ≈ p' → mk (a.1 • p.1) (a.2 * p.2) = mk (a.1 • p'.1) (a.2 * p'.2)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) (x * y) = f (x * y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑(↑i + 1)).IsSupported s

Tactic:
by

Goal state after:
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
r : R
m : M
s s' : ↥S
⊢ IsLocalization.mk' T r s • mk m s' = mk (r • m) (s * s')

Tactic:
by

Goal state after:
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
r : R
m : M
s t : ↥S
⊢ r • m /ₒ (t * s) = mk (r • m) (s * t)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i - 1)).IsSupported s

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ PreservesColimitsOfShape WalkingSpan F

Tactic:
by

Goal state after:
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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
p : LocalizedModule S M
⊢ t • t' • p = t' • t • p

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
by

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

Goal state before:
pp: 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
T✝ : C
u : T✝ ⟶ X
v : T✝ ⟶ Y
⊢ u ≫ f = v ≫ g

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : T ⟶ X) (g_1 : T ⟶ Y), h.lift f_1 g_1 ⋯ ≫ (BinaryFan.mk fst snd).fst = f_1

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : T ⟶ X) (g_1 : T ⟶ Y), h.lift f_1 g_1 ⋯ ≫ (BinaryFan.mk fst snd).snd = g_1

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : T ⟶ X) (g_1 : T ⟶ Y) (m : T ⟶ (BinaryFan.mk fst snd).pt),
    m ≫ (BinaryFan.mk fst snd).fst = f_1 → m ≫ (BinaryFan.mk fst snd).snd = g_1 → m = h.lift f_1 g_1 ⋯

Tactic:
by

Goal state after:
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
p : LocalizedModule S M
⊢ 1 • p = p

Tactic:
by

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

Goal state before:
pp: 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))
⊢ fst ≫ f = snd ≫ g

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PullbackCone f g), BinaryFan.IsLimit.lift h.some s.fst s.snd ≫ fst = s.fst

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PullbackCone f g), BinaryFan.IsLimit.lift h.some s.fst s.snd ≫ snd = s.snd

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P),
    m ≫ fst = s.fst → m ≫ snd = s.snd → m = BinaryFan.IsLimit.lift h.some s.fst s.snd

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsPullback fst snd f g ↔ Nonempty (IsLimit (BinaryFan.mk fst snd))

Tactic:
by

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

Goal state before:
pp: 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
T✝ : C
u : X ⟶ T✝
v : Y ⟶ T✝
⊢ f ≫ u = g ≫ v

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : X ⟶ T) (g_1 : Y ⟶ T), (BinaryCofan.mk inl inr).inl ≫ h.desc f_1 g_1 ⋯ = f_1

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : X ⟶ T) (g_1 : Y ⟶ T), (BinaryCofan.mk inl inr).inr ≫ h.desc f_1 g_1 ⋯ = g_1

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ {T : C} (f_1 : X ⟶ T) (g_1 : Y ⟶ T) (m : (BinaryCofan.mk inl inr).pt ⟶ T),
    (BinaryCofan.mk inl inr).inl ≫ m = f_1 → (BinaryCofan.mk inl inr).inr ≫ m = g_1 → m = h.desc f_1 g_1 ⋯

Tactic:
by

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

Goal state before:
pp: 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))
⊢ f ≫ inl = g ≫ inr

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PushoutCocone f g), inl ≫ BinaryCofan.IsColimit.desc h.some s.inl s.inr = s.inl

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PushoutCocone f g), inr ≫ BinaryCofan.IsColimit.desc h.some s.inl s.inr = s.inr

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt),
    inl ≫ m = s.inl → inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h.some s.inl s.inr

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsPushout f g inl inr ↔ Nonempty (IsColimit (BinaryCofan.mk inl inr))

Tactic:
by

Goal state after:
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
p : LocalizedModule S M
⊢ (x * y) • p = x • y • p

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
⊢ PreservesColimitsOfShape WalkingSpan F

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
fst : P ⟶ X
snd : P ⟶ Y
h : IsPullback fst snd f g
⊢ (isoIsPullback X Y h ⋯).hom ≫ (Over.mk (pullback.fst f g)).hom = (Over.mk fst).hom

Tactic:
by

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

Goal state before:
pp: 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
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ ((Over.forget X).mapIso e).hom ≫ pullback.fst f g = p ≫ (Iso.refl X).hom

Tactic:
by

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

Goal state before:
pp: 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
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ ((Over.forget X).mapIso e).hom ≫ pullback.snd f g = (Over.Hom.left e.hom ≫ pullback.snd f g) ≫ (Iso.refl Y).hom

Tactic:
by

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

Goal state before:
pp: 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
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ (Iso.refl X).hom ≫ f = f ≫ (Iso.refl Z).hom

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ X.coeff 1 = (C w).coeff 1

Tactic:
by

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

Goal state before:
pp: 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
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ (Iso.refl Y).hom ≫ g = g ≫ (Iso.refl Z).hom

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
⊢ p ∈ s

Tactic:
by

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

Goal state before:
pp: 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
h : IsPullback p q f g
⊢ q = Over.Hom.left h.isoOverPullback.hom ≫ pullback.snd f g

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
X' : C
i : X' ⟶ X
inst✝¹ : IsIso i
inst✝ : HasPullback f g
⊢ (pullback.fst f g ≫ inv i) ≫ i = 𝟙 (pullback f g) ≫ pullback.fst f g

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
X' : C
i : X' ⟶ X
inst✝ : IsIso i
⊢ HasPullback (i ≫ f) g ↔ HasPullback f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs : x.IsSupported s
⊢ x.IsSupported ↑hfs.toFinset

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z Z' : C
f : X ⟶ Z
g : Y ⟶ Z'
i : Z ⟶ Z'
inst✝¹ : IsIso i
inst✝ : HasPullback (f ≫ i) g
⊢ HasPullback f (g ≫ inv i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
⊢ ↑(-x) = -↑x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z Z' : C
f : X ⟶ Z
g : Y ⟶ Z'
i : Z ⟶ Z'
inst✝ : IsIso i
h : HasPullback f (g ≫ inv i)
⊢ HasPullback (f ≫ i) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x y : FreeRing α
⊢ ↑(x - y) = ↑x - ↑y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝¹ : IsIso i
inst✝ : HasPushout f g
⊢ i ≫ inv i ≫ pushout.inl f g = pushout.inl f g ≫ 𝟙 (pushout f g)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
⊢ HasPushout (f ≫ i) g ↔ HasPushout f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z Z' : C
f : Z ⟶ X
g : Z' ⟶ Y
i : Z' ⟶ Z
inst✝¹ : IsIso i
inst✝ : HasPushout (i ≫ f) g
⊢ HasPushout f (inv i ≫ g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z Z' : C
f : Z ⟶ X
g : Z' ⟶ Y
i : Z' ⟶ Z
inst✝ : IsIso i
h : HasPushout f (inv i ≫ g)
⊢ HasPushout (i ≫ f) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ (FreeMonoid.lift FreeCommRing.of) (FreeMonoid.of hd * tl) = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
⊢ castFreeCommRing = Functor.map fun l ↦ ↑l

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
⊢ Bijective ⇑(coeRingHom α)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by

Goal state after:
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
p : LocalizedModule S M
⊢ (x + y) • p = x • p + y • p

Tactic:
by

Goal state after:
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
p : LocalizedModule S M
⊢ 0 • p = 0

Tactic:
by

Goal state after:
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
s' s : ↥S
m : M
⊢ 1 • s • s' • m = 1 • (s' * s) • m

Tactic:
by

Goal state after: