mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Tactic:
·

Goal state after:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2

pp: case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0

Tactic:
·

Goal state after:
case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0

Tactic:
·

Goal state after:
case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y

pp: case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| < ↑n

Tactic:
·

Goal state after:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e (0 x) = 0 x

pp: case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)

Tactic:
LinearMap.zero_apply,

Goal state after:
case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e 0 = 0 x

case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e 0 = 0 x

pp: case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)

Tactic:
LinearMap.zero_apply,

Goal state after:
case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e 0 = 0

case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

pp: case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
·

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
·

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : n ≤ k
⊢ (algebraMap B (B ⧸ Q)) (f.coeff (n + j)) = q.coeff n

pp: case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : ¬n ≤ k
⊢ (algebraMap B (B ⧸ Q)) 0 = q.coeff n

Tactic:
·

Goal state after:
case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : n ≤ k
⊢ (algebraMap B (B ⧸ Q)) (f.coeff (n + j)) = q.coeff n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : a.val ≤ n / 2
⊢ ↑(↑a.val).natAbs = a

pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(↑a.val - ↑n).natAbs = -a

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : a.val ≤ n / 2
⊢ ↑(↑a.val).natAbs = a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(↑a.val - ↑n).natAbs = -a

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(↑a.val - ↑n).natAbs = -a
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : ¬n ≤ k
⊢ (algebraMap B (B ⧸ Q)) 0 = q.coeff n

Tactic:
·

Goal state after:
case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : ¬n ≤ k
⊢ (algebraMap B (B ⧸ Q)) 0 = q.coeff n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

pp: case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
·

Goal state after:
case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)

pp: case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

pp: case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Tactic:
·

Goal state after:
case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

pp: case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Tactic:
·

Goal state after:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Tactic:
·

Goal state after:
case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

pp: case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
·

Goal state after:
case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
·

Goal state after:
case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mp
n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b

pp: case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
·

Goal state after:
case mp
n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
·

Goal state after:
case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mpr.inl
n : ℕ
a : ZMod n
⊢ a.valMinAbs.natAbs = a.valMinAbs.natAbs

pp: case mpr.inr
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
·

Goal state after:
case mpr.inl
n : ℕ
a : ZMod n
⊢ a.valMinAbs.natAbs = a.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mpr.inr
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
·

Goal state after:
case mpr.inr
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ((minpoly K pb.gen).aroots E).Nodup

pp: case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := ⋯
this : Fintype (L →ₐ[K] E) := ⋯
⊢ { x // x ∈ (minpoly K pb.gen).aroots E } → E

pp: case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x

pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = ?f✝ (pb.liftEquiv' x)

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ((minpoly K pb.gen).aroots E).Nodup
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case zero
a : ℕ
ha : a ≤ 0 / 2
⊢ (↑a).valMinAbs = ↑a

pp: case succ
a n✝ : ℕ
ha : a ≤ (n✝ + 1) / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
·

Goal state after:
case zero
a : ℕ
ha : a ≤ 0 / 2
⊢ (↑a).valMinAbs = ↑a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ
a n✝ : ℕ
ha : a ≤ (n✝ + 1) / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
·

Goal state after:
case succ
a n✝ : ℕ
ha : a ≤ (n✝ + 1) / 2
⊢ (↑a).valMinAbs = ↑a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case zero
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ (↑a).valMinAbs = ↑a - ↑0

pp: case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)

Tactic:
·

Goal state after:
case zero
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ (↑a).valMinAbs = ↑a - ↑0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)

Tactic:
·

Goal state after:
case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x

pp: case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := ⋯
this : Fintype (L →ₐ[K] E) := ⋯
⊢ { x // x ∈ (minpoly K pb.gen).aroots E } → E

pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = ?f✝ (pb.liftEquiv' x)

Tactic:
·

Goal state after:
case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

pp: case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
·

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)

pp: case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Tactic:
·

Goal state after:
case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = _root_.id ↑(pb.liftEquiv' x)

Tactic:
·

Goal state after:
case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = _root_.id ↑(pb.liftEquiv' x)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Tactic:
·

Goal state after:
case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ a, ∑ s, ⟨a, s⟩.fst pb.gen = ∑ x, finrank L F • x pb.gen

pp: K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ a, ∑ s, ⟨a, s⟩.fst pb.gen = ∑ x, finrank L F • x pb.gen
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ finrank (↥K⟮x⟯) L • ∑ σ, σ pb.gen = ∑ σ, σ x

pp: K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ IsSeparable K pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ finrank (↥K⟮x⟯) L • ∑ σ, σ pb.gen = ∑ σ, σ x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ IsSeparable K pb.gen

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ IsSeparable K pb.gen