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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
hB : ∀ (m : M), (B m) ((φ x) n) = -1 • (B ((φ x) m)) n
this : (-1) ^ k • -1 = (-1) ^ (k + 1)
| (-1) ^ k • -1 • (B ((φ x) ((φ x ^ k) m))) n

Tactic:
← (φ x).comp_apply,

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
hB : ∀ (m : M), (B m) ((φ x) n) = -1 • (B ((φ x) m)) n
this : (-1) ^ k • -1 = (-1) ^ (k + 1)
| (-1) ^ k • -1 • (B ((φ x ∘ₗ φ x ^ k) m)) n
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
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = -⁅z, S y⁆ + ⁅y, S z⁆
⊢ ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆

Tactic:
add_comm,

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
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ + -⁅z, S y⁆
⊢ ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case neg
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
x : ↥H
h_two : α x = 2
h₀ : ¬α.IsZero
h_mem : x ∈ K ∙ coroot α
⊢ x = coroot α

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp h_mem

Goal state after:
case neg
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₀ : ¬α.IsZero
t : K
h_two : α (t • coroot α) = 2
h_mem : t • coroot α ∈ K ∙ coroot α
⊢ t • coroot α = coroot α
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
m : ℕ
k : ℤ := ↑m / 2
e : ℤ
he : e = 0 ∨ e = 1
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((e - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((e - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((e - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((e - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (e / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((e - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (e - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (e + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (e + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((e + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((e + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((e + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((e + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((e + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((e + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (e - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (e + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

Tactic:
obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R (↑(m + 1 + 1) - 2)).degree = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)

Tactic:
| succ m =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1) ≠ -1
⊢ (U R (↑(m + 1) - 2)).degree = ↑((-↑(m + 1) + 1).natAbs - 1)

Tactic:
| succ m =>

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

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ 2 * 1 * 2 ^ (n + 1) = 2 ^ (n + 2)

pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
· norm_cast; rw [pow_add, pow_add]; ring_nf

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree
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
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H ⇑α
hy₀ : ⟨y, hyα⟩ ≠ 0
hy : ⁅y, f⁆ = 0
⊢ False

Tactic:
have P : ht.symm.HasPrimitiveVectorWith y (-2 : K) :=
    { ne_zero := by simpa [LieSubmodule.mk_eq_zero] using! hy₀
      lie_h := by simp only [neg_smul, neg_lie, ht.h_eq_coroot hα heα hfα,
        ← H.coe_bracket_of_module, lie_eq_smul_of_mem_rootSpace hyα (coroot α),
        root_apply_coroot hα]
      lie_e := by rw [← lie_skew, hy, neg_zero] }

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
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
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H ⇑α
hy₀ : ⟨y, hyα⟩ ≠ 0
hy : ⁅y, f⁆ = 0
P : ⋯.HasPrimitiveVectorWith y (-2)
⊢ False
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (↑n + 1)) = U R' (↑n + 1)
ih2 : map f (U R ↑n) = U R' ↑n
⊢ map f (U R (↑n + 2)) = U R' (↑n + 2)

Tactic:
simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

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

Goal state before:
pp: case h
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
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
c₂ : K
hx_neg : c₂ • f ∈ ↑(genWeightSpace L (-⇑α))
hx_αneg : c₁ • e + c₂ • f ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
c₃ : K
hy_coroot : c₃ • coroot α ∈ ↑↑(corootSpace ⇑α)
hx :
  c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) ∈
    genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl (c₃ • coroot α) = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
simp [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, -LieSubmodule.incl_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
p : Submodule R M
⊢ Surjective ⇑(tensorToSpan A p)

Tactic:
intro v

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
p : Submodule R M
v : ↥(span A ↑p)
⊢ ∃ a, (tensorToSpan A p) a = v
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: case h
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
v : A
h : (algebraMap A K) v = x
⊢ (algebraMap A K) (num A x) = x * (algebraMap A K) ↑(den A x)

Tactic:
← div_eq_iff

Goal state after:
case h
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
v : A
h : (algebraMap A K) v = x
⊢ (algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x

case h
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
v : A
h : (algebraMap A K) v = x
⊢ (algebraMap A K) ↑(den A 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
n : ℕ
b : Basis (Fin n) L M
b' : Basis (Fin n) K ↥M'
hb : ∀ (i : Fin n), b i = ↑(b' i)
⊢ finrank K ↥M' = finrank L M

Tactic:
finrank_eq_card_basis b,

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
n : ℕ
b : Basis (Fin n) L M
b' : Basis (Fin n) K ↥M'
hb : ∀ (i : Fin n), b i = ↑(b' i)
⊢ finrank K ↥M' = Fintype.card (Fin n)
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
let cov := s.step i

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
⊢ IsFiniteLength R ↥(s.toFun i.succ)
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
h : ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊤

Tactic:
obtain ⟨s, s_head, s_last⟩ := h
    rw [← s_last]
    suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
    intro i
    induction i using Fin.induction with
    | zero => change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
    | succ i ih =>
      let cov := s.step i
      have := (covBy_iff_quot_is_simple cov.le).mp cov
      have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
        _ (Submodule.injective_subtype _)
      rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
      exact .of_simple_quotient (this.symm.isFiniteLength ih)

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀ˣ
⊢ embedding ((restrict₀ f) 0) < embedding ↑a

Tactic:
rw [embedding_strictMono.lt_iff_lt]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀ˣ
⊢ (restrict₀ f) 0 < ↑a
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
intro H

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
⊢ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R

Tactic:
intro H

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R
Module: Mathlib.RingTheory.Length

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

Tactic:
add_comm,

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
⊢ v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)

Tactic:
by
  obtain ⟨z, rfl⟩ := h
  grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]

Goal state after:
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 : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : m ∈ ⊤
⊢ r • m ∈ (J ^ n).toAddSubmonoid • ⊤

Tactic:
rw [← algebraMap_smul S r m]

Goal state after:
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 : ℕ
r : R
hr : r ∈ (I ^ n).toAddSubmonoid
m : M
hm : m ∈ ⊤
⊢ (algebraMap R S) r • m ∈ (J ^ n).toAddSubmonoid • ⊤
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

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:
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
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.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
⊢ ¬DenselyOrdered ↑(range ⇑v)

Tactic:
intro H

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
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
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
intro H

Goal state after:
case mp
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 : ValuationRing R
⊢ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
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
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R

Tactic:
intro H

Goal state after:
case mpr
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⁻¹
⊢ ValuationRing R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ

Tactic:
add_comm,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (n + 1))
⊢ Associated p ϖ
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
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
b : R
u : Rˣ
m : ℕ
h : p ∣ Classical.choose hR ^ m.succ * b
ha : ¬Classical.choose hR ^ m.succ * ↑u = 0
hm : ¬m.succ = 0
⊢ p ∣ Classical.choose hR * Classical.choose hR ^ m

Tactic:
apply dvd_mul_of_dvd_left dvd_rfl _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P

Tactic:
rw [jacobson, mem_sInf] at hx

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P