K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
⊢ lift (#ι) = lift (#ι')
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
⊢ lift (#ι) = lift (#ι')
haveI := nontrivial_of_invariantBasisNumber R
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Fintype ι
⊢ lift (#ι) = lift (#ι')

case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
⊢ lift (#ι) = lift (#ι')
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
⊢ lift (#ι) = lift (#ι')
cases fintypeOrInfinite ι
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Fintype ι
this : Fintype ↑(range ↑v)
⊢ lift (#ι) = lift (#ι')
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Fintype ι
⊢ lift (#ι) = lift (#ι')
haveI : Fintype (range v) := Set.fintypeRange v
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ lift (#ι) = lift (#ι')
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Fintype ι
this : Fintype ↑(range ↑v)
⊢ lift (#ι) = lift (#ι')
haveI := basisFintypeOfFiniteSpans _ v.span_eq v'
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ lift ↑(Fintype.card ι) = lift ↑(Fintype.card ι')
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ lift (#ι) = lift (#ι')
rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ Fintype.card ι = Fintype.card ι'
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ lift ↑(Fintype.card ι) = lift ↑(Fintype.card ι')
simp only [Cardinal.lift_natCast, Cardinal.natCast_inj]
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ (ι → R) ≃ₗ[R] ι' → R
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ Fintype.card ι = Fintype.card ι'
apply card_eq_of_linearEquiv R
no goals
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝¹ : Nontrivial R
val✝ : Fintype ι
this✝ : Fintype ↑(range ↑v)
this : Fintype ι'
⊢ (ι → R) ≃ₗ[R] ι' → R
exact
  (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
    Finsupp.linearEquivFunOnFinite R R ι'
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
⊢ lift (#ι) = lift (#ι')
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
⊢ lift (#ι) = lift (#ι')
have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
⊢ lift (#ι) = lift (#ι')
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
⊢ lift (#ι) = lift (#ι')
rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
this : Infinite ι'
⊢ lift (#ι) = lift (#ι')
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
⊢ lift (#ι) = lift (#ι')
haveI : Infinite ι' := Infinite.of_injective f f.2
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift (#ι') ≤ lift (#ι)
⊢ lift (#ι) = lift (#ι')
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
this : Infinite ι'
⊢ lift (#ι) = lift (#ι')
have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
no goals
case inr.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.266192
R : Type u
inst✝³ : Ring R
inst✝² : InvariantBasisNumber R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift (#ι) ≤ lift (#ι')
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift (#ι') ≤ lift (#ι)
⊢ lift (#ι) = lift (#ι')
exact le_antisymm w₁ w₂