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

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

Tactic:
← P.pairing_smul_coroot_eq j i j hij.symm,

Goal state after:
case calc_4
ι : 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.pairing j j • P.coroot j) • P.root j = (P.toLinearMap x) (2 • P.coroot j) • P.root j
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
this : ∀ (i : ι), (Nat.cast ∘ (m + n)) i = 0
i : ι
⊢ n i = 0 i

Tactic:
specialize this i

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
i : ι
this : (Nat.cast ∘ (m + n)) i = 0
⊢ n i = 0 i
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (T R n) -
      ((⇑derivative)^[0 + 2] (T R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (T R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (T R n)) =
    (⇑derivative)^[0 + 1] (T R n) * X + 0 • (⇑derivative)^[0] (T R n) - ↑(n ^ 2) * (⇑derivative)^[0] (T R n)
⊢ (⇑derivative)^[0] (T R n) * ↑0 + (⇑derivative)^[0] (T R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (T R n) * ↑0 ^ 2 = 0

Tactic:
grind

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

Goal state before:
pp: case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (T R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (T R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (T R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (T R n)) =
    (⇑derivative)^[n✝ + 1 + 1] (T R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (T R n) -
      ↑(n ^ 2) * (⇑derivative)^[n✝ + 1] (T R n)
⊢ (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) ^ 2 =
    0

Tactic:
grind

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

Goal state before:
pp: case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (U R n) -
      ((⇑derivative)^[0 + 2] (U R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (U R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (U R n)) =
    ↑3 * ((⇑derivative)^[0 + 1] (U R n) * X + 0 • (⇑derivative)^[0] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[0] (U R n)
⊢ (⇑derivative)^[0] (U R n) * ↑0 + (⇑derivative)^[0] (U R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (U R n) * ↑0 ^ 2 = 0

Tactic:
grind

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

Goal state before:
pp: case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (U R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (U R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (U R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (U R n)) =
    ↑3 * ((⇑derivative)^[n✝ + 1 + 1] (U R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[n✝ + 1] (U R n)
⊢ (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) ^ 2 =
    0

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
h : ↑(2 * 0 + 3) * eval 1 (derivative (U R n)) = ↑((n + 1) ^ 2 - (↑0 + 1) ^ 2) * (↑n + 1)
⊢ 3 * eval 1 (derivative (U R n)) = (↑n + 2) * (↑n + 1) * ↑n

Tactic:
grind

Goal state after:
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' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hM : span L ↑i.range = ⊤
hN : span L ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
n : ℕ
b' : Basis (Fin n) K ↥i.range
⊢ FiniteDimensional K M'

Tactic:
have : FiniteDimensional K (LinearMap.range i) := b'.finiteDimensional_of_finite

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' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hM : span L ↑i.range = ⊤
hN : span L ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
n : ℕ
b' : Basis (Fin n) K ↥i.range
this : FiniteDimensional K ↥i.range
⊢ FiniteDimensional K M'
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
x✝ : ↥(I ^ a • ⊤)
⊢ ((factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝ =
    ((powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(I ^ a • ⊤) ⋯) ∘ₗ (I ^ (b + d) • ⊤).mkQ) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N

Tactic:
by
  induction h generalizing N with
  | of_subsingleton =>
    have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  | @of_simple_quotient M _ _ S _ _ ih =>
    have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsDomain R
inst✝ : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : a = b ∨ n = 0
⊢ a = b

Tactic:
grind

Goal state after:
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
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : length R M ≠ ⊤
⊢ IsFiniteLength R M

case refine_2
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsFiniteLength R M
⊢ length R M ≠ ⊤
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : length R M ≠ ⊤
⊢ IsFiniteLength R M

Tactic:
length_ne_top_iff_finiteDimensionalOrder

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : FiniteDimensionalOrder (Submodule R M)
⊢ IsFiniteLength R M
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.span (insert (f x) (⇑f '' {y}))

Tactic:
Set.image_singleton

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.span {f x, f y}
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span (⇑f '' {gcd x y}) = S ∙ f (gcd x y)

Tactic:
Set.image_singleton

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f (gcd x y)} = S ∙ f (gcd x y)
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
a b : { N // N.FG }
⊢ ↑b < ↑a ↔ b < a

Tactic:
rfl

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
r : R
⊢ r ∈ v.integer ↔ v r ≤ 1

Tactic:
rfl

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 : K
ha : a = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) 0 = 0

Tactic:
rfl

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
      refine .of_mul_eq_one (c + 1) ?_
      simp [mul_add, h]

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

Goal state before:
pp: case pos
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case neg
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· subst hb; exact ⟨0, Or.inl <| mul_zero a⟩

Goal state after:
case neg
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ c, a * c = b ∨ b * c = a
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✝ : ℕ
a✝ : m✝ ≤ n✝
⊢ 0 m✝ ≡ 0 n✝ [SMOD I ^ m✝ • ⊤]

Tactic:
rfl

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

Goal state before:
pp: case mpr.base
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 : ℕ
⊢ f m ≡ f m [SMOD I ^ m • ⊤]

Tactic:
rfl

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

Goal state before:
pp: 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 • ⊤]
⊢ ⊤ ≤ ⊤

Tactic:
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
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
x y : M
⊢ ⟨fun n ↦ (f n) x + (f n) y, ⋯⟩ = ⟨fun n ↦ (f n) x, ⋯⟩ + ⟨fun n ↦ (f n) y, ⋯⟩

Tactic:
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
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 ↦ r • (f n) x, ⋯⟩ = r • ⟨fun n ↦ (f n) x, ⋯⟩

Tactic:
rfl

Goal state after:
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
I : Ideal R
inst✝ : IsJacobsonRing R
b✝ : R ⧸ I
x : R
⊢ (Ideal.Quotient.mk I) x = Quot.mk (⇑(Submodule.quotientRel I)) x

Tactic:
rfl

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

Goal state before:
pp: A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ↑a ∈ nonunits A

Tactic:
← IsLocalRing.mem_maximalIdeal

Goal state after:
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ↑a ∈ maximalIdeal A
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0

Tactic:
by
  rw [Ring.KrullDimLE, Order.krullDimLE_iff, le_antisymm_iff, ← ringKrullDim, Nat.cast_zero,
    iff_self_and]
  exact fun _ ↦ ringKrullDim_nonneg_of_nontrivial

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

Goal state before:
pp: case h
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 = ⊤
⊢ I = maximalIdeal R ^ 0

Tactic:
rw [pow_zero, hI', Ideal.one_eq_top]

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

Goal state before:
pp: case coe.coe
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 ↔ ↑vx ≤ (addVal R) y

Tactic:
hvy

Goal state after:
case coe.coe
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 ↔ ↑vx ≤ ↑vy
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y),
      Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X) (x_1 : M), (h (f x)) x_1 = (g x) x_1) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f →
        ∀ (b : N →ₗ[R] CharacterModule M),
          ∃ a, ∀ (x : N) (x_1 : M), (((lcomp R (CharacterModule M) f) a) x) x_1 = (b x) x_1

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates R
⊢ ↑((associatesEquivIsPrincipal R) x✝¹) * ↑((associatesEquivIsPrincipal R) x✝) =
    ↑((associatesEquivIsPrincipal R).toFun x✝¹ * (associatesEquivIsPrincipal R).toFun x✝)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates ↥R⁰
⊢ ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝¹) * ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝) =
    ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝¹ * (associatesNonZeroDivisorsEquivIsPrincipal R) x✝)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : IsJacobsonRing R[X]
x : R
⊢ (eval₂RingHom (RingHom.id R) 1) (C x) = x

Tactic:
by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]

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
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
⊢ (((Ideal.Quotient.mk (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P)).comp C).comp
      (Ideal.Quotient.mk (comap C P))).IsIntegral

Tactic:
refine ((Ideal.Quotient.mk P').isIntegral_of_surjective Quotient.mk_surjective).trans _ _ ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
⊢ ((Ideal.Quotient.mk (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P)).comp C).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
⊢ (↑↑Polynomial.C).toFun ((algebraMap R S) r) = (algebraMap R S[X]) r

Tactic:
rfl

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

Goal state before:
pp: case hf.hg
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
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ w'.toRingHom = quotientMap Q Polynomial.C ⋯

Tactic:
rfl

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
h' : w.IsEquiv v
⊢ h.orderMonoidIso.symm = h'.orderMonoidIso

Tactic:
rfl

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

Goal state before:
pp: case mp
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ v.IsEquiv v' → ∀ {x : K}, v x = 1 ↔ v' x = 1

Tactic:
intro h x

Goal state after:
case mp
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : v.IsEquiv v'
x : K
⊢ v x = 1 ↔ v' x = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr
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
⊢ v.IsEquiv v'

Tactic:
apply isEquiv_of_val_le_one

Goal state after:
case mpr
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 : K), v x ≤ 1 ↔ v' x ≤ 1