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

Goal state before:
pp: 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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
⊢ IsCompl M₀ (posFittingComp R L M)

Tactic:
set M₁ := posFittingComp R L M

Goal state after:
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
⊢ IsCompl M₀ M₁
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.inl
ι : 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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
⊢ b.h i ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
apply LieSubmodule.mem_sup_left

Goal state after:
case mem.inl
ι : 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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
⊢ b.h i ∈ H.toLieSubmodule
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
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j ∈ s, w j * (B (v j)) (v i) = w i * (B (v i)) (v i)
this : w i * (B (v i)) (v i) = 0
⊢ w i = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this

Goal state after:
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅↑x, z⁆ = 0

Tactic:
← LieSubmodule.mem_bot (R := K) (L := L),

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅↑x, z⁆ ∈ ⊥
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (x_1 : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) x_1) m = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B (y + z)) ↑m = 0

Tactic:
rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m, ∃ a_1 < count a m, (a, a_1) = (x, i)) ↔ (x, i) ∈ {p | p.2 < count p.1 m}

Tactic:
Prod.mk_inj,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m, ∃ a_1 < count a m, a = x ∧ a_1 = i) ↔ (x, i) ∈ {p | p.2 < count p.1 m}
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
⊢ ∀ (x : α × ℕ),
    x ∈ m.toFinset.disjiUnion (fun x ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) ⋯ ↔
      x ∈ {p | p.2 < count p.1 m}

Tactic:
rintro ⟨x, i⟩
      simp_rw [Finset.mem_disjiUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range,
        Function.Embedding.coeFn_mk, Prod.mk_inj, Set.mem_ofPred_eq]
      simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]
      exact fun h ↦ Multiset.count_pos.mp (by lia)

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

Goal state before:
pp: case right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
case right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
⊢ ⊤ ≤ J
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
set K := s'.sup id

Goal state after:
case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
⊢ ∃ t ⊆ s, I = t.sup id
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: K : Type u_2
M : Type u_3
N : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
p : M →ₗ[K] N →ₗ[K] K
inst✝ : FiniteDimensional K M
h : Injective ⇑p
h' : Injective ⇑p.flip
⊢ Surjective ⇑p

Tactic:
by rwa [← p.flip_injective_iff₁]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteSpan

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun x ↦ e' * x) k 1
⊢ IsOfFinOrder e

Tactic:
refine ⟨k, hk₀, ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun x ↦ e' * x) k 1
⊢ IsPeriodicPt (fun x ↦ e * x) k 1
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
y : L
⊢ ((killingForm R L) y) x = 0

Tactic:
LieModule.traceForm_apply_apply

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
⊢ (trace R L) ((LieModule.toEnd R L L) y ∘ₗ (LieModule.toEnd R L L) 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:
by
  suffices ∀ y ∈ p, reflection h y ∈ p from
    (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy
  intro y hy
  simpa only [reflection_apply, p.sub_mem_iff_right hy] using p.smul_mem (f y) hx

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
this : IsUnit (2 * (α α')⁻¹)
⊢ K ∙ coroot α = K ∙ α'

Tactic:
change (K ∙ (2 • (α α')⁻¹ • α')) = _

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α : ¬α.IsZero
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
this : IsUnit (2 * (α α')⁻¹)
⊢ K ∙ 2 • (α α')⁻¹ • α' = K ∙ α'
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α : ¬α.IsZero
x : ↥H
hx : x ∈ Weight.ker
y : ↥H
hy : y ∈ K ∙ coroot α
⊢ ((traceForm K (↥H) L) y) x = 0

Tactic:
have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy

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α : ¬α.IsZero
x : ↥H
hx : x ∈ Weight.ker
y : ↥H
hy : y ∈ K ∙ coroot α
this : ((traceForm K (↥H) L) x) y = 0
⊢ ((traceForm K (↥H) L) y) x = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : 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 : L
t : R
u : L
hu : u ∈ H
hv' : ∀ (hx : u ∈ H), (b.baseSupp i) ⟨u, hx⟩ • b.e i = ⁅u, b.e i⁆
hx : t • u ∈ H
⊢ (b.baseSupp i) ⟨t • u, hx⟩ • b.e i = ⁅t • u, b.e i⁆

Tactic:
rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]

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

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

Tactic:
norm_cast; simp [pow_add, mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ C R 2 = X ^ 2 - 2

Tactic:
simpa [pow_two, mul_assoc] using C_add_two R 0

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

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

Tactic:
by simpa [sub_sub] using S_neg_sub_one R (n - 1)

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : 2 * S R (↑n + 1 + 1) = X * S R (↑n + 1) + C R (↑n + 1 + 1)
ih2 : 2 * S R (↑n + 1) = X * S R ↑n + C R (↑n + 1)
⊢ 2 * S R (↑n + 2 + 1) = X * S R (↑n + 2) + C R (↑n + 2 + 1)

Tactic:
have h₁ := S_add_two R (n + 1)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : 2 * S R (↑n + 1 + 1) = X * S R (↑n + 1) + C R (↑n + 1 + 1)
ih2 : 2 * S R (↑n + 1) = X * S R ↑n + C R (↑n + 1)
h₁ : S R (↑n + 1 + 2) = X * S R (↑n + 1 + 1) - S R (↑n + 1)
⊢ 2 * S R (↑n + 2 + 1) = X * S R (↑n + 2) + C R (↑n + 2 + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (U R n) = eval x (U R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_U]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (T R n)) = eval ((algebraMap R R') x) (T R' n)

Tactic:
by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]

Goal state after:
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 ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ⇑(∑ i, m i • b.baseSupp i) + ⇑(∑ i, n i • b.baseSupp i) = 0
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0

Tactic:
change ⇑(∑ i, m i • b.baseSupp i + ∑ i, n i • b.baseSupp i) = 0 at hn'

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 ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : ⇑(∑ i, m i • b.baseSupp i) ∈ sU
hg : ⇑(∑ i, m i • b.baseSupp i) ∈ sV
hn' : ⇑(∑ i, m i • b.baseSupp i + ∑ i, n i • b.baseSupp i) = 0
⊢ ∑ i, (Nat.cast ∘ (m + n)) i • b.baseSupp i = 0
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.flip.coxeterWeight i j = P.coxeterWeight i j

Tactic:
by
  simp [coxeterWeight, mul_comm (P.pairing j i)]

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 K Subtype.val
x✝ : { x // x ∈ v }
⊢ ↑x✝ = (⇑M'.subtype ∘ v') x✝

Tactic:
simp [v']

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' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hM : span L ↑i.range = ⊤
hN : span L ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
⊢ ∀ x ∈ i.range, ∀ y ∈ j.range, (p x) y ∈ (algebraMap K L).range

Tactic:
rintro - ⟨m, rfl⟩ - ⟨n, rfl⟩
    exact hp m n

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
⊢ IsBezout S

Tactic:
rw [iff_span_pair_isPrincipal]

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 : S), Submodule.IsPrincipal (Ideal.span {x, y})
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hf : Function.Injective ⇑f
⊢ length R N ≤ length R M

Tactic:
rw [Module.length_eq_add_of_exact f (LinearMap.range f).mkQ hf
    (Submodule.mkQ_surjective _) (LinearMap.exact_map_mkQ_range f)]
  exact le_self_add

Goal state after:
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
⊢ Nontrivial O

Tactic:
obtain ⟨o0, ho0⟩ := hv.exists_of_le_one (r := 0) (by simp)
    obtain ⟨o1, ho1⟩ := hv.exists_of_le_one (r := 1) (by simp)
    refine ⟨o0, o1, ?_⟩
    rintro rfl
    simp [ho1] at ho0

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
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : v ((algebraMap O F) x) ≤ v ((algebraMap O F) x) * v ((algebraMap O F) d)
⊢ 0 < v ((algebraMap O F) x)

Tactic:
simp [hv.valuation_pos_iff_ne_zero, hx0]

Goal state after:
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
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) y)⁻¹

Tactic:
obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y

Goal state after:
case mp.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
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s))⁻¹

case mp.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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y)⁻¹
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
inst✝⁶ : SMul S R
inst✝⁵ : SMul Sᵐᵒᵖ R
inst✝⁴ : SMul S M
inst✝³ : SMul Sᵐᵒᵖ M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower Sᵐᵒᵖ R M
inst✝ : IsCentralScalar S M
s : S
f : AdicCompletion I M
⊢ MulOpposite.op s • f = s • f

Tactic:
ext; simp [val_smul, op_smul_eq_smul]

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

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ I = 1

Tactic:
hI',

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ ⊤ = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ quotient x 0 = 0

Tactic:
simp [quotient]

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

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
⊢ Function.Injective ⇑(algebraMap S Sₘ)

Tactic:
exact IsLocalization.injective Sₘ hM

Goal state after: