mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m) x = y) → p.SameCycle x y ∧ x ∈ p.support

Tactic:
rintro ⟨n, hx, rfl⟩

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ p.SameCycle x ((p ^ n) x) ∧ x ∈ p.support
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ ∑ k ∈ Finset.range n with ↑i < k, f k = ∑ k ∈ Finset.range n, if ↑i < k then f k else 0

Tactic:
Finset.sum_filter

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ (∑ a ∈ Finset.range n, if ↑i < a then f a else 0) = ∑ k ∈ Finset.range n, if ↑i < k then f k else 0
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
⊢ I.rootSpan ≤ Submodule.comap (↑((rootSystem H).reflection β)) I.rootSpan

Tactic:
rootSpan,

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
⊢ Submodule.span K (⇑(rootSystem H).root '' I.rootSet) ≤
    Submodule.comap (↑((rootSystem H).reflection β)) (Submodule.span K (⇑(rootSystem H).root '' I.rootSet))
Module: Mathlib.RingTheory.FractionalIdeal.Basic

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ ↑I = ⊥

Tactic:
eq_bot_iff

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ ↑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
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
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
h_sum : ↑a + ↑b = x
h_b_eq : ↑b = x - ↑a
⊢ x - ↑a ∈ I

Tactic:
exact I.toSubmodule.sub_mem hxI haI

Goal state after:
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 ≠ ⊥
w✝ : Ideal A
hPZ' : w✝ ∈ Multiset.map asIdeal Z
hPM : w✝ ≤ M
⊢ ∃ Z, (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨P, hPZ, rfl⟩ := Multiset.mem_map.mp hPZ'

Goal state after:
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
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsIntegrallyClosed A

Tactic:
by
  let := h.commGroupWithZero (FractionRing A)
  -- It suffices to show that for integral `x`,
  -- `A[x]` (which is a fractional ideal) is in fact equal to `A`.
  refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)
  rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]
  · exact mem_adjoinIntegral_self A⁰ x hx
  · exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ p = under R P ↔ P ∣ map (algebraMap R A) p

Tactic:
dvd_iff_le,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ p = under R P ↔ map (algebraMap R A) p ≤ P
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_1 ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y_1 = y

Tactic:
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h

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
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y = z • (IsLocalization.map P' (RingHom.id R) ⋯) x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

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

Tactic:
Algebra.smul_mul_assoc

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ a • (x * y') = a • (x * y')
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
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors ?m.252) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤

Tactic:
by rw [this, zero_min, pow_zero, Ideal.one_eq_top]

Goal state after:
Module: Mathlib.RingTheory.Flat.IsBaseChange

Goal state before:
pp: case refine_4
R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
isb₃ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)))
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
⊢ Function.Injective ⇑(↑R (LinearMap.baseChange S f))

Tactic:
· exact Module.Flat.lTensor_preserves_injective_linearMap f inj₁

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

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]

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
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • x * zI ∈ J

Tactic:
Algebra.smul_mul_assoc

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
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J
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✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ IsNoetherian R₁ ↥↑↑I

Tactic:
isNoetherian_iff

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ J ≤ ↑I, (↑J).FG
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₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)

Tactic:
isNoetherian_iff

Goal state after:
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₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
⊢ ∀ J ≤ spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I, (↑J).FG
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)
⊢ gcd I J ∣ I ⊔ J

Tactic:
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)
⊢ I ⊔ J ≤ gcd I J
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)
⊢ I ⊔ J ∣ I ∧ I ⊔ J ∣ J

Tactic:
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)
⊢ I ≤ I ⊔ J ∧ I ⊔ J ∣ J
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 ∣ I ⊓ J ∧ J ∣ I ⊓ J

Tactic:
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 ⊓ J ≤ I ∧ J ∣ I ⊓ J
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:
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
⊢ lcm I J ≤ I ⊓ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

Tactic:
dvd_iff_le,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ≤ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ↔ L ∣ M
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ≤ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ↔ L ∣ M

Tactic:
dvd_iff_le,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ≤ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ↔ M ≤ L
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J

Tactic:
by
  have hI : I ≠ ⊥ := by
    intro hI
    rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
    exact Finset.notMem_empty _ hL
  refine mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
  rintro ⟨l, hl⟩ ⟨l', hl'⟩
  rw [Subtype.coe_mk, Subtype.coe_mk]
  apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f

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

Goal state before:
pp: case hlt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a a₀ x : R
n : ℕ
hx : Prime x
ha : ¬x ∣ a
heq : a₀ = x ^ n * a
hx0 : x ≠ 0
⊢ ¬span {x} ^ (n + 1) ∣ span {a₀}

Tactic:
simp only [span_singleton_pow, heq, dvd_span_singleton, mem_span_singleton]
    rw [pow_add, pow_one, mul_dvd_mul_iff_left (pow_ne_zero n hx0)]
    exact ha

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

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

Tactic:
rw [LinearMap.exact_iff] at this

Goal state after:
R : Type u_2
M : Type u_3
N : Type ?u.13
N' : Type ?u.18
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
S : Submonoid R
f✝ : N →ₗ[R] N'
inst✝³ : IsLocalizedModule S f✝
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FinitePresentation R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst : Module.FinitePresentation A (A ⊗[R] (Fin n → R))
this : (LinearMap.baseChange A f).ker = (LinearMap.baseChange A f.ker.subtype).range
⊢ (LinearMap.baseChange A f).ker.FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (p.primesOver B).Finite

Tactic:
hpb

Goal state after:
case pos
A : Type u_4
inst✝⁶ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁵ : CommRing B
inst✝⁴ : IsDedekindDomain B
inst✝³ : Algebra A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite
Module: Mathlib.Algebra.Module.PID

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

Tactic:
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha

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

Goal state before:
pp: R : Type u_5
N : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
S : Type u_3
ι : Type u_4
inst✝² : Finite ι
inst✝¹ : CommRing S
inst✝ : Algebra R S
this : Fintype ι
e₁ : S ⊗[R] (ι → R) ≃ₗ[S] ι → S ⊗[R] R := piRight R S S fun x ↦ R
⊢ IsBaseChange S (baseChangeHom R S (ι → R) N)

Tactic:
let e₂ := (LinearEquiv.piCongrRight (fun _ ↦ (LinearMap.ringLmapEquivSelf S S _).symm ≪≫ₗ
    (LinearEquiv.congrLeft (S ⊗[R] N) S (AlgebraTensorModule.rid R S S).symm))) ≪≫ₗ
    (LinearMap.lsum S (fun _ : ι ↦ _) S) ≪≫ₗ (e₁.symm.congrLeft (S ⊗[R] N) S)

Goal state after:
R : Type u_5
N : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
S : Type u_3
ι : Type u_4
inst✝² : Finite ι
inst✝¹ : CommRing S
inst✝ : Algebra R S
this : Fintype ι
e₁ : S ⊗[R] (ι → R) ≃ₗ[S] ι → S ⊗[R] R := piRight R S S fun x ↦ R
e₂ : (ι → S ⊗[R] N) ≃ₗ[S] S ⊗[R] (ι → R) →ₗ[S] S ⊗[R] N :=
  (LinearEquiv.piCongrRight fun x ↦
        (ringLmapEquivSelf S S (S ⊗[R] N)).symm ≪≫ₗ
          LinearEquiv.congrLeft (S ⊗[R] N) S (AlgebraTensorModule.rid R S S).symm) ≪≫ₗ
      LinearMap.lsum S (fun x ↦ S ⊗[R] R) S ≪≫ₗ
    LinearEquiv.congrLeft (S ⊗[R] N) S e₁.symm
⊢ IsBaseChange S (baseChangeHom R S (ι → R) N)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (r • x).val = r • x.val

Tactic:
rw [val_smul''', ← sub_eq_zero, ← sub_smul]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (P.σ ((algebraMap P.Ring S) r) - r) • x.val = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ Function.Surjective ⇑(Q.ofComp P).toAlgHom

Tactic:
intro p
  induction p using MvPolynomial.induction_on with
  | C a =>
      use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp
  | add p q hp hq =>
      obtain ⟨p, rfl⟩ := hp
      obtain ⟨q, rfl⟩ := hq
      use p + q
      simp
  | mul_X p i hp =>
      obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
      use p * MvPolynomial.X (R := R) (Sum.inl i)
      simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]

Goal state after: