harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isAdjointPair_zero : IsAdjointPair B B' 0 0 := fun _ _ ↦ by
  simp only [Pi.zero_apply, map_zero, zero_apply]

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
x✝¹ : M
x✝ : M₁
⊢ (B' (0 x✝¹)) x✝ = (B x✝¹) (0 x✝)

Tactic:
simp only [Pi.zero_apply, map_zero, zero_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem isOpen_extend_source : IsOpen (f.extend I).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen (f.extend I).source

Tactic:
rw [extend_source]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen f.source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen f.source

Tactic:
exact f.open_source

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
theorem transferSylow_eq_pow_aux (g : G) (hg : g ∈ P) (k : ℕ) (g₀ : G)
    (h : g₀⁻¹ * g ^ k * g₀ ∈ P) : g₀⁻¹ * g ^ k * g₀ = g ^ k

Proof state:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ (↑P).normalizer
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Proof state:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
replace hg := (P : Subgroup G).pow_mem hg k

Result:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Proof state:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
haveI : (P : Subgroup G).IsCommutative :=
  ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩

Result:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : (↑P).IsCommutative
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ (↑P).normalizer
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_three : bernoulli' 3 = 0

Proof state:
⊢ bernoulli' 3 = 0

Tactic:
rw [bernoulli'_def]

Result:
⊢ 1 - ∑ k ∈ range 3, ↑(Nat.choose 3 k) / (↑3 - ↑k + 1) * bernoulli' k = 0

Proof state:
⊢ 1 - ∑ k ∈ range 3, ↑(Nat.choose 3 k) / (↑3 - ↑k + 1) * bernoulli' k = 0

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_two_bne_one : ((a % 2) != 1) = (a % 2 == 0)

Proof state:
a : Nat
⊢ (a % 2 != 1) = (a % 2 == 0)

Tactic:
cases mod_two_eq_zero_or_one a <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
@[simp]
lemma _root_.NonUnitalAlgHom.toAlgHom_zero :
    ⇑(0 : A →ₙₐ[R] R).toAlgHom = Unitization.fst

Proof state:
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
⊢ ⇑(NonUnitalAlgHom.toAlgHom 0) = fst

Tactic:
ext

Result:
case h
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x✝ : Unitization R A
⊢ (NonUnitalAlgHom.toAlgHom 0) x✝ = x✝.fst

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x✝ : Unitization R A
⊢ (NonUnitalAlgHom.toAlgHom 0) x✝ = x✝.fst

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
theorem submodule_pow_eq_zero_of_pow_eq_zero {N : Submodule R M} {g : Module.End R N}
    {G : Module.End R M} (h : G.comp N.subtype = N.subtype.comp g) {k : ℕ} (hG : G ^ k = 0) :
    g ^ k = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
⊢ g ^ k = 0

Tactic:
ext m

Result:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ ↑((g ^ k) m) = ↑(0 m)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ (N.subtype ∘ₗ g ^ k) m = 0

Tactic:
rw [← commute_pow_left_of_commute h, hG, zero_comp, zero_apply]

Result:
no goals

Proof state:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
hg : (N.subtype ∘ₗ g ^ k) m = 0
⊢ ↑((g ^ k) m) = ↑(0 m)

Tactic:
simpa using hg

Result:
no goals

Proof state:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ ↑((g ^ k) m) = ↑(0 m)

Tactic:
have hg : N.subtype.comp (g ^ k) m = 0 := by
  rw [← commute_pow_left_of_commute h, hG, zero_comp, zero_apply]

Result:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
hg : (N.subtype ∘ₗ g ^ k) m = 0
⊢ ↑((g ^ k) m) = ↑(0 m)
-- Mathlib/Algebra/Lie/Basic.lean
theorem lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

Proof state:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0

Tactic:
abel

Result:
no goals

Proof state:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

Tactic:
rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]

Result:
L : Type v
inst✝ : LieRing L
x y z : L
⊢ -(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorZero_eq :
    CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = shiftFunctorZero' C 0 rfl

Proof state:
case w.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app x✝).f i✝ = ((shiftFunctorZero' C 0 ⋯).hom.app x✝).f i✝

Tactic:
rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
⊢ shiftFunctorZero (CochainComplex C ℤ) ℤ = shiftFunctorZero' C 0 ⋯

Tactic:
ext

Result:
case w.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app x✝).f i✝ = ((shiftFunctorZero' C 0 ⋯).hom.app x✝).f i✝
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem symm_toHom_comp_toHom : f.symm.toHom.comp f.toHom = Hom.id

Proof state:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
v : V
⊢ (f.symm.toHom.comp f.toHom) v = Hom.id v

Tactic:
simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
  RelIso.symm_apply_apply, RelHom.id_apply]

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
⊢ f.symm.toHom.comp f.toHom = Hom.id

Tactic:
ext v

Result:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
v : V
⊢ (f.symm.toHom.comp f.toHom) v = Hom.id v
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem continuous_toUpper [TopologicalSpace α] [ClosedIicTopology α] :
    Continuous (toUpper : α → WithUpper α) :=
  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Iic.isOpen_compl

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
⊢ ∀ s ∈ {s | ∃ a, (Iic a)ᶜ = s}, IsOpen (⇑toUpper ⁻¹' s)

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen (⇑toUpper ⁻¹' (Iic a)ᶜ)

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen (⇑toUpper ⁻¹' (Iic a)ᶜ)

Tactic:
exact isClosed_Iic.isOpen_compl

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem IsBilimit.total {f : J → C} {b : Bicone f} (i : b.IsBilimit) :
    ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt :=
  i.isLimit.hom_ext fun j => by
    classical
    cases j
    simp [sum_comp, b.ι_π, comp_dite]

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
j : Discrete J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
cases j

Result:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
as✝ : J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as✝ } = 𝟙 b.pt ≫ b.toCone.π.app { as := as✝ }

Proof state:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
as✝ : J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as✝ } = 𝟙 b.pt ≫ b.toCone.π.app { as := as✝ }

Tactic:
simp [sum_comp, b.ι_π, comp_dite]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
j : Discrete J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
classical
cases j
simp [sum_comp, b.ι_π, comp_dite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem?_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : i ≤ j) :
    (l.eraseIdx i)[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?

Tactic:
simp only [dite_eq_ite, ite_eq_right_iff]

Result:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?

Tactic:
intro h'

Result:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
⊢ (l.eraseIdx i)[j]? = l[j + 1]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
l : List α
i j : Nat
h : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_le_self (a : Int) {b : Int} (h : 0 ≤ b) : a - b ≤ a :=
  calc  a + -b
    _ ≤ a + 0 := Int.add_le_add_left (Int.neg_nonpos_of_nonneg h) _
    _ = a

Proof state:
a b : Int
h : 0 ≤ b
⊢ a + 0 = a

Tactic:
rw [Int.add_zero]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_sdiff_add_dens (s t : Finset α) : dens (s \ t) + dens t = (s ∪ t).dens

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + t.dens = (s ∪ t).dens

Tactic:
rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_zero : enumOrd s 0 = sInf s

Proof state:
s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s

Tactic:
simp [Ordinal.not_lt_zero]

Result:
no goals

Proof state:
s : Set Ordinal.{u}
⊢ enumOrd s 0 = sInf s

Tactic:
rw [enumOrd]

Result:
s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_im_pow_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
    (fun z : ℂ => z.im ^ n) =o[l] fun z => Real.exp z.re :=
  flip IsLittleO.of_pow two_ne_zero <|
    calc
      (fun z : ℂ ↦ (z.im ^ n) ^ 2) = (fun z ↦ z.im ^ (2 * n))

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => (z.im ^ n) ^ 2) = fun z => z.im ^ (2 * n)

Tactic:
simp only [pow_mul']

Result:
no goals

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => Real.exp z.re) = fun z => Real.exp z.re ^ 1

Tactic:
simp only [pow_one]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff_eq_expand_X_sub_C : (minpoly F x).natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), minpoly F x = expand F (q ^ n) (X - C y)

Proof state:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : minpoly F x = (expand F (q ^ n)) (X - C y)
⊢ (minpoly F x).natSepDegree = 1

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩

Result:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : minpoly F x = (expand F (q ^ n)) (X - C y)
⊢ (minpoly F x).natSepDegree = 1

Proof state:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
have halg : IsIntegral F x := by_contra fun h' ↦ by
  simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h

Result:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Proof state:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
  (minpoly.monic halg) |>.1 h

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
h' : ¬IsIntegral F x
⊢ False

Tactic:
simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem length_think (s : Computation α) [h : Terminates s] : length (think s) = length s + 1

Proof state:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

Tactic:
exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))

Result:
no goals

Proof state:
case a
α : Type u
s : Computation α
h : s.Terminates
this : (↑s.think s.think.length).isSome = true
⊢ s.length + 1 ≤ s.think.length

Tactic:
revert this

Result:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (↑s.think s.think.length).isSome = true → s.length + 1 ≤ s.think.length

Proof state:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length

Tactic:
have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
  Nat.find_spec ((terminates_def _).1 s.think_terminates)

Result:
case a
α : Type u
s : Computation α
h : s.Terminates
this : (↑s.think s.think.length).isSome = true
⊢ s.length + 1 ≤ s.think.length

Proof state:
case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1

Tactic:
apply Nat.succ_le_succ

Result:
case a.succ.a
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ s.length ≤ n

Proof state:
case a.succ.a.h
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ (↑s n).isSome = true

Tactic:
apply this

Result:
no goals

Proof state:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (↑s.think s.think.length).isSome = true → s.length + 1 ≤ s.think.length

Tactic:
rcases length (think s) with - | n <;> intro this

Result:
case a.zero
α : Type u
s : Computation α
h : s.Terminates
this : (↑s.think 0).isSome = true
⊢ s.length + 1 ≤ 0

case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1

Proof state:
case a.succ.a
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ s.length ≤ n

Tactic:
apply Nat.find_min'

Result:
case a.succ.a.h
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (↑s.think (n + 1)).isSome = true
⊢ (↑s n).isSome = true

Proof state:
case a.zero
α : Type u
s : Computation α
h : s.Terminates
this : (↑s.think 0).isSome = true
⊢ s.length + 1 ≤ 0

Tactic:
simp [think, Stream'.cons] at this

Result:
no goals

Proof state:
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length = s.length + 1

Tactic:
apply le_antisymm

Result:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem eq_neg_one_at_prime_divisor_of_eq_neg_one {a : ℤ} {n : ℕ} (h : J(a | n) = -1) :
    ∃ p : ℕ, p.Prime ∧ p ∣ n ∧ J(a | p) = -1

Proof state:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
rw [← Nat.prod_primeFactorsList hn₀, list_prod_right hf₀] at h

Result:
a : ℤ
n : ℕ
h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Proof state:
a : ℤ
h : J(a | 0) = -1
⊢ False

Tactic:
rw [zero_right, CharZero.eq_neg_self_iff] at h

Result:
a : ℤ
h : 1 = 0
⊢ False

Proof state:
a : ℤ
n : ℕ
h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
obtain ⟨p, hmem, hj⟩ := List.mem_map.mp (List.neg_one_mem_of_prod_eq_neg_one h)

Result:
case intro.intro
a : ℤ
n : ℕ
h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
p : ℕ
hmem : p ∈ n.primeFactorsList
hj : J(a | p) = -1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Proof state:
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
have hn₀ : n ≠ 0 := by
  rintro rfl
  rw [zero_right, CharZero.eq_neg_self_iff] at h
  exact one_ne_zero h

Result:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Proof state:
a : ℤ
h : 1 = 0
⊢ False

Tactic:
exact one_ne_zero h

Result:
no goals

Proof state:
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
a : ℤ
h : J(a | 0) = -1
⊢ False

Proof state:
case intro.intro
a : ℤ
n : ℕ
h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
p : ℕ
hmem : p ∈ n.primeFactorsList
hj : J(a | p) = -1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
exact ⟨p, Nat.prime_of_mem_primeFactorsList hmem, Nat.dvd_of_mem_primeFactorsList hmem, hj⟩

Result:
no goals

Proof state:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
have hf₀ (p) (hp : p ∈ n.primeFactorsList) : p ≠ 0 := (Nat.pos_of_mem_primeFactorsList hp).ne.symm

Result:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1