mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b ≤ ↑(count (normalize a) (normalizedFactors b))

pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Tactic:
·

Goal state after:
case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b ≤ ↑(count (normalize a) (normalizedFactors b))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
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
hx0 : x = 0
⊢ count p (normalizedFactors x) = n

pp: case neg
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
hx0 : ¬x = 0
⊢ count p (normalizedFactors x) = n

Tactic:
·

Goal state after:
case pos
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
hx0 : x = 0
⊢ count p (normalizedFactors x) = n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case e'_2.e'_3
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
hx0 : ¬x = 0
⊢ p = normalize p

pp: case e'_3
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
hx0 : ¬x = 0
⊢ ↑n = emultiplicity p x

Tactic:
·

Goal state after:
case e'_2.e'_3
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
hx0 : ¬x = 0
⊢ p = normalize p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

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

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

Tactic:
·

Goal state after:
case inl
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
n : ℕ
hnorm : normalize 0 = 0
hle : 0 ^ n ∣ x
hlt : ¬0 ^ (n + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inl.zero
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
hle : 0 ^ 0 ∣ x
hlt : ¬0 ^ (0 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = 0

pp: case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ^ (n✝ + 1) ∣ x
hlt : ¬0 ^ (n✝ + 1 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1

Tactic:
·

Goal state after:
case inl.zero
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
hle : 0 ^ 0 ∣ x
hlt : ¬0 ^ (0 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

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

Tactic:
·

Goal state after:
case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ^ (n✝ + 1) ∣ x
hlt : ¬0 ^ (n✝ + 1 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

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

Tactic:
·

Goal state after:
case inr
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hp : Irreducible p
⊢ count p (normalizedFactors x) = n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : b = 0
⊢ a ∣ b

pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
⊢ a ∣ b

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : b = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∈ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∈ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
·

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ IsUnit ((algebraMap R S) (r * ↑u))

pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

pp: case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ IsUnit ((algebraMap R S) (r * ↑u))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

pp: case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0

pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Function.Surjective ⇑(map S Q f r) ↔ ∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a

pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Function.Surjective ⇑(map S Q f r) ↔ ∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a
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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
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
⊢ IsUnit ((algebraMap R T) (y * x))

pp: 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

pp: 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:
·

Goal state after:
case refine_1
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
⊢ IsUnit ((algebraMap R T) (y * x))
Module: Mathlib.RingTheory.Localization.Away.Basic

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

pp: 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:
·

Goal state after:
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
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: 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:
·

Goal state after:
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
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case e'_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
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 ^ m * x ^ n * (x ^ m * (y ^ n * a))

pp: case e'_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 : ℕ
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) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

pp: 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 ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
·

Goal state after:
case e'_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
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 ^ m * x ^ n * (x ^ m * (y ^ n * a))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case e'_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 : ℕ
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) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

pp: 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 ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
·

Goal state after:
case e'_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 : ℕ
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) * b = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: 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 ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
·

Goal state after:
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 ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))