case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
⊢ False

case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
⊢ n ≤ m
R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
refine' ⟨fun h n => fun f hf => _, fun h => ⟨@fun n m f hf => _⟩⟩
case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
this : StrongRankCondition R := h
⊢ False
case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
⊢ False
letI : StrongRankCondition R := h
no goals
case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
this : StrongRankCondition R := h
⊢ False
exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)
case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
H : ¬n ≤ m
⊢ False
case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
⊢ n ≤ m
by_contra H
no goals
case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
H : ¬n ≤ m
⊢ False
exact
  h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
    (hf.comp (Function.extend_injective (RelEmbedding.injective _) _))