mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_2
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✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

Tactic:
[

Goal state after:
case refine_2
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✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_3
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✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
[

Goal state after:
case refine_3
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✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)

Tactic:
[

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ tensorμ M N M N

Tactic:
← tensorμ_natural_right

Goal state after:
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ tensorμ M N M N
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg : ∀ i ∈ t.disjSum t, (algebraMap R Rₛ) (fg i) = ↑a • Sum.elim g₁ g₂ i
⊢ g₁ i = g₂ i

Tactic:
[

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg : ∀ i ∈ t.disjSum t, (algebraMap R Rₛ) (fg i) = ↑a • Sum.elim g₁ g₂ i
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ↑a • ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ↑a • ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
⊢ g₁ i = g₂ i

Tactic:
[

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ↑a • ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ↑a • ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : s • ∑ i ∈ t, fg (Sum.inl i) • v i = s • ∑ i ∈ t, fg (Sum.inr i) • v i
⊢ g₁ i = g₂ i

Tactic:
[

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : s • ∑ i ∈ t, fg (Sum.inl i) • v i = s • ∑ i ∈ t, fg (Sum.inr i) • v i
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case e_6
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
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
w✝¹ w✝ : ι →₀ R
eq✝ : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
i : ι
s : ↥S
eq : s • (Finsupp.linearCombination R v) w✝¹ = s • (Finsupp.linearCombination R v) w✝
⊢ w✝¹ i = w✝ i

Tactic:
[

Goal state after:
case e_6
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
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
w✝¹ w✝ : ι →₀ R
eq✝ : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
i : ι
s : ↥S
eq : s • (Finsupp.linearCombination R v) w✝¹ = s • (Finsupp.linearCombination R v) w✝
⊢ w✝¹ i = w✝ i
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 g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t, (g i * ↑(sec (v i)).2) • v i = ∑ i ∈ t, (g' i * ↑(sec (v i)).2) • v i

Tactic:
[

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
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t, (g i * ↑(sec (v i)).2) • v i = ∑ i ∈ t, (g' i * ↑(sec (v i)).2) • v i
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (β_ X Y).hom ▷ (X ⊗ Y) ≫ (Y ⊗ X) ◁ (β_ X Y).hom

pp: case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y X (Y ⊗ X)).hom

pp: case a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ X Y X).inv

pp: case a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (β_ X Y).hom ▷ X

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ Y X X).hom

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y Y (X ⊗ X)).inv

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| μ ⊗ₘ μ

Tactic:
← tensorHom_def

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (β_ X Y).hom ⊗ₘ (β_ X Y).hom

case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y X (Y ⊗ X)).hom

case a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ X Y X).inv

case a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (β_ X Y).hom ▷ X

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ Y X X).hom

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y Y (X ⊗ X)).inv

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| μ ⊗ₘ μ
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ («μ» F X X ≫ F.map μ) ▷ F.obj X ≫ «μ» F X X ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ («μ» F X X ≫ F.map μ) ≫ «μ» F X X ≫ F.map μ

Tactic:
[

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ («μ» F X X ≫ F.map μ) ▷ F.obj X ≫ «μ» F X X ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ («μ» F X X ≫ F.map μ) ≫ «μ» F X X ≫ F.map μ
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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g ⋯)
⊢ IsColimit (BinaryCofan.mk f g)

Tactic:
apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁

Goal state after:
case hc
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 : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g ⋯)
⊢ IsColimit
    (PushoutCocone.mk ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left })
      ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right }) ⋯)

case f
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 : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g ⋯)
⊢ W ⟶ (pair X Y).obj { as := WalkingPair.left }

case g
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 : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g ⋯)
⊢ W ⟶ (pair X Y).obj { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingCospan ⥤ C
c : Cone D
hc : IsLimit c
⊢ c.π.app WalkingCospan.left ≫ D.map WalkingCospan.Hom.inl = c.π.app WalkingCospan.right ≫ D.map WalkingCospan.Hom.inr

Tactic:
[

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingCospan ⥤ C
c : Cone D
hc : IsLimit c
⊢ c.π.app WalkingCospan.left ≫ D.map WalkingCospan.Hom.inl = c.π.app WalkingCospan.right ≫ D.map WalkingCospan.Hom.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingSpan ⥤ C
c : Cocone D
hc : IsColimit c
⊢ D.map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left = D.map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right

Tactic:
[

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingSpan ⥤ C
c : Cocone D
hc : IsColimit c
⊢ D.map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left = D.map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right
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_5
M₂ : Type u_6
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₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
[

Goal state after:
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_5
M₂ : Type u_6
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₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_3
f : M × ↥S → α
wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'
m : M
s : ↥S
⊢ (mk m s).liftOn f wd = f (m, s)

Tactic:
convert! Quotient.liftOn_mk f wd ⟨m, s⟩

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)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) x)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) ↑y))

Tactic:
[

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)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) x)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) ↑y))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l

Tactic:
simpa [← hm₁] using hl.symm

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)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ B, Algebra.IsPushout.comm,
    ← Algebra.IsPushout.comp_iff R _ S]

Goal state after:
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)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1

Tactic:
[

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1