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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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 e f : L
t : IsSl2Triple h e f
x y : L
hx : x ∈ (span R {e, f, h}).carrier
hy : y ∈ (span R {e, f, h}).carrier
⊢ ⁅x, y⁆ ∈ (span R {e, f, h}).carrier

Tactic:
simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
    induction hx using span_induction with
    | zero => simp
    | add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
    | smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
    | mem u hu =>
      induction hy using span_induction with
      | zero => simp
      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
      | mem v hv =>
        push _ ∈ _ at hu hv
        rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
        · rw [t.lie_e_f]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_e_nsmul]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

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

Goal state before:
pp: case mem
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
χ₁ : ↥H → R
u : L
hu : u ∈ ⨆ (_ : χ₁ ∈ s), rootSpace H χ₁
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
by_cases hχ₁ : χ₁ ∈ s

Goal state after:
case pos
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
χ₁ : ↥H → R
u : L
hu : u ∈ ⨆ (_ : χ₁ ∈ s), rootSpace H χ₁
hχ₁ : χ₁ ∈ s
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

case neg
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
χ₁ : ↥H → R
u : L
hu : u ∈ ⨆ (_ : χ₁ ∈ s), rootSpace H χ₁
hχ₁ : χ₁ ∉ s
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ ↑(toModuleHom R L M) = ↑(toModuleHom R L M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ ∃ y_1, (φ ^ k) y_1 = ⁅y, (φ ^ (N + k)) m⁆

Tactic:
use toModuleHom R L M (q (y ⊗ₜ m))

Goal state after:
case h
K : Type u_1
R : Type u_2
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
x : L
φ : Module.End R M := ⋯
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := ⋯
f₂ : Module.End R (L ⊗[R] M) := ⋯
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ ↑(toModuleHom R L M) = ↑(toModuleHom R L M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ (φ ^ k) ((toModuleHom R L M) (q (y ⊗ₜ[R] m))) = ⁅y, (φ ^ (N + k)) m⁆
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case refine_2
R : Type u_2
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
⊢ genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)

Tactic:
rw [← LieSubmodule.map_le_iff_le_comap]

Goal state after:
case refine_2
R : Type u_2
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ
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
⊢ H = lieSpan R L (range (-b.h))

Tactic:
rw [← neg_range', lieSpan_neg]

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
⊢ H = lieSpan R L (range b.h)
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W)

Tactic:
calc
    finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) := le_self_add
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W) := ?_
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) := by simp [h.eq_bot]

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W)
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
hx : x ∈ ↑m.toFinset
y : α
hy : y ∈ ↑m.toFinset
hxy : x ≠ y
⊢ Function.onFun Disjoint (fun x ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) x y

Tactic:
by simp [Function.onFun, Finset.disjoint_right, hxy]

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f (↑x).1 (↑x).2

Tactic:
← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ i, f (↑i).1 (↑i).2 = ∏ x, f (↑x).1 (↑x).2
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
⊢ (trace R ↥p) (f.restrict hf') = ((toMatrix snf.bM snf.bM) f).trace

Tactic:
trace_eq_matrix_trace R snf.bN

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
⊢ ((toMatrix snf.bN snf.bN) (f.restrict hf')).trace = ((toMatrix snf.bM snf.bM) f).trace
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: case add
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 χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
hm₁' : ∃ n, ((toEnd K L M) x ^ n) m₁ = 0
hm₂' : ∃ n, ((toEnd K L M) x ^ n) m₂ = 0
⊢ ∃ n, ((toEnd K L M) x ^ n) (m₁ + m₂) = 0

Tactic:
obtain ⟨n₁, hn₁⟩ := hm₁'

Goal state after:
case add
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 χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂' : ∃ n, ((toEnd K L M) x ^ n) m₂ = 0
n₁ : ℕ
hn₁ : ((toEnd K L M) x ^ n₁) m₁ = 0
⊢ ∃ n, ((toEnd K L M) x ^ n) (m₁ + m₂) = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
x : L
hx : x ∈ I
⊢ x ∈ killingCompl R L ⊤

Tactic:
simp only [mem_killingCompl, LieSubmodule.mem_top, forall_true_left]

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
x : L
hx : x ∈ I
⊢ ∀ (y : L), ((killingForm R L) y) x = 0
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 : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
⊢ p ∈ End.invtSubmodule ↑(reflection h)

Tactic:
suffices ∀ y ∈ p, reflection h y ∈ p from
    (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
⊢ ∀ y ∈ p, (reflection h) y ∈ p
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 1 (U R n) = ↑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_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring

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
⊢ -x ∈ range ⇑P.root ↔ x ∈ range ⇑P.root

Tactic:
suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root by
    refine ⟨this x, fun h ↦ ?_⟩
    rw [← neg_neg x] at h
    exact this (-x) h

Goal state after:
ι : 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
⊢ ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : derivative (T R (n + 2)) = derivative (X * T R (n + 1) - (1 - X ^ 2) * U R n)
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)
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'
this : span K v = M'
⊢ span K (⇑M'.subtype '' v' '' univ) = Submodule.map M'.subtype ⊤

Tactic:
Set.image_image

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'
this : span K v = M'
⊢ span K ((fun x ↦ M'.subtype (v' x)) '' univ) = Submodule.map M'.subtype ⊤
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)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * (↑n ^ 2 - ↑k ^ 2) * eval 1 ((⇑derivative)^[k] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)

Tactic:
mul_comm _ (_ ^ 2 - _ ^ 2),

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, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)
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 + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)

Tactic:
mul_comm _ (_ ^ 2 - _ ^ 2),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * ∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (-↑k) = T R (m + -↑k) + T R (m - -↑k)
ih2 : 2 * T R m * T R (-↑k + 1) = T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))
⊢ 2 * T R m * T R (-↑k - 1) = T R (m + (-↑k - 1)) + T R (m - (-↑k - 1))

Tactic:
| neg_add_one k ih1 ih2 =>

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

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))

Tactic:
| neg_add_one k ih1 ih2 =>

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 ∈ ⊤
⊢ (algebraMap R S) r • m ∈ (J ^ n).toAddSubmonoid • ⊤

Tactic:
apply AddSubmonoid.smul_mem_smul ?_ hm

Goal state after:
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 ∈ (J ^ n).toAddSubmonoid
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
· exact ⟨⟨x, hx.trans h'.le⟩, hx, 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
⊢ x ∈ I

Tactic:
rw [← hI.radical, radical_eq_sInf I, mem_sInf]

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 : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 → 0 ≤ ringKrullDim R

Tactic:
exact fun _ ↦ ringKrullDim_nonneg_of_nontrivial

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v

Tactic:
rw [← sub_mul, mul_eq_zero] at h

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
⊢ (addVal R) a ≤ (addVal R) b ↔ a ∣ b

Tactic:
have hp := Classical.choose_spec (exists_prime R)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b ↔ a ∣ b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ (addVal R) x = 0 ↔ IsUnit x

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · simp
  obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
  obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ
  simp [isUnit_pow_iff_of_not_isUnit hϖ.not_isUnit, hϖ]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
⊢ Flat R M ↔ torsion R M = ⊥

Tactic:
by
  refine ⟨fun _ ↦ Flat.torsion_eq_bot, fun h ↦ ?_⟩
  apply flat_of_localized_maximal
  intro P hP
  rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at h
  rw [← flat_iff_of_isLocalization (Localization P.primeCompl) P.primeCompl,
    Flat.flat_iff_torsion_eq_bot_of_isBezout, ← Submodule.isTorsionFree_iff_torsion_eq_bot]
  infer_instance

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Tactic:
let rj : span S (range P.root) := ⟨P.root j, hj⟩

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ 0 ≤ ↑(chainTopCoeff (⇑α) β) - n

Tactic:
le_sub_iff_add_le,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ 0 + n ≤ ↑(chainTopCoeff (⇑α) β)