mathlib-initiative/mathlib-tactics huggingface dataset:
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
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ F.obj A ◁ (F.map Δ ≫ δ F A A) =
    (F.map Δ ≫ δ F A A) ≫ (F.map Δ ≫ δ F A A) ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom

Tactic:
simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc,
      ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]

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

Goal state before:
pp: case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single 1 r)

Tactic:
intro

Goal state after:
case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
r✝ : ↑R
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single 1 r✝)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑X✝),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single m 1)

Tactic:
intro

Goal state after:
case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m✝ : ↑X✝
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single m✝ 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
                ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯ ≫
              (𝟭 (Under R)).map f)))
        (MonoidAlgebra.single 1 r)

Tactic:
intro

Goal state after:
case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single 1 r✝)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ∀ (m : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)),
    (Hom.hom
          (Under.Hom.right
            (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
                ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯ ≫
              (𝟭 (Under R)).map f)))
        (MonoidAlgebra.single m 1)

Tactic:
intro

Goal state after:
case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
m✝ : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single m✝ 1)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ normalize a ::ₘ replicate n (normalize a) ≤ {normalize a} + normalizedFactors (a ^ n * c)

Tactic:
singleton_add,

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ normalize a ::ₘ replicate n (normalize a) ≤ normalize a ::ₘ normalizedFactors (a ^ n * c)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
G : CommMonCat
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r)

Tactic:
intro

Goal state after:
case h₁
R : CommRingCat
G : CommMonCat
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r✝)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h_of
R : CommRingCat
G : CommMonCat
⊢ ∀ (m : ↑G),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single m 1) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m 1)

Tactic:
intro

Goal state after:
case h_of
R : CommRingCat
G : CommMonCat
m✝ : ↑G
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m✝ 1)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
⊢ count p (normalizedFactors x) = n

Tactic:
by_cases hx0 : x = 0
  · simp [hx0] at hlt
  apply Nat.cast_injective (R := ℕ∞)
  convert! (emultiplicity_eq_count_normalizedFactors hp hx0).symm
  · exact hnorm.symm
  exact (emultiplicity_eq_coe.mpr ⟨hle, hlt⟩).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.powers (f a)) Bₚ

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ span s ≤ I ↔ s ⊆ ↑I

Tactic:
by
  rw [TwoSidedIdeal.ringCon_le_iff, RingCon.gi _ |>.gc]
  exact ⟨fun h x hx ↦ by aesop, fun h x y hxy ↦ (rel_iff I x y).mpr (h hxy)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N * ↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N * ↑a ^ N)

Tactic:
mul_comm

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r = 1
⊢ IsUnit r

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : r * s = 1
⊢ IsUnit r
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R

Tactic:
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
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
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ (algebraMap R B) x ^ m.natAbs * mk' B 1 (Submonoid.pow x n.natAbs) =
    mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs

Tactic:
mul_comm

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
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs =
    mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ IsInteger R (a • b)

Tactic:
use a * b'

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) (a * b') = a • b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
gh : Y₂ ⊗ Z₂ ⟶ W
⊢ (α_ X₁ Y₁ Z₁).hom ≫ (f ⊗ₘ (g ⊗ₘ h) ≫ gh) = ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).hom ≫ (𝟙 X₂ ⊗ₘ gh)

Tactic:
simp [tensorHom_def]

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

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

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X : C
inst✝ : MonObj M
f : X ⟶ M
⊢ (α_ X M M).hom ≫ (f ⊗ₘ μ) ≫ μ = ((f ⊗ₘ 𝟙 M) ≫ μ ⊗ₘ 𝟙 M) ≫ μ

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
⊢ ∀ (g_1 : ι → R), ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g_1 i • (sec (v i)).1 → ∀ i ∈ t, g i = g_1 i

Tactic:
g'

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
t : Finset ι
g g' : ι → R
⊢ ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1 → ∀ i ∈ t, g i = g' i
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
inst✝ : BraidedCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom

Tactic:
simp [tensorHom_def]

Goal state after:
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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst✝ : MonObj (F.obj X)
⊢ F.map (hF.preimage («η» F ≫ η) ▷ X ≫ hF.preimage (δ F X X ≫ μ)) = F.map (λ_ X).hom

Tactic:
by simp [← δ_natural_left_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ h.isoPushout.inv = inl

Tactic:
by
  dsimp [isoPushout, cocone, CommSq.cocone]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ h.isoPushout.inv = inr

Tactic:
by
  dsimp [isoPushout, cocone, CommSq.cocone]
  simp

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

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
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
⊢ IsLimit sq.cone

Tactic:
refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by cat_disch)
      simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]

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

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 : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)

Tactic:
infer_instance

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'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x✝ : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
⊢ Algebra.IsPushout R S A (S ⊗[R] A)

Tactic:
infer_instance

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'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
⊢ Algebra.IsPushout R S A (A ⊗[R] S)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this✝³ : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this✝² : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this✝¹ : IsScalarTower R A (S ⊗[R] B)
this✝ : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
⊢ Algebra.IsPushout R B S (S ⊗[R] B)

Tactic:
infer_instance

Goal state after: