awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' Set.univ)) ≤ n
rw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' (↑Finset.univ : Set ι))) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw₂ : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
Tactic: classical
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  rw [← Finset.card_univ] at hc
  exact finrank_vectorSpan_image_finset_le _ _ _ hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' Set.univ)) ≤ n
rw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k (p '' (↑Finset.univ : Set ι))) ≤ n
rw₂ rw₃ rw₄ : finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw₅ : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p Finset.univ) : Set P)) ≤ n
Tactic: classical
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  rw [← Finset.card_univ] at hc
  exact finrank_vectorSpan_image_finset_le _ _ _ hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have hn : Nonempty ι
Tactic: have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
hn : Nonempty ι
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have obtain : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
Tactic: obtain ⟨i₁⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have rw : finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
    Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
have rw : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: rw [← Finset.card_univ] at hc
Cleared hypotheses: hc, i₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1
i₁ : ι
⊢ finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
have rw : finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
    Finset.card.{u_4} (α := ι) {x : ι | x ≠ i₁} ↔
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: rw [Fintype.subtype_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have : Nonempty ι
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₂ : Nonempty ι
have₃ have₄ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have₅ : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₂ : Nonempty ι
have₃ have₄ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₅ : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have₆ : ∀ (i₁ : ι),
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₂ : Nonempty ι
have₃ have₄ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₅ : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₆ :
  ∀ (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have₇ : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
have : Nonempty ι
have₁ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₂ : Nonempty ι
have₃ have₄ : ∀ (hn : Nonempty ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₅ : ∀ (i₁ : ι), AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have₆ :
  ∀ (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
have₇ :
  ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
        Fintype.card.{u_4} { x : ι // x ≠ i₁ } ↔
      finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
⊢ AffineIndependent k p ↔ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
have have₈ : ∀ (hc : Finset.card.{u_4} (α := ι) Finset.univ = n + 1) (i₁ : ι),
  finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) =
      Finset.card.{u_4} (α := ι) {x : ι | x ≠ i₁} ↔
    finrank.{u_1, u_2} k ↥(Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₁ }) ↦ p (↑i : ι) -ᵥ p i₁)) = n
Tactic: classical
  have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
Tactic: rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
have mp : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n → n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
mp : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n → n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
have mpr : n ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) → finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
⊢ AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw : n + 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
Tactic: rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
rw :
  n + 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
⊢ AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw₁ : n < finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
Tactic: rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
rw :
  n + 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
rw₁ : n < finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
⊢ AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
have rw₂ : ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ n
Tactic: rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
have inl : IsEmpty ι → Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
inl : IsEmpty ι → Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
have inr : Nonempty ι → Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
h : Nonempty ι
⊢ Fintype.card ι ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) + 1
have inr : Fintype.card ι - 1 ≤ finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p))
Tactic: rw [← tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
⊢ #s ≤ #t
have inl : ∀ (hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x)))
  (hst : (↑∅ : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)), card.{u_2} (α := V) ∅ ≤ #t
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
inl :
  ∀ (hs : AffineIndependent k (P := V) (ι := ↥∅) (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Finset V) ∅ x)))
    (hst : (↑∅ : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)), card.{u_2} (α := V) ∅ ≤ #t
⊢ #s ≤ #t
have inr : ∀ (hs' : s.Nonempty), #s ≤ #t
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
⊢ #s ≤ #t
have inr : ∀ (hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑∅ : Set V)) : Set V)), #s ≤ card.{u_2} (α := V) ∅
Tactic: obtain rfl | ht' := t.eq_empty_or_nonempty
Cleared hypotheses: t, hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
inr : ∀ (hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑∅ : Set V)) : Set V)), #s ≤ card.{u_2} (α := V) ∅
⊢ #s ≤ #t
have inr₁ : ∀ (ht' : t.Nonempty), #s ≤ #t
Tactic: obtain rfl | ht' := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
⊢ #s ≤ #t
have this : Nonempty.{u_2 + 1} ↥s
Tactic: have := hs'.to_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty.{u_2 + 1} ↥s
⊢ #s ≤ #t
have this₁ : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
Tactic: have := ht'.to_set.to_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
s t : Finset V
hs : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
hst : (↑s : Set V) ⊆ (↑(affineSpan k (↑t : Set V)) : Set V)
hs' : s.Nonempty
ht' : t.Nonempty
this_1 : Nonempty.{u_2 + 1} ↥s
this : Nonempty.{u_2 + 1} (↑(↑t : Set V) : Type u_2)
⊢ #s ≤ #t
have direction_le : LE.le (α := Submodule k V) (direction (affineSpan k (↑s : Set V)))
  (direction (affineSpan k (↑(affineSpan k (↑t : Set V)) : Set V)))
Tactic: have direction_le := AffineSubspace.direction_le (affineSpan_mono k hst)