mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
⊢ ((killingForm K L) x) y = 0

Tactic:
by
  /- If `ad R L z` is semisimple for all `z ∈ H` then writing `⟪x, y⟫ = killingForm K L x y`, there
  is a slick proof of this lemma that requires only invariance of the Killing form as follows.
  For any `z ∈ H`, we have:
  `α z • ⟪x, y⟫ = ⟪α z • x, y⟫ = ⟪⁅z, x⁆, y⟫ = - ⟪x, ⁅z, y⁆⟫ = - ⟪x, β z • y⟫ = - β z • ⟪x, y⟫`.
  Since this is true for any `z`, we thus have: `(α + β) • ⟪x, y⟫ = 0`, and hence the result.
  However the semisimplicity of `ad R L z` is (a) non-trivial and (b) requires the assumption
  that `K` is a perfect field and `L` has non-degenerate Killing form. -/
  let σ : (H → K) → (H → K) := fun γ ↦ α + (β + γ)
  have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_ne_right.mpr hαβ
  let f : Module.End K L := (ad K L x) ∘ₗ (ad K L y)
  have hf : ∀ γ, MapsTo f (rootSpace H γ) (rootSpace H (σ γ)) := fun γ ↦
    (mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (β + γ) hx).comp <|
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L β γ hy
  classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
  exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : x ∈ ((ad K L) ↑h).maxGenEigenspace (α h)
⊢ ⁅h, x⁆ = α h • x

Tactic:
(isSemisimple_ad_of_mem_isCartanSubalgebra
    h.property).isFinitelySemisimple.maxGenEigenspace_eq_eigenspace,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : ↥H → K
x : L
h : ↥H
hx : x ∈ ((ad K L) ↑h).eigenspace (α h)
⊢ ⁅h, x⁆ = α h • x
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
⊢ ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)

Tactic:
replace hef : ⁅⁅e, f⁆, e⁆ = 2 • e := by
    have : ⁅⁅e, f'⁆, e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
    rw [lie_smul, smul_lie, this, ← smul_assoc, smul_eq_mul, mul_assoc, inv_mul_cancel₀ hh,
      mul_one, two_smul, two_smul]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
hef : ⁅⁅e, f⁆, e⁆ = 2 • e
⊢ ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ∃ s, s • h = coroot α

Tactic:
have h_eq : h = killingForm K L e f • α' := by
    simp only [hα', Subtype.ext_iff, ← ht.lie_e_f, hef]
    rw [Submodule.coe_smul_of_tower]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
⊢ ∃ s, s • h = coroot α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 2 (C R n) = 2

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [C_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [C_sub_one, -C_neg, ih1, ih2]; norm_num

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 : ι
⊢ (P.reflectionPerm i) ((P.reflectionPerm i) j) = j

Tactic:
apply P.root.injective
  simp only [root_reflectionPerm, reflection_same]

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
x : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
h : - -x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root

Tactic:
exact this (-x) h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (↑n ^ 2 - ↑k ^ 2) * ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2) = ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)

Tactic:
Finset.prod_insert Finset.notMem_range_self

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (↑n ^ 2 - ↑k ^ 2) * ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2) =
    (↑n ^ 2 - ↑k ^ 2) * ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
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
h : IsInteger A x
⊢ IsUnit ↑(den A x)

Tactic:
have ⟨v, h⟩ := h
    apply IsRelPrime.isUnit_of_dvd (num_den_reduced A x).symm
    use v
    apply_fun algebraMap A K
    · simp only [map_mul, h]
      rw [mul_comm, ← div_eq_iff]
      · simp only [mk'_num_den']
      simp
    exact FaithfulSMul.algebraMap_injective A K

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' : 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'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
i : ↑w
j : ↑v
⊢ (p.toPerfPair (b j)) (bN i) ∈ (algebraMap K L).fieldRange

Tactic:
exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)

Goal state after:
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
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian]
  obtain ⟨s, hs⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
  tfae_have 1 ↔ 2 := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
  tfae_have 2 → 5 := fun _ ↦ ⟨s, WellFoundedGT.finite_of_sSupIndep hs.1, hs⟩
  tfae_have 3 → 5 := fun _ ↦ ⟨s, WellFoundedLT.finite_of_sSupIndep hs.1, hs⟩
  tfae_have 5 → 4 := fun ⟨s, fin, _, sSup_eq_top, simple⟩ ↦ by
    rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']
    rw [SetCoe.forall'] at simple
    have := fin.to_subtype
    exact ⟨isNoetherian_iSup, isArtinian_iSup⟩
  tfae_have 4 → 2 := And.left
  tfae_have 4 → 3 := And.right
  tfae_finish

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

Goal state before:
pp: case h
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
b : K
e f : A
hf : (algebraMap A K) (f * e) * b = (algebraMap A K) 1 * b
hb : ¬b = 0
⊢ 1 = f * e

Tactic:
exact IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm

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)) a = 0

Tactic:
ha

Goal state after:
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
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing S
inst✝³ : Module S M
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ (I ^ n • ⊤).toAddSubgroup ≤ (J ^ n • ⊤).toAddSubgroup

pp: case hxy
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing S
inst✝³ : Module S M
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
· rw [← AddSubgroup.toAddSubmonoid_le]
    simp only [Submodule.smul_toAddSubmonoid, Submodule.top_toAddSubmonoid]
    rw [AddSubmonoid.smul_le]
    intro r hr m hm
    rw [← algebraMap_smul S r m]
    apply AddSubmonoid.smul_mem_smul ?_ hm
    have := Ideal.mem_map_of_mem (algebraMap R S) hr
    simp only [Ideal.map_pow] at this
    exact Ideal.pow_right_mono hIJ n this

Goal state after:
case hxy
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing S
inst✝³ : Module S M
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ≡ 0 [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case left
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 y : A
h :
  (algebraMap (↥(valuation A K).integer) K)
      ((have this := { toFun := fun a ↦ ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this)
        x) =
    (algebraMap (↥(valuation A K).integer) K)
      ((have this := { toFun := fun a ↦ ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this)
        y)
⊢ x = y

Tactic:
exact IsFractionRing.injective _ _ h

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

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
⊢ v.leIdeal (v ↑x) ≤ I

Tactic:
rcases eq_or_ne x 0 with rfl | hx0
  · simp
  intro y hy
  have : v ((y : K) / x) ≤ 1 := by simpa using div_le_one_of_le₀ hy zero_le
  convert! I.smul_mem ⟨_, this⟩ hx using 1
  simp [Subtype.ext_iff, div_mul_cancel₀ _ (ZeroMemClass.coe_eq_zero.not.mpr hx0)]

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

Goal state before:
pp: case refine_1
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
⊢ r • ↑x n = 0 n

Tactic:
induction x.val n using Quotient.inductionOn' with | _ a
       =>  _ 

Goal state after:
case refine_1.h
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
a : M
⊢ r • Quotient.mk'' a = 0 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
f : AdicCauchySequence I M → ℕ → M := Subtype.val
⊢ AddCommGroup (AdicCauchySequence I M)

Tactic:
apply Subtype.val_injective.addCommGroup f rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Goal state after:
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
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ a ∨ p ∣ b

Tactic:
ha

Goal state after:
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
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ 0 ∨ p ∣ b
Module: Mathlib.RingTheory.Jacobson.Ring

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

Tactic:
exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)

Goal state after:
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
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
⊢ (fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n))
      ((fun I ↦ OrderDual.toDual ((addVal R) (generator I))) I) =
    I

Tactic:
suffices (addVal R x).recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) = span {x} by
      rwa [Ideal.span_singleton_generator] at this

Goal state after:
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
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ((addVal R) x) = span {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
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
⊢ maximalIdeal R ^ n = span {ϖ ^ n}

Tactic:
hϖ.maximalIdeal_eq,

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
⊢ span {ϖ} ^ n = span {ϖ ^ n}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case coe
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
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) (generator (maximalIdeal R ^ k)) = ↑k

Tactic:
hϖ.maximalIdeal_eq,

Goal state after:
case coe
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
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) (generator (span {ϖ} ^ k)) = ↑k
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ maximalIdeal R ^ n = span {ϖ ^ n}

Tactic:
hϖ.maximalIdeal_eq,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ span {ϖ} ^ n = span {ϖ ^ n}
Module: Mathlib.RingTheory.Jacobson.Ring

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

Tactic:
refine ⟨X - C (algebraMap _ _ ((Ideal.Quotient.mk P') (p.coeff 0))), monic_X_sub_C _, ?_⟩

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

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀✝
v✝ : Valuation R Γ₀✝
Γ₀ : Type u_7
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : v x ≠ 0
h1 : v x ≠ 1
⊢ ∃ x ∈ (MonoidWithZeroHom.ofClass v).valueMonoid, x ≠ 1

Tactic:
use (Units.mk0 (v x) h0), (MonoidWithZeroHom.ofClass v).mem_valueMonoid (Set.mem_range_self x)

Goal state after:
case right
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀✝
v✝ : Valuation R Γ₀✝
Γ₀ : Type u_7
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : v x ≠ 0
h1 : v x ≠ 1
⊢ Units.mk0 (v x) h0 ≠ 1
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ inst✝⁴.toIsNoetherian
this : IsLocalRing Aₘ := isLocalRing Aₘ P
hnf : ¬IsField Aₘ
⊢ IsDiscreteValuationRing Aₘ

Tactic:
exact
    ((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
      (IsLocalization.AtPrime.isDedekindDomain A P _)

Goal state after: