mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case pred
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-↑m - 1)) x =
    (Polynomial.eval t (S R (-↑m - 1)) + Polynomial.eval t (S R (-↑m - 1 - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1 - 1)) * -g x) • y

Tactic:
sub_eq_add_neg (-m : ℤ) 1,

Goal state after:
case pred
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-↑m + -1)) x =
    (Polynomial.eval t (S R (-↑m + -1)) + Polynomial.eval t (S R (-↑m + -1 - 1))) • x +
      (Polynomial.eval t (S R (-↑m + -1 - 1)) * -g x) • y
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-↑n)) = S R' (-↑n)
ih2 : map f (S R (-↑n + 1)) = S R' (-↑n + 1)
⊢ map f (S R (-↑n - 1)) = S R' (-↑n - 1)

Tactic:
simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

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

Goal state before:
pp: case calc_3
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

Tactic:
← smul_comm,

Goal state after:
case calc_3
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ P.pairing i j • (P.toLinearMap x) (P.coroot i) • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case add
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : u ∈ span R (⇑P.root '' s)
hv : v ∈ span R (⇑P.root '' s)
hu' : (P.reflection j) u = u
hv' : (P.reflection j) v = v
⊢ u + (P.reflection j) v = u + v

Tactic:
hv'

Goal state after:
case add
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u v : M
hu : u ∈ span R (⇑P.root '' s)
hv : v ∈ span R (⇑P.root '' s)
hu' : (P.reflection j) u = u
hv' : (P.reflection j) v = v
⊢ u + v = u + v
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝ : IsReflexive L M
this : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = span L ↑M'
hv₃ : LinearIndependent L Subtype.val
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
hM

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝ : IsReflexive L M
this : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)
Module: Mathlib.RingTheory.DedekindDomain.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ comap e.symm P ≠ ⊥

Tactic:
simp [Ideal.map_eq_bot_iff_of_injective e.injective, hP_ne]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
· rw [coeff_scaleRoots]
    refine (dvd_mul_of_dvd_right ?_ _).mul_right _
    convert! pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
    · exact (pow_one _).symm
    simpa using h

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
tfae_have 2 → 5 := fun _ ↦ ⟨s, WellFoundedGT.finite_of_sSupIndep hs.1, hs⟩

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
⊢ (Order.krullDim (Submodule S M)).unbot ⋯ = (Order.krullDim (Submodule R M)).unbot ⋯

Tactic:
WithBot.unbot_inj,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
⊢ Order.krullDim (Submodule S M) = Order.krullDim (Submodule R M)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
⊢ Order.krullDim (Submodule S M) = Order.krullDim (Submodule R M)

Tactic:
Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
⊢ Order.krullDim (Submodule R M) = Order.krullDim (Submodule R M)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.inl
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 b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)

Tactic:
right

Goal state after:
case mk.mk.inl
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 b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)
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
x : K
⊢ x ∈ (valuation A K).integer ↔ ∃ a, (algebraMap A K) a = x

Tactic:
by
  constructor
  · rintro ⟨c, rfl⟩
    use c
    rw [Algebra.smul_def, mul_one]
  · rintro ⟨c, rfl⟩
    use c
    rw [Algebra.smul_def, mul_one]

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

Goal state before:
pp: case inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
right

Goal state after:
case inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ IsUnit (1 - a)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
h : ∃ x ∈ α, x ∉ β
⊢ α ≤ β ∨ β ≤ α

Tactic:
obtain ⟨a, h₁, h₂⟩ := h

Goal state after:
case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
⊢ α ≤ β ∨ β ≤ α
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
⊢ α ≤ β ∨ β ≤ α

Tactic:
right

Goal state after:
case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
⊢ β ≤ α
Module: Mathlib.RingTheory.Valuation.Integers

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

Tactic:
rcases min_cases 1 γ with ⟨h, h'⟩ | ⟨h, h'⟩ <;> rw [h] at hx

Goal state after:
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

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.Valuation.ValuationRing

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
right

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
h : p ∣ b
⊢ p ∣ 1 ∨ p ∣ b

Tactic:
right

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
h : p ∣ b
⊢ p ∣ 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
⊢ (Multiset.map Associates.mk fx).card = fx.card ∧ ∀ b ∈ Multiset.map Associates.mk fx, b = Associates.mk p

Tactic:
simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]

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
⊢ ∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk p
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_sInf_maximal]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ {I : Ideal S}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
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).card = fx.card ∧ ∀ b ∈ Multiset.map Associates.mk fx, b = Associates.mk ϖ

Tactic:
simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]

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
⊢ ∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk ϖ
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ v x < 1 ↔ 1 < v x⁻¹

Tactic:
by
  simp [one_lt_inv₀ (v.pos_iff.2 h)]

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

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

Tactic:
by_cases hx : x = 0

Goal state after:
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

case neg
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
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:
φ'.map_mul,

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'' * φ' ((algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0) + if y ∣ x then 0 else x) = x

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : y ∣ x
⊢ y * 0 + 0 = x

case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x

case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ y * Exists.choose h₂ + 0 = x

case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : x = 0
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ ¬toWithBotNat (x * y) < toWithBotNat x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ toWithBotNat x ≤ toWithBotNat (x * y)

Tactic:
toWithBotNat_le_toWithBotNat_iff hx (mul_ne_zero hx hy)

Goal state after:
case neg
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ x ∣ x * y