mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩

Tactic:
let ih' := ih h2

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) ↑⟨y, h2⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ ↑((decomposeTensorEquiv ℳ N i) x) = (rTensor N (ℳ i).subtype) x

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ l.attach.formPerm.cycleType = {l.length}

Tactic:
by
  rw [← length_attach] at hn
  rw [← nodup_attach] at hl
  rw [cycleType_eq [l.attach.formPerm]]
  · simp only [map, Function.comp_apply]
    rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
    · simp
    · intro x h
      simp [h] at hn
  · simp
  · simpa using isCycle_formPerm hl hn
  · simp

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

Goal state before:
pp: case inl.inl
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
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Subsingleton L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

pp: case inl.inr
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
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
· use 0
      simpa [trivial_lie_zero, mem_weightSpace, nontrivial_iff] using exists_pair_ne V

Goal state after:
case inl.inr
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
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i : Fin n
⊢ C n i i = 2

Tactic:
simp [C, Matrix.of_apply]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
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
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
h : ∃ i_1 ≤ ↑i, Associated (c j) (c 1 ^ i_1)
⊢ c j ∈ Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ

pp: case refine_1
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
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)

Tactic:
· rcases h with ⟨u, hu, hu'⟩
      refine Finset.mem_image.mpr ⟨⟨u, Nat.lt_succ_of_le hu⟩, Finset.mem_univ _, ?_⟩
      rwa [associated_iff_eq, eq_comm] at hu'

Goal state after:
case refine_1
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
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg.refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ c₂ t < c₂ u

Tactic:
rw [c₂_def, c₂_def, Subtype.coe_lt_coe, d.lt_iff_lt, Subtype.mk_lt_mk, hc₁'.lt_iff_lt]

Goal state after:
case neg.refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ t < u
Module: Mathlib.Algebra.Lie.Weights.IsSimple

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

Tactic:
subst hab

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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
hb : 0 ∈ ↑span_compl_roots
hbI : ↑0 ∈ I
ha : ⟨x, hxH⟩ ∈ ↑span_I_roots
haI : ↑⟨x, hxH⟩ ∈ I
⊢ x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : Subsingleton Mˣ
inst✝ : Subsingleton Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
x : Associates M
hx : x ∈ Set.Iic (Associates.mk m)
⊢ x ≤ Associates.mk m

Tactic:
exact hx

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : Subsingleton Mˣ
inst✝ : Subsingleton Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
x : Associates N
hx : x ∈ Set.Iic (Associates.mk n)
⊢ x ≤ Associates.mk n

Tactic:
exact hx

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
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ (↑I⁻¹).IsPrincipal

Tactic:
rw [val_eq_coe, isPrincipal_iff]
  use (generator (I : Submodule R₁ K))⁻¹
  have hI : I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 :=
    mul_generator_self_inv _ I h
  exact (right_inverse_eq _ I (spanSingleton _ (generator (I : Submodule R₁ K))⁻¹) hI).symm

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ x ∈ (canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Tactic:
by
  rw [canonicalEquiv, mapEquiv_apply, mem_map]
  exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

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

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ aJ • y = 0

Tactic:
← hy',

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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ (algebraMap R₁ K) y' = 0
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 J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * aJ • y)

Tactic:
← hy',

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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * (algebraMap R₁ K) y')
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₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
by
  by_cases H : J = 0
  · rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
  · 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: case mp.refine_2
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_1 y : P), (∃ y' ∈ I, x_1 = x * y') → (∃ y' ∈ I, y = x * y') → ∃ y' ∈ I, x_1 + y = x * y'

Tactic:
rintro _ _ ⟨y, hy, rfl⟩ ⟨y', hy', rfl⟩
      exact ⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).symm⟩

Goal state after:
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 < normalizedFactors (P ^ (i + 1))
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I

Tactic:
normalizedFactors_pow,

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I < (i + 1) • normalizedFactors P
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
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 ≤ normalizedFactors (P ^ i)

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:
normalizedFactors_pow,

Goal state after:
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 ≤ i • normalizedFactors P

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

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
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
⊢ Associates.mk I ^ n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n

Tactic:
by
  simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
    Ideal.dvd_span_singleton]

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
r s : ⨁ (i : ιA), A i
x : ⨁ (i : ιB), M i
⊢ (r + s) • x = r • x + s • x

Tactic:
simp only [smul_def, map_add, AddMonoidHom.add_apply]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S ⊓ T).CoFG

Tactic:
← Submodule.ker_mkQ S,

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S.mkQ.ker ⊓ T).CoFG
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✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V₂
inst✝² : Module K V₂
inst✝¹ : AddCommMonoid V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
h : u.HasNoetherianRange
v : V₂ →ₗ[K] V₃
⊢ (v ∘ₗ u).HasNoetherianRange

Tactic:
by
  rw [LinearMap.HasNoetherianRange, LinearMap.range_comp] at *
  infer_instance

Goal state after:
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₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian K (V ⧸ A)
eqOn_A : Set.EqOn ⇑u ⇑v ↑A
A_le : A ≤ u.eqLocus v
⊢ IsNoetherian K (V ⧸ u.eqLocus v)

Tactic:
refine isNoetherian_of_surjective (A.mapQ (eqLocus u v) id A_le) (by simp [range_mapQ])

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
⊢ ↑(finrank k ↥(-f).ker) - ↑(finrank k (N ⧸ (-f).range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))

Tactic:
ker_neg,

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
⊢ ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ (-f).range)) = ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range))
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)
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
have aux : f.range ≤ comap g (g ∘ₗ f).range := by rw [← map_le_iff_le_comap, range_comp]

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
⊢ (g ∘ₗ f).index = g.index + f.index
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: 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✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : (↥s →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
⊢ Submodule.map f.range.mkQ l.ker = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
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✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : (↥s →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
⊢ ⊤ ≤ Submodule.map f.range.mkQ l.ker
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: 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
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
y : ↥S := commonDenomOfFinset S f s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
have hx₁ : y • (s : Set M') = f '' _ :=
    (IsLocalizedModule.finsetIntegerMultiple_image S f s).symm

Goal state after:
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
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
y : ↥S := commonDenomOfFinset S f s
hx₁ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {b} ≠ 0

pp: case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ Prime (span {a})

Tactic:
· by_contra h
      exact hb (span_singleton_eq_bot.mp h)

Goal state after:
case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ Prime (span {a})