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

Goal state before:
pp: case mpr
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
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
hx :
  x ∈
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker
this : ((ofProd c).symm x).1 = 0
⊢ x ∈ { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.range

Tactic:
simp only [LieHom.mem_range, LieHom.coe_mk]

Goal state after:
case mpr
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
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
hx :
  x ∈
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker
this : ((ofProd c).symm x).1 = 0
⊢ ∃ y, (ofProd c) (0, y) = x
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: case mpr
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
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
⊢ x ∈
      LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
        { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker →
    x ∈ { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.range

Tactic:
intro hx
          have : ((ofProd c).symm x).1 = 0 := hx
          simp only [LieHom.mem_range, LieHom.coe_mk]
          use ((ofProd c).symm x).2
          nth_rw 2 [← Equiv.apply_symm_apply (ofProd c) x]
          rw [← this]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn✝⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm✝⟩ → ⟨n, hn✝⟩ = ⟨m, hm✝⟩

Tactic:
rw [← cycleOf_apply_self, ← Ne, ← mem_support] at hx

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn✝⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm✝⟩ → ⟨n, hn✝⟩ = ⟨m, hm✝⟩
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⁆⁆)
⊢ ⁅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:
map_neg,

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⁆⁆)
⊢ ⁅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
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:
map_neg,

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 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
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case intro.refine_2.mk.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ x ∈ l

Tactic:
← mem_toFinset

Goal state after:
case intro.refine_2.mk.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ x ∈ l.toFinset
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
⊢ pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j) =
    pminor A α * A i j - ∑ s, bminor A i (α s) (s.removeNth α) * A (α s) j

Tactic:
by
    simp only [Finset.sum_neg_distrib, sub_eq_add_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ A n i j ≤ 0

Tactic:
simp only [A, Matrix.of_apply]

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0) ≤ 0
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
rw [Fin.le_iff_val_le_val, Fin.val_one, Nat.succ_le_iff, ← Fin.val_zero (n.succ + 1), ←
      Fin.lt_def, Fin.pos_iff_ne_zero]
    rintro rfl
    exact hp.not_isUnit (first_of_chain_isUnit h₁ @h₂)

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
⊢ ∃ i, r = c 1 ^ ↑i

Tactic:
let i := Multiset.card (normalizedFactors r)
    have hi : normalizedFactors r = Multiset.replicate i (c 1) := by
      apply Multiset.eq_replicate_of_mem
      intro b hb
      refine
        eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
          (dvd_of_mem_normalizedFactors hb)
    have H : r = c 1 ^ i := by
      have := UniqueFactorizationMonoid.prod_normalizedFactors (ne_zero_of_dvd_ne_zero hq hr)
      rw [associated_iff_eq, hi, Multiset.prod_replicate] at this
      rw [this]
    refine ⟨⟨i, ?_⟩, H⟩
    have : (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card = i + 1 := by
      conv_rhs => rw [← Finset.card_fin (i + 1)]
      cases n
      · contradiction
      rw [Finset.card_image_iff]
      refine Set.injOn_of_injective (fun m m' h => Fin.ext ?_)
      refine
        pow_injective_of_not_isUnit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) ?_ h
      exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
    suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q by
      simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
      apply card_subset_divisors_le_length_of_chain (@h₂) H'
    simp only [Finset.mem_image]
    rintro r ⟨a, _, rfl⟩
    refine dvd_trans ?_ hr
    use c 1 ^ (i - (a : ℕ))
    rw [pow_mul_pow_sub (c 1)]
    · exact H
    · exact Nat.succ_le_succ_iff.mp a.2

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
⊢ α ∈ I.rootSet

Tactic:
by_contra hα_not
  have hα_nz := H.isNonZero_coe_root α
  have : I.rootSpan ≤ LinearMap.ker (Dual.eval K H (coroot (α : Weight K H L))) := by
    rw [LieIdeal.rootSpan, Submodule.span_le]
    rintro _ ⟨γ, hγ, rfl⟩
    simp only [SetLike.mem_coe, LinearMap.mem_ker, Dual.eval_apply, rootSystem_root_apply]
    exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not
  have := LinearMap.mem_ker.mp (this hα_span)
  simp only [Dual.eval_apply, Weight.toLinear_apply, root_apply_coroot hα_nz] at this
  exact absurd this two_ne_zero

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₁
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) ≤ 1

Tactic:
apply mul_le.mpr _

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
inst✝ : IsDomain R₁
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ i ∈ I, ∀ j ∈ 1 / I, i * j ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ I = ⊥

Tactic:
eq_bot_iff,

Goal state after:
case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: 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₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
simp [← coeToSubmodule_inj, div_of_ne_zero H, div_of_ne_zero (map_ne_zero _ H)]

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
inst✝ : IsLocalization S P
x✝ : P
⊢ ∀ (a : R), a • 1 = x✝ ↔ (algebraMap R P) a = x✝

Tactic:
intro x'

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✝ : IsLocalization S P
x✝ : P
x' : R
⊢ x' • 1 = x✝ ↔ (algebraMap R P) x' = x✝
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp.refine_1
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
⊢ ∀ i ∈ spanSingleton S x, ∀ j ∈ I, ∃ y' ∈ I, i * j = x * y'

Tactic:
intro x'

Goal state after:
case mp.refine_1
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
⊢ x' ∈ spanSingleton S x → ∀ j ∈ I, ∃ y' ∈ I, x' * j = x * y'
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : Ideal K[X]
hq : q ∈ Multiset.map (fun q ↦ span {q}) (factors p)
⊢ Prime q

Tactic:
obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq

Goal state after:
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
r : K[X]
hr : r ∈ factors p
hq : span {r} ∈ Multiset.map (fun q ↦ span {q}) (factors p)
⊢ Prime (span {r})
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ⊔ J ≤ (normalizedFactors I ∩ normalizedFactors J).prod

pp: case a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≤ I ⊔ J

Tactic:
· rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
    constructor <;>
      rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
        normalizedFactors_prod_inter_eq_inter]
    exacts [inf_le_left, inf_le_right]

Goal state after:
case a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≤ I ⊔ 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
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
⊢ span K ↑(M ⊓ N) = ⊤

Tactic:
by
    rw [← range_subtype (M ⊓ N)]
    apply Submodule.span_range_eq_top_of_injective_of_rank_le (M ⊓ N).injective_subtype
    have h := Submodule.rank_sup_add_rank_inf_eq M N
    rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
    rw [Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)]

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

Goal state before:
pp: case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Goal state after:
case neg
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : ↑n ≤ ↑(count J (normalizedFactors I))
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ J ^ n ⊔ I = J ^ multiplicity J I

Tactic:
rw [irreducible_pow_sup hI hJ, min_eq_left]

Goal state after:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ J ^ count J (normalizedFactors I) = J ^ multiplicity J I

T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ count J (normalizedFactors I) ≤ n
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ count J (normalizedFactors I) ≤ n

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Goal state after:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : ↑(count J (normalizedFactors I)) ≤ ↑n
⊢ count J (normalizedFactors I) ≤ n
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ ∃ Q, P ⊔ Q = ⊤ ∧ I = P ^ count P (normalizedFactors I) * Q

Tactic:
use (filter (¬ P = ·) (normalizedFactors I)).prod

Goal state after:
case h
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ P ⊔ (filter (fun x ↦ ¬P = x) (normalizedFactors I)).prod = ⊤ ∧
    I = P ^ count P (normalizedFactors I) * (filter (fun x ↦ ¬P = x) (normalizedFactors I)).prod
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case h.right
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ (filter (fun x ↦ P = x) (normalizedFactors I) + filter (fun a ↦ ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun x ↦ ¬P = x) (normalizedFactors I)).prod

Tactic:
prod_add,

Goal state after:
case h.right
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ (filter (fun x ↦ P = x) (normalizedFactors I)).prod * (filter (fun a ↦ ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun x ↦ ¬P = x) (normalizedFactors I)).prod
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
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₃
u u' : V₃ →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h : u.IsQuasiInverse v
h' : u'.IsQuasiInverse v'
hu : u ≈ u'
⊢ v ∘ₗ u' ∘ₗ v' ≈ v ∘ₗ u ∘ₗ v'

Tactic:
grw [hu]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
let f₃ : (N ⧸ f.range) →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
⊢ (g ∘ₗ f).index = g.index + f.index
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
k : Type u_3
inst✝² : Field k
inst✝¹ : Module k M
inst✝ : Module k N
f : M →ₗ[k] N
t : k
ht : t ≠ 0
⊢ ↑(finrank k ↥(t • f).ker) - ↑(finrank k (N ⧸ (t • f).range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))

Tactic:
ker_smul _ _ ht,

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
k : Type u_3
inst✝² : Field k
inst✝¹ : Module k M
inst✝ : Module k N
f : M →ₗ[k] N
t : k
ht : t ≠ 0
⊢ ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ (t • f).range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • x

Tactic:
rw [← hx, LinearMapClass.map_smul]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s id _⟩

Goal state after: