awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
refine_1 : (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ) ⊆ (↑s : Set ℕ)
refine_2 refine_2₁ :
  ∀ (m : ℕ) (hm : m ∈ s),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
refine_2₂ :
  ∀ (m : ℕ) (hm : m ∈ s) (le : n ≤ m),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
refine_2₃ refine_2₄ :
  ∀ (m : ℕ) (hm : m ∈ s) (gt : m < n),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
⊢ s.FG

Tactic:
classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)

Premises used: le_or_gt, Submodule.subset_span
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : AddSubmonoid ℕ
rw : Submodule.FG (R := ℕ) (M := ℕ) ((AddSubmonoid.toNatSubmodule : (a : AddSubmonoid ℕ) → Submodule ℕ ℕ) s)
⊢ s.FG

Tactic:
rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]

Premises used: AddSubmonoid.toNatSubmodule_toAddSubmonoid, Submodule.fg_iff_addSubmonoid_fg
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : AddSubmonoid ℕ
⊢ Submodule.FG (R := ℕ) (M := ℕ) ((AddSubmonoid.toNatSubmodule : (a : AddSubmonoid ℕ) → Submodule ℕ ℕ) s)

Tactic:
apply IsNoetherian.noetherian

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : ∃ (n : ℕ), FrobeniusNumber n s
n : ℕ
hn : FrobeniusNumber n s
⊢ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
rw [frobeniusNumber_iff] at hn

Premises used: frobeniusNumber_iff
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : ∃ (n : ℕ), FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ n + 1 > n

Tactic:
lia
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : ∃ (n : ℕ), FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ n + 2 > n

Tactic:
lia
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : ∃ (n : ℕ), FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ setGcd s = 1 ∧ 1 ∉ s

Tactic:
exact ⟨dvd_one.mp <| Nat.dvd_add_iff_right (setGcd_dvd_of_mem_closure (hn.2 (n + 1)
      (by lia))) (n := 1) |>.mpr (setGcd_dvd_of_mem_closure (hn.2 (n + 2) (by lia))),
      fun h ↦ hn.1 <| AddSubmonoid.closure_mono (Set.singleton_subset_iff.mpr h)
        (addSubmonoidClosure_one.ge ⟨⟩)⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
have :
  ∀ (n : ℕ) (hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m),
    ∃ (n : ℕ), FrobeniusNumber n s
⊢ ∃ (n : ℕ), FrobeniusNumber n s

Tactic:
have ⟨n, hn⟩ := exists_mem_closure_of_ge s
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
⊢ P 1

Tactic:
have : P 1 := h.2 ∘ one_mem_closure_iff.mp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
⊢ ∃ (n : ℕ), FrobeniusNumber n s

Tactic:
⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩

Premises used: Iff.mpr, frobeniusNumber_iff, Nat.findGreatest_spec, Eq.dvd, le_of_not_gt, LT.lt.le, Nat.findGreatest, And.left, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ ∃ (n : ℕ), FrobeniusNumber n s

Tactic:
refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
inl : ∀ (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
inr : ∀ (le : n ≤ k), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
obtain le | le := le_total k n

Premises used: le_total
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
le : k ≤ n
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
of_not_not (findGreatest_is_greatest gt le)

Premises used: Nat.findGreatest_is_greatest, of_not_not
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
le : k ≤ n
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
exact of_not_not (findGreatest_is_greatest gt le)

Premises used: Nat.findGreatest_is_greatest, of_not_not
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
le : n ≤ k
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
hn k le (h.1.dvd.trans <| one_dvd k)

Premises used: Eq.dvd, one_dvd, And.left, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
le : n ≤ k
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
exact hn k le (h.1.dvd.trans <| one_dvd k)

Premises used: Eq.dvd, one_dvd, And.left, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
inl :
  ∀ (k : ℕ) (gt : k > findGreatest P n) (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
inr inr₁ :
  ∀ (k : ℕ) (gt : k > findGreatest P n) (le : n ≤ k), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ ∃ (n : ℕ), FrobeniusNumber n s

Tactic:
classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
rw :
  HMul.hMul (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K) x =
    HMul.hMul (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K) x
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x

Tactic:
rw [Algebra.smul_def, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a :
  Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K)
⊢ HMul.hMul (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K) x =
    HMul.hMul (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K) x

Tactic:
congr
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K)

Tactic:
congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c

Premises used: congr_fun
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a :
  Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K)

Tactic:
refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c

Premises used: congr_fun
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)

Tactic:
IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_

Premises used: nonZeroDivisors, IsLocalization.ext, Polynomial
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
e_a₁ : Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)
e_a₂ :
  ∀ (a b : F⟮X⟯),
    (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) (a * b) : Ft) =
      HMul.hMul (α := K) (β := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) a : Ft) : K)
        ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) b : Ft) : K)
e_a₃ :
  ∀ (a b : F⟮X⟯),
    (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) (a * b) =
      HMul.hMul (α := K) (β := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) a : K)
        ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) b : K)
e_a₄ :
  ∀ (a : F[X]),
    Eq.{u_2 + 1} (α := K)
      ((algebraMap Ft K : (a : Ft) → K)
          ((e : (a : F⟮X⟯) → Ft) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : Ft) :
        K)
      ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : K)
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)

Tactic:
refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_

Premises used: nonZeroDivisors, IsLocalization.ext, Polynomial
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, map_mul, map_one, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, map_mul, map_one, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a b : F⟮X⟯
⊢ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) (a * b) : Ft) =
    HMul.hMul (α := K) (β := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) a : Ft) : K)
      ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) b : Ft) : K)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, map_mul, map_one, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a b : F⟮X⟯
⊢ (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) (a * b) =
    HMul.hMul (α := K) (β := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) a : K)
      ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) b : K)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, map_mul, map_one, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a : F[X]
⊢ Eq.{u_2 + 1} (α := K)
    ((algebraMap Ft K : (a : Ft) → K)
        ((e : (a : F⟮X⟯) → Ft) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : Ft) :
      K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : K)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, map_mul, map_one, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
⊢ ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x

Tactic:
have : ∀ (c) (x : K), e c • x = c • x := by
    intro c x
    rw [Algebra.smul_def, Algebra.smul_def]
    congr
    refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c
    refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
      simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
mp : FunctionField F K → FiniteDimensional Ft K
mpr : FiniteDimensional Ft K → FunctionField F K
⊢ FunctionField F K ↔ FiniteDimensional Ft K

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FunctionField F K
b : Module.Basis.{0, u_1, u_2} (Fin (Module.finrank.{u_1, u_2} F⟮X⟯ K)) F⟮X⟯ K := Module.finBasis F⟮X⟯ K
⊢ FiniteDimensional Ft K

Tactic:
(b.mapCoeffs e this).finiteDimensional_of_finite

Premises used: Module.Basis.mapCoeffs, Module.Basis.finiteDimensional_of_finite
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FunctionField F K
b : Module.Basis.{0, u_1, u_2} (Fin (Module.finrank.{u_1, u_2} F⟮X⟯ K)) F⟮X⟯ K := Module.finBasis F⟮X⟯ K
⊢ FiniteDimensional Ft K

Tactic:
exact (b.mapCoeffs e this).finiteDimensional_of_finite

Premises used: Module.Basis.mapCoeffs, Module.Basis.finiteDimensional_of_finite
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
⊢ FunctionField F K

Tactic:
(b.mapCoeffs e.symm ?_).finiteDimensional_of_finite

Premises used: Module.Basis.mapCoeffs, Module.Basis.finiteDimensional_of_finite
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
mpr :
  ∀ (c : Ft) (x : K),
    HSMul.hSMul.{u_1, u_2, u_2} (α := F⟮X⟯) ((e.symm.toRingEquiv : (a : Ft) → F⟮X⟯) c : F⟮X⟯) x = c • x
⊢ FunctionField F K

Tactic:
refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite

Premises used: Module.Basis.mapCoeffs, Module.Basis.finiteDimensional_of_finite