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

Goal state before:
pp: L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
⊢ _root_.IsNilpotent ((toEnd K L M) x)

Tactic:
refine Module.End.isNilpotent_iff_of_finite.mpr fun m ↦ ?_
  have hm : m ∈ ⨆ χ : LieModule.Weight K H M, genWeightSpace M χ := by
    simp [iSup_genWeightSpace_eq_top' K H M]
  induction hm using LieSubmodule.iSup_induction' with
  | zero => exact ⟨0, map_zero _⟩
  | mem χ₂ m₂ hm₂ =>
    obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ
    use n
    have := toEnd_pow_apply_mem hx hm₂ n
    rwa [hn, LieSubmodule.mem_bot] at this
  | add m₁ m₂ hm₁ hm₂ hm₁' hm₂' =>
    obtain ⟨n₁, hn₁⟩ := hm₁'
    obtain ⟨n₂, hn₂⟩ := hm₂'
    refine ⟨max n₁ n₂, ?_⟩
    rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]

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

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
V : Submodule R N
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤

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

Goal state after:
case refine_1
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
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ V = ⊤

case refine_2
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
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V
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 ι
i j : ι
⊢ (b.baseSupp i) (b.h' j) = ↑(b.A i j)

Tactic:
simp only [baseSupp, LinearMap.coe_sum, Finset.sum_apply]

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 ι
i j : ι
⊢ ∑ c,
      (b.A i c • ((Basis.span ⋯).map (LinearEquiv.ofEq H.toSubmodule (Submodule.span R (range b.h)) ⋯).symm).coord c)
        (b.h' j) =
    ↑(b.A i 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 ι
i : ι
x : ↥H
this : (-b.baseSupp i) x • b.f i = ⁅x, b.f i⁆
⊢ (-b.baseSupp i) x • b.f i = ⁅x, b.f i⁆

Tactic:
exact this

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

Goal state before:
pp: case refine_2
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
this : ⁅⁅e, f'⁆, f'⁆ = -α h • f'
⊢ ⁅⁅e, f⁆, f⁆ = -(2 • f)

Tactic:
rw [lie_smul, lie_smul, smul_lie, this]

Goal state after:
case refine_2
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
this : ⁅⁅e, f'⁆, f'⁆ = -α h • f'
⊢ (2 * (α h)⁻¹) • (2 * (α h)⁻¹) • -α h • f' = -(2 • f)
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
contra : 1 < finrank K ↥(rootSpace H ⇑α)
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
F : ↥(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype
⊢ finrank K K < finrank K ↥(rootSpace H ⇑α)

Tactic:
by rwa [finrank_self]

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

Goal state before:
pp: case pred
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R (-↑n) ^ 2 + S R (-↑n + 1) ^ 2 - X * S R (-↑n) * S R (-↑n + 1) = 1
⊢ S R (-↑n - 1) ^ 2 + S R (-↑n - 1 + 1) ^ 2 - X * S R (-↑n - 1) * S R (-↑n - 1 + 1) = 1

Tactic:
| pred n ih =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
⊢ (⇑derivative)^[k + 1] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))

Tactic:
Function.iterate_succ_apply'

Goal state after:
R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
⊢ derivative ((⇑derivative)^[k] (T R ↑n)) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case add
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 : f x = 0
n x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑j.range
hy✝ : y✝ ∈ span R ↑j.range
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p (i x)) (x✝ + y✝) = 0

Tactic:
map_add

Goal state after:
case add
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 : f x = 0
n x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑j.range
hy✝ : y✝ ∈ span R ↑j.range
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p (i x)) x✝ + (p (i x)) y✝ = 0
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
this : Associated (num A x) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
exact this

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
⊢ m ∈ span K v

Tactic:
have hbM (j : w) (x : M) (hx : x ∈ M') : bM.repr x j = p x (j : N) := by simp [bM, bN]

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'
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
⊢ m ∈ span K v
Module: Mathlib.RingTheory.Polynomial.RationalRoot

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

Tactic:
convert! pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))

Goal state after:
case e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝

case pos.convert_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ ℕ

case pos.convert_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ j + ?pos.convert_1✝ < p.natDegree
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
⊢ x ∈ RingHom.ker (factor H) ↔ x ∈ map (mk I) J

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

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ RingHom.ker (factor H)
⊢ x ∈ map (mk I) J

case refine_2
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ map (mk I) J
⊢ x ∈ RingHom.ker (factor H)
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
⊢ x ∈ comap (factor hJK) (map (mk J) I) ↔ x ∈ map (mk K) I

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

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
⊢ x ∈ map (mk K) I

case refine_2
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ map (mk K) I
⊢ x ∈ comap (factor hJK) (map (mk J) I)
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case h
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} = S ∙ f (gcd x y)

Tactic:
trans Ideal.map f (Ideal.span {gcd x y})

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.map f (Ideal.span {gcd x y})

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.map f (Ideal.span {gcd x y}) = S ∙ f (gcd x y)
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:
M

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_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 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:
M

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_1 : (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 : ValueGroup A K), a ≠ 0 → a * a⁻¹ = 1

Tactic:
by
      rintro ⟨a⟩ ha
      apply Quotient.sound'
      use 1
      simp only [one_smul]
      apply (mul_inv_cancel₀ _).symm
      contrapose ha
      rw [ha]
      rfl

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

Goal state before:
pp: case zero
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 : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD 1 • ⊤]

Tactic:
Ideal.one_eq_top,

Goal state after:
case zero
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 : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊤ • ⊤]
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
⊢ ∀ {p : R}, Irreducible p → Associated p ϖ

Tactic:
intro p

Goal state after:
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
⊢ Irreducible p → Associated p ϖ
Module: Mathlib.RingTheory.Valuation.ValuationRing

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

Tactic:
rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]

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

case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
h' : IsUnit (y * b)
⊢ b * g ∣ a * g
Module: Mathlib.RingTheory.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 ↦ ?_⟩

Goal state after:
case refine_1
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
h : ↑x m ∈ I ^ n • ⊤
⊢ ↑x n = 0

case refine_2
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
h : ↑x n = 0
⊢ ↑x m ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ {I : Ideal S}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Tactic:
intro p

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
⊢ p.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_prime_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : ∀ i ∈ insert a s, v (f i) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g

Tactic:
Finset.forall_mem_insert

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_prime_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : ∀ i ∈ insert a s, v (f i) < g
⊢ v (∑ i ∈ insert a s, f i) < g

Tactic:
Finset.forall_mem_insert

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g
⊢ v (∑ i ∈ insert a s, f i) < g
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
⊢ ∑ i ∈ range m, (x * y) ^ i - ∑ i ∈ range n, (x * y) ^ i ∈ I ^ m

Tactic:
← add_tsub_cancel_of_le h,

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
⊢ ∑ i ∈ range m, (x * y) ^ i - ∑ i ∈ range (m + (n - m)), (x * y) ^ i ∈ I ^ m
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ (addVal R) r = ↑n

Tactic:
rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
      (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
    emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
    emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

Goal state after: