mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ ⦃a : ValueGroup A K⦄, 0 < a → ∀ ⦃b c : ValueGroup A K⦄, b < c → a * b < a * c

Tactic:
by
    simp_rw [← not_le]
    rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ hbc
    contrapose hbc
    obtain ⟨d, hd⟩ := hbc
    simp only [Algebra.smul_def, mul_left_comm, mul_eq_mul_left_iff] at hd
    obtain rfl | rfl := hd
    · exact ⟨d, by simp [Algebra.smul_def]⟩
    · cases ha le_rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) (0 n✝) = 0 m✝

Tactic:
Pi.zero_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) 0 = 0 m✝
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) 0 = 0 m✝

Tactic:
Pi.zero_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) 0 = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : IsPrime (R ∙ q)
hq : q ≠ 0
⊢ R ∙ q = maximalIdeal R

Tactic:
submodule_span_eq,

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : (span {q}).IsPrime
hq : q ≠ 0
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr.succ
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ f (n + 1) [SMOD I ^ m • ⊤]

Tactic:
trans

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ ?m.68 [SMOD I ^ m • ⊤]

R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ?m.68 ≡ f (n + 1) [SMOD I ^ m • ⊤]

R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ M
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ span {a} = span {b}

Tactic:
← ha,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ maximalIdeal R = span {b}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ Associates.mk p ^ fx.card = (Multiset.map Associates.mk fx).prod

Tactic:
← Multiset.prod_replicate

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.replicate fx.card (Associates.mk p)).prod = (Multiset.map Associates.mk fx).prod
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.map Associates.mk fx).prod = Associates.mk ϖ ^ fx.card

Tactic:
← Multiset.prod_replicate

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.map Associates.mk fx).prod = (Multiset.replicate fx.card (Associates.mk ϖ)).prod
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (-x * y + 1)

Tactic:
rw [add_comm]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (1 + -x * y)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x : K
hx : x ≠ 0
⊢ ∃ n u, x = u • (algebraMap R K) ϖ ^ n

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x y : R
hy : y ∈ nonZeroDivisors R
hx : (algebraMap R K) x / (algebraMap R K) y ≠ 0
⊢ ∃ n u, (algebraMap R K) x / (algebraMap R K) y = u • (algebraMap R K) ϖ ^ n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h.zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : f 0 - L ∈ I ^ 0
⊢ (1 - x * y) * f 0 - 1 ∈ I ^ 0

pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ (1 - x * y) * f (n✝ + 1) - 1 ∈ I ^ (n✝ + 1)

Tactic:
· simp only [Ideal.one_eq_top, pow_zero, mem_top]

Goal state after:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ (1 - x * y) * f (n✝ + 1) - 1 ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (x + y) = v x

Tactic:
rw [add_comm]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (y + x) = v x
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ∀ b ∈ {J | I ≤ J ∧ J.IsPrime}, IsLocalRing.maximalIdeal R ≤ b

Tactic:
rintro J ⟨h₁, h₂⟩
    exact (Ring.KrullDimLE.eq_maximalIdeal_of_isPrime J).ge

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ b ∈ f, Irreducible b
hf₂ : f ≠ ∅
hr₁ : f.prod ≠ 0
hr₂ : f.prod ∈ nonunits R
this : ∀ b ∈ f, Associated x b
⊢ ∃ n, Associated (x ^ n) f.prod

Tactic:
clear hr₁ hr₂ hf₁

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂ : f ≠ ∅
this : ∀ b ∈ f, Associated x b
⊢ ∃ n, Associated (x ^ n) f.prod
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case h.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
⊢ s ∈ maximalIdeal R ^ Nat.find this

Tactic:
by_cases hs₃ : s = 0

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ 0
H : ¬v (x + y) = 0
hy : v y = 0
⊢ v (x + y) ≤ v x ∨ ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩ ≤ if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simpa [hy] using map_add_le _ (le_rfl (a := v x)) (hy ▸ zero_le)

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ∞
hvx : (addVal R) x = vx
⊢ vx ≤ (addVal R) y ↔ x ∣ y

Tactic:
generalize hvy : addVal R y = vy

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ∞
hvx : (addVal R) x = vx
vy : ℕ∞
hvy : (addVal R) y = vy
⊢ vx ≤ vy ↔ x ∣ y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)) =
    ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)

Tactic:
rw [valueGroup₀Fun_spec h, valueGroup₀Fun_spec h.symm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
property✝¹ : R ∙ x ∈ (Ideal R)⁰
y : R
property✝ : R ∙ y ∈ (Ideal R)⁰
⊢ (R ∙ x) * (R ∙ y) = R ∙ x * y

Tactic:
submodule_span_eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
property✝¹ : R ∙ x ∈ (Ideal R)⁰
y : R
property✝ : R ∙ y ∈ (Ideal R)⁰
⊢ span {x} * span {y} = span {x * y}
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
refine ⟨⟨y, ?_⟩⟩

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ maximalIdeal R = R ∙ y
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
⊢ (algebraMap R (T ⧸ P)).IsIntegral

Tactic:
let Q' := Q.comap (Polynomial.C)

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
⊢ (algebraMap R (T ⧸ P)).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case hp
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ ∀ x ∈ Q.rootSpan K, ∀ y ∈ Q.corootSpan K, (Q.toLinearMap x) y ∈ (algebraMap K L).range

Tactic:
· exact Q.toLinearMap_apply_apply_mem_range_algebraMap K

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ v x ≤ v y ↔ v' x ≤ v' y

Tactic:
rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀] <;>
      rwa [zero_lt_iff, ne_zero_iff]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ v 1 = 0

Tactic:
rw [← mem_supp_iff, h]

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ 1 ∈ ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (2 * 2) • P.root i = 4 • P.root i

Tactic:
norm_num

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x✝ : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
⊢ 2 * 2 = 4

Tactic:
norm_num

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝¹ : IsAddTorsionFree M
this✝ : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : 4 • P.root i = 2 • P.root j
⊢ 4 = 2 * 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot j) = 1 ∧ (P.root' j) (2 • P.coroot j) = 4

Tactic:
norm_num

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ P.pairing i j = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ (pi Q) (Pi.single i m) = (Q i) m

Tactic:
rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ (pi Q) (Pi.single i m) = (Q i) m

Tactic:
by
  rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]
  rw [Pi.single_eq_of_ne hj, map_zero]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(ρ.asGroupHom g) = ρ g

Tactic:
simp only [asGroupHom, MonoidHom.coe_toHomUnits]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Nontrivial M
⊢ IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤

Tactic:
refine ⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
⊢ q = ⊤

case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
⊢ q = ⊥ ∨ q = ⊤
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
this : ∀ (z : α), x < z → y ≤ z
⊢ Ioo x y = ∅

Tactic:
ext z

Goal state after:
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
this : ∀ (z : α), x < z → y ≤ z
z : α
⊢ z ∈ Ioo x y ↔ z ∈ ∅