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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
⊢ engel K x ≤ engel K y

Tactic:
set Ex : {engel K z | z ∈ engel K x} := ⟨engel K x, x, self_mem_engel _ _, rfl⟩

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
⊢ engel K x ≤ engel K y
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (((coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i))) ∘ₗ
      ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) =
    LinearMap.id

Tactic:
rw [← LinearEquiv.eq_comp_toLinearMap_symm]

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ ((coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
      ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) =
    LinearMap.id ∘ₗ ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).symm
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList (l.get k) ~r l

Tactic:
get_eq_get_rotate l k k

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨(l.length - ↑k % l.length + ↑k) % l.length, ⋯⟩) ~r l
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n lo : ℕ
f : ℕ → R
⊢ BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
induction lo using BirdDet.sumFrom_induct n with
  | step lo hlo ih => rw [sumFrom_step n lo f hlo, ih, ← Finset.sum_eq_sum_Ico_succ_bot hlo f]
  | stop lo hlo => rw [sumFrom_stop n lo f hlo, Finset.Ico_eq_empty hlo, Finset.sum_empty]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin p → Fin n
i : Fin n
q : Fin p
⊢ bminor A i (α q) α = 0

Tactic:
exact Matrix.det_zero_of_column_eq q.succ_ne_zero <| by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
k : Fin n
α : Fin p → Fin n
i : Fin n
hk : k ∈ Set.range α
⊢ bminor A i k α = 0

Tactic:
by
  obtain ⟨q, rfl⟩ := hk
  -- The repeated columns in the submatrix used in bminor are `0` and `q + 1`.
  exact Matrix.det_zero_of_column_eq q.succ_ne_zero <| by simp

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' L₂' : LieRinehartSubalgebra A L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
SetLike.ext'_iff

Goal state after:
A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.toLieSubalgebra R) L₁' = (fun L' ↦ L'.toLieSubalgebra R) L₂'
⊢ L₁' = L₂'

Tactic:
SetLike.ext'_iff

Goal state after:
A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ L₁' = L₂'
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ E.charPoly.coeff E.charPoly.natDegree = 1

Tactic:
natDegree_eq_of_degree_eq_some <| charPoly_degree_eq_order _,

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ E.charPoly.coeff E.order = 1
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝¹ x✝ : ↥↑I
hxy : ((DistribSMul.toLinearMap R P I.den).restrict ⋯) x✝¹ = ((DistribSMul.toLinearMap R P I.den).restrict ⋯) x✝
⊢ x✝¹ = x✝

pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : y ∈ Submodule.map (Algebra.linearMap R P) I.num
⊢ ∃ a, ((DistribSMul.toLinearMap R P I.den).restrict ⋯) a = ⟨y, hy⟩

Tactic:
· simpa [LinearMap.restrict_apply, reg.eq_iff] using hxy

Goal state after:
case refine_3
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : ↥(Submodule.map (Algebra.linearMap R P) I.num)
y : P
hy : y ∈ Submodule.map (Algebra.linearMap R P) I.num
⊢ ∃ a, ((DistribSMul.toLinearMap R P I.den).restrict ⋯) a = ⟨y, hy⟩
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
⊢ ↑span_compl_roots = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)

Tactic:
simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ I.den • ↑I = ⊥

Tactic:
den_mul_self_eq_num,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ Submodule.map (Algebra.linearMap R P) I.num = ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case mp.refine_4.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } → x ∈ J

pp: case mp.refine_4.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ J → x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Tactic:
· rintro ⟨y, hy, eq_y⟩
        rwa [← eq_y]

Goal state after:
case mp.refine_4.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ J → x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hI : I * I⁻¹ = 1
⊢ generator ↑I ≠ 0

Tactic:
hg

Goal state after:
case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator ↑I = 0
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
              { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩

Tactic:
apply mem_div_iff_forall_mul_mem.mpr

Goal state after:
case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ ∀ y ∈ ↑1, x✝ * y ∈ ↑I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsIntegrallyClosed A

Tactic:
let := h.commGroupWithZero (FractionRing A)
  -- It suffices to show that for integral `x`,
  -- `A[x]` (which is a fractional ideal) is in fact equal to `A`.
  refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)
  rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]
  · exact mem_adjoinIntegral_self A⁰ x hx
  · exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ x ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J

Tactic:
h_xd

Goal state after:
case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁴ : CommRing R₁
K✝ : Type u_4
inst✝¹³ : Field K✝
inst✝¹² : Algebra R₁ K✝
inst✝¹¹ : IsFractionRing R₁ K✝
inst✝¹⁰ : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal R⁰ K
x : L
⊢ x ∈ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑(I + J), ⋯⟩ ↔
    x ∈
      ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩ +
        ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J, ⋯⟩

Tactic:
simp [← mem_coe]

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

Goal state before:
pp: case hp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
h_minus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_eq : i = j
⊢ False

Tactic:
exact w_minus (by rw [← hi, ← hj, h_eq, sub_self])

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
⊢ P.asIdeal ≠ Q.asIdeal

Tactic:
simpa [HeightOneSpectrum.ext_iff] using hPQ

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : IsDedekindDomain A
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : { p // p ∣ I }
⊢ comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)) ∣ J

Tactic:
have : RingHom.ker (Ideal.Quotient.mk J) ≤
        comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)) :=
      ker_le_comap (Ideal.Quotient.mk J)
    rw [mk_ker] at this
    exact dvd_iff_le.mpr this

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hlt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬span {x} ^ (n + 1) ∣ span {a₀}

pp: case hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {a₀} ≠ 0

pp: case hJ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ (span {x}).IsPrime

pp: case hJ₀
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ≠ ⊥

Tactic:
· simp only [span_singleton_pow, heq, dvd_span_singleton, mem_span_singleton]
    rw [pow_add, pow_one, mul_dvd_mul_iff_left (pow_ne_zero n hx0)]
    exact ha

Goal state after:
case hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {a₀} ≠ 0

case hJ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ (span {x}).IsPrime

case hJ₀
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ span {x} ≠ ⊥
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ ↑(primesOverFinset p B) ↔ P ∈ p.primesOver B

Tactic:
coe_primesOverFinset hpb

Goal state after:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ p.primesOver B ↔ P ∈ p.primesOver B
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
f : HeightOneSpectrum A → HeightOneSpectrum R := fun p ↦ HeightOneSpectrum.under R p
x✝ : HeightOneSpectrum R
p : Ideal R
isPrime✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∃ a, f a = { asIdeal := p, isPrime := isPrime✝, ne_bot := hp }

Tactic:
obtain ⟨P, hP, rfl⟩ := p.exists_ideal_over_prime_of_isIntegral_of_isDomain (S := A) (by simp)

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
f : HeightOneSpectrum A → HeightOneSpectrum R := fun p ↦ HeightOneSpectrum.under R p
x✝ : HeightOneSpectrum R
P : Ideal A
hP : P.IsPrime
isPrime✝ : (Ideal.comap (algebraMap R A) P).IsPrime
hp : Ideal.comap (algebraMap R A) P ≠ ⊥
⊢ ∃ a, f a = { asIdeal := Ideal.comap (algebraMap R A) P, isPrime := isPrime✝, ne_bot := hp }
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
i : Fin d
fi : R ⧸ R ∙ p ^ k i →ₗ[R] M ⧸ R ∙ s j := ↑f.symm ∘ₗ DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i
⊢ ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1

Tactic:
obtain ⟨x, h0, h1⟩ := exists_smul_eq_zero_and_mk_eq hp hM hj fi

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
i : Fin d
fi : R ⧸ R ∙ p ^ k i →ₗ[R] M ⧸ R ∙ s j := ↑f.symm ∘ₗ DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i
x : M
h0 : p ^ k i • x = 0
h1 : Submodule.Quotient.mk x = fi 1
⊢ ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      (monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    (monomial s) 1 • (monomial 0) ↑1 • f i +
      (monomial (Finsupp.single i 1)) 1 • s.sum fun i k ↦ (monomial (s - Finsupp.single i 1)) ↑k • f i

Tactic:
add_tsub_cancel_right,

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) + (monomial s) ↑1 • f i =
    (monomial s) 1 • (monomial 0) ↑1 • f i +
      (monomial (Finsupp.single i 1)) 1 • s.sum fun i k ↦ (monomial (s - Finsupp.single i 1)) ↑k • f i
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = a • D f

Tactic:
have : C a • D f = D (C a * f) := by simp
  rw [this, C_mul', D.map_smul]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ (aeval (Generators.localizationAway S r).val) (X x) =
    ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (X x)

Tactic:
simp only [aeval_X, Generators.localizationAway_val, AlgHom.coe_comp,
      AlgEquiv.coe_toAlgHom, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x))