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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) ⁅x, y⁆ =
    ⁅x, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) y⁆ -
      ⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) x⁆

Tactic:
by
      have hM (k : ι) (b : ⨁ i, ℒ i) (hb : (decompose ℒ).symm b ∈ ℒ k) :
          (toModule R ι (⨁ (i : ι), ℒ i) fun i ↦ lof R ι (ℒ ·) i ∘ₗ (φ i • .id)) b = (φ k) • b := by
        obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]
        simp
      ext j
      induction x using DirectSum.induction_on' with
      | h0 => simp
      | hadd i a f _ _ ih =>
        simp only [Module.End.smulLeft_eq, DirectSum.sub_apply, AddSubgroupClass.coe_sub] at ih
        simp only [Module.End.smulLeft_eq, add_lie, map_add, DirectSum.add_apply, Submodule.coe_add,
          ih, lie_add, DirectSum.sub_apply, AddSubgroupClass.coe_sub]
        rw [add_sub_add_comm, add_right_cancel_iff, hM i (of (ℒ ·) i a) (by simp)]
        clear ih
        induction y using DirectSum.induction_on' with
        | h0 => simp
        | hadd k b f _ _ ih =>
          simp only [lie_add, map_add, DirectSum.add_apply, Submodule.coe_add, ih, lie_smul,
            add_lie, smul_add, add_sub, ← sub_sub]
          congr 1
          have : (decompose ℒ).symm ⁅of (fun i ↦ ℒ i) i a, of (fun i ↦ ℒ i) k b⁆ ∈ ℒ (i + k) := by
            simp [SetLike.GradedBracket.bracket_mem (Submodule.coe_mem a) (Submodule.coe_mem b)]
          rw [hM _ _ this, hM k (of (ℒ ·) k b) (by simp), ← lie_skew (of (ℒ ·) k b),
            add_sub_right_comm, add_right_cancel_iff, add_comm i k, map_add, add_smul,
            DirectSum.add_apply, Submodule.coe_add, sub_eq_add_neg, lie_smul, add_left_cancel_iff,
            smul_neg, ← sub_eq_zero, sub_neg_eq_add, ← Submodule.coe_add, Submodule.coe_eq_zero,
            ← DirectSum.add_apply, add_neg_cancel, DirectSum.zero_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l'

Tactic:
rw [disjoint_iff_eq_or_eq, List.Disjoint]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x).support

Tactic:
hn'

Goal state after:
case neg.succ.succ.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ (p.cycleOf x).support ⊆ (p.cycleOf x).support
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
⊢ ∀ (h₂ : n < ((p.toList x).rotate k).length), (p.toList ((p ^ k) x))[n] = ((p.toList x).rotate k)[n]

Tactic:
hn'

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.toList ((p ^ k) x))[n] = ((p.toList x).rotate k)[n]
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
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Tactic:
toList,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) (l.formPerm.cycleOf (l.get ⟨0, ⋯⟩)).support.card = l
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩)

Tactic:
projection_apply,

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅↑(((k ∙ z).projectionOnto ↑A ⋯) x), v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A

Tactic:
intros
    exact hAL <| LieSubmodule.lie_mem_lie (LieSubmodule.mem_top _) (LieSubmodule.mem_top _)

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

Goal state before:
pp: case h.refine_1
k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv : v ∈ weightSpace V ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ v ∈ weightSpace V ⇑(χ ∘ₗ toEndo)

Tactic:
rw [mem_weightSpace] at hv ⊢
    intro x
    apply hv (toEndo x)

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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ (rootSystem H).root α ∈
    ↑(Submodule.comap (↑((rootSystem H).reflection β)) (Submodule.span K (⇑(rootSystem H).root '' I.rootSet)))

Tactic:
rw [SetLike.mem_coe, Submodule.mem_comap, LinearEquiv.coe_coe, ← RootPairing.root_reflectionPerm]

Goal state after:
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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ (rootSystem H).root (((rootSystem H).reflectionPerm β) α) ∈ Submodule.span K (⇑(rootSystem H).root '' I.rootSet)
Module: Mathlib.RingTheory.FractionalIdeal.Basic

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
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ J ≤ 1

Tactic:
← hI

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
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ ↑I ≤ 1
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: 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⁻¹

Tactic:
rw [mul_comm, ← den_mul_self_eq_num']

Goal state after:
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
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) ↑I.den) * I ≤ I⁻¹ * I
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
⊢ canonicalEquiv S P P = (canonicalEquiv S P P).symm

Tactic:
exact (canonicalEquiv_symm S P P).symm

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

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
inst✝¹ : Algebra A K✝
inst✝ : IsFractionRing A K✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ J ≤ K

Tactic:
← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A),

Goal state after:
R : Type u_1
A : Type u_2
K✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K✝
inst✝ : IsFractionRing A K✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ ↑J ≤ ↑K
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

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
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J

Tactic:
rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ ∀ ⦃x : A⦄, x ∈ J → x ∈ P
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
⊢ ∀ ⦃y : Ideal R⦄,
    y ∈ ↑(factors I).toFinset → p ≠ y → (fun i j ↦ i ^ Multiset.count i P ⊔ j ^ Multiset.count j P = ⊤) p y

Tactic:
q

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
⊢ q ∈ ↑(factors I).toFinset → p ≠ q → (fun i j ↦ i ^ Multiset.count i P ⊔ j ^ Multiset.count j P = ⊤) p q
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: 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
⊢ ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J

Tactic:
suffices ↑J / I < I⁻¹ by
    obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
    rw [mem_inv_iff hI0] at hI
    refine ⟨a, fun i hi => ?_, ?_⟩
    -- By definition, `a ∈ I⁻¹` multiplies elements of `I` into elements of `1`,
    -- in other words, `a * f i` is an integer.
    · exact (mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))
    · contrapose! hpI
      -- And if all `a`-multiples of `I` are an element of `J`,
      -- then `a` is actually an element of `J / I`, contradiction.
      refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
      · rintro _ ⟨i, hi, rfl⟩; exact hpI i hi
      · rw [mul_zero]; exact Submodule.zero_mem _
      · intro x y _ _ hx hy; rw [mul_add]; exact Submodule.add_mem _ hx hy
      · intro b x _ hx; rw [mul_smul_comm]; exact Submodule.smul_mem _ b hx

Goal state after:
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
⊢ ↑J / I < I⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
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 : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K) r' = r • x
⊢ (algebraMap S L) (f r') = f r • ↑(semilinearEquivOfRingEquiv K L f) x

Tactic:
simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
    EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]

Goal state after:
case h
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 : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K) r' = r • x
⊢ (algebraMap S L) (f r') = f r • (IsFractionRing.ringEquivOfRingEquiv f) x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J K : Ideal A
⊢ (I ⊓ J) * K = I * K ⊓ J * K

Tactic:
by
  simp only [mul_inf, mul_comm _ K]

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

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ ((smulAddMonoidHom A M) (((mulHom A) ((of A ai) ax)) ((of A bi) bx))) ((of M ci) cx) =
    (of M (ai +ᵥ bi +ᵥ ci)) (GSMul.smul ax (GSMul.smul bx cx))

Tactic:
DirectSum.mulHom_of_of,

Goal state after:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ ((smulAddMonoidHom A M) ((of A (ai + bi)) (GMul.mul ax bx))) ((of M ci) cx) =
    (of M (ai +ᵥ bi +ᵥ ci)) (GSMul.smul ax (GSMul.smul bx cx))
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J

Tactic:
rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J
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
    exact_mod_cast hn

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

Goal state before:

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

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

Goal state before:
pp: case mp.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
hx : (linearCombination R Subtype.val) x = 0
⊢ f (b.repr.symm (mapDomain σ x)) = x

Tactic:
simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
      rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]

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
a b : R
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
by_cases h : FiniteMultiplicity a b
  · rw [h.emultiplicity_eq_multiplicity]
    apply emultiplicity_eq_of_dvd_of_not_dvd <;>
      rw [span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
    · exact pow_multiplicity_dvd a b
    · apply h.not_pow_dvd_of_multiplicity_lt
      apply lt_add_one
  · suffices ¬FiniteMultiplicity (span ({a} : Set R)) (span ({b} : Set R)) by
      rw [emultiplicity_eq_top.2 h, emultiplicity_eq_top.2 this]
    exact FiniteMultiplicity.not_iff_forall.mpr fun n => by
      rw [span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
      exact FiniteMultiplicity.not_iff_forall.mp h n

Goal state after:
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)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R), D (p * q) = p • D q + q • D p

Tactic:
q

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
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)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p q : MvPolynomial σ R
⊢ D (p * q) = p • D q + q • D p
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case C
σ : 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)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p : MvPolynomial σ R
c : R
⊢ D (c • p) = 0 + C c • D p

Tactic:
zero_add,

Goal state after:
case C
σ : 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)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p : MvPolynomial σ R
c : R
⊢ D (c • p) = C c • D p
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case mul_X
σ : 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)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p q : MvPolynomial σ R
i : σ
hq : D (p * q) = p • D q + q • D p
⊢ D (p * (q * X i)) = p • D (q * X i) + (q * X i) • D p

Tactic:
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
    rw [smul_comm (X i), smul_comm (X i)]

Goal state after: