awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
rwa :
  ∀ (this : (Polynomial.map Polynomial.C (Q₂ h)).natDegree + (Φ E).natDegree = (θ E).natDegree),
    (Φ E).natDegree = (θ E).natDegree
rwa₁ : ∀ (this : (Q₂ h).natDegree + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
rwa₂ : ∀ (this : 0 + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
⊢ (Φ E).natDegree = (θ E).natDegree

Tactic:
rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_map, _private.0.RatFunc.Luroth.Q₂_natDegree, zero_add, _private.0.RatFunc.Luroth.Q₂_ne_zero, Polynomial.map_ne_zero, _private.0.RatFunc.Luroth.Φ_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ natDegree.{u_1} (R := K[X])
      ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
        (Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E)) =
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))

Tactic:
have := congr((Bivariate.swap $(Q₃_mul_Φ h)).natDegree)
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
pos : ∀ (h : E = ⊥), E = K⟮generator E⟯
neg : ∀ (h : ¬E = ⊥), E = K⟮generator E⟯
⊢ E = K⟮generator E⟯

Tactic:
by_cases h : E = ⊥
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
pos : E = K⟮0⟯
pos₁ pos₂ pos₃ pos₄ : E = ⊥
⊢ E = K⟮generator E⟯

Tactic:
rwa [generator_eq_zero h, adjoin_zero]

Premises used: IntermediateField.adjoin_zero, RatFunc.Luroth.generator_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ E = K⟮generator E⟯

Tactic:
le_antisymm (relfinrank_eq_one_iff.mp ?_) adjoin_generator_le

Premises used: le_antisymm, Iff.mp, RatFunc.Luroth.adjoin_generator_le, IntermediateField.relfinrank_eq_one_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
neg : relfinrank K⟮generator E⟯ E = 1
⊢ E = K⟮generator E⟯

Tactic:
refine le_antisymm (relfinrank_eq_one_iff.mp ?_) adjoin_generator_le

Premises used: le_antisymm, Iff.mp, RatFunc.Luroth.adjoin_generator_le, IntermediateField.relfinrank_eq_one_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
⊢ relfinrank K⟮generator E⟯ E = 1

Tactic:
(mul_eq_right₀ ?_).mp <| this ▸ (generator E).finrank_eq_max_natDegree ▸
      φ_natDegree h ▸ relfinrank_mul_finrank_top (adjoin_generator_le (E := E))

Premises used: mul_eq_right₀, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
refine : m E ≠ 0
⊢ relfinrank K⟮generator E⟯ E = 1

Tactic:
refine (mul_eq_right₀ ?_).mp <| this ▸ (generator E).finrank_eq_max_natDegree ▸
      φ_natDegree h ▸ relfinrank_mul_finrank_top (adjoin_generator_le (E := E))

Premises used: mul_eq_right₀, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
H : m E = 0
⊢ False

Tactic:
generator_ne_C h ((eq_C_iff _).mpr (Nat.max_eq_zero_iff.mp H))

Premises used: Iff.mpr, RatFunc.Luroth.generator_ne_C, Nat.max_eq_zero_iff, Iff.mp, RatFunc.eq_C_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
H : m E = 0
⊢ False

Tactic:
exact generator_ne_C h ((eq_C_iff _).mpr (Nat.max_eq_zero_iff.mp H))

Premises used: Iff.mpr, RatFunc.Luroth.generator_ne_C, Nat.max_eq_zero_iff, Iff.mp, RatFunc.eq_C_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
neg : (φ E).natDegree = m E
⊢ relfinrank K⟮generator E⟯ E = 1

Tactic:
suffices (φ E).natDegree = m E by
    refine (mul_eq_right₀ ?_).mp <| this ▸ (generator E).finrank_eq_max_natDegree ▸
      φ_natDegree h ▸ relfinrank_mul_finrank_top (adjoin_generator_le (E := E))
    intro H
    exact generator_ne_C h ((eq_C_iff _).mpr (Nat.max_eq_zero_iff.mp H))
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
neg : (θ E).natDegree = m E
⊢ (φ E).natDegree = m E

Tactic:
rw [← Φ_natDegree_eq_φ_natDegree h, Φ_natDegree_eq_θ_natDegree h]

Premises used: _private.0.RatFunc.Luroth.Φ_natDegree_eq_θ_natDegree, _private.0.RatFunc.Luroth.Φ_natDegree_eq_φ_natDegree
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ (θ E).natDegree = m E

Tactic:
le_antisymm (θ_natDegree_le h) (swap_Φ_natDegree_eq_θ_natDegree h ▸ m_le_swap_Φ_natDegree h)

Premises used: _private.0.RatFunc.Luroth.m_le_swap_Φ_natDegree, Eq.rec, _private.0.RatFunc.Luroth.θ_natDegree_le, le_antisymm, _private.0.RatFunc.Luroth.swap_Φ_natDegree_eq_θ_natDegree
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ (θ E).natDegree = m E

Tactic:
exact le_antisymm (θ_natDegree_le h) (swap_Φ_natDegree_eq_θ_natDegree h ▸ m_le_swap_Φ_natDegree h)

Premises used: _private.0.RatFunc.Luroth.m_le_swap_Φ_natDegree, Eq.rec, _private.0.RatFunc.Luroth.θ_natDegree_le, le_antisymm, _private.0.RatFunc.Luroth.swap_Φ_natDegree_eq_θ_natDegree
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
g : K[X]
⊢ Eq (α := K⟮X⟯) ((↑((algEquiv h : (a : K⟮X⟯) → ↥E) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) g)) : K⟮X⟯) : K⟮X⟯)
    ((aeval (generator E) : (a : K[X]) → K⟮X⟯) g : K⟮X⟯)

Tactic:
simp [algEquiv]

Premises used: RatFunc.Luroth.algEquiv
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (↑((algEquiv h : (a : K⟮X⟯) → ↥E) X) : K⟮X⟯) = generator E

Tactic:
simp [algEquiv]

Premises used: RatFunc.Luroth.algEquiv
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
u : K⟮X⟯
⊢ (↑((algEquiv h : (a : K⟮X⟯) → ↥E) u) : K⟮X⟯) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((aeval (generator E) : (a : K[X]) → K⟮X⟯) u.num : K⟮X⟯)
      ((aeval (generator E) : (a : K[X]) → K⟮X⟯) u.denom : K⟮X⟯)

Tactic:
simp [algEquiv, algEquivOfTranscendental_apply]

Premises used: RatFunc.Luroth.algEquiv, RatFunc.algEquivOfTranscendental_apply
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
⊢ inftyValuationDef F 0 = 0

Tactic:
if_pos rfl

Premises used: if_pos, RatFunc.inftyValuationDef, rfl
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
⊢ exp (intDegree.{u_1} (K := F) 1) = 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0 else exp (x * y).intDegree) =
      (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
neg :
  ∀ (hx : ¬x = 0),
    (if x * y = 0 then 0 else exp (x * y).intDegree) =
      (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
pos :
  (if 0 * y = 0 then 0 else exp (0 * y).intDegree) =
    (if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)) *
      if y = 0 then 0 else exp y.intDegree
pos₁ :
  (if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)) =
    (if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)) *
      if y = 0 then 0 else exp y.intDegree
pos₂ : 0 = 0 * if y = 0 then 0 else exp y.intDegree
pos₃ pos₄ : Eq (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]

Premises used: MulZeroClass.zero_mul, if_pos, Eq.refl
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    (if x * y = 0 then 0 else exp (x * y).intDegree) =
      (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
neg :
  ∀ (hy : ¬y = 0),
    (if x * y = 0 then 0 else exp (x * y).intDegree) =
      (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
pos :
  (if x * 0 = 0 then 0 else exp (x * 0).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) *
      if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)
pos₁ :
  (if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)) =
    (if x = 0 then 0 else exp x.intDegree) *
      if Eq.{u_1 + 1} (α := F⟮X⟯) 0 0 then 0 else exp (intDegree.{u_1} (K := F) 0)
pos₂ : 0 = (if x = 0 then 0 else exp x.intDegree) * 0
pos₃ pos₄ : Eq (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]

Premises used: if_pos, MulZeroClass.mul_zero, Eq.refl
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
simp_all [RatFunc.intDegree_mul]

Premises used: RatFunc.intDegree_mul
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
unfold :
  (if x + y = 0 then 0 else exp (x + y).intDegree) ≤
    max (if x = 0 then 0 else exp x.intDegree) (if y = 0 then 0 else exp y.intDegree)
⊢ inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y)

Tactic:
unfold inftyValuationDef

Premises used: RatFunc.inftyValuationDef
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ ∀ [inst : Field F] {x y : F⟮X⟯} (hy : y ≠ 0) (hxy : x + y ≠ 0), (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
have := @RatFunc.intDegree_add_le F
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x y : F⟮X⟯
this : ∀ [inst : Field F] {x y : F⟮X⟯} (hy : y ≠ 0) (hxy : x + y ≠ 0), (x + y).intDegree ≤ max x.intDegree y.intDegree
⊢ (if x + y = 0 then 0 else exp (x + y).intDegree) ≤
    max (if x = 0 then 0 else exp x.intDegree) (if y = 0 then 0 else exp y.intDegree)

Tactic:
aesop
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x : F⟮X⟯
hx : x ≠ 0
rw : (if x = 0 then 0 else exp x.intDegree) = exp x.intDegree
rw₁ rw₂ : exp x.intDegree = exp x.intDegree
⊢ inftyValuationDef F x = exp x.intDegree

Tactic:
rw [inftyValuationDef, if_neg hx]

Premises used: RatFunc.inftyValuationDef, if_neg
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x : F⟮X⟯
⊢ ((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ)) x =
    inftyValuationDef F x

Tactic:
rfl

Premises used: RatFunc.inftyValuationDef, rfl, ite
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
k : F
hk : k ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        ((RatFunc.C : (a : F) → F⟮X⟯) k) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [inftyValuation_apply, hk]

Premises used: RatFunc.inftyValuation_apply
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X :
      WithZero (Multiplicative ℤ))
    (exp 1 : WithZero (Multiplicative ℤ))

Tactic:
simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]

Premises used: RatFunc.X_ne_zero, RatFunc.inftyValuation_apply, RatFunc.intDegree_X, RatFunc.inftyValuationDef, if_neg
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
m : ℤ
⊢ ((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := F⟮X⟯) RatFunc.X m) =
    exp m

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X⁻¹ :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := F⟮X⟯) (β := ℤ) RatFunc.X (-1)) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₂ rw₃ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-1)) (exp (-1))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := F⟮X⟯) 1 RatFunc.X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]

Premises used: zpow_neg_one, RatFunc.inftyValuation.X_zpow, one_div
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
⊢ ¬Eq (α := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯) (0 : F⟮X⟯)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
rw :
  (if Eq (α := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯) (0 : F⟮X⟯) then 0
    else exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p))) =
    exp (↑p.natDegree : ℤ)
rw₁ : exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p)) = exp (↑p.natDegree : ℤ)
rw₂ rw₃ : Eq (α := WithZero (Multiplicative ℤ)) (exp (↑p.natDegree : ℤ)) (exp (↑p.natDegree : ℤ))
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p) = exp (↑p.natDegree : ℤ)

Tactic:
rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]

Premises used: RatFunc.intDegree_polynomial, RatFunc.inftyValuationDef, if_neg
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : DecidableEq F⟮X⟯
⊢ Ne (α := WithZero (Multiplicative ℤ))
      (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
          X :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ∧
    Ne (α := WithZero (Multiplicative ℤ))
      (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
          X :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : DecidableEq F⟮X⟯
x : F
hx : x ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        ((algebraMap F F⟮X⟯ : (a : F) → F⟮X⟯) x) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [inftyValuation.C _ hx]

Premises used: RatFunc.inftyValuation.C
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x : F⟮X⟯
⊢ ((Valued.v : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ)) x =
    inftyValuationDef F x

Tactic:
rfl

Premises used: RatFunc.inftyValuationDef, rfl, ite
-- Module: Mathlib.FieldTheory.RatFunc.Valuation
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
x : CompletionAtInfty F
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (CompletionAtInfty F) (WithZero (Multiplicative ℤ))) :
          (a : CompletionAtInfty F) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((Valued.extensionValuation.{u_1, 0} (K := F⟮X⟯) :
            Valuation (UniformSpace.Completion F⟮X⟯) (WithZero (Multiplicative ℤ))) :
          (a : UniformSpace.Completion F⟮X⟯) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ A.relfinrank B = (toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B)

Tactic:
rfl

Premises used: Subfield.relrank, Subfield.relfinrank, Module.finrank, rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ Module.rank ↥(A ⊓ C) ↥(extendScalars ⋯) = Module.rank ↥(B ⊓ C) ↥(extendScalars ⋯)

Tactic:
congr!
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ A.relfinrank C = B.relfinrank C

Tactic:
congr(toNat $(relrank_eq_of_inf_eq h))

Premises used: congrArg, Cardinal.toNat, Subfield.relrank_eq_of_inf_eq, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A ⊓ B = A

Tactic:
have := inf_of_le_left h
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
this : A ⊓ B = A
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)

Tactic:
congr!
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relfinrank B = finrank.{v, v} ↥A ↥(extendScalars h)

Tactic:
congr(toNat $(relrank_eq_rank_of_le h))

Premises used: congrArg, Cardinal.toNat, id, Subfield.relrank_eq_rank_of_le, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ (A ⊓ B).relrank B = A.relrank B

Tactic:
relrank_eq_rank_of_le (inf_le_right : A ⊓ B ≤ B)

Premises used: Subfield.relrank, Set.Mem, inf_le_right, Subfield.relrank_eq_rank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ (A ⊓ B).relfinrank B = A.relfinrank B

Tactic:
congr(toNat $(inf_relrank_right A B))

Premises used: congrArg, Cardinal.toNat, id, DFunLike.coe, Subfield.inf_relrank_right
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : (B ⊓ A).relrank A = B.relrank A
rw₁ rw₂ : B.relrank A = B.relrank A
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

Premises used: inf_comm, Subfield.inf_relrank_right
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ (A ⊓ B).relfinrank A = B.relfinrank A

Tactic:
congr(toNat $(inf_relrank_left A B))

Premises used: Subfield.inf_relrank_left, congrArg, Cardinal.toNat, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
rw : Module.rank ↥A ↥(extendScalars ⋯) = 1
rw₁ : Module.rank ↥A ↥⊥ = 1
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
⊢ A.relrank A = 1

Tactic:
rw [relrank_eq_rank_of_le (le_refl A), extendScalars_self, IntermediateField.rank_bot]

Premises used: le_refl, IntermediateField.rank_bot, Subfield.relrank_eq_rank_of_le, Subfield.extendScalars_self
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
⊢ A.relfinrank A = 1

Tactic:
simp [relfinrank_eq_toNat_relrank]

Premises used: Subfield.relfinrank_eq_toNat_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₄ : B = RingHom.fieldRange (K := ↥(A ⊓ B)) (algebraMap (↥(A ⊓ B)) E) ↔ B ≤ A
rw₅ : B = (A ⊓ B).subtype.fieldRange ↔ B ≤ A
rw₆ : B = A ⊓ B ↔ B ≤ A
rw₇ rw₈ : B ≤ A ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A

Tactic:
rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]

Premises used: Subfield.relrank, Subfield.extendScalars_toSubfield, Subfield.algebraMap_ofSubfield, Subfield.fieldRange_subtype, IntermediateField.toSubfield_inj, IntermediateField.rank_eq_one_iff, IntermediateField.bot_toSubfield, right_eq_inf
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B) : ℕ) (1 : ℕ) ↔ B ≤ A
rw₁ : A.relrank B = 1 ↔ B ≤ A
rw₂ rw₃ : B ≤ A ↔ B ≤ A
⊢ A.relfinrank B = 1 ↔ B ≤ A

Tactic:
rw [relfinrank_eq_toNat_relrank, toNat_eq_one, relrank_eq_one_iff]

Premises used: Cardinal.toNat_eq_one, Subfield.relfinrank_eq_toNat_relrank, Subfield.relrank_eq_one_iff
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
rw : Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le h]

Premises used: Subfield.relrank_eq_rank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ IsScalarTower (↥A) (↥B) E

Tactic:
haveI : IsScalarTower A B E := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
this_1 : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower (↥A) (↥B) E
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
rank_mul_rank A B E

Premises used: Set.Mem, rank_mul_rank, Membership.mem, Subtype, Subfield.extendScalars, Subfield.toIntermediateField
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
this_1 : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower (↥A) (↥B) E
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
exact rank_mul_rank A B E

Premises used: rank_mul_rank, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relfinrank B * finrank (↥B) E = finrank (↥A) E

Tactic:
simpa using congr(toNat $(relrank_mul_rank_top h))