mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 7
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

pp: case «1»
j : Fin 7
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

pp: case «2»
j : Fin 7
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

pp: case «3»
j : Fin 7
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

pp: case «4»
j : Fin 7
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

pp: case «5»
j : Fin 7
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

pp: case «6»
j : Fin 7
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0

Tactic:
<;>

Goal state after:
case «0»
j : Fin 7
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 7
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 7
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 7
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 7
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 7
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

case «6»
j : Fin 7
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 8
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

pp: case «1»
j : Fin 8
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

pp: case «2»
j : Fin 8
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

pp: case «3»
j : Fin 8
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

pp: case «4»
j : Fin 8
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

pp: case «5»
j : Fin 8
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

pp: case «6»
j : Fin 8
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0

pp: case «7»
j : Fin 8
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) j ≤ 0

Tactic:
<;>

Goal state after:
case «0»
j : Fin 8
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 8
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 8
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 8
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 8
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 8
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

case «6»
j : Fin 8
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0

case «7»
j : Fin 8
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) j ≤ 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ ↑(Nat.unaryCast 0) = ↑0

pp: case succ
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
n✝ : ℕ
a✝ : ↑n✝.unaryCast = ↑n✝
⊢ ↑(n✝ + 1).unaryCast = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ ↑(Nat.unaryCast 0) = ↑0

case succ
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
n✝ : ℕ
a✝ : ↑n✝.unaryCast = ↑n✝
⊢ ↑(n✝ + 1).unaryCast = ↑(n✝ + 1)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 4
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

pp: case «1»
j : Fin 4
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

pp: case «2»
j : Fin 4
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

pp: case «3»
j : Fin 4
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

Tactic:
<;>

Goal state after:
case «0»
j : Fin 4
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 4
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 4
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 4
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

pp: case «1»
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

Tactic:
<;>

Goal state after:
case «0»
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

pp: case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

pp: case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

pp: case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
<;>

Goal state after:
case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case e'_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = I * I * I⁻¹

pp: case e'_3
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ 1 = I * I⁻¹

Tactic:
<;>

Goal state after:
case e'_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = I * I * I⁻¹

case e'_3
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ 1 = I * I⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case a
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
| I

pp: case a
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
| spanSingleton R₁⁰ (generator ↑I)⁻¹

Tactic:
rw [eq_spanSingleton_of_principal I]

Goal state after:
case a
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
| spanSingleton R₁⁰ (generator ↑I)

case a
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
| spanSingleton R₁⁰ (generator ↑I)⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case mpr
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
hg : generator ↑I ≠ 0
⊢ I ≠ 0

Tactic:
rw [eq_spanSingleton_of_principal I]

Goal state after:
case mpr
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
hg : generator ↑I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) ≠ 0
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]

Goal state after:
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ ∃ x, I⁻¹ = spanSingleton R₁⁰ x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr.refine_1
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑I ≠ 0

pp: case inr.refine_2
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑M ≠ 0

pp: case inr.refine_3
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑I ≤ ↑M

Tactic:
<;>

Goal state after:
case inr.refine_1
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑I ≠ 0

case inr.refine_2
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑M ≠ 0

case inr.refine_3
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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ↑I ≤ ↑M
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)

Tactic:
hI_nz,

Goal state after:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ 0 ≤ 0 * (1 / 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 J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J

Tactic:
rw [div_of_ne_zero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]
  exact Submodule.le_div_iff_mul_le

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

Goal state before:
pp: case mp
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩ → x✝ ∈ I

pp: case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ I → x✝ ∈ ⟨↑I / ↑1, ⋯⟩

Tactic:
<;>

Goal state after:
case mp
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩ → x✝ ∈ I

case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ I → x✝ ∈ ⟨↑I / ↑1, ⋯⟩
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case pos
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
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
⊢ 0 = map (↑h) I / 0

Tactic:
div_zero

Goal state after:
case pos
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
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
⊢ 0 = 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
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'
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x) → y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

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'
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x) → y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
<;>

Goal state after:
case mp
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'
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x) → y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

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'
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x) → y ∈ (canonicalEquiv S P P') (spanSingleton S x)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
⊢ I ∣ J

Tactic:
have hI' : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI

Goal state after:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ I ∣ 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✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Tactic:
by
  classical
  exact if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one_right _ _ (by simp [h])).symm

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

Goal state before:
pp: 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
hr : ∀ b ∈ I, IsInteger R (r • b)
⊢ ¬f r = 0

Tactic:
by simp [hr0]

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

Goal state before:
pp: case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
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 J : FractionalIdeal R⁰ K
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (↑I * ↑J) ≤
    Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J

pp: case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
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 J : FractionalIdeal R⁰ K
⊢ Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J ≤
    Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (↑I * ↑J)

Tactic:
<;>

Goal state after:
case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
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 J : FractionalIdeal R⁰ K
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (↑I * ↑J) ≤
    Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J

case a
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
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₁
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 J : FractionalIdeal R⁰ K
⊢ Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I * Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑J ≤
    Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (↑I * ↑J)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case a.left
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

pp: case a.right
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 ∣ J

Tactic:
<;>

Goal state after:
case a.left
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

case a.right
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 ∣ J
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : CommRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S T : Submodule K V
hST : IsCompl S T
⊢ S.projection T hST ≈ 0 ↔ IsNoetherian K ↥S

Tactic:
rw [equiv_zero_iff_hasNoetherianRange, hasNoetherianRange_iff_range, range_projection]

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

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
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : ⟨X, hX⟩ ≤ ⟨Y, hY⟩
⊢ (fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨X, hX⟩ ≤
    (fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨Y, hY⟩

Tactic:
← Subtype.coe_le_coe,

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
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : ↑⟨X, hX⟩ ≤ ↑⟨Y, hY⟩
⊢ ↑((fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨X, hX⟩) ≤
    ↑((fun X ↦ ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨Y, hY⟩)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: 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
⊢ (Associates.mk (span {x})).count (Associates.mk (span {a₀})).factors = n

Tactic:
count_associates_factors_eq,

Goal state after:
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
⊢ Multiset.count (span {x}) (normalizedFactors (span {a₀})) = n

case hI
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 {a₀} ≠ 0

case hJ
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}).IsPrime

case hJ₀
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} ≠ ⊥
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hnorm
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
⊢ normalize (span {x}) = span {x}

Tactic:
exact normalize_eq _

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

Goal state before:
pp: case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ span {a} ^ multiplicity a b ∣ span {b}

pp: case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬span {a} ^ (multiplicity a b + 1) ∣ span {b}

Tactic:
<;>

Goal state after:
case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ span {a} ^ multiplicity a b ∣ span {b}

case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬span {a} ^ (multiplicity a b + 1) ∣ span {b}