awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
have obtain : ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
  netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
Tactic: obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
have apply : LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (s i))
  (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
Tactic: apply (netEntropyInfEntourage_antitone T F si_U).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ coverEntropy T F = ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
have rw : Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
Tactic: rw [coverEntropy_eq_iSup_netEntropyEntourage T F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
have apply : LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
Tactic: apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
have refine : ∀ (U : SetRel X X) (U_uni : U ∈ 𝓤 X), netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
have obtain : ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
  netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
Tactic: obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
have apply : LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (s i))
  (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
Tactic: apply (netEntropyEntourage_antitone T F si_U).trans _
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀
have rw : IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite
Tactic: rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite
have mp : IsNoetherian K V → (Basis.ofVectorSpaceIndex K V).Finite
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite
have mpr : (Basis.ofVectorSpaceIndex K V).Finite → IsNoetherian K V
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
have mpr : IsNoetherian.{u, v} K ↥⊤
Tactic: refine
      @isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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 ↥⊤
have mpr : Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
Tactic: refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
have mpr : Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V)) ⊤
Tactic: rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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)) ⊤
⊢ Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
have 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)))
Tactic: rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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)))
⊢ Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
have 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))))
Tactic: rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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))))
⊢ Eq (α := Submodule K V) (span K (↑(hbfinite.toFinset (s := Basis.ofVectorSpaceIndex K V)) : Set V)) ⊤
have mpr₃ : Eq (α := Submodule K V) (span K (Basis.ofVectorSpaceIndex K V)) (span K (Basis.ofVectorSpaceIndex K V))
Tactic: rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
⊢ (↑(Basis.ofVectorSpaceIndex K V) : Type v) ≃ ↥(finsetBasisIndex K V)
have rw : (↑(Basis.ofVectorSpaceIndex K V) : Type v) ≃ (↑(Basis.ofVectorSpaceIndex K V) : Type v)
Tactic: rw [coeSort_finsetBasisIndex]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsNoetherian K V
⊢ Set.range (ι := ↥(finsetBasisIndex K V)) (⇑(finsetBasis K V) : (a : ↥(finsetBasisIndex K V)) → V) =
    Basis.ofVectorSpaceIndex K V
have rw : Set.range (ι := ↥(finsetBasisIndex K V))
    (⇑(Basis.reindex (Basis.ofVectorSpace K V) (Eq.mpr sorry (Equiv.refl (↑(Basis.ofVectorSpaceIndex K V) : Type v)))) :
      (a : ↥(finsetBasisIndex K V)) → V) =
  Basis.ofVectorSpaceIndex K V
Tactic: rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Set.range (ι := ↥(finsetBasisIndex K V)) (⇑(finsetBasis K V) : (a : ↥(finsetBasisIndex K V)) → V) =
    Basis.ofVectorSpaceIndex K V
have 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
Tactic: rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Set.range (ι := ↥(finsetBasisIndex K V)) (⇑(finsetBasis K V) : (a : ↥(finsetBasisIndex K V)) → V) =
    Basis.ofVectorSpaceIndex K V
have rw₂ : Basis.ofVectorSpaceIndex K V = Basis.ofVectorSpaceIndex K V
Tactic: rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Fintype.card V = Fintype.card K ^ finrank K V
have rw : Fintype.card K ^ Fintype.card.{v} ↥(finsetBasisIndex K V) = Fintype.card K ^ finrank K V
Tactic: rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Fintype.card V = Fintype.card K ^ finrank K V
have rw₁ : Fintype.card K ^ finrank K V = Fintype.card K ^ finrank K V
Tactic: rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Nat.card V = Nat.card K ^ finrank K V
have rw : Nat.card (↥(finsetBasisIndex K V) → K) = Nat.card K ^ finrank K V
Tactic: rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Nat.card V = Nat.card K ^ finrank K V
have rw₁ : Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V) = Nat.card K ^ finrank K V
Tactic: rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.FieldTheory.Finiteness (goal)
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
⊢ Nat.card V = Nat.card K ^ finrank K V
have rw₂ : Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V) = Nat.card K ^ Nat.card.{v} ↥(finsetBasisIndex K V)
Tactic: rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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 (HAdd.hAdd (β := S) x ((algebraMap K S : (a : K) → S) r : S))
    (HAdd.hAdd (β := S) y ((algebraMap K S : (a : K) → S) r : S))
have 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)))
Tactic: rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)))
⊢ 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))
have 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))
Tactic: rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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))
⊢ 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))
have 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]))
Tactic: rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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]))
⊢ 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))
have 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]))
Tactic: rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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
⊢ IsConjRoot K (-x) (-y)
have rw : Eq (α := K[X]) (minpoly K (-x)) (minpoly K (-y))
Tactic: rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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))
⊢ IsConjRoot K (-x) (-y)
have rw₁ : HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x)) * comp (minpoly K x) (-X) = minpoly K (-y)
Tactic: rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)
⊢ IsConjRoot K (-x) (-y)
have 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)
Tactic: rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)
⊢ IsConjRoot K (-x) (-y)
have 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)
Tactic: rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y
have 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
Tactic: rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y
have 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)
Tactic: rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y
have 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)
Tactic: rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsConjRoot (goal)
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)
⊢ IsConjRoot.{u_1, u_6} R (A := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) ↔ IsConjRoot R x y
have rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R y) ↔ Eq (α := R[X]) (minpoly R x) (minpoly R y)
Tactic: rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]