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

Goal state before:
pp: case intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1
⊢ (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = B

Tactic:
classical
  simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using! congr_arg (B * ·) hB

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

Goal state before:
pp: 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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
⊢ 1 = inv * ↑(den A r)

Tactic:
simpa [mul_comm] using h_inv

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

Goal state before:
pp: case left
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) / (algebraMap A K) ↑(den A r) = (algebraMap A K) (num A r * inv)

Tactic:
div_eq_iff d_ne_zero,

Goal state after:
case left
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r * inv) * (algebraMap A K) ↑(den A r)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Tactic:
have h₁ := T_mul_T R ((m + 1) * n) n

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
⊢ f (-1) ^ Nat.succ 1 = 1

Tactic:
rw [← map_pow, neg_one_sq, map_one]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝ : Ring R
α β : Type u_5
⊢ ∀ [inst : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case of_equiv
R : Type u_1
inst✝¹ : Ring R
α β : Type u_5
inst✝ : Fintype β
⊢ ∀ (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝¹ : Ring R
α β : Type u_5
inst✝ : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    length R ((i : α) → M i) = ∑ i, length R (M i)
M : β → Type u_6
⊢ ∀ [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)],
    length R ((i : β) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case of_equiv
R : Type u_1
inst✝² : Ring R
α β : Type u_5
inst✝¹ : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    length R ((i : α) → M i) = ∑ i, length R (M i)
M : β → Type u_6
inst✝ : (i : β) → AddCommGroup (M i)
⊢ ∀ [inst : (i : β) → Module R (M i)], length R ((i : β) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝² : Ring R
α β : Type u_5
inst✝¹ : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    length R ((i : α) → M i) = ∑ i, length R (M i)
M : β → Type u_6
inst✝ : (i : β) → AddCommGroup (M i)
⊢ ∀ [inst : (i : β) → Module R (M i)], length R ((i : β) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case of_equiv
R : Type u_1
inst✝³ : Ring R
α β : Type u_5
inst✝² : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    length R ((i : α) → M i) = ∑ i, length R (M i)
M : β → Type u_6
inst✝¹ : (i : β) → AddCommGroup (M i)
inst✝ : (i : β) → Module R (M i)
⊢ length R ((i : β) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_empty
R : Type u_1
inst✝ : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
⊢ ∀ [inst : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)] [inst_1 : (i : PEmpty.{u_5 + 1}) → Module R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case h_empty
R : Type u_1
inst✝¹ : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
inst✝ : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)
⊢ ∀ [inst : (i : PEmpty.{u_5 + 1}) → Module R (M i)], length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_empty
R : Type u_1
inst✝¹ : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
inst✝ : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)
⊢ ∀ [inst : (i : PEmpty.{u_5 + 1}) → Module R (M i)], length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case h_empty
R : Type u_1
inst✝² : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
inst✝¹ : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)
inst✝ : (i : PEmpty.{u_5 + 1}) → Module R (M i)
⊢ length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝ : Ring R
ι : Type u_5
⊢ ∀ [inst : Fintype ι],
    (∀ (M : ι → Type u_6) [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)],
        length R ((i : ι) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option ι → Type u_6) [inst_1 : (i : Option ι) → AddCommGroup (M i)]
        [inst_2 : (i : Option ι) → Module R (M i)], length R ((i : Option ι) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case h_option
R : Type u_1
inst✝¹ : Ring R
ι : Type u_5
inst✝ : Fintype ι
⊢ (∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
      length R ((i : ι) → M i) = ∑ i, length R (M i)) →
    ∀ (M : Option ι → Type u_6) [inst : (i : Option ι) → AddCommGroup (M i)] [inst_1 : (i : Option ι) → Module R (M i)],
      length R ((i : Option ι) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝¹ : Ring R
ι : Type u_5
inst✝ : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
⊢ ∀ [inst : (i : Option ι) → AddCommGroup (M i)] [inst_1 : (i : Option ι) → Module R (M i)],
    length R ((i : Option ι) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case h_option
R : Type u_1
inst✝² : Ring R
ι : Type u_5
inst✝¹ : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝ : (i : Option ι) → AddCommGroup (M i)
⊢ ∀ [inst : (i : Option ι) → Module R (M i)], length R ((i : Option ι) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝² : Ring R
ι : Type u_5
inst✝¹ : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝ : (i : Option ι) → AddCommGroup (M i)
⊢ ∀ [inst : (i : Option ι) → Module R (M i)], length R ((i : Option ι) → M i) = ∑ i, length R (M i)

Tactic:
_

Goal state after:
case h_option
R : Type u_1
inst✝³ : Ring R
ι : Type u_5
inst✝² : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ length R ((i : Option ι) → M i) = ∑ i, length R (M i)
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 b c : ValueGroup A K), a * b * c = a * (b * c)

Tactic:
by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]

Goal state after:
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⦄, ¬a ≤ 0 → ∀ ⦃b c : ValueGroup A K⦄, ¬c ≤ b → ¬a * c ≤ a * b

Tactic:
rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ hbc

Goal state after:
case mk.mk.mk
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
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
hbc : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
⊢ ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ ∀ (n : ℕ), f m ≡ g m [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ ∀ (n : ℕ), f m ≡ g m [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (f r) = (Ideal.Quotient.mk (I ^ n)) (g r)
r : R
⊢ f r = g r

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Goal state after:
R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (f r) = (Ideal.Quotient.mk (I ^ n)) (g r)
r : R
⊢ ∀ (n : ℕ), f r ≡ g r [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
m : R
⊢ f m = g m

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := I)]

Goal state after:
R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
m : R
⊢ ∀ (n : ℕ), f m ≡ g m [SMOD I ^ n • ⊤]
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
inst✝⁶ : SMul S R
inst✝⁵ : SMul Sᵐᵒᵖ R
inst✝⁴ : SMul S M
inst✝³ : SMul Sᵐᵒᵖ M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower Sᵐᵒᵖ R M
inst✝ : IsCentralScalar S M
s : S
f : AdicCompletion I M
⊢ MulOpposite.op s • f = s • f

Tactic:
by ext; simp [val_smul, op_smul_eq_smul]

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 : ℕ}, m✝ ≤ n → 0 m✝ ≡ 0 n [SMOD I ^ m✝ • ⊤]

Tactic:
_

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✝ : ℕ
⊢ m✝ ≤ n✝ → 0 m✝ ≡ 0 n✝ [SMOD I ^ 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✝ : ℕ
⊢ m✝ ≤ n✝ → 0 m✝ ≡ 0 n✝ [SMOD I ^ m✝ • ⊤]

Tactic:
_

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✝ : ℕ
a✝ : m✝ ≤ n✝
⊢ 0 m✝ ≡ 0 n✝ [SMOD I ^ m✝ • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

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

Tactic:
intro h m n hmn

Goal state after:
case mpr
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 : ℕ
hmn : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ span {p} ≠ ⊥

pp: case refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ (span {p}).IsPrime

pp: case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}

Tactic:
· rw [Submodule.ne_bot_iff]
    exact ⟨p, Ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩

Goal state after:
case refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ (span {p}).IsPrime

case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}

Tactic:
· intro I
    rw [← Submodule.IsPrincipal.span_singleton_generator I]
    rintro ⟨I0, hI⟩
    apply span_singleton_eq_span_singleton.mpr
    apply h₂ _ hp
    rw [Ne, Submodule.span_singleton_eq_bot] at I0
    rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]

Goal state after:
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
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
⊢ n ∈ range (n✝ - m) → (x * y) ^ (m + n) ∈ I ^ m

Tactic:
_

Goal state after:
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
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ (x * y) ^ (m + n) ∈ I ^ m
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
⊢ I ≤ ⊥.jacobson

Tactic:
by
  intro x hx
  rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
  intro y
  rw [add_comm]
  let f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i
  have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] := by
    intro m n h
    simp only [f, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
    rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
      @neg_mem_iff]
    apply Submodule.sum_mem
    intro n _
    rw [mul_pow, pow_add, mul_assoc]
    exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
  obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
  rw [isUnit_iff_exists_inv]
  use L
  rw [← sub_eq_zero, neg_mul]
  apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
  intro n
  specialize hL n
  rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] at hL ⊢
  rw [sub_zero]
  suffices (1 - x * y) * f n - 1 ∈ I ^ n by
    convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
    ring
  cases n
  · simp only [Ideal.one_eq_top, pow_zero, mem_top]
  · rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm (_ ^ _), ← sub_sub,
      sub_self, zero_sub, @neg_mem_iff, mul_pow]
    exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔
    ∀ ⦃x : Ideal (R ⧸ I)⦄, x ∈ minimalPrimes (R ⧸ I) → (comap (Quotient.mk I) x).IsMaximal

Tactic:
refine forall₂_congr fun J hJ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : Ideal (R ⧸ I)
hJ : J ∈ minimalPrimes (R ⧸ I)
h : J.IsMaximal
⊢ (comap (Quotient.mk I) J).IsMaximal

case refine_2
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : Ideal (R ⧸ I)
hJ : J ∈ minimalPrimes (R ⧸ I)
h : (comap (Quotient.mk I) J).IsMaximal
⊢ J.IsMaximal
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
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ((addVal R) x) = span {x}

Tactic:
obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx0 hϖ

Goal state after:
case neg
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = ↑u * ϖ ^ n
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ((addVal R) x) = span {x}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
⊢ ∀ {ϖ : O}, Irreducible ϖ → ↑(maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}

Tactic:
_

Goal state after:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ✝ : O
⊢ Irreducible ϖ✝ → ↑(maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ✝)}
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg.zero
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}
hn : Nat.find this✝ = 0
this : ⊤ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r s : R
⊢ v₁ r = v₁ s ↔ v₂ r = v₂ s

Tactic:
simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
this : ⊥.IsMaximal
⊢ (under (R ⧸ P') (Ideal.map (algebraMap (R ⧸ P') (Localization M)) ⊥)).IsMaximal

Tactic:
exact ((IsLocalization.isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp
      (by rwa [Ideal.map_bot])).1

Goal state after: