-- Mathlib/RingTheory/Localization/Away/Basic.lean
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `y * x`. See `IsLocalization.Away.mul'` for the `x * y` version. -/
lemma mul (T : Type*) [CommSemiring T] [Algebra S T]
    [Algebra R T] [IsScalarTower R S T] (x y : R)
    [IsLocalization.Away x S] [IsLocalization.Away (algebraMap R S y) T] :
    IsLocalization.Away (y * x) T

Proof state:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

Tactic:
obtain ⟨m, p, hpq⟩ := surj (algebraMap R S y) z

Result:
case refine_2.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

Proof state:
case refine_3.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
use n + m

Result:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ (y * x) ^ (n + m) * a = (y * x) ^ (n + m) * b

Proof state:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ m * (algebraMap S T) ((algebraMap R S) y) ^ n *
      (algebraMap S T) ((algebraMap R S) x) ^ n =
    (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ n * (algebraMap S T) ((algebraMap R S) x) ^ m *
      (algebraMap S T) ((algebraMap R S) y) ^ n

Tactic:
ring

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

Tactic:
use m + n, a * x ^ m * y ^ n

Result:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ z * (algebraMap R T) (y * x) ^ (m + n) = (algebraMap R T) (a * x ^ m * y ^ n)

Proof state:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ z * (algebraMap R T) (y * x) ^ (m + n) = (algebraMap R T) (a * x ^ m * y ^ n)

Tactic:
simp only [mul_pow, pow_add, map_pow, map_mul, ← mul_assoc, hpq,
  IsScalarTower.algebraMap_apply R S T, ← hab]

Result:
case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ m * (algebraMap S T) ((algebraMap R S) y) ^ n *
      (algebraMap S T) ((algebraMap R S) x) ^ n =
    (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ n * (algebraMap S T) ((algebraMap R S) x) ^ m *
      (algebraMap S T) ((algebraMap R S) y) ^ n

Proof state:
case refine_3.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
obtain ⟨m, hm⟩ := exists_of_eq x hn

Result:
case refine_3.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Proof state:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
repeat rw [IsScalarTower.algebraMap_apply R S T] at h

Result:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b