-- Mathlib/RingTheory/Artinian/Module.lean
theorem IsArtinian.finite_of_linearIndependent [Nontrivial R] [h : IsArtinian R M] {s : Set M}
    (hs : LinearIndependent R ((↑) : s → M)) : s.Finite

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
⊢ s.Finite

Tactic:
refine by_contradiction fun hf ↦ (RelEmbedding.wellFounded_iff_no_descending_seq.1 h.wf).elim' ?_

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
⊢ (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
x y : ℕ
⊢ (fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m})) x = (fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m})) y → x = y

Tactic:
rw [le_antisymm_iff, ← this y x, ← this x y]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
x y : ℕ
⊢ y ≤ x ∧ x ≤ y → x = y

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})

Tactic:
rw [span_le_span_iff hs (this b) (this a),
  Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective), Set.subset_def]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ ∀ x ∈ {m | b ≤ m}, x ∈ {m | a ≤ m}

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
⊢ (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2

Tactic:
have : ∀ n, (↑) ∘ f '' { m | n ≤ m } ⊆ s := by
  rintro n x ⟨y, _, rfl⟩
  exact (f y).2

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
⊢ (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
⊢ ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})

Tactic:
intro a b

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
a b : ℕ
⊢ a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
a b : ℕ
⊢ { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } a <
      { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } b ↔
    a > b

Tactic:
conv_rhs => rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
a b : ℕ
⊢ { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } a <
      { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } b ↔
    span R (Subtype.val ∘ ⇑f '' {m | a ≤ m}) < span R (Subtype.val ∘ ⇑f '' {m | b ≤ m})

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
⊢ (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2

Tactic:
exact ⟨⟨fun n ↦ span R (Subtype.val ∘ f '' { m | n ≤ m }), fun x y ↦ by
  rw [le_antisymm_iff, ← this y x, ← this x y]
  exact fun ⟨h₁, h₂⟩ ↦ le_antisymm_iff.2 ⟨h₂, h₁⟩⟩, by
  intro a b
  conv_rhs => rw [GT.gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le]
  rfl⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
n y : ℕ
left✝ : y ∈ {m | n ≤ m}
⊢ (Subtype.val ∘ ⇑f) y ∈ s

Tactic:
exact (f y).2

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
⊢ ∀ {a b : ℕ},
    { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } a <
        { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } b ↔
      a > b

Tactic:
intro a b

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent R Subtype.val
hf : ¬s.Finite
f : ℕ ↪ ↑s
this✝ : ∀ (n : ℕ), Subtype.val ∘ ⇑f '' {m | n ≤ m} ⊆ s
this : ∀ (a b : ℕ), a ≤ b ↔ span R (Subtype.val ∘ ⇑f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ ⇑f '' {m | a ≤ m})
a b : ℕ
⊢ { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } a <
      { toFun := fun n => span R (Subtype.val ∘ ⇑f '' {m | n ≤ m}), inj' := ⋯ } b ↔
    a > b