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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : IsOfFinOrder u
⊢ f = g

Tactic:
obtain ⟨n, hn₀, hn₁⟩ := isOfFinOrder_iff_pow_eq_one.mp this
    replace hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id := LinearEquiv.toLinearMap_inj.mpr hn₁
    simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n

Goal state after:
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, m i • b.baseSupp i + ∑ i, n i • b.baseSupp i) = 0
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0

Tactic:
LinearMap.coe_zero_iff,

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, m i • b.baseSupp i + ∑ i, n i • b.baseSupp i = 0
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h := congr_arg derivative <| add_one_mul_T_eq_poly_in_U (R := R) n
  simp only [derivative_add, derivative_sub, derivative_mul, derivative_X, derivative_one,
    derivative_X_pow, derivative_intCast, C_eq_natCast, T_derivative_eq_U] at h
  rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
  linear_combination (norm := (push_cast; ring_nf)) h

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i✝ j✝ : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
i j : ι
h : P.pairing i j = 0
⊢ P.pairing j i = 0

Tactic:
simpa [P.ne_zero i, reflectionPerm_eq_iff_smul_root] using
    P.reflectionPerm_eq_of_pairing_eq_zero' h

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ i x = 0

Tactic:
← p.map_eq_zero_iff p.toPerfPair.injective

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ p (i x) = 0
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 = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
suffices span K (Set.range v') = ⊤ by
    let e := (Module.Finite.finite_basis b).equivFin
    let b' : Basis _ K M' := Basis.mk hv' (by rw [this])
    exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩

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
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
⊢ span K (Set.range 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 = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
⊢ span K (Set.range v') = ⊤

Tactic:
suffices span K v = M' by
    apply Submodule.map_injective_of_injective M'.injective_subtype
    rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
    simpa [v']

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
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
⊢ span K v = M'
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ (algebraMap A K) (num A x⁻¹ * num A x) / (algebraMap A K) (↑(den A x⁻¹) * ↑(den A x)) = 1

Tactic:
by simp [mul_div_mul_comm, hx]

Goal state after:
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ (algebraMap A K) (num A x * num A x⁻¹) / (algebraMap A K) (↑(den A x) * ↑(den A x⁻¹)) = 1

Tactic:
by simp [mul_div_mul_comm, hx]

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

Goal state before:
pp: case mp
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:
rintro ⟨c, rfl⟩
    use c
    rw [Algebra.smul_def, mul_one]

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

Goal state before:
pp: case mpr
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
⊢ (∃ a, (algebraMap A K) a = x) → x ∈ (valuation A K).integer

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

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
x✝¹ x✝ : A
⊢ ⟨(algebraMap A K) (x✝¹ * x✝), ⋯⟩ = ⟨(algebraMap A K) x✝¹, ⋯⟩ * ⟨(algebraMap A K) x✝, ⋯⟩

Tactic:
by ext1; exact (algebraMap A K).map_mul _ _

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

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝¹ : Field F
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ ¬IsUnit x ↔ v ↑x < 1

Tactic:
rw [← not_le, not_iff_not, isUnit_iff_valuation_eq_one (F := F) (Γ₀ := Γ₀),
    le_antisymm_iff]
  exacts [and_iff_right x.2, integer.integers v]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
constructor
  · intro RDVR
    rcases id RDVR with ⟨Rlocal⟩
    constructor
    · assumption
    use IsLocalRing.maximalIdeal R
    constructor
    · exact ⟨Rlocal, inferInstance⟩
    · rintro Q ⟨hQ1, hQ2⟩
      obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
      have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp
      rw [submodule_span_eq, span_singleton_prime hq] at hQ2
      replace hQ2 := hQ2.irreducible
      rw [irreducible_iff_uniformizer] at hQ2
      exact hQ2.symm
  · rintro ⟨RPID, Punique⟩
    have : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique
    refine { not_a_field' := ?_ }
    rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
    have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
    order

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

Goal state before:
pp: 𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ValuationRing 𝒪

Tactic:
by
  have := hh.hom_inj.isDomain
  suffices PreValuationRing 𝒪 from .mk
  constructor
  intro a b
  rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h
  · obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
    use c; exact Or.inr hc.symm
  · obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
    use c; exact Or.inl hc.symm

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
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
⊢ ↑x m ∈ I ^ n • ⊤ ↔ ↑x n = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← x.prop m_ge, transitionMap, Submodule.factorPow, Submodule.factor, mapQ,
      ← LinearMap.mem_ker]
    simpa [ker_liftQ]
  simpa [mapQ, h, ← LinearMap.mem_ker, ker_liftQ] using x.prop m_ge

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
I J : Ideal R
inst✝ : I.IsPrime
⊢ I ∈ J.minimalPrimes ↔ J ≤ I

Tactic:
by
  rwa [mem_minimalPrimes_iff, and_iff_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ x ∈ nilradical R ↔ x ∈ IsLocalRing.maximalIdeal R

Tactic:
nilradical,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ x ∈ Ideal.radical 0 ↔ x ∈ IsLocalRing.maximalIdeal R
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) b
ha0 : a = 0
⊢ a ∣ b

Tactic:
top_le_iff,

Goal state after:
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) b = ⊤
ha0 : a = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case a
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
I : Ideal R
hI : I ∈ {J | Ideal.span {a} ≤ J ∧ J.IsPrime}
e : I = ⊥
⊢ a = 0

Tactic:
← Ideal.span_singleton_eq_bot,

Goal state after:
case a
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
I : Ideal R
hI : I ∈ {J | Ideal.span {a} ≤ J ∧ J.IsPrime}
e : I = ⊥
⊢ Ideal.span {a} = ⊥
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
r s : R
hr : (ofClass v) r ≠ 0
hs : (ofClass v) s ≠ 0
hr' : (ofClass w) r ≠ 0
hs' : (ofClass w) s ≠ 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
H : ∃ d, ↑(valueGroup.mk (ofClass v) r s hr hs) = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑H.choose).1 ≠ 0
pf✝ : (ofClass w) (↑H.choose).2 ≠ 0
c_spec : v (r * (↑⋯.choose).2) = v ((↑⋯.choose).1 * s)
⊢ w ((↑⋯.choose).1 * s) = w (r * (↑⋯.choose).2)

Tactic:
← h.eq_iff,

Goal state after:
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
r s : R
hr : (ofClass v) r ≠ 0
hs : (ofClass v) s ≠ 0
hr' : (ofClass w) r ≠ 0
hs' : (ofClass w) s ≠ 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
H : ∃ d, ↑(valueGroup.mk (ofClass v) r s hr hs) = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑H.choose).1 ≠ 0
pf✝ : (ofClass w) (↑H.choose).2 ≠ 0
c_spec : v (r * (↑⋯.choose).2) = v ((↑⋯.choose).1 * s)
⊢ v ((↑⋯.choose).1 * s) = v (r * (↑⋯.choose).2)
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p // p.IsPrime ∧ Disjoint ↑q.primeCompl ↑p } ≃o { p // p.IsPrime } :=
  (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q)).symm
P : { p // p.IsPrime } := f ⟨p, ⋯⟩
Q : { p // p.IsPrime } := f ⟨q, ⋯⟩
hinj : Function.Injective ⇑(algebraMap A (Localization.AtPrime q))
⊢ p.IsMaximal

Tactic:
have hp1 : P.1 ≠ ⊥ := fun x => hp ((p.map_eq_bot_iff_of_injective hinj).mp x)

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p // p.IsPrime ∧ Disjoint ↑q.primeCompl ↑p } ≃o { p // p.IsPrime } :=
  (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q)).symm
P : { p // p.IsPrime } := f ⟨p, ⋯⟩
Q : { p // p.IsPrime } := f ⟨q, ⋯⟩
hinj : Function.Injective ⇑(algebraMap A (Localization.AtPrime q))
hp1 : ↑P ≠ ⊥
⊢ p.IsMaximal
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
⊢ ((Ideal.Quotient.mk P).comp C).IsIntegral

Tactic:
refine (isIntegral_quotientMap_iff _).mp ?_
  let P' : Ideal R := P.comap C
  obtain ⟨pX, hpX, hp0⟩ := exists_nonzero_mem_of_ne_bot
    (ne_of_lt (bot_lt_of_maximal P (Polynomial.not_isField R))).symm hP'
  let a : R ⧸ P' := (pX.map (Ideal.Quotient.mk P')).leadingCoeff
  let M : Submonoid (R ⧸ P') := Submonoid.powers a
  let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C le_rfl
  have hP'_prime : P'.IsPrime := comap_isPrime C P
  have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ =>
    hp0 <| leadingCoeff_eq_zero.mp (eq_zero_of_pow_eq_zero hn)
  let M' : Submonoid (R[X] ⧸ P) := M.map φ
  refine RingHom.IsIntegral.tower_bot φ (algebraMap _ (Localization M')) ?_ ?_
  · refine IsLocalization.injective (Localization M')
      (show M' ≤ _ from le_nonZeroDivisors_of_noZeroDivisors fun hM' => hM ?_)
    exact
      let ⟨z, zM, z0⟩ := hM'
      quotientMap_injective (_root_.trans z0 φ.map_zero.symm) ▸ zM
  · suffices RingHom.comp (algebraMap (R[X] ⧸ P) (Localization M')) φ =
      (IsLocalization.map (Localization M') φ M.le_comap_map).comp
        (algebraMap (R ⧸ P') (Localization M)) by
      rw [this]
      refine RingHom.IsIntegral.trans (algebraMap (R ⧸ P') (Localization M))
        (IsLocalization.map (Localization M') φ M.le_comap_map) ?_ ?_
      · exact (algebraMap (R ⧸ P') (Localization M)).isIntegral_of_surjective
          (IsField.localization_map_bijective hM ((Quotient.maximal_ideal_iff_isField_quotient _).mp
            (isMaximal_comap_C_of_isMaximal P hP'))).2
      · -- `convert` here is faster than `exact`, and this proof is near the time limit.
        -- convert isIntegral_isLocalization_polynomial_quotient P pX hpX
        have isloc : IsLocalization M' (Localization M') := by infer_instance
        exact @isIntegral_isLocalization_polynomial_quotient R _
          (Localization M) (Localization M') _ _ P pX hpX _ _ _ isloc
    rw [IsLocalization.map_comp M.le_comap_map]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : Nontrivial R
inst✝¹ : P.IsCrystallographic
inst✝ : Algebra ℚ R
i j : ι
⊢ P.pairingIn ℚ i j = ↑(P.pairingIn ℤ i j)

Tactic:
simp [← P.algebraMap_pairingIn' ℚ ℤ]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j

Tactic:
by
  simpa only [← (algebraMap_injective S R).eq_iff, algebraMap_pairingIn, map_mul,
    B.algebraMap_rootLength] using! B.toInvariantForm.pairing_mul_eq_pairing_mul_swap i j

Goal state after: