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

Goal state before:
pp: case mpr.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ 1
h : min 1 γ = 1
h' : 1 ≤ γ
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

pp: case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
· exact ⟨⟨x, hx⟩, hx.trans h', rfl⟩

Goal state after:
case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
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
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
r : R
x : M
⊢ ⟨fun n ↦ (f n) (r • x), ⋯⟩ = (RingHom.id R) r • ⟨fun n ↦ (f n) x, ⋯⟩

Tactic:
simp only [LinearMapClass.map_smul, RingHom.id_apply]
    rfl

Goal state after:
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
q : R
hq : q ∈ fx
⊢ Associates.mk q = Associates.mk p

Tactic:
rw [Associates.mk_eq_mk_iff_associated]

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
q : R
hq : q ∈ fx
⊢ Associated q p
Module: Mathlib.RingTheory.Jacobson.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ⊥.jacobson ≤ sInf (map C '' {J | J.IsMaximal})

Tactic:
refine le_sInf fun J => exists_imp.2 fun j hj => ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
⊢ ⊥.jacobson ≤ J
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ (∀ J ∈ Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal}, J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm

Goal state after:
case right
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})
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
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associates.mk x✝ = Associates.mk ϖ

Tactic:
rw [Associates.mk_eq_mk_iff_associated]

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
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associated x✝ ϖ
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ∃ n_1 u_1, ϖ ^ n * ↑u = ↑u_1 * ϖ ^ n_1

Tactic:
use n, u

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ϖ ^ n * ↑u ≠ 0
hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)
⊢ ϖ ^ n * ↑u = ↑u * ϖ ^ n
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x

Tactic:
intro ⟨h₁, h₂⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
⊢ ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m n : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ n
⊢ u = v

Tactic:
by
  obtain rfl : m = n := unit_mul_pow_congr_pow hirr hirr u v m n h
  rw [← sub_eq_zero] at h
  rw [← sub_mul, mul_eq_zero] at h
  rcases h with h | h
  · rw [sub_eq_zero] at h
    exact mod_cast h
  · apply (hirr.ne_zero (eq_zero_of_pow_eq_zero h)).elim

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : (addVal R) a ≤ (addVal R) b
ha0 : a = 0
⊢ a ∣ b

Tactic:
rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
      rw [h]
      apply dvd_zero

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : x = 0
⊢ Associated x y

Tactic:
simp_all only [AddValuation.map_zero]
      rw [addVal_eq_top_iff.mp h.symm]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ φ' q'' * (algebraMap (R[X] ⧸ P) Sₘ) (φ q') = φ' q'' * φ' ((algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩)

Tactic:
← φ'.comp_apply

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ φ' q'' * (algebraMap (R[X] ⧸ P) Sₘ) (φ q') = φ' q'' * (φ'.comp (algebraMap (R ⧸ P') Rₘ)) ↑⟨q', hq'⟩
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) =
    φ' ((algebraMap (R ⧸ P') Rₘ) ((Ideal.Quotient.mk P') (p.coeff 0)))

Tactic:
← φ'.comp_apply

Goal state after:
case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) =
    (φ'.comp (algebraMap (R ⧸ P') Rₘ)) ((Ideal.Quotient.mk P') (p.coeff 0))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
⊢ ⊥.jacobson = ⊥

Tactic:
have hϕ' : comap (algebraMap S Sₘ) (⊥ : Ideal Sₘ) = (⊥ : Ideal S) := by
      rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
      exact IsLocalization.injective Sₘ hM

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
⊢ ⊥.jacobson = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : (algebraMap R K) b * (algebraMap R K) y / (algebraMap R K) a = 1
⊢ ∃ y ∈ maximalIdeal R, b * y = a

Tactic:
div_eq_one_iff_eq ha₃,

Goal state after:
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
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : (algebraMap R K) b * (algebraMap R K) y = (algebraMap R K) a
⊢ ∃ y ∈ maximalIdeal R, b * y = a
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
hFG : ⊥.FG
x y : ↥⊥ ⊗[R] M
⊢ x = y

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case neg.hxy
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
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hx'.choose).2 * (ofClass v) (↑hy'.choose).1 ≠ 0

Tactic:
· simpa only [MonoidWithZeroHom.coe_ofClass, ← map_mul v, ne_eq, h.eq_zero, map_mul w]
          using mul_ne_zero hx20 hy10

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

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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j : ι
⊢ root ((RootPairing.equiv_of_mapsTo p root coroot i hr hp) j) = (preReflection (root i) (p.flip (coroot i))) (root j)

Tactic:
equiv_of_mapsTo_apply,

Goal state after:
ι : 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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j : ι
⊢ root ⋯.choose = (preReflection (root i) (p.flip (coroot i))) (root j)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
n : ℕ
⊢ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j) ∈ range ⇑P.root

Tactic:
rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo (P.coroot_root_two i)
      (P.mapsTo_reflection_root i)).comp (bijOn_reflection_of_mapsTo (P.coroot_root_two j)
      (P.mapsTo_reflection_root j))).image_eq n]

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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
n : ℕ
⊢ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j) ∈
    (⇑(Module.reflection ⋯) ∘ ⇑(Module.reflection ⋯))^[n] '' range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case h
ι : 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✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
i j : ι
⊢ root ((RootPairing.equiv_of_mapsTo p root coroot i hs hp) j) = (preReflection (root i) (p.flip (coroot i))) (root j)

Tactic:
equiv_of_mapsTo_apply,

Goal state after:
case h
ι : 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✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
i j : ι
⊢ root ⋯.choose = (preReflection (root i) (p.flip (coroot i))) (root j)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : x = 0
⊢ 0 • x = ⁅coroot α, x⁆

Tactic:
by simp [hx']

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
i : ↑s
⊢ 2 / (P.RootForm (P.root ↑i)) (P.root ↑i) ≠ 0

Tactic:
by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert.inr.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ x ∈ ⋃ i ∈ s, ↑(p i)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y ∉ p j := by specialize h₁ j; contrapose! h₁; ext; simp [h₁]

Goal state after:
case insert.inr.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
⊢ x ∈ ⋃ i ∈ s, ↑(p i)