-- Mathlib/FieldTheory/MvRatFunc/Rank.lean
theorem MvRatFunc.rank_eq_max_lift
    {σ : Type u} {F : Type v} [Field F] [Nonempty σ] :
    Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u} #F ⊔ lift.{v} #σ ⊔ ℵ₀

Proof state:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank

Result:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : Module.rank F R ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
rw [MvPolynomial.rank_eq_lift, mk_finsupp_nat, lift_max, lift_aleph0, max_le_iff] at h1

Result:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
obtain ⟨i⟩ := ‹Nonempty σ›

Result:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
let R := MvPolynomial σ F

Result:
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Proof state:
case refine_1
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ #(FractionRing (MvPolynomial σ F)) ≤ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]

Result:
no goals

Proof state:
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
refine ((rank_le_card _ _).trans ?_).antisymm ?_

Result:
case refine_1
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ #(FractionRing (MvPolynomial σ F)) ≤ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{u, v} #F ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
exact max_le (max_le h2 h1.1) h1.2

Result:
no goals

Proof state:
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
let K := FractionRing R

Result:
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀

Proof state:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
rw [lift_id'.{v, u}, lift_umax.{v, u}] at h2

Result:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{u, v} #F ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
have hinj := IsFractionRing.injective R K

Result:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Proof state:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
have hx : Transcendental F (algebraMap R K (MvPolynomial.X i)) :=
  (transcendental_algebraMap_iff hinj).2 (MvPolynomial.transcendental_X F i)

Result:
case refine_2.intro
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))