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
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
⊢ counit ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P) = counit

Tactic:
by ext; simp

Goal state after:
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
⊢ counit ∘ₗ ↑(_root_.TensorProduct.lid R P) = counit

Tactic:
by ext; simp

Goal state after:
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
⊢ counit ∘ₗ ↑(AlgebraTensorModule.rid R S M) = counit

Tactic:
by ext; simp

Goal state after:
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
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0

Tactic:
have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a : A
b : B
ℛa : Coalgebra.Repr R a ι
ℛb : Coalgebra.Repr R b κ
⊢ ∑ i ∈ ℛa.index ×ˢ ℛb.index, ℛa.left i.1 ⊗ₜ[R] ℛb.left i.2 ⊗ₜ[R] (ℛa.right i.1 ⊗ₜ[R] ℛb.right i.2) = comul (a ⊗ₜ[R] b)

Tactic:
by
    simp [← ℛa.eq, ← ℛb.eq, TensorProduct.sum_tmul ℛa.index, TensorProduct.tmul_sum,
      ← Finset.sum_product']

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O : C
inst✝³ : ComonObj M
inst✝² : ComonObj N
inst✝¹ : ComonObj O
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.inv ≫ ε = ε

Tactic:
simp [Iso.inv_comp_eq]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O : C
inst✝³ : ComonObj M
inst✝² : ComonObj N
inst✝¹ : ComonObj O
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.inv ≫ Δ = Δ ≫ (f.inv ⊗ₘ f.inv)

Tactic:
simp [Iso.inv_comp_eq]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (Δ ≫ A.X ◁ Δ ≫ (α_ A.X A.X A.X).inv).op = (α_ A.X A.X A.X).inv.op ≫ (Δ ≫ A.X ◁ Δ).op

Tactic:
op_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (A.X ◁ Δ ≫ (α_ A.X A.X A.X).inv).op ≫ Δ.op = (α_ A.X A.X A.X).inv.op ≫ (Δ ≫ A.X ◁ Δ).op
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
M N O : C
inst✝⁵ : ComonObj M
inst✝⁴ : ComonObj N
inst✝³ : ComonObj O
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
A : Comon C
⊢ { hom := F.map (𝟙 A).hom, isComonHom_hom := ⋯ } = 𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
⊢ (coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom =
    (RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
M N O : C
inst✝⁵ : ComonObj M
inst✝⁴ : ComonObj N
inst✝³ : ComonObj O
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X✝ Y✝ Z✝ : Comon C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ } =
    { hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }

Tactic:
by ext; simp

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
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
obtain ⟨z, rfl⟩ := H' z
    exact ⟨⟨z, 1⟩, by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ (TwoSidedIdeal.asIdeal I).toTwoSided = I

Tactic:
by ext; simp

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

Goal state before:
pp: case inl.inr
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 : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.inr
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 : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
· have : n + m = n.natAbs - m.natAbs := by
      rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
    rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]

Goal state after:
case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inr.inr
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 : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
e : M ≅ X
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom

Tactic:
(Tactic.exact
 "exact"
 (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm = LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f = LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[R] N
⊢ (fun e ↦ restrictScalars R e) ((fun e ↦ extendScalarsOfIsLocalization S A e) e) = e

Tactic:
by ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[A] N
⊢ (fun e ↦ extendScalarsOfIsLocalization S A e) ((fun e ↦ restrictScalars R e) e) = e

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ fst = pullback.fst f g

Tactic:
simp [Iso.inv_comp_eq]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ snd = pullback.snd f g

Tactic:
simp [Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

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
inst✝²⁸ : IsLocalization S A
M : Type u_3
inst✝²⁷ : AddCommMonoid M
inst✝²⁶ : Module R M
M' : Type u_4
inst✝²⁵ : AddCommMonoid M'
inst✝²⁴ : Module R M'
inst✝²³ : Module A M'
inst✝²² : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
⊢ IsLocalizedModule S (TensorProduct.map f g)

Tactic:
let eM := IsLocalizedModule.linearEquiv S f (TensorProduct.mk R (Localization S) M 1)
  let eN := IsLocalizedModule.linearEquiv S g (TensorProduct.mk R (Localization S) N 1)
  convert!
    IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm
  ext; congrm (?_ ⊗ₜ ?_) <;> simp [LinearEquiv.eq_symm_apply, eM, eN]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] IsLocalization.mk' (Localization M) x y) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)

Tactic:
h1,

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (tensorLeftAlgEquiv M S) ((algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)
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 f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
fapply Fork.IsLimit.mk
  · exact fun s => H.isLimit.lift (PullbackCone.mk s.ι s.ι s.condition)
  · exact fun s => H.isLimit.fac _ WalkingCospan.left
  · intro s m e
    apply PullbackCone.IsLimit.hom_ext H.isLimit <;> refine e.trans ?_ <;> symm <;>
      exact H.isLimit.fac _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ mk (a₁ * a₂) (s₂ * s₁) = mk (a₁ * a₂) (s₁ * s₂)

Tactic:
mul_comm s₁ s₂

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ mk (a₁ * a₂) (s₂ * s₁) = mk (a₁ * a₂) (s₂ * s₁)
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
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : F.Faithful
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
by simpa only [F.map_comp] using H.w

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
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : F.Faithful
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
by simpa only [F.map_comp] using H.w

Goal state after:
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.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 ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤

Tactic:
rw [← Subring.comap_map_eq_self_of_injective e.symm.injective (.closure _), RingHom.map_closure,
    ← top_le_iff, ← Subring.map_le_iff_le_comap, Set.image_union]

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (⇑(Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) '' Set.range ⇑(ConcreteCategory.hom a) ∪
        ⇑(Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) '' Set.range ⇑(ConcreteCategory.hom b))
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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ ∃ s', s' • m = 0

Tactic:
← mk'_zero f (1 : S),

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = mk' f 0 1 ↔ ∃ s', s' • m = 0
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
a b : B
f : a ⟶ b
⊢ (F.mapId a).inv ▷ F.map f = (λ_ (F.map f)).hom ≫ F.map₂ (λ_ f).inv ≫ (F.mapComp (𝟙 a) f).hom

Tactic:
simpa using congrArg (·.inv) (F.whiskerRightIso_mapId f)

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (const J).obj X✝ ⟶ (const J).obj Y✝
⊢ (const J).map (f.app (Classical.arbitrary J)) = f

Tactic:
ext j

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (const J).obj X✝ ⟶ (const J).obj Y✝
j : J
⊢ ((const J).map (f.app (Classical.arbitrary J))).app j = f.app j
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
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
← essentiallySmall_congr (ιOfLE h₁).asEquivalence

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} Q.FullSubcategory
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A

Tactic:
· rintro ⟨n, f, hfs, hfk⟩
    set ulift_var := MvPolynomial.renameEquiv R Equiv.ulift
    refine
      ⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
        Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩
    simpa using! Submodule.fg_bot

Goal state after:
case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁸ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁷ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁶ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P✝ : MorphismProperty T
Q✝ : MorphismProperty A
W✝ : MorphismProperty B
inst✝⁵ : Q✝.IsMultiplicative
inst✝⁴ : W✝.IsMultiplicative
P P' : MorphismProperty T
Q Q' : MorphismProperty A
W W' : MorphismProperty B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst✝³ : Q.IsMultiplicative
inst✝² : Q'.IsMultiplicative
inst✝¹ : W.IsMultiplicative
inst✝ : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h : (changeProp L R hP hQ hW).map f = (changeProp L R hP hQ hW).map g
⊢ Hom.hom f = Hom.hom g

Tactic:
exact congr($(h).hom)

Goal state after: