mathlib-initiative/mathlib-tactics huggingface dataset:
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) *
      (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)

Tactic:
mul_assoc,

Goal state after:
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) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N)) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) *
      ((algebraMap R (Away (↑a * ↑b))) (↑b ^ N) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N))
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)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r a * ↑b ^ N) =
    (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r b * ↑a ^ N)

Tactic:
mul_assoc,

Goal state after:
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)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
        (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
          N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
      ((↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ * (r a * ↑b ^ N)) =
    (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r b * ↑a ^ N)
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)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ i, c i * r i * ↑a ^ N) = (algebraMap R (Away ↑a)) (r a)

Tactic:
mul_assoc,

Goal state after:
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)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ x, c x * (r x * ↑a ^ N)) = (algebraMap R (Away ↑a)) (r a)
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit ((CommRingCat.Hom.hom f.hom) a)
⊢ IsUnit a

Tactic:
convert! f.inv.hom.isUnit_map ha
      simp

Goal state after:
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
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [selfZPow_of_neg _ _ (lt_of_le_of_ne hn hn0)]

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

Goal state before:
pp: 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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * selfZPow x B (-d) * mk' B a 1 = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
mul_assoc,

Goal state after:
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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * (selfZPow x B (-d) * mk' B a 1) = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) * selfZPow x B d = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
mul_assoc,

Goal state after:
case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' B a 1 * (selfZPow x B (-d) * selfZPow x B d) = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' B a 1 * (selfZPow x B (-d) * selfZPow x B d) = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
mul_assoc,

Goal state after:
case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * (mk' B a 1 * (selfZPow x B (-d) * selfZPow x B d)) = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
⊢ ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b

Tactic:
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H : b * (algebraMap R B) ↑(a₀, y).2 = (algebraMap R B) (a₀, y).1
⊢ ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
⊢ ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b

Tactic:
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
  obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
  have ha₀ : a₀ ≠ 0 := by
    have := isDomain_of_le_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
    simp only [← hy, map_pow] at H
    apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
    · rw [← H]
      apply mul_ne_zero hb (pow_ne_zero _ _)
      exact
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
          (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
    · exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
  simp only [← hy] at H
  obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx
  refine ⟨a, m - d, ?_⟩
  rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast,
    ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
  exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩

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

Goal state before:
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 ≫ μ

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
| tensorμ M N M N ▷ (M ⊗ N)

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
| tensorμ (M ⊗ M) (N ⊗ N) M N

Tactic:
mul_assoc,

Goal state after:
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 M M).hom ≫ M ◁ μ ≫ μ ⊗ₘ μ ▷ 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
| tensorμ M N M N ▷ (M ⊗ N)

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
| tensorμ (M ⊗ M) (N ⊗ N) M N
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
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 M M).hom ≫ M ◁ μ ≫ μ ⊗ₘ μ ▷ 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
| tensorμ M N M N ▷ (M ⊗ N)

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
| tensorμ (M ⊗ M) (N ⊗ N) M N

Tactic:
mul_assoc,

Goal state after:
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 M M).hom ≫ M ◁ μ ≫ μ ⊗ₘ (α_ N N N).hom ≫ 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
| tensorμ M N M N ▷ (M ⊗ N)

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
| tensorμ (M ⊗ M) (N ⊗ 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ₛ
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 (∑ x, fg (Sum.inr ↑x) • v ↑x)
⊢ g₁ i = g₂ i

Tactic:
t.sum_coe_sort (f := fun x ↦ fg (Sum.inr x) • v x)

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)
⊢ g₁ i = g₂ i
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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'

Tactic:
← cancel_epi e₁.hom,

Goal state after:
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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'

Tactic:
← cancel_epi e₁.hom,

Goal state after:
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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: M : Type u_7
N : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ map f (IsUnit.submonoid M) ≤ IsUnit.submonoid N

Tactic:
by
  rintro x ⟨y, hy, rfl⟩
  exact hy.map _

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S

Tactic:
by
  rintro x ⟨y, hy, rfl⟩
  exact hy.map _

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * ↑a.2 * ↑b.2 = ↑u * ↑b.2 * ↑a.2

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * (↑a.2 * ↑b.2) = ↑u * ↑b.2 * ↑a.2
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * (↑a.2 * ↑b.2) = ↑u * ↑b.2 * ↑a.2

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * (↑a.2 * ↑b.2) = ↑u * (↑b.2 * ↑a.2)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑s' * (↑c * ↑s) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    (↑s' * (↑c * ↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2) * r) • m

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑s' * (↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1))) • m =
    (↑s' * (↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r))) • m
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 : X ⟶ Z
g : Y ⟶ Z
X' : C
i : X' ⟶ X
inst✝ : IsIso i
⊢ HasPullback (i ≫ f) g ↔ HasPullback f g

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
X' : C
i : X' ⟶ X
inst✝ : IsIso i
h : HasPullback (i ≫ f) g
⊢ HasPullback f g
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 : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
⊢ HasPushout (f ≫ i) g ↔ HasPushout f g

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
h : HasPushout (f ≫ i) g
⊢ HasPushout f g
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case add
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝

Tactic:
| add _ _ hx hy =>

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

Goal state before:
pp: case h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
        ↑s) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m

pp: case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)

Tactic:
· simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_eq_mul]; ring_nf

Goal state after:
case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))