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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
⊢ χ ⁅z, a⁆ = 0

Tactic:
have hzU (x : V) (hx : x ∈ U) : (π z) x ∈ U := by
    suffices Submodule.map (π z) U ≤ U from this <| Submodule.mem_map_of_mem hx
    simp only [U, Submodule.map_iSup, iSup_le_iff]
    exact fun i ↦ (map_U'_le i).trans (le_iSup _ _)

Goal state after:
case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
⊢ χ ⁅z, a⁆ = 0
Module: Mathlib.Algebra.Lie.Extension

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✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
y : M
z : E.L
⊢ ⁅E.proj z, y⁆ = E.toKer.symm ⁅z, E.toKer y⁆

Tactic:
obtain ⟨x, hx⟩ : E.proj_surjective.hasRightInverse.choose (E.proj z) - z ∈ E.incl.range := by
    rw [E.IsExtension.exact]
    change _ ∈ E.proj.ker
    simp [E.proj_surjective.hasRightInverse.choose_spec (E.proj z)]

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✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
y : M
z : E.L
x : M
hx : ↑E.incl x = Exists.choose ⋯ (E.proj z) - z
⊢ ⁅E.proj z, y⁆ = E.toKer.symm ⁅z, E.toKer y⁆
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p ^ n) ((p ^ k) x) = ((p.toList x).rotate k)[n]

Tactic:
getElem_rotate,

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p ^ n) ((p ^ k) x) = (p.toList x)[(n + k) % (p.toList x).length]
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x✝¹ : R
x✝ : L
⊢ { toFun := fun y ↦ ⟨⁅s (x✝¹ • x✝), s y⁆ - s ⁅x✝¹ • x✝, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := fun y ↦ ⟨⁅s x✝, s y⁆ - s ⁅x✝, y⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp [smul_sub]

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 + 1) → Fin n
i j : Fin n
⊢ A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det =
    pminor A α * A i j + ∑ s, (-1) ^ (↑s + 1) * (A.submatrix (Fin.cons i (s.removeNth α)) α).det * A (α s) j

Tactic:
by
    simp only [mul_comm (A i j), mul_right_comm]

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

Goal state before:
pp: n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hα : α ∈ S p i
hik : i < k
hk : k ∉ Set.range α
⊢ ∃ t, t.insertNth k α ∈ S (p + 1) i

Tactic:
set t := ⨅ j ∈ {j | k < α j}, j.castSucc with t_eq

Goal state after:
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hα : α ∈ S p i
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
⊢ ∃ t, t.insertNth k α ∈ S (p + 1) i
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:

Tactic:
⁅x, v⁆
          = ⁅π₁ x, v⁆ + ⁅projection _ _ hA.symm x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v    := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
a : A
b : B
hm : m ∈ ↑p
⊢ a ⊗ₜ[R] b • m ∈ ↑p

Tactic:
by simpa only [TensorProduct.Algebra.smul_def] using! hA a (hB b hm)

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ 1

Tactic:
hr

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ c i
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
⊢ r ≤ q → r ∈ Finset.image c Finset.univ

Tactic:
hr

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
⊢ r ∈ Finset.image c Finset.univ
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
r : Associates M
⊢ r ∈ Finset.image c Finset.univ → r ∈ Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ

Tactic:
hr

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
r : Associates M
hr : r ∈ Finset.image c Finset.univ
⊢ r ∈ Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
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:
intro hx
        obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)
        exact mem_ofPred.mpr ⟨y, hx, rfl⟩

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J
⊢ I * I⁻¹ = 1

Tactic:
suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹) = 1 by
    rw [mul_inv_cancel_iff]
    exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J
⊢ I * (spanSingleton A⁰ ((algebraMap A (FractionRing A)) a) * (↑J)⁻¹) = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ x' * y' = x * a • y'

Tactic:
rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

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

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
⊢ spanSingleton R₁⁰ (mk' K y ⟨y, hy⟩) = 1

Tactic:
IsLocalization.mk'_self,

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
⊢ spanSingleton R₁⁰ 1 = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1
y' : (FractionalIdeal R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this
coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔
    spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = spanSingleton R₁⁰ (mk' K y ⟨y, hy⟩) * ↑J

Tactic:
IsLocalization.mk'_self,

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1
y' : (FractionalIdeal R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this
coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = spanSingleton R₁⁰ 1 * ↑J
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := ↑s) K (⇑f ∘ Subtype.val)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
⊢ (Set.range fun x ↦ f ↑x) ⊆ ↑f.range

Tactic:
rintro x ⟨a, rfl⟩

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := ↑s) K (⇑f ∘ Subtype.val)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
a : ↑s
⊢ (fun x ↦ f ↑x) a ∈ ↑f.range
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' v' : V₂ →ₗ[K] V₃
h : u ≈ v
h' : u' ≈ v'
⊢ u' ∘ₗ u ≈ v' ∘ₗ v

Tactic:
equiv_comp_right h',

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' v' : V₂ →ₗ[K] V₃
h : u ≈ v
h' : u' ≈ v'
⊢ v' ∘ₗ u ≈ v' ∘ₗ v
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ I ≠ ⊤ ↔ ∃ P, I ≤ P.asIdeal

Tactic:
Ideal.ne_top_iff_exists_maximal

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ (∃ M, M.IsMaximal ∧ I ≤ M) ↔ ∃ P, I ≤ P.asIdeal
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:

Tactic:
_ = .id ∘ₗ (u ∘ₗ (w ∘ₗ v)) := rfl
    _ ≈ (v' ∘ₗ v) ∘ₗ (u ∘ₗ (w ∘ₗ v)) := by grw [hv.equiv]
    _ = v' ∘ₗ ((v ∘ₗ u) ∘ₗ w) ∘ₗ v := rfl
    _ ≈ v' ∘ₗ .id ∘ₗ v := by grw [hw.equiv]
    _ ≈ .id := hv.equiv

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
h : Module.Finite R M
⊢ FinitePresentation R M

Tactic:
by
  obtain ⟨s, hs⟩ := h
  exact ⟨s, hs, IsNoetherian.noetherian _⟩

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

Goal state before:
pp: case hle
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 ∣ span {a₀}

Tactic:
simp only [span_singleton_pow, heq, dvd_span_singleton]

Goal state after:
case hle
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
⊢ x ^ n * a ∈ span {x ^ n}
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
ι : Type ?u.14
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype ι
I : Ideal R
P : ι → HeightOneSpectrum R
e : ι → ℕ
coprime : Pairwise fun i j ↦ P i ≠ P j
prod_eq : ∏ i, (P i).asIdeal ^ e i = I
⊢ I = ⨅ i, (P i).asIdeal ^ e i

Tactic:
by simp [← prod_eq, Finset.inf_eq_iInf, Finset.mem_univ,
      ← HeightOneSpectrum.inf_pow_eq_prod _ _ _ (coprime.set_pairwise _)]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
h.emultiplicity_eq_multiplicity

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = ↑(multiplicity a b)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

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✝³ : 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_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
h_neg_zero : ⁅x_χ, m_neg⁆ = 0
h_pairing_eq : 0 = ↑i (coroot ↑j)
w_eq : ∀ {w₁ w₂ : Weight K (↥H) L}, Weight.toLinear K (↥H) L w₁ = Weight.toLinear K (↥H) L w₂ → w₁ = w₂
⊢ Weight.toLinear K (↥H) L ↑i = Weight.toLinear K (↥H) L χ

Tactic:
rw [← hi]; rfl

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
S : Submonoid R
f✝ : N →ₗ[R] N'
inst✝³ : IsLocalizedModule S f✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
⊢ Module.FinitePresentation A (A ⊗[R] M)

Tactic:
apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)

Goal state after:
R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
S : Submonoid R
f✝ : N →ₗ[R] N'
inst✝³ : IsLocalizedModule S f✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
⊢ (LinearMap.baseChange A f).ker.FG
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
this : Function.Surjective f
⊢ Nontrivial (HeightOneSpectrum A)

Tactic:
exact this.nontrivial

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Submodule.map f (Submodule.span A (Set.range g₁)) ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker

Tactic:
Submodule.map_span,

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Submodule.span A (⇑f '' Set.range g₁) ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker
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
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
r : R
⊢ D (C r) = 0

Tactic:
rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = p ^ k • a • y

Tactic:
rw [smul_smul, mul_comm]

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
a : R
ha : f (Submodule.Quotient.mk (a * p ^ k)) = ⟨p ^ k • x, h⟩
⊢ p ^ k • x = (a * p ^ k) • y