mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

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
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
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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Irreducible ↑(d ⟨p, ⋯⟩)

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Irreducible ↑(d ⟨p, ⋯⟩)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case 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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬p = 1

Tactic:
]

Goal state after:
case 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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬p = 1
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this⟩
⊢ b = ⊥

Tactic:
]

Goal state after:
case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this⟩
⊢ b = ⊥
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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : ⊥ = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ b = ⊥

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : ⊥ = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ b = ⊥
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ a = ⊥

pp: case refine_2.hbot
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⊥ ∈ Set.Iic m

Tactic:
]

Goal state after:
case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ a = ⊥

case refine_2.hbot
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⊥ ∈ Set.Iic m
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
hb : 0 ∈ ↑span_compl_roots
hbI : ↑0 ∈ I
ha : ⟨x, hxH⟩ ∈ ↑span_I_roots
haI : ↑⟨x, hxH⟩ ∈ I
⊢ x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α

Tactic:
exact hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha

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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ q ∈ normalizedFactors n

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ q ∈ normalizedFactors n
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ multiplicity p m ∣ n

Tactic:
]

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ multiplicity p m ∣ n
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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑⟨p, ⋯⟩) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity (↑⟨p, ⋯⟩) m
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n ≤ emultiplicity p m
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:
]

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ˣ
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
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:
]

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ˣ
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
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 : Prime ↑(d ⟨p, ⋯⟩)
q : N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ q ∈ normalizedFactors n

Tactic:
]

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 : Prime ↑(d ⟨p, ⋯⟩)
q : N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ q ∈ normalizedFactors n
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'
⊢ Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩, ⋯⟩)

Tactic:
]

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ˣ
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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ Prime ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)

Tactic:
]

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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ Prime ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ (b a : ι), a ≠ b → Aᵀ a b = 0 ∨ Aᵀ a b = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1

Tactic:
]

Goal state after:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ (b a : ι), a ≠ b → Aᵀ a b = 0 ∨ Aᵀ a b = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1
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'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)

Tactic:
]

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'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 6⦄, j < i → E₆ i j = 0 ∨ E₆ i j = -1

Tactic:
]

Goal state after:
⊢ ∀ ⦃i j : Fin 6⦄, j < i → E₆ i j = 0 ∨ E₆ i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 7⦄, j < i → E₇ i j = 0 ∨ E₇ i j = -1

Tactic:
]

Goal state after:
⊢ ∀ ⦃i j : Fin 7⦄, j < i → E₇ i j = 0 ∨ E₇ i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1

Tactic:
]

Goal state after:
⊢ ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1
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
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * J = 1

Tactic:
]

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
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * J = 1
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
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ 1 / map (↑h) I = 1 / map (↑h) I

Tactic:
]

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ˣ
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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)) (Associates.mk n)

Tactic:
]

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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
⊢ emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)) (Associates.mk n)
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
x y : K
⊢ spanSingleton R₁⁰ (x * y⁻¹) = spanSingleton R₁⁰ (x * y⁻¹)

Tactic:
]

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
x : K
hx : x ≠ 0
⊢ 1 = 1

Tactic:
]

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
x : R₁
hx : x ≠ 0
⊢ 1 = 1

Tactic:
]

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ˣ
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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
q : Associates M
hq : q ∈ normalizedFactors (Associates.mk m)
hq' : Associated (Associates.mk p) q
⊢ q ∈ normalizedFactors (Associates.mk m)

Tactic:
]

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 :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
q : Associates M
hq : q ∈ normalizedFactors (Associates.mk m)
hq' : Associated (Associates.mk p) q
⊢ q ∈ normalizedFactors (Associates.mk m)