awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))

Tactic:
exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyEntourage T F (s i)) i h_i

Premises used: le_iSup₂
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
inst : UniformSpace X
T : X → X
F : Set X
h : U ∈ 𝓤 X
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
coverEntropyInf_eq_iSup_netEntropyInfEntourage T F ▸
    le_iSup₂ (f := fun (U : SetRel X X) (_ : U ∈ 𝓤 X) ↦ netEntropyInfEntourage T F U) U h

Premises used: le_iSup₂, Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage, Eq.rec, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
inst : UniformSpace X
T : X → X
F : Set X
h : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
coverEntropy_eq_iSup_netEntropyEntourage T F ▸
    le_iSup₂ (f := fun (U : SetRel X X) (_ : U ∈ 𝓤 X) ↦ netEntropyEntourage T F U) U h

Premises used: le_iSup₂, Eq.rec, Dynamics.coverEntropy_eq_iSup_netEntropyEntourage, Eq.symm
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
rw : IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀

Tactic:
rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]

Premises used: Module.Basis.mk_eq_rank'', Cardinal.lt_aleph0_iff_set_finite
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
mp : IsNoetherian K V → (Basis.ofVectorSpaceIndex K V).Finite
mpr : (Basis.ofVectorSpaceIndex K V).Finite → IsNoetherian K V
⊢ IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
h : IsNoetherian K V
⊢ (Basis.ofVectorSpaceIndex K V).Finite

Tactic:
(Basis.ofVectorSpaceIndex.linearIndependent K V).set_finite_of_isNoetherian

Premises used: Module.Basis.ofVectorSpaceIndex.linearIndependent, LinearIndependent.set_finite_of_isNoetherian
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
h : IsNoetherian K V
⊢ (Basis.ofVectorSpaceIndex K V).Finite

Tactic:
exact (Basis.ofVectorSpaceIndex.linearIndependent K V).set_finite_of_isNoetherian

Premises used: Module.Basis.ofVectorSpaceIndex.linearIndependent, LinearIndependent.set_finite_of_isNoetherian
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ IsNoetherian K V

Tactic:
@isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)

Premises used: LinearEquiv.ofTop, isNoetherian_of_linearEquiv, rfl
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
mpr : IsNoetherian.{u, v} K ↥⊤
⊢ IsNoetherian K V

Tactic:
refine
      @isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)

Premises used: LinearEquiv.ofTop, isNoetherian_of_linearEquiv, rfl
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ IsNoetherian.{u, v} K ↥⊤

Tactic:
isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩

Premises used: Set.Mem, Set.Finite.toFinset, isNoetherian_of_fg_of_noetherian, Exists.intro
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
mpr : Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
⊢ IsNoetherian.{u, v} K ↥⊤

Tactic:
refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩

Premises used: Set.Finite.toFinset, isNoetherian_of_fg_of_noetherian, Exists.intro
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type v) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
mpr : Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V)) ⊤
mpr₁ :
  Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V))
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type v))
        (⇑b : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V)))
mpr₂ :
  Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V))
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type v))
        (Subtype.val (p := fun (x : V) ↦ x ∈ Basis.ofVectorSpaceIndex K V))))
mpr₃ mpr₄ : Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V)) (span K (Basis.ofVectorSpaceIndex K V))
⊢ Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤

Tactic:
rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]

Premises used: Set.Finite.coe_toFinset, Subtype.range_coe, Module.Basis.coe_ofVectorSpace, Module.Basis.span_eq
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
s : Set ι
inst_3 : IsNoetherian K V
b : Basis.{u_1, u, v} (↑s : Type u_1) K V
⊢ s.Finite

Tactic:
b.finite_index_of_rank_lt_aleph0 (rank_lt_aleph0 K V)

Premises used: Module.Basis.finite_index_of_rank_lt_aleph0, Module.rank_lt_aleph0
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
⊢ (↑(finsetBasisIndex K V) : Set V) = Basis.ofVectorSpaceIndex K V

Tactic:
Set.Finite.coe_toFinset _

Premises used: setOf, Set.Finite.coe_toFinset
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
⊢ ↥(finsetBasisIndex K V) = (↑(Basis.ofVectorSpaceIndex K V) : Type v)

Tactic:
Set.Finite.coeSort_toFinset _

Premises used: Set.Finite.coeSort_toFinset, Set.Mem, setOf
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
rw rw₁ : (↑(Basis.ofVectorSpaceIndex K V) : Type v) ≃ (↑(Basis.ofVectorSpaceIndex K V) : Type v)
⊢ (↑(Basis.ofVectorSpaceIndex K V) : Type v) ≃ ↥(finsetBasisIndex K V)

Tactic:
rw [coeSort_finsetBasisIndex]

Premises used: IsNoetherian.coeSort_finsetBasisIndex
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
rw :
  Set.range (ι := ↥(finsetBasisIndex K V))
      (⇑(Basis.reindex (Basis.ofVectorSpace K V) (Eq.mpr ⋯ (Equiv.refl (↑(Basis.ofVectorSpaceIndex K V) : Type v)))) :
        (a : ↥(finsetBasisIndex K V)) → V) =
    Basis.ofVectorSpaceIndex K V
rw₁ :
  Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type v))
      (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) =
    Basis.ofVectorSpaceIndex K V
rw₂ rw₃ : Basis.ofVectorSpaceIndex K V = Basis.ofVectorSpaceIndex K V
⊢ Set.range (ι := ↥(finsetBasisIndex K V)) (⇑(finsetBasis K V) : (a : ↥(finsetBasisIndex K V)) → V) =
    Basis.ofVectorSpaceIndex K V

Tactic:
rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]

Premises used: Module.Basis.range_ofVectorSpace, IsNoetherian.finsetBasis, Module.Basis.range_reindex
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Fintype V
b : Basis (↥(finsetBasisIndex K V)) K V := finsetBasis K V
rw : Fintype.card K ^ Fintype.card.{v} ↥(finsetBasisIndex K V) = Fintype.card K ^ finrank K V
rw₁ rw₂ : Fintype.card K ^ finrank K V = Fintype.card K ^ finrank K V
⊢ Fintype.card V = Fintype.card K ^ finrank K V

Tactic:
rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis, Module.card_fintype
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
b : Basis (↥(finsetBasisIndex K V)) K V := finsetBasis K V
rw : Nat.card (↥(finsetBasisIndex K V) → K) = Nat.card K ^ finrank K V
rw₁ : Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V) = Nat.card K ^ finrank K V
rw₂ rw₃ : Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V) = Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V)
⊢ Nat.card V = Nat.card K ^ finrank K V

Tactic:
rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]

Premises used: Nat.card_fun, Nat.card_congr, Module.finrank_eq_nat_card_basis, LinearEquiv.toEquiv, Module.Basis.equivFun
-- Module: Mathlib.FieldTheory.Finiteness
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ IsNoetherian K V ↔ Module.Finite K V

Tactic:
⟨fun _ ↦ IsNoetherian.finite _ _, fun _ ↦ isNoetherian_of_isNoetherianRing_of_finite _ _⟩

Premises used: Iff.intro, Module.IsNoetherian.finite, isNoetherian_of_isNoetherianRing_of_finite
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
⊢ IsConjRoot R x y ↔ Eq (α := R[X]) (minpoly R x) (minpoly R y)

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsConjRoot
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ IsConjRoot R x x

Tactic:
rfl

Premises used: IsConjRoot, rfl
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
h : IsConjRoot R x y
⊢ IsConjRoot R y x

Tactic:
Eq.symm h

Premises used: IsConjRoot, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y z : A
h₁ : IsConjRoot R x y
h₂ : IsConjRoot R y z
⊢ IsConjRoot R x z

Tactic:
Eq.trans h₁ h₂

Premises used: IsConjRoot, Eq.trans
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
⊢ IsConjRoot R x y ↔ IsConjRoot R y x

Tactic:
⟨symm, symm⟩

Premises used: Iff.intro, IsConjRoot.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
h : IsConjRoot R x y
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval y : (a : R[X]) → A) (minpoly R x) : A) (0 : A)

Tactic:
h ▸ minpoly.aeval R y

Premises used: Eq.rec, minpoly.aeval, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
rw :
  Eq (α := K[X]) (minpoly K (HAdd.hAdd (β := S) x ((algebraMap K S : (a : K) → S) r : S)))
    (minpoly K (HAdd.hAdd (β := S) y ((algebraMap K S : (a : K) → S) r : S)))
rw₁ :
  comp (minpoly K x) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) r : K[X])) =
    minpoly K (HAdd.hAdd (β := S) y ((algebraMap K S : (a : K) → S) r : S))
rw₂ :
  comp (minpoly K x) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) r : K[X])) =
    comp (minpoly K y) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) r : K[X]))
rw₃ rw₄ :
  comp (minpoly K y) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) r : K[X])) =
    comp (minpoly K y) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) r : K[X]))
⊢ IsConjRoot K (HAdd.hAdd (β := S) x ((algebraMap K S : (a : K) → S) r : S))
    (HAdd.hAdd (β := S) y ((algebraMap K S : (a : K) → S) r : S))

Tactic:
rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]

Premises used: isConjRoot_def, minpoly.add_algebraMap
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ IsConjRoot K (HSub.hSub (β := S) x ((algebraMap K S : (a : K) → S) r : S))
    (HSub.hSub (β := S) y ((algebraMap K S : (a : K) → S) r : S))

Tactic:
simpa only [sub_eq_add_neg, map_neg] using add_algebraMap (-r) h

Premises used: sub_eq_add_neg, map_neg, IsConjRoot.add_algebraMap, Neg.neg
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
x y : S
h : IsConjRoot K x y
rw : Eq (α := K[X]) (minpoly K (-x)) (minpoly K (-y))
rw₁ : HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x)) * comp (minpoly K x) (-X) = minpoly K (-y)
rw₂ :
  HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x)) * comp (minpoly K x) (-X) =
    HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K y)) * comp (minpoly K y) (-X)
rw₃ rw₄ :
  HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K y)) * comp (minpoly K y) (-X) =
    HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K y)) * comp (minpoly K y) (-X)
⊢ IsConjRoot K (-x) (-y)

Tactic:
rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]

Premises used: isConjRoot_def, minpoly.neg
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
B : Type u_6
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x y : A
f : A →ₐ[R] B
hf : Function.Injective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
rw :
  Eq (α := R[X]) (minpoly.{u_1, u_6} R (B := B) ((f : (a : A) → B) x : B))
      (minpoly.{u_1, u_6} R (B := B) ((f : (a : A) → B) y : B)) ↔
    IsConjRoot R x y
rw₁ :
  Eq (α := R[X]) (minpoly.{u_1, u_6} R (B := B) ((f : (a : A) → B) x : B))
      (minpoly.{u_1, u_6} R (B := B) ((f : (a : A) → B) y : B)) ↔
    Eq (α := R[X]) (minpoly R x) (minpoly R y)
rw₂ :
  Eq (α := R[X]) (minpoly R x) (minpoly.{u_1, u_6} R (B := B) ((f : (a : A) → B) y : B)) ↔
    Eq (α := R[X]) (minpoly R x) (minpoly R y)
rw₃ rw₄ : Eq (α := R[X]) (minpoly R x) (minpoly R y) ↔ Eq (α := R[X]) (minpoly R x) (minpoly R y)
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y

Tactic:
rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]

Premises used: isConjRoot_def, minpoly.algHom_eq
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
B : Type u_6
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
A : Type u_7
inst_3 : DivisionRing A
inst_4 : Algebra R A
inst_5 : Nontrivial B
x y : A
f : A →ₐ[R] B
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y

Tactic:
isConjRoot_algHom_iff_of_injective f.injective

Premises used: isConjRoot_algHom_iff_of_injective, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
A : Type u_5
inst : Ring A
inst_1 : Field K
inst_2 : Algebra K A
inst_3 : IsDomain A
x y : A
hx : IsIntegral K x
h : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval y : (a : K[X]) → A) (minpoly K x) : A) (0 : A)
⊢ IsConjRoot K x y

Tactic:
minpoly.eq_of_irreducible_of_monic (minpoly.irreducible hx) h (minpoly.monic hx)

Premises used: minpoly.monic, IsConjRoot, minpoly.eq_of_irreducible_of_monic, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
A : Type u_5
inst : Ring A
inst_1 : Field K
inst_2 : Algebra K A
inst_3 : IsDomain A
x y : A
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval y : (a : K[X]) → A) (minpoly K x) : A) (0 : A)

Tactic:
⟨IsConjRoot.aeval_eq_zero, isConjRoot_of_aeval_eq_zero h⟩

Premises used: isConjRoot_of_aeval_eq_zero, IsConjRoot.aeval_eq_zero, Iff.intro
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
s : A ≃ₐ[R] A
⊢ IsConjRoot R x ((s : (a : A) → A) x)

Tactic:
Eq.symm (minpoly.algEquiv_eq s x)

Premises used: minpoly.algEquiv_eq, IsConjRoot, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
s : A ≃ₐ[R] A
⊢ IsConjRoot R ((s : (a : A) → A) x) x

Tactic:
(minpoly.algEquiv_eq s x)

Premises used: minpoly.algEquiv_eq, IsConjRoot
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
s₁ s₂ : A ≃ₐ[R] A
⊢ IsConjRoot R (A := A) ((s₁ : (a : A) → A) x : A) ((s₂ : (a : A) → A) x : A)

Tactic:
isConjRoot_def.mpr <| (minpoly.algEquiv_eq s₂ x) ▸ (minpoly.algEquiv_eq s₁ x)

Premises used: Iff.mpr, isConjRoot_def, Eq.rec, minpoly.algEquiv_eq, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
h : IsConjRoot K x y
obtain : ∀ (σ : L →ₐ[K] L) (hσ : (σ : (a : L) → L) y = x), ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
obtain ⟨σ, hσ⟩ :=
    exists_algHom_of_splits_of_aeval (normal_iff.mp inferInstance) (h ▸ minpoly.aeval K x)

Premises used: inferInstance, normal_iff, Iff.mp, IntermediateField.exists_algHom_of_splits_of_aeval
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
h : IsConjRoot K x y
σ : L →ₐ[K] L
hσ : (σ : (a : L) → L) y = x
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
⟨AlgEquiv.ofBijective σ (σ.normal_bijective _ _ _), hσ⟩

Premises used: AlgEquiv.ofBijective, Exists.intro, AlgHom.normal_bijective
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
h : IsConjRoot K x y
σ : L →ₐ[K] L
hσ : (σ : (a : L) → L) y = x
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
exact ⟨AlgEquiv.ofBijective σ (σ.normal_bijective _ _ _), hσ⟩
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
⊢ IsConjRoot K x y ↔ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
⟨exists_algEquiv, fun ⟨_, h⟩ => h ▸ (isConjRoot_of_algEquiv _ _).symm⟩

Premises used: isConjRoot_of_algEquiv, Eq.rec, IsConjRoot, _private.0.isConjRoot_iff_exists_algEquiv.match_1, IsConjRoot.exists_algEquiv, Iff.intro, IsConjRoot.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
⊢ IsConjRoot K x y ↔ (MulAction.orbitRel Gal(L/K) L : L → L → Prop) x y

Tactic:
(isConjRoot_iff_exists_algEquiv)

Premises used: isConjRoot_iff_exists_algEquiv, Set.Mem, setOf, MulAction.orbit, Set.range
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
inst_5 : Algebra L S
inst_6 : IsDomain S
inst_7 : IsScalarTower K L S
x y : S
hx : IsIntegral K x
h : IsConjRoot L x y
⊢ IsConjRoot K x y

Tactic:
isConjRoot_of_aeval_eq_zero hx <| minpoly.aeval_of_isScalarTower K x y (aeval_eq_zero h)

Premises used: isConjRoot_of_aeval_eq_zero, IsConjRoot.aeval_eq_zero, minpoly.aeval_of_isScalarTower
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
rw :
  Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) ↔
    Ne (α := K[X]) (minpoly K x) 0 ∧
      Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S)
⊢ IsConjRoot K x y ↔ y ∈ aroots (minpoly K x) S

Tactic:
rw [Polynomial.mem_aroots, isConjRoot_iff_aeval_eq_zero h]

Premises used: isConjRoot_iff_aeval_eq_zero, Polynomial.mem_aroots
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
simp :
  Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) →
    Ne (α := K[X]) (minpoly K x) 0
⊢ Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) ↔
    Ne (α := K[X]) (minpoly K x) 0 ∧
      Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S)

Tactic:
simp only [iff_and_self]

Premises used: iff_and_self
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
⊢ Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) →
    Ne (α := K[X]) (minpoly K x) 0

Tactic:
fun _ => minpoly.ne_zero h

Premises used: minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
⊢ Eq.{u_4 + 1} (α := S) ((Polynomial.aeval y : (a : K[X]) → S) (minpoly K x) : S) (0 : S) →
    Ne (α := K[X]) (minpoly K x) 0

Tactic:
exact fun _ => minpoly.ne_zero h

Premises used: minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
K : Type u_2
S : Type u_4
inst : CommRing S
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : IsDomain S
x y : S
h : IsIntegral K x
⊢ y ∈ aroots (minpoly K x) S ↔ y ∈ rootSet (minpoly K x) S

Tactic:
simp [rootSet]

Premises used: Polynomial.rootSet
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Ring B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra R S
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra K S
inst_10 : Algebra K L
inst_11 : Algebra K A
inst_12 : Algebra L S
inst_13 : IsDomain S
⊢ IsEquiv A (IsConjRoot R)

Tactic:
letI := IsConjRoot.setoid R A
  inferInstanceAs <| IsEquiv A (· ≈ ·)

Premises used: _private.0.IsConjRoot.instIsEquiv._proof_1
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
hx : IsIntegral R x
h : IsConjRoot R x y
⊢ IsIntegral R y

Tactic:
⟨minpoly R x, minpoly.monic hx, h ▸ minpoly.aeval R y⟩

Premises used: minpoly.monic, Eq.rec, minpoly.aeval, RingHom.IsIntegralElem, minpoly, IsIntegral, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsConjRoot
Goal:
R : Type u_1
A : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x y : A
h : IsConjRoot R x y
⊢ IsIntegral R x ↔ IsIntegral R y

Tactic:
⟨fun hx ↦ isIntegral hx h, fun hy ↦ isIntegral hy h.symm⟩

Premises used: Iff.intro, IsConjRoot.symm, IsConjRoot.isIntegral