internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) (ζ ^ i) = (ζ ^ i)⁻¹
Tactic:
simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg]
Proof state after:
no goals
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
letI : NumberField K := IsCyclotomicExtension.numberField { p } ℚ _
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
have : Fact (p : ℕ).Prime := ⟨hp⟩
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨k, H⟩ := unit_inv_conj_is_root_of_unity hζ hpodd hp u
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
refine' ⟨k, _⟩
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
rw [← exists_int_sum_eq_zero'_aux, h, ← H, Units.val_mul, mul_assoc, ← mul_sub, _root_.map_mul,
  ← coe_unitGalConj, ← mul_assoc, ← Units.val_mul, inv_mul_self, Units.val_one, one_mul]
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑u * (α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑u * (α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)) ∈ Ideal.span {↑↑p}
Tactic:
exact Ideal.mul_mem_left _ _ (pow_sub_intGalConj_mem hp α)
Proof state after:
no goals
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨k, hk⟩ := exists_int_sum_eq_zero' hζ hpodd hp x y i h
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
use k
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * ↑k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * ↑k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
convert hk
Proof state after:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ hζ.unit' ^ (2 * ↑k) = (hζ.unit' ^ k) ^ 2
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero
Proof state before:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ hζ.unit' ^ (2 * ↑k) = (hζ.unit' ^ k) ^ 2
Tactic:
rw [mul_comm, zpow_mul, zpow_ofNat]
Proof state after:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ (hζ.unit' ^ ↑k) ^ 2 = (hζ.unit' ^ k) ^ 2
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero
Proof state before:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ (hζ.unit' ^ ↑k) ^ 2 = (hζ.unit' ^ k) ^ 2
Tactic:
rfl
Proof state after:
no goals
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
by_cases H : finrank R M = 0
Proof state after:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
haveI := nonempty_linearIndependent_set R M
Proof state after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
have := (Cardinal.toNat_eq_iff H).mp rfl
Proof state after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : Module.rank R M = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : Module.rank R M = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
rw [Module.rank_def] at this
Proof state after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
obtain ⟨⟨s, hs⟩, hι : #s = _⟩ :=
  Cardinal.exists_eq_natCast_of_iSup_eq _ (Cardinal.bddAbove_range.{v, v} _) _ this
Proof state after:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
have : Finite s := Cardinal.lt_aleph0_iff_finite.mp (hι ▸ nat_lt_aleph0 (finrank R M))
Proof state after:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
cases nonempty_fintype s
Proof state after:
case neg.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case neg.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
exact ⟨s.toFinset,
  Cardinal.natCast_injective (by rwa [Set.toFinset_card, ← Cardinal.mk_fintype]),
  by convert hs <;> simp only [Set.mem_toFinset]⟩
Proof state after:
no goals
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
use ∅
Proof state after:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∅.card = finrank R M ∧ LinearIndependent R Subtype.val
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∅.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
simp only [Finset.card_empty, H, linearIndependent_empty_type, and_self]
Proof state after:
no goals
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ↑s.toFinset.card = ↑(finrank R M)
Tactic:
rwa [Set.toFinset_card, ← Cardinal.mk_fintype]
Proof state after:
no goals
Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent
Proof state before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndependent R Subtype.val
Tactic:
convert hs <;> simp only [Set.mem_toFinset]
Proof state after:
no goals
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨s, hs, hs'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R N
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨t, ht, ht'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R (M ⧸ N)
Proof state after:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
obtain ⟨f, hf⟩ := N.mkQ_surjective.hasRightInverse
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Theorem: FiniteDimensional.finrank_add_finrank_quotient_le
Proof state before:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
Tactic:
have H : Disjoint (Submodule.span R (Subtype.val '' (s : Set N))) (Submodule.span R (f '' t)) := by
  apply Disjoint.mono_left (Submodule.span_le.mpr Set.image_val_subset)
  rw [disjoint_iff, eq_bot_iff, ← @Subtype.range_val (M ⧸ N) t, ← Set.range_comp,
    ← Finsupp.range_total]
  rintro _ ⟨h, l, rfl⟩
  rw [SetLike.mem_coe, ← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
    Finsupp.apply_total, ← Function.comp.assoc, show N.mkQ ∘ f = id from funext hf] at h
  rw [linearIndependent_iff.mp ht' l h, map_zero]
  exact zero_mem _
Proof state after:
case intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
t : Finset (M ⧸ N)
ht : t.card = finrank R (M ⧸ N)
ht' : LinearIndependent R Subtype.val
f : M ⧸ N → M
hf : Function.RightInverse f ⇑N.mkQ
H : Disjoint (Submodule.span R (Subtype.val '' ↑s)) (Submodule.span R (f '' ↑t))
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M