awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : L
rw : (equiv i i p : (a : L) → L) x = x
rw₁ rw₂ : x = x
⊢ (equiv j i p : (a : M) → L) ((equiv i j p : (a : L) → M) x : M) = x

Tactic:
rw [equiv_comp_equiv_apply, equiv_self_apply]

Premises used: IsPerfectClosure.equiv_self_apply, IsPerfectClosure.equiv_comp_equiv_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
⊢ (equiv i j p).trans (equiv j i p) = RingEquiv.refl L

Tactic:
RingEquiv.ext (equiv_comp_equiv_apply_eq_self i j p)

Premises used: IsPerfectClosure.equiv_comp_equiv_apply_eq_self, RingEquiv.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
rw :
  Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[x.1] (mk K p x) :
      PerfectClosure K p)
rw₁ rw₂ :
  Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
    ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
⊢ (of K p : (a : K) → PerfectClosure K p) x.2 = HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ x.1)

Tactic:
rw [← iterate_frobenius, iterate_frobenius_mk K p x.1 x.2]

Premises used: Prod.fst, iterate_frobenius, PerfectClosure.iterate_frobenius_mk, Prod.snd
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (F := K →+* PerfectClosure K p) (of K p)) x
⊢ ∃ (z : ℕ),
    (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + z] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + z] (0, 0).2

Tactic:
rw [RingHom.mem_ker, of_apply, zero_def, mk_eq_iff] at h

Premises used: RingHom.mem_ker, PerfectClosure.of_apply, PerfectClosure.mk_eq_iff, PerfectClosure.zero_def
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
h :
  ∃ (z : ℕ),
    (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + z] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + z] (0, 0).2
obtain :
  ∀ (n : ℕ)
    (h :
      (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + n] (0, x).2 =
        (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + n] (0, 0).2),
    Membership.mem (γ := Submodule K K) (pNilradical K p) x
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
n : ℕ
h : (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + n] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + n] (0, 0).2
⊢ Eq (α := K) ((iterateFrobenius K p n : (a : K) → K) x : K) (0 : K)

Tactic:
simp_rw [zero_add, ← coe_iterateFrobenius, map_zero] at h

Premises used: map_zero, zero_add, coe_iterateFrobenius
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
n : ℕ
h : Eq (α := K) ((iterateFrobenius K p n : (a : K) → K) x : K) (0 : K)
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x

Tactic:
mem_pNilradical.2 ⟨n, h⟩

Premises used: Iff.mpr, Set.Mem, mem_pNilradical, Exists.intro
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
n : ℕ
h : Eq (α := K) ((iterateFrobenius K p n : (a : K) → K) x : K) (0 : K)
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x

Tactic:
exact mem_pNilradical.2 ⟨n, h⟩

Premises used: Iff.mpr, mem_pNilradical, Exists.intro
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : ℕ
inst_3 : ExpChar K p
inst_4 : IsPRadical (algebraMap K L) p
⊢ IsPurelyInseparable K L

Tactic:
(isPurelyInseparable_iff_pow_mem K p).2 (IsPRadical.pow_mem (algebraMap K L) p)

Premises used: Iff.mpr, IsPRadical.pow_mem, Algebra.algebraMap, isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
inl : ∀ (neg : x ≤ 0), IsSquare x ∨ IsSquare (-x)
inr : ∀ (pos : 0 ≤ x), IsSquare x ∨ IsSquare (-x)
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
rcases le_total x 0 with (neg | pos)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
neg : x ≤ 0
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
.inr <| isSquare_of_nonneg (neg_nonneg_of_nonpos neg)

Premises used: neg_nonneg_of_nonpos, Or.inr
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
neg : x ≤ 0
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
exact .inr <| isSquare_of_nonneg (neg_nonneg_of_nonpos neg)

Premises used: neg_nonneg_of_nonpos
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
pos : 0 ≤ x
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
.inl <| isSquare_of_nonneg pos

Premises used: Or.inl
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
pos : 0 ≤ x
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
exact .inl <| isSquare_of_nonneg pos
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : ¬IsSquare (-x)
⊢ IsSquare x

Tactic:
aesop
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : ¬IsSquare x
⊢ IsSquare (-x)

Tactic:
aesop
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ Odd (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).natDegree

Tactic:
simp [hn]
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
rcases :
  ∀ (r : R) (hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r),
    ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases exists_isRoot_of_odd_natDegree (f := X ^ n - C x) (by simp [hn]) with ⟨r, hr⟩

Premises used: IsRealClosed.exists_isRoot_of_odd_natDegree
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r
⊢ r ^ n - x = 0

Tactic:
simpa using hr
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r
linear_combination : r ^ n - x = 0
⊢ x = r ^ n

Tactic:
linear_combination - (by simpa using hr : r ^ n - x = 0)
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r
⊢ ∃ (r : R), x = r ^ n

Tactic:
exact ⟨r, by linear_combination - (by simpa using hr : r ^ n - x = 0)⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
k : ℤ
hk : Odd k
inl : ∀ (n : ℕ) (hk : Odd (α := ℤ) (↑n : ℤ)), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
inr : ∀ (n : ℕ) (hk : Odd (α := ℤ) (-(↑n : ℤ))), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
⊢ ∃ (r : R), x = r ^ k

Tactic:
rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (↑n : ℤ)
⊢ Odd n

Tactic:
simpa using hk
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (↑n : ℤ)
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)

Tactic:
simpa using exists_eq_pow_of_odd x (by simpa using hk)

Premises used: IsRealClosed.exists_eq_pow_of_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (-(↑n : ℤ))
⊢ Odd n

Tactic:
simpa using hk
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (-(↑n : ℤ))
inr : ∀ (r : R) (hr : x = r ^ n), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))

Tactic:
rcases exists_eq_pow_of_odd x (by simpa using hk) with ⟨r, hr⟩

Premises used: IsRealClosed.exists_eq_pow_of_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (-(↑n : ℤ))
r : R
hr : x = r ^ n
⊢ x = HPow.hPow (β := ℤ) r⁻¹ (-(↑n : ℤ))

Tactic:
simpa using hr
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (-(↑n : ℤ))
r : R
hr : x = r ^ n
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))

Tactic:
exact ⟨r⁻¹, by simpa using hr⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
h : ∀ (even : Even n), ∃ (r : R), x = r ^ n
h₁ : ∀ (odd : Odd n), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases Nat.even_or_odd n with (even | odd)

Premises used: Nat.even_or_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
even : Even n
h : ∀ (m : ℕ) (hm : n = m + m), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases even with ⟨m, hm⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
m : ℕ
hm : n = m + m
h : ∀ (s : R) (hs : x = s * s), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases hx with ⟨s, hs⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : ∀ (h : IsSquare s), ∃ (r : R), x = r ^ n
h₁ : ∀ (h : IsSquare (-s)), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases isSquare_or_isSquare_neg s with (h | h)

Premises used: IsRealClosed.isSquare_or_isSquare_neg
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
⊢ m < n

Tactic:
lia
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
⊢ m ≠ 0

Tactic:
lia
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
h₁ : ∀ (r : R) (hr : s = r ^ m), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases ih m (by lia) h (by lia) with ⟨r, hr⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
⊢ m < n

Tactic:
lia
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
⊢ m ≠ 0

Tactic:
lia
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
h₁ : ∀ (r : R) (hr : -s = r ^ m), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
rcases ih m (by lia) h (by lia) with ⟨r, hr⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
r : R
hr : s = r ^ m
⊢ x = r ^ n

Tactic:
simp [hm, pow_add, ← hr, hs]

Premises used: pow_add
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
r : R
hr : s = r ^ m
⊢ ∃ (r : R), x = r ^ n

Tactic:
exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
r : R
hr : -s = r ^ m
⊢ x = r ^ n

Tactic:
simp [hm, pow_add, ← hr, hs]

Premises used: pow_add
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
r : R
hr : -s = r ^ m
⊢ ∃ (r : R), x = r ^ n

Tactic:
exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
odd : Odd n
⊢ ∃ (r : R), x = r ^ n

Tactic:
exists_eq_pow_of_odd x odd

Premises used: IsRealClosed.exists_eq_pow_of_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
odd : Odd n
⊢ ∃ (r : R), x = r ^ n

Tactic:
exact exists_eq_pow_of_odd x odd

Premises used: IsRealClosed.exists_eq_pow_of_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hn : n ≠ 0
h :
  ∀ (n : ℕ) (ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m) {x : R} (hx : IsSquare x)
    (hn : n ≠ 0), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n

Tactic:
induction n using Nat.strong_induction_on generalizing x with
  | h n ih =>
    rcases Nat.even_or_odd n with (even | odd)
    · rcases even with ⟨m, hm⟩
      rcases hx with ⟨s, hs⟩
      rcases isSquare_or_isSquare_neg s with (h | h) <;>
        rcases ih m (by lia) h (by lia) with ⟨r, hr⟩ <;>
        exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩
    · exact exists_eq_pow_of_odd x odd

Premises used: Nat.even_or_odd
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
k : ℤ
hk : k ≠ 0
inl : ∀ (n : ℕ) (hk : Ne (α := ℤ) (↑n : ℤ) 0), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
inr : ∀ (n : ℕ) (hk : Ne (α := ℤ) (-(↑n : ℤ)) 0), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
⊢ ∃ (r : R), x = r ^ k

Tactic:
rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (↑n : ℤ) 0
⊢ n ≠ 0

Tactic:
simpa using hk
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (↑n : ℤ) 0
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)

Tactic:
simpa using exists_eq_pow_of_isSquare hx (by simpa using hk)

Premises used: IsRealClosed.exists_eq_pow_of_isSquare
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (-(↑n : ℤ)) 0
⊢ n ≠ 0

Tactic:
simpa using hk
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (-(↑n : ℤ)) 0
inr : ∀ (r : R) (hr : x = r ^ n), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))

Tactic:
rcases exists_eq_pow_of_isSquare hx (by simpa using hk) with ⟨r, hr⟩

Premises used: IsRealClosed.exists_eq_pow_of_isSquare
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (-(↑n : ℤ)) 0
r : R
hr : x = r ^ n
⊢ x = HPow.hPow (β := ℤ) r⁻¹ (-(↑n : ℤ))

Tactic:
simpa using hr
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : Ne (α := ℤ) (-(↑n : ℤ)) 0
r : R
hr : x = r ^ n
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))

Tactic:
exact ⟨r⁻¹, by simpa using hr⟩
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
h : 0 ≤ x
this : IsSquare (-x) → x = 0
⊢ IsSquare x

Tactic:
aesop
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
h : 0 ≤ x
suffices : IsSquare (-x) → x = 0
⊢ IsSquare x

Tactic:
suffices IsSquare (-x) → x = 0 by aesop
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
h : 0 ≤ x
⊢ IsSquare (-x) → x = 0

Tactic:
fun hc ↦ le_antisymm (nonpos_of_neg_nonneg (IsSquare.nonneg hc)) h

Premises used: le_antisymm, IsSquare.nonneg, nonpos_of_neg_nonneg
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
h : 0 ≤ x
⊢ IsSquare (-x) → x = 0

Tactic:
exact fun hc ↦ le_antisymm (nonpos_of_neg_nonneg (IsSquare.nonneg hc)) h

Premises used: le_antisymm, nonpos_of_neg_nonneg
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
hx : 0 ≤ x
n : ℕ
hn : n ≠ 0
⊢ ∃ (r : R), x = r ^ n

Tactic:
exists_eq_pow_of_isSquare (.of_nonneg hx) hn

Premises used: IsRealClosed.exists_eq_pow_of_isSquare, IsSquare.of_nonneg
-- Module: Mathlib.FieldTheory.IsRealClosed.Basic
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
x : R
hx : 0 ≤ x
k : ℤ
hk : k ≠ 0
⊢ ∃ (r : R), x = r ^ k

Tactic:
exists_eq_zpow_of_isSquare (.of_nonneg hx) hk

Premises used: IsRealClosed.exists_eq_zpow_of_isSquare, IsSquare.of_nonneg
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed k
⊢ IsSepClosed k

Tactic:
⟨fun p _ ↦ IsAlgClosed.splits p⟩

Premises used: IsSepClosed.mk, IsAlgClosed.splits
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed K
f : k →+* K
p : k[X]
h : p.Separable
⊢ (map f p).Splits

Tactic:
IsSepClosed.splits_of_separable (p.map f) (Separable.map h)

Premises used: Polynomial.Separable.map, Polynomial.map, IsSepClosed.splits_of_separable
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsSepClosed k
f : k →+* K
p : k[X]
h : p.Separable
⊢ (map f p).Splits

Tactic:
(IsSepClosed.splits_of_separable _ h).map f

Premises used: IsSepClosed.splits_of_separable, Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ ∃ (x : k), p.IsRoot x

Tactic:
(IsSepClosed.splits_of_separable p hsep).exists_eval_eq_zero hp

Premises used: Polynomial.IsRoot, Polynomial.Splits.exists_eval_eq_zero, IsSepClosed.splits_of_separable
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
⊢ (C : (a : k) → k[X]) 0 * HPow.hPow (α := k[X]) X n +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X =
    0 * HPow.hPow (α := k[X]) X n + HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X

Tactic:
grind
-- Module: Mathlib.FieldTheory.IsSepClosed
Goal:
k : Type u
inst : Field k
inst_1 : IsSepClosed k
n : ℕ
a b c : k
hn : Eq.{u + 1} (α := k) (↑n : k) 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] :=
  HAdd.hAdd (β := k[X])
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) a : k[X]) (HPow.hPow (α := k[X]) X n) +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X)
    ((C : (a : k) → k[X]) c : k[X])
⊢ (C : (a : k) → k[X]) 0 * HPow.hPow (α := k[X]) X n +
      HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X =
    0 * HPow.hPow (α := k[X]) X n + HMul.hMul (α := k[X]) (β := k[X]) ((C : (a : k) → k[X]) b : k[X]) X

Tactic:
have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind