mathlib-initiative/mathlib-tactics huggingface dataset:
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ˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this :
  emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case mpr.inl
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : i < j
⊢ A i j = 0 ∨ A i j = -1

Tactic:
simpa using

Goal state after:
case mpr.inl
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : i < j
⊢ A i j = 0 ∨ A i j = -1
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
I : Submodule R P
hI : I.FG
⊢ IsFractional S I

Tactic:
by
  rcases hI with ⟨I, rfl⟩
  rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩
  rw [isFractional_span_iff]
  exact ⟨s, hs1, hs⟩

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
I J : FractionalIdeal S P
x : P
hx : x ∈ I * J
⊢ x ∈ ↑I * ↑J

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
hx : x ∈ I * J
⊢ x ∈ ↑I * ↑J
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 ∈
      (mapEquiv
          (let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
          { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }))
        I ↔
    ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Tactic:
mapEquiv_apply,

Goal state after:
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 ∈
      map
        (↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
          { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }))
        I ↔
    ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x
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 ∈
      (mapEquiv
          (let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm)
        I ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x

Tactic:
mapEquiv_apply,

Goal state after:
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 ∈
      map
        (↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm)
        I ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x
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').symm I ↔ x ∈ (canonicalEquiv S P' P) I

Tactic:
by
      rw [mem_canonicalEquiv_apply, canonicalEquiv, mapEquiv_symm, 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_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ y ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ ¬y = 0
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
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
h : 0 = 1
⊢ (algebraMap R₁ K) 1 ∈ 0

Tactic:
simpa using

Goal state after:
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
h : 0 = 1
⊢ (algebraMap R₁ K) 1 ∈ 1
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
⊢ H.toLieSubmodule.incl y ∈ H.toLieSubmodule

Tactic:
exact y.property

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
h : x✝ ∈ ⟨↑I / ↑1, ⋯⟩
⊢ x✝ ∈ I

Tactic:
simpa using

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
h : x✝ ∈ ⟨↑I / ↑1, ⋯⟩
⊢ x✝ ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

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

Tactic:
by_cases hJ0 : J = ⊥

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

case neg
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
⊢ ↑I * (↑I)⁻¹ = 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: 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 ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
this : x ∈ integralClosure A K
⊢ x ∈ 1

Tactic:
by
    rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
      ← mem_one_iff] at this

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✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
this : I / J * J ≤ I
⊢ I / J ≤ I * J⁻¹

Tactic:
simpa using

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✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
this : I / J * J ≤ I
⊢ I / J ≤ I * J⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
⊢ M = ⊤

Tactic:
have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
⊢ M = ⊤
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I : ∀ β_lin ∈ q, β_lin ≠ 0 → genWeightSpace L ⇑β_lin ≤ I
h_plus_contain : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ≤ I
this : -Weight.toLinear K (↥H) L α = -1 • Weight.toLinear K (↥H) L α
⊢ Weight.toLinear K (↥H) L χ + -1 • Weight.toLinear K (↥H) L α ∈ q

Tactic:
exact q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
y : P
h : spanSingleton S y = 0
⊢ R ∙ y = ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
y : P
h : spanSingleton S y = 0
⊢ y = 0
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 : FractionalIdeal A⁰ K✝
hJK : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ (fun x1 x2 ↦ x1 ≤ x2) J K

Tactic:
simpa using

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 : FractionalIdeal A⁰ K✝
hJK : (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✝
I : { x // 0 < x }
J K : FractionalIdeal A⁰ K✝
hJK : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) I J) ((fun x y ↦ y * ↑x) I K)
⊢ (fun x1 x2 ↦ x1 ≤ x2) J K

Tactic:
simpa using

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 : FractionalIdeal A⁰ K✝
hJK : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) I J) ((fun x y ↦ y * ↑x) 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✝
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)
⊢ 0 < ↑↑I

Tactic:
simpa using

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)
⊢ ¬↑I = ⊥
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
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Tactic:
let P := factors I
  have prime_of_mem := fun p (hp : p ∈ P.toFinset) =>
    prime_of_factor p (Multiset.mem_toFinset.mp hp)
  apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _
  · convert! hM
    rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_pow_eq_prod_of_prime,
      ← Finset.prod_multiset_count, ← associated_iff_eq]
    · exact factors_prod hI
    · exact prime_of_mem
    · exact fun _ _ _ _ ij => ij
  · intro p hp q hq pq
    rw [Ideal.irreducible_pow_sup]
    · suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
      rw [Multiset.count_eq_zero,
        normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
        Multiset.mem_replicate]
      exact fun H => pq <| H.2.trans <| normalize_eq q
    · rw [← Ideal.zero_eq_bot]; apply pow_ne_zero; exact (prime_of_mem q hq).ne_zero
    · exact (prime_of_mem p hp).irreducible

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

Goal state before:
pp: case refine_1
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'
s : S
m : M₁
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁))))
        s)
      m =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
            ↑R (LinearMap.baseChange S f)))
        s)
      m

Tactic:
simpa using

Goal state after:
case refine_1
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'
s : S
m : M₁
⊢ s • f' (h₁ m) = s • h₂ (f m)
Module: Mathlib.RingTheory.Flat.IsBaseChange

Goal state before:
pp: case refine_2
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'
s : S
m : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑R g' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂))))
        s)
      m =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)) ∘ₗ
            ↑R (LinearMap.baseChange S g)))
        s)
      m

Tactic:
simpa using

Goal state after:
case refine_2
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'
s : S
m : M₂
⊢ s • g' (h₂ m) = s • h₃ (g m)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J

Tactic:
simpa using

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ I ≤ P ∨ J ≤ P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ span {a} ≠ ⊥

Tactic:
simpa using

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ ¬a = 0
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
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I⁻¹ ≤ J ↔ J⁻¹ ≤ I

Tactic:
simpa using

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
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I⁻¹ ≤ J ↔ J⁻¹ ≤ I
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 * ⨅ b, bif b then J else K) = I * J ⊓ I * K

Tactic:
mul_iInf,

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J K : Ideal A
⊢ (⨅ i, I * bif i then J else K) = I * J ⊓ I * K