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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ ↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul =
    LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul

Tactic:
ext x y

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry
          (↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul))
        x)
      y =
    ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul)) x) y
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul = (mk S S (A ⊗[R] B)) 1

Tactic:
ext x y

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul = (mk S (A ⊗[R] B) S).flip 1

Tactic:
ext x y

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
⊢ ↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ comul = comul

Tactic:
ext x y

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
x : A
y : B
⊢ ((AlgebraTensorModule.curry (↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ comul)) x) y =
    ((AlgebraTensorModule.curry comul) x) y
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ _root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
        (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ∘ₗ
      comul =
    comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap

Tactic:
ext x y

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
x : M
y : P
⊢ ((AlgebraTensorModule.curry
          (_root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
              (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ∘ₗ
            comul))
        x)
      y =
    ((AlgebraTensorModule.curry (comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap)) x) y
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑β.toPartOrd
⊢ (Hom.hom (ofHom ↑e.symm ≫ ofHom ↑e)) a✝ = (Hom.hom (𝟙 β)) a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
a✝ : ↑β.toLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 β)) a✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
a✝ : ↑β
⊢ (Hom.hom
        (ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
          ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }))
      a✝ =
    (Hom.hom (𝟙 β)) a✝

Tactic:
exact e.apply_symm_apply _

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✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f ⊥ = ⊥

Tactic:
← @sdiff_self α _ ⊤,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ⊥
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:
← @sdiff_self α _ ⊤,

Goal state after:
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 (⊤ \ ⊤) = ⊥
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
x✝ : ↑β
⊢ (Hom.hom ({ hom' := ↑e.symm } ≫ { hom' := ↑e })) x✝ = (Hom.hom (𝟙 β)) x✝

Tactic:
exact e.apply_symm_apply _

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.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ

Tactic:
TensorProduct.map_comp,

Goal state after:
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.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ s → x ∈ ↑(span s)

Tactic:
hx

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x ∈ ↑(span s)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
⊢ x ∈ span s → x ∈ span t

Tactic:
hx

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : x ∈ span s
⊢ x ∈ span t
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
⊢ x ∉ I → ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
hx

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
⊢ x ∈ I.jacobson → x ∈ J.jacobson

Tactic:
hx

Goal state after:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
⊢ x ∈ J.jacobson
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
⊢ x ∉ maximalIdeal R → x ∈ I → 1 ∈ I

Tactic:
hx

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
⊢ x ∈ I → 1 ∈ I
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
⊢ Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))

Tactic:
rcases R with ⟨α, str⟩

Goal state after:
α : Type u_1
commRing✝ : CommRing α
M : Submonoid ↑(CommRingCat.of α)
⊢ Epi (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of α)) (Localization M)))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) * (algebraMap R B) ↑(Submonoid.pow x m) = (algebraMap R B) (x ^ n)

Tactic:
Submonoid.pow_apply,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) * (algebraMap R B) ↑⟨x ^ m, ⋯⟩ = (algebraMap R B) (x ^ n)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 (Submonoid.pow x d.natAbs) * (algebraMap R B) (x ^ d.natAbs) = 1

pp: case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d

Tactic:
Submonoid.pow_apply,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 ⟨x ^ d.natAbs, ⋯⟩ * (algebraMap R B) (x ^ d.natAbs) = 1

case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ (algebraMap R B) (x ^ d.natAbs) * mk' B 1 (Submonoid.pow x d.natAbs) = 1

pp: case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0

Tactic:
Submonoid.pow_apply,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ (algebraMap R B) (x ^ d.natAbs) * mk' B 1 ⟨x ^ d.natAbs, ⋯⟩ = 1

case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A

Tactic:
convert! isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)
  exact (Submonoid.map_id S).symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ tensorμ (𝟙_ C) M (𝟙_ C) M ≫ (λ_ (𝟙_ C)).hom ▷ (M ⊗ M) ≫ (λ_ (M ⊗ M)).hom ≫ μ =
    ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ

Tactic:
slice_lhs 1 3 => rw [← leftUnitor_monoidal]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
⊢ tensorμ M M M M ≫ (μ ⊗ₘ μ) ≫ μ = (μ ⊗ₘ μ) ≫ μ

Tactic:
simp only [mon_tauto]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
⊢ tensorδ M M M M ≫ (μ ⊗ₘ μ) ≫ μ = (μ ⊗ₘ μ) ≫ μ

Tactic:
simp only [mon_tauto]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ f₂ ≫ t₂.inr ≫ m = f₂ ≫ t₂.inr ≫ l₂

Tactic:
hm₂,

Goal state after:
case h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
⊢ f₂ ≫ s.inr = f₂ ≫ t₂.inr ≫ l₂
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:
rw [map_add, f.map_add, ihx, ihy]

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:
hx

Goal state after:
α : 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) x = ↑n
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
have := Classical.decPred (· ∈ s)
  have : ∀ x, IsSupported x s →
        ∃ n : ℤ, lift (fun a => if a ∈ s then (0 : ℤ[X]) else Polynomial.X) x = n := by
    intro x hx
    refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
    · use 1
      rw [map_one]
      norm_cast
    · use -1
      rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
    · rintro _ ⟨z, hzs, rfl⟩ _ _
      use 0
      rw [map_mul, lift_of, if_pos hzs, zero_mul]
      norm_cast
    · rintro x y ⟨q, hq⟩ ⟨r, hr⟩
      refine ⟨q + r, ?_⟩
      rw [map_add, hq, hr]
      norm_cast
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ IsUnit (↑e ∘ₗ (algebraMap R (End R M')) ↑s ∘ₗ ↑e.symm)

Tactic:
Module.End.isUnit_iff,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ Function.Bijective ⇑(↑e ∘ₗ (algebraMap R (End R M')) ↑s ∘ₗ ↑e.symm)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
⊢ IsConnected (ULiftHom (ULift.{u₂, u₁} J))

Tactic:
apply IsConnected.of_induct
  · rintro p hj₀ h ⟨j⟩
    let p' : Set J := {j : J | ⟨j⟩ ∈ p}
    have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
      simp only [p']
      exact hj₀
    apply induct_on_objects p' hj₀' fun f => h ((ULiftHomULiftCategory.equiv J).functor.map f)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : EssentiallySmall.{w, v, u} C
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage

Tactic:
← ObjectProperty.map_top

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : EssentiallySmall.{w, v, u} C
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (⊤.map F)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
⊢ x ∈ RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) →
    x ∈ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)

Tactic:
hx

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : x ∈ RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ x ∈ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)