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

Goal state before:
pp: case mem
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q

Tactic:
rw [genWeightSpaceChain]

Goal state after:
case mem
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x : L
hx : x ∈ LieAlgebra.derivedSeries R L 1
⊢ (trace R M) (φ x * y) = 0

Tactic:
by
  replace hx : x ∈ Submodule.span R {⁅u, v⁆ | (u : L) (v : L)} := by
    rw [← LieAlgebra.coe_derivedSeries_one_eq]; exact hx
  induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨a, b, rfl⟩ := hu
    obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
    replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
    rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, hbc, mul_neg, map_neg, neg_eq_zero,
      Module.End.mul_eq_comp, ← traceForm_apply_apply, h, LinearMap.zero_apply,
      LinearMap.zero_apply]
  | zero => simp
  | add u v _ _ hu hv => simp [add_mul, hu, hv]
  | smul t u _ hu => simp [hu]

Goal state after:
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
hm₀ : m₀ ∈ genWeightSpace M 0
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
⊢ ∀ (x : L), ∀ m ∈ posFittingCompOf R M x, (B m₀) m = 0

Tactic:
intro x m₁ hm₁

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
hm₀ : m₀ ∈ genWeightSpace M 0
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
m₁ : M
hm₁ : m₁ ∈ posFittingCompOf R M x
⊢ (B m₀) m₁ = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ (trace K M) ((toEnd K L M) x ∘ₗ (toEnd K L M) y) = ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
LinearMap.trace_eq_sum_trace_restrict hds hxy,

Goal state after:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ ∑ i, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-↑(k + 1) + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) -
      (2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1)) + T R (Int.negSucc k)) =
    0

Tactic:
(simp [Int.negSucc_eq]; ring_nf)

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x x✝ y✝ : L
hx✝ : x✝ ∈ lieSpan R L (range b.e)
hy✝ : y✝ ∈ lieSpan R L (range b.e)
hu : x✝ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : y✝ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
⊢ x✝ + y✝ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
| add _ _ _ _ hu hv =>

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-↑(k + 1) + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) -
      (2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1)) + U R (Int.negSucc k)) =
    0

Tactic:
(simp [Int.negSucc_eq]; ring_nf)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval (-1) (U R n) = ↑↑n.negOnePow * (↑n + 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
      Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
    norm_cast
    norm_num
    ring

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-↑(k + 1) + 2) + (X * C R (-↑k) - C R (-↑k + 1)) -
      (X * C R (-↑(k + 1) + 1) - C R (-↑(k + 1)) + C R (Int.negSucc k)) =
    0

Tactic:
(simp [Int.negSucc_eq]; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-↑(k + 1) + 2) + (X * S R (-↑k) - S R (-↑k + 1)) -
      (X * S R (-↑(k + 1) + 1) - S R (-↑(k + 1)) + S R (Int.negSucc k)) =
    0

Tactic:
(simp [Int.negSucc_eq]; ring_nf)

Goal state after:
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
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) * (-(g x * 1) - 2 * -(g x * 1)) +
      Polynomial.eval t (S R (-↑m - 1)) * -g x * (1 - 2 * 1 - f y * -(g x * 1)) =
    Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x * 1

Tactic:
linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)

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
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
h : P.root j = t • P.root i
⊢ t • P.coroot j = P.coroot i

Tactic:
by
  have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).symm
  refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i)
    (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_
    (P.mapsTo_coreflection_coroot i) (mem_range_self i)
  convert! P.mapsTo_coreflection_coroot j
  ext x
  replace h : P.root' j = t • P.root' i := by ext; simp [h, root']
  simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (↑n + 1) * ↑n * T R (n + 1) = ↑n * X * derivative (T R (n + 1)) - (↑n + 1) * derivative (T R n)

Tactic:
have h := T_eq_X_mul_U_sub_U (R := R) (n - 1)
  rw [T_derivative_eq_U, T_derivative_eq_U]
  linear_combination (norm := (push_cast; ring_nf))
    (n + 1) * n * h

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

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

Tactic:
have h := congr_arg derivative^[k] <| one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T
    (R := R) n
  norm_cast at h
  rw [sub_mul, iterate_derivative_sub, one_mul, ← Function.iterate_add_apply, mul_comm (X ^ 2),
    iterate_derivative_sub, mul_comm X, iterate_derivative_intCast_mul,
    iterate_derivative_derivative_mul_X_sq, iterate_derivative_derivative_mul_X] at h
  linear_combination (norm := (push_cast; ring_nf)) h
  cases k <;> grind

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

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : 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
⊢ ⊤ ≤ span L (Set.range Subtype.val)

Tactic:
rw [← hv₂, Subtype.range_coe_subtype, Set.ofPred_mem_eq]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ ↑s.length = length R M

Tactic:
rw [← WithBot.coe_inj, Module.coe_length]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ ↑↑s.length = Order.krullDim (Submodule R M)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr
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
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
o1 : O
ho1 : (algebraMap O R) o1 = 1
⊢ Nontrivial O

Tactic:
refine ⟨o0, o1, ?_⟩

Goal state after:
case mpr
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
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
o1 : O
ho1 : (algebraMap O R) o1 = 1
⊢ o0 ≠ o1
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 : ℕ
⊢ ∀ m ∈ (I ^ n).toAddSubmonoid, ∀ n_1 ∈ ⊤, m • n_1 ∈ (J ^ n).toAddSubmonoid • ⊤

Tactic:
intro r hr m hm

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 ∈ ⊤
⊢ r • m ∈ (J ^ n).toAddSubmonoid • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
m : R
n : ℕ
⊢ f m ≡ g m [SMOD I ^ n • ⊤]

Tactic:
apply SModEq.mono (Submodule.pow_smul_top_le I S ha.le_apply)

Goal state after:
R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
m : R
n : ℕ
⊢ f m ≡ g m [SMOD I ^ a 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 : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f n ≡ f 1 [SMOD ⊥ ^ n • ⊤]

Tactic:
rcases n with - | n

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 ⊥ ^ 0 • ⊤]

case succ
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 • ⊤]
n : ℕ
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]

Tactic:
obtain ⟨x, hx⟩ := h u

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
x : M
hx : (of I M) x = u
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_2
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Tactic:
exact isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective h.1 h.2

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ ¬v (x + y) < max (v x) (v y)

Tactic:
intro h'

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < max (v x) (v y)
⊢ False
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) a ≤ (addVal R) b
ha0 : a = 0
⊢ a ∣ b

Tactic:
rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h

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 : b = 0
ha0 : a = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
⊢ (f.comp C).IsIntegral

Tactic:
have : (f'.comp C).IsIntegral := by
    have : (RingHom.ker f').IsMaximal := ker_isMaximal_of_surjective f' hf'
    let g : MvPolynomial _ R ⧸ (RingHom.ker f') →+* S :=
      Ideal.Quotient.lift (RingHom.ker f') f' fun _ h => h
    have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' :=
      ringHom_ext (fun r => rfl) fun i => rfl
    rw [← hfg, RingHom.comp_assoc]
    refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g
      (g.isIntegral_of_surjective ?_)
    rw [← hfg, coe_comp] at hf'
    exact Function.Surjective.of_comp hf'

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f'.comp C).IsIntegral
⊢ (f.comp C).IsIntegral
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
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
⊢ P.IsValuedIn S ↔ ∀ (i j : ι), P.pairing i j ∈ range ⇑(algebraMap S R)

Tactic:
by
  simp only [isValuedIn_iff, mem_range]

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

Goal state before:
pp: T : Type u_2
inst✝ : CommSemiring T
⊢ closure {x | IsSquare x} = sumSq T

Tactic:
apply_fun toNonUnitalSubsemiring using toNonUnitalSubsemiring_injective
  simp [← Submonoid.square_subsemiringClosure]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : (Q₁.prod Q₂).Anisotropic
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic

Tactic:
simp_rw [Anisotropic, prod_apply, Prod.forall, Prod.mk_eq_zero] at h
  constructor
  · intro x hx
    refine (h x 0 ?_).1
    rw [hx, zero_add, map_zero]
  · intro x hx
    refine (h 0 x ?_).2
    rw [hx, add_zero, map_zero]

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

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : x = g.indexEquiv.symm (f.indexEquiv x)
⊢ y = g.indexEquiv x

Tactic:
rw [this, Equiv.apply_symm_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Finite ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : Nontrivial R
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
b : Basis (↑s) R M := Basis.mk hli ⋯
_i : Fintype ↑s
⊢ s.ncard = finrank R M

Tactic:
ncard_eq_toFinset_card

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Finite ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : Nontrivial R
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
b : Basis (↑s) R M := Basis.mk hli ⋯
_i : Fintype ↑s
⊢ ⋯.toFinset.card = finrank R M
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainBotCoeff i j) = sSup {k | P.root j - k • P.root i ∈ range ⇑P.root}

Tactic:
rw [setOfPred_root_sub_zsmul_mem_eq_Icc h]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainBotCoeff i j) = sSup (Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j))
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i✝ j✝ : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i✝ + P.root j✝ ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
i j k : ι
hk : P.root k = P.root i + P.root j
hi : P.root i ∈ q
hij₀ : P.pairing i j ≠ 0
hq : P.root i - P.pairing i j • P.root j ∈ q
⊢ P.root j ∈ q

Tactic:
rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq

Goal state after: