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

Goal state before:
pp: case inr.refine_3
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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ ⁅z, (T χ w) (((toEnd R L V) z ^ n) v)⁆ ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
exact map_U'_le _ <| Submodule.mem_map_of_mem <| hn w n n.lt_succ_self

Goal state after:
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
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) + (⁅s z, ⁅s x, s y⁆⁆ - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - s ⁅z, ⁅x, y⁆⁆)) -
      (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - s ⁅z, ⁅y, x⁆⁆)) =
    0

Tactic:
rw [hjac, hj, hja, ← lie_skew y z, ← lie_skew _ (s (-⁅z, y⁆)), ← lie_skew (s ⁅x, z⁆),
      ← lie_skew (s ⁅x, y⁆), ← lie_skew x z]

Goal state after:
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
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - -⁅s (-⁅z, y⁆), s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s (-⁅z, x⁆)⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (-⁅s z, s ⁅x, y⁆⁆ - (s ⁅x, -⁅z, y⁆⁆ - s ⁅y, -⁅z, x⁆⁆)) +
        (-⁅s y, s (-⁅z, x⁆)⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, -⁅z, y⁆⁆ - ⁅y, -⁅z, x⁆⁆))) -
      (⁅s (-⁅z, y⁆), s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, -⁅z, x⁆⁆ - ⁅x, -⁅z, y⁆⁆))) =
    0
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
⊢ bminor A i j α =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det

Tactic:
by
      rw [bminor, Matrix.det_succ_column_zero, Fin.sum_univ_succ]; 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 : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α =
    (-1) ^ (p + 1) * ∑ x > i, ∑ i ∈ Finset.image (Fin.cons x) (S p x), pminor A i

Tactic:
congrm (((-1) ^ (p + 1) * ∑ k ∈ Finset.Ioi i, ?_))

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
k : Fin n
⊢ ∑ α ∈ S p k, bminor A k k α = ∑ i ∈ Finset.image (Fin.cons k) (S p k), pminor A i
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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ ((traceForm K (↥H) L).toLinHomAux₁ (coroot ↑α)) (coroot ↑β) = 0

Tactic:
exact traceForm_eq_zero_of_mem_ker_of_mem_span_coroot h_ker (Submodule.mem_span_singleton_self _)

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

Goal state before:
pp: 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
x : R₁
hx : x ≠ 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) x) * (spanSingleton R₁⁰ ((algebraMap R₁ K) x))⁻¹ = 1

Tactic:
spanSingleton_mul_inv K <|
      (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx

Goal state after:
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
x : R₁
hx : x ≠ 0
⊢ 1 = 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1

Tactic:
exact coeIdeal_le_one hy

Goal state after:
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
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
γ : ↥LieSubalgebra.root
hγ : γ ∈ I.rootSet
⊢ (Weight.toLinear K (↥H) L ↑γ) (coroot ↑α) = 0

Tactic:
exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not

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

Goal state before:
pp: 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
⊢ ↑I.num ≤ I * I⁻¹

Tactic:
by_cases hI : I = 0

Goal state after:
case pos
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
hI : I = 0
⊢ ↑I.num ≤ I * I⁻¹

case neg
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
hI : ¬I = 0
⊢ ↑I.num ≤ I * I⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
⊢ ∃ Z, (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
classical
    have := Multiset.map_erase asIdeal (fun _ _ => PrimeSpectrum.ext) P Z
    obtain ⟨hP0, hZP0⟩ : P.asIdeal ≠ ⊥ ∧ ((Z.erase P).map asIdeal).prod ≠ ⊥ := by
      rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
        this] at hprodZ
    -- By maximality of `P` and `M`, we have that `P ≤ M` implies `P = M`.
    have hPM' := (P.isPrime.isMaximal hP0).eq_of_le hM.ne_top hPM
    subst hPM'
    -- By minimality of `Z`, erasing `P` from `Z` is exactly what we need.
    refine ⟨Z.erase P, ?_, ?_⟩
    · convert! hZI
      rw [this, Multiset.cons_erase hPZ']
    · refine fun h => h_eraseZ (Z.erase P) ⟨h, ?_⟩ (Multiset.erase_lt.mpr hPZ)
      exact hZP0

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
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ I * (1 / I) ≤ 1

Tactic:
by_cases hI : I = 0

Goal state after:
case pos
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
hI : I = 0
⊢ I * (1 / I) ≤ 1

case neg
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
hI : ¬I = 0
⊢ I * (1 / I) ≤ 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
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ I / 1 = I

Tactic:
by
  rw [div_of_ne_zero (one_ne_zero' (FractionalIdeal R₁⁰ K))]
  ext
  constructor <;> intro h
  · simpa using mem_div_iff_forall_mul_mem.mp h 1 ((algebraMap R₁ K).map_one ▸ coe_mem_one R₁⁰ 1)
  · apply mem_div_iff_forall_mul_mem.mpr
    rintro y ⟨y', _, rfl⟩
    convert! Submodule.smul_mem _ y' h using 1
    rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]

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

Goal state before:
pp: case mpr
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
mem_canonicalEquiv_apply

Goal state after:
case mpr
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y_1 ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y_1 = y
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)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J

Tactic:
exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx

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

Goal state before:
pp: case 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
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d

Tactic:
le_div_iff_mul_le h_spand,

Goal state after:
case 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
⊢ 1 / spanSingleton R₁⁰ d * J * spanSingleton R₁⁰ d ≤ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime ⊤
⊢ False

Tactic:
rw [← one_eq_top] at h

Goal state after:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime 1
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i (normalize P)

pp: case hx
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

pp: case hy
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0

Tactic:
all_goals assumption

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

Goal state before:
pp: case refine_2.refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ a * 0 ∈ ↑J

Tactic:
rw [mul_zero]

Goal state after:
case refine_2.refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
⊢ I * ⨅ i, J i = ⨅ i, I * J i

Tactic:
by_cases hI : I = 0

Goal state after:
case pos
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : I = 0
⊢ I * ⨅ i, J i = ⨅ i, I * J i

case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
⊢ I * ⨅ i, J i = ⨅ i, I * J i
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)
hs : Cardinal.mk ↑s = ↑(finrank K N)
⊢ span K ↑f.range = ⊤

Tactic:
Cardinal.mk_eq_nat_iff_fintype

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)
hs : ∃ h, Fintype.card ↑s = finrank K N
⊢ span K ↑f.range = ⊤
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u.eqLocus v).CoFG

Tactic:
eqLocus_eq_ker_sub,

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u - v).ker.CoFG
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
a✝ : Nontrivial R
⊢ ↑(finrank R ↥id.ker) - ↑(finrank R (M ⧸ id.range)) = 0

Tactic:
range_id

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
a✝ : Nontrivial R
⊢ ↑(finrank R ↥id.ker) - ↑(finrank R (M ⧸ ⊤)) = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
y : N
⊢ ∃ n x, r ^ n • y = f x

Tactic:
by
  obtain ⟨⟨x, ⟨_, n, rfl⟩⟩, h⟩ := IsLocalizedModule.surj (S := .powers r) f y
  use n, x, h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Tactic:
emultiplicity_eq_count_normalizedFactors (Prime.irreducible ?_),

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  ↑(Multiset.count (normalize (span {X})) (normalizedFactors (span {r}))) =
    ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case add
R : Type u
inst✝ : CommRing R
σ : Type u_1
f✝ g✝ : MvPolynomial σ R →₀ MvPolynomial σ R
a✝¹ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) (f✝ + g✝))) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) (f✝ + g✝)

Tactic:
simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom] at *

Goal state after:
case add
R : Type u
inst✝ : CommRing R
σ : Type u_1
f✝ g✝ : MvPolynomial σ R →₀ MvPolynomial σ R
a✝¹ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) +
      (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝ +
      (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
⊢ ∃ x, (toSpanSingleton R M x).ker = annihilator R M

Tactic:
have ⟨m, ι, _, p, irr, n, ⟨e⟩⟩ := equiv_free_prod_directSum (R := R) (M := M)
  refine ⟨e.symm (Finsupp.equivFunOnFinite.symm fun _ ↦ 1, DFinsupp.equivFunOnFintype.symm
    fun _ ↦ mkQ _ 1), le_antisymm (fun x h ↦ ?_) fun x h ↦ mem_annihilator.mp h _⟩
  rw [mem_ker, toSpanSingleton_apply, ← map_smul,
    e.symm.map_eq_zero_iff, Prod.ext_iff, Finsupp.ext_iff, DFinsupp.ext_iff] at h
  obtain _ | m := m
  · rw [← mul_one x, ← smul_eq_mul, e.annihilator_eq, annihilator_prod]
    simp_rw [annihilator_eq_top_iff.mpr inferInstance, DirectSum, annihilator_dfinsupp,
      top_inf_eq, mem_iInf, Ideal.annihilator_quotient, ← Quotient.mk_eq_zero]
    exact h.2
  · rw [show x = 0 by simpa using h.1 0]
    exact zero_mem _

Goal state after: