mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 ≫ F.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).1) = μ F X Y

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 ≫ 𝟙 (F.obj ((diag C).obj X ⊗ (diag C).obj Y).1) = μ F X Y
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ G.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ 𝟙 (G.obj ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ F.map (𝟙 ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ 𝟙 (F.obj ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ G.map (𝟙 ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ 𝟙 (G.obj ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ F.map (𝟙 ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ 𝟙 (F.obj ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ G.map (𝟙 ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ 𝟙 (G.obj ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePushouts C
ι : Type w
⊢ HasLimitsOfShape (WidePullbackShape ι) Cᵒᵖ

Tactic:
hasLimitsOfShape_opposite_iff

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePushouts C
ι : Type w
⊢ HasColimitsOfShape (WidePullbackShape ι)ᵒᵖ C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} J✝
inst✝ : HasFiniteWidePushouts C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) Cᵒᵖ

Tactic:
hasLimitsOfShape_opposite_iff

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} J✝
inst✝ : HasFiniteWidePushouts C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePullbackShape J)ᵒᵖ C
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F) (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
erw [QuotientAddGroup.lift_mk']

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.ulift.symm a) - (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.ulift.symm a) = 0

Tactic:
sub_self

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ ↑(FreeAlgebra.ι R (x + y)) = ↑(FreeAlgebra.ι R x) + ↑(FreeAlgebra.ι R y)

Tactic:
by
      rw [← RingCon.coe_add]
      exact Quotient.sound <| RingConGen.Rel.of _ _ Rel.add

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
fst_comp_inr,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ 0 = (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = TensorProduct.map (LinearMap.fst R A B ∘ₗ inr R A B) (LinearMap.fst R A B ∘ₗ inr R A B) ∘ₗ comul

Tactic:
fst_comp_inr,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = TensorProduct.map 0 0 ∘ₗ comul
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ map LinearMap.id = AlgHom.id R' (tsze R' M)

Tactic:
by
  apply algHom_ext
  simp only [map_inr, LinearMap.id_coe, id_eq, AlgHom.coe_id, forall_const]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : ↑Y
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (r • y))) 1 =
    (RingHom.id R) r • ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
rw [← map_smul]

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : ↑Y
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (r • y))) 1 =
    ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) ((RingHom.id R) r • 1)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a ⊔ b = b ⊔ a

Tactic:
dsimp only [(· ⊔ ·)]

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b + a * b = b + a + b * a
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Tactic:
dsimp only [(· ⊔ ·)]

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ

Tactic:
by
  rw [← symm_comp_map_assoc, ← LinearMap.lTensor_def, ← LinearMap.lTensor_def,
    ← LinearMap.lTensor_def, ← Coalgebra.coassoc, ← f.comp_id,
    TensorProduct.map_comp, ← LinearMap.rTensor_def]
  simp only [← LinearMap.comp_assoc]
  congr 2
  ext
  rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
x y : R
h : (algebraMap R S) x = (algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
by
    obtain ⟨n, hn⟩ := exists_of_eq x y h
    use ⟨r ^ n, n, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
r x : R
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r x ∈ ↑I

Tactic:
exact mul_mem_left _ _ _ (h hx)

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀

Tactic:
exact mem_sInf.mp xJ ⟨I𝔪₀, 𝔪₀_maximal⟩

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : comap (Quotient.mk I) ⊥.jacobson = comap (Quotient.mk I) ⊥
⊢ I.jacobson = I

Tactic:
rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : (RingHom.ker (Quotient.mk I)).jacobson = RingHom.ker (Quotient.mk I)
⊢ I.jacobson = I
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ IsLocalHom f

Tactic:
refine ((local_hom_TFAE f).out 3 0).mp ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
⊢ f = g

Tactic:
have := hI.isIso_from f
  have := hI.isIso_from g
  exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S), IsUnit ((algebraMap R Aₛ) ↑x)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)

Tactic:
Subtype.forall,

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ a ∈ S, IsUnit ((algebraMap R Aₛ) a)) ↔ ∀ a ∈ Algebra.algebraMapSubmonoid A S, IsUnit ((algebraMap A Aₛ) a)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZPow x B (↑m - ↑d) * (algebraMap R B) a = b

Tactic:
rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast,
    ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) x ^ m * (algebraMap R B) a
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (ρ_ X).inv ≫ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).inv ≫ (ρ_ X).hom

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp, tensorHom_def', Category.assoc,
      whiskerLeft_hom_inv_assoc, Iso.inv_hom_id]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (ρ_ X).inv ≫ X ◁ η ≫ e.inv ▷ M ≫ μ ≫ e.hom = 𝟙 X
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m = hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯)

Tactic:
apply hc.hom_ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g := ⋯
⊢ ∀ (j : WalkingCospan),
    m ≫ (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯).π.app j =
      hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
        (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯).π.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ m = hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
apply hc.hom_ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g := ⋯
⊢ ∀ (j : WalkingSpan),
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯).ι.app j ≫ m =
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯).ι.app j ≫
        hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ -1 = -f 1

Tactic:
f.map_one

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ -1 = -1
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:
intro x y ihx ihy
    rw [map_add, map_add, ihx, ihy]

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

Tactic:
show (x + y) • _ = IsLocalization.mk' T _ _ • _ by
    rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s],

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ Z✝ : Monad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z✝.map h

Tactic:
f.1.naturality_assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ Z✝ : Monad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ f.app X ≫ Y✝.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z✝.map h
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ Z✝ : Comonad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z✝.map h

Tactic:
f.1.naturality_assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ Z✝ : Comonad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ f.app X ≫ Y✝.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z✝.map h