awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
apply apply₁ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
apply₂ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) :
        R₂)
apply₃ apply₄ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂)
      (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) :
        R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
apply₅ :
  ∀ (j : ι),
    HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) (if j = i then 1 else 0) =
      HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) (if j = i then 1 else 0)
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

Tactic:
classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]

Premises used: LinearMap.smul_apply, Module.Basis.unitsSMul, Units.smul_def, Finsupp.single_apply, Module.Basis.ext, Module.Basis.coord_apply, SemigroupAction.mul_smul, Module.Basis.repr_self, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
v : M
i : ι
⊢ ((((e.unitsSMul w).repr : (a : M) → ι →₀ R₂) v : ι →₀ R₂) : (a : ι) → R₂) i =
    HSMul.hSMul (β := R₂) (w i)⁻¹ ((((e.repr : (a : M) → ι →₀ R₂) v : ι →₀ R₂) : (a : ι) → R₂) i : R₂)

Tactic:
congr_arg (fun f : M →ₗ[R₂] R₂ => f v) (e.coord_unitsSMul w i)

Premises used: congr_arg, DFunLike.coe, Module.Basis.coord_unitsSMul
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : Basis ι R M
w : ι → R
hw : ∀ (i : ι), IsUnit (w i)
i : ι
⊢ (v.isUnitSMul hw : (a : ι) → M) i = HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)

Tactic:
unitsSMul_apply i

Premises used: Module.Basis.unitsSMul_apply
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
v : Basis ι R₂ M
w : ι → R₂
hw : ∀ (i : ι), IsUnit (w i)
x : M
i : ι
⊢ ((((v.isUnitSMul hw).repr : (a : M) → ι →₀ R₂) x : ι →₀ R₂) : (a : ι) → R₂) i =
    HSMul.hSMul (β := R₂) ⋯.unit⁻¹ ((((v.repr : (a : M) → ι →₀ R₂) x : ι →₀ R₂) : (a : ι) → R₂) i : R₂)

Tactic:
repr_unitsSMul _ _ _ _

Premises used: Module.Basis.repr_unitsSMul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Submodule R M
b : Basis.{u_1, u_3, u_5} ι R ↥P
x : M
rw :
  Membership.mem (γ := Submodule R M)
    (LinearMap.range (M := ι →₀ R)
      (linearCombination R (comp (β := ↥P) (⇑P.subtype : (a : ↥P) → M) (⇑b : (a : ι) → ↥P))))
    x
| x ∈ P

Tactic:
rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]

Premises used: Set.range_comp, Submodule.map_top, Finsupp.range_linearCombination, Submodule.map_span, Module.Basis.span_eq, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Submodule R M
b : Basis.{u_1, u_3, u_5} ι R ↥P
x : M
conv_lhs :
  Membership.mem (γ := Submodule R M)
      (LinearMap.range (M := ι →₀ R)
        (linearCombination R (comp (β := ↥P) (⇑P.subtype : (a : ↥P) → M) (⇑b : (a : ι) → ↥P))))
      x ↔
    ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul (β := M) x (↑((b : (a : ι) → ↥P) i) : M)
⊢ x ∈ P ↔ ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul (β := M) x (↑((b : (a : ι) → ↥P) i) : M)

Tactic:
conv_lhs =>
    rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]

Premises used: Set.range_comp, Submodule.map_top, Finsupp.range_linearCombination, Submodule.map_span, Module.Basis.span_eq, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Submodule R M
b : Basis.{u_1, u_3, u_5} ι R ↥P
x : M
⊢ Membership.mem (γ := Submodule R M)
      (LinearMap.range (M := ι →₀ R)
        (linearCombination R (comp (β := ↥P) (⇑P.subtype : (a : ↥P) → M) (⇑b : (a : ι) → ↥P))))
      x ↔
    ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul (β := M) x (↑((b : (a : ι) → ↥P) i) : M)

Tactic:
simp [@eq_comm _ x, Function.comp, Finsupp.linearCombination_apply]

Premises used: Function.comp, Finsupp.linearCombination_apply, eq_comm
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
P : Submodule R M
b : Basis.{u_1, u_3, u_5} ι R ↥P
x : M
c : ι → R
⊢ (x =
      sum ((Equiv.symm equivFunOnFinite : (a : ι → R) → ι →₀ R) c) fun (i : ι) (x : R) ↦
        HSMul.hSMul (β := M) x (↑((b : (a : ι) → ↥P) i) : M)) ↔
    x = ∑ i : ι, HSMul.hSMul (β := M) (c i) (↑((b : (a : ι) → ↥P) i) : M)

Tactic:
simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]

Premises used: Finsupp.sum_fintype, Finsupp.equivFunOnFinite
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m = 0
rw : ∀ x ∈ N, x = 0
⊢ N = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m = 0
x : M
hx : x ∈ N
contrapose! :
  ∀ (x_ne : x ≠ 0), ∃ (m : ℕ) (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) ∧ m ≠ 0
⊢ x = 0

Tactic:
contrapose! rank_eq with x_ne
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∃ (m : ℕ) (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) ∧ m ≠ 0

Tactic:
⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩

Premises used: Subtype.mk, And.intro, Exists.intro, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
refine :
  LinearIndependent.{0, u_3, u_5} (ι := Fin 1) R (M := M)
    (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) fun (x_1 : Fin 1) ↦
      Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx)
⊢ ∃ (m : ℕ) (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) ∧ m ≠ 0

Tactic:
refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
rw :
  ∀ (g : Fin 1 → R),
    Eq.{u_5 + 1} (α := M)
        (∑ i : Fin 1,
          HSMul.hSMul (β := M) (g i)
            (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
              (fun (x_1 : Fin 1) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) i))
        0 →
      ∀ (i : Fin 1), g i = 0
⊢ LinearIndependent.{0, u_3, u_5} (ι := Fin 1) R (M := M)
    (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) fun (x_1 : Fin 1) ↦
      Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx)

Tactic:
rw [Fintype.linearIndependent_iff]

Premises used: Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq :
  Eq.{u_5 + 1} (α := M)
    (∑ i : Fin 1,
      HSMul.hSMul (β := M) (g i)
        (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
          (fun (x_1 : Fin 1) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) i))
    0
i : Fin 1
⊢ HSMul.hSMul (β := M) (g 0)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
        (fun (x_1 : Fin 1) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) 0) =
    0

Tactic:
simp only [Fin.default_eq_zero, Finset.univ_unique,
    Finset.sum_singleton] at sum_eq

Premises used: Finset.univ_unique, Finset.sum_singleton, Fin.default_eq_zero
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
i : Fin 1
sum_eq :
  HSMul.hSMul (β := M) (g 0)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
        (fun (x_1 : Fin 1) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) 0) =
    0
⊢ g 0 = 0

Tactic:
(b.smul_eq_zero.mp sum_eq).resolve_right x_ne

Premises used: Module.Basis.smul_eq_zero, Iff.mp, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
i : Fin 1
sum_eq :
  HSMul.hSMul (β := M) (g 0)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
        (fun (x_1 : Fin 1) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) 0) =
    0
⊢ g i = 0

Tactic:
convert! (b.smul_eq_zero.mp sum_eq).resolve_right x_ne

Premises used: Module.Basis.smul_eq_zero, Iff.mp, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n
haveI : (this : DecidableEq M) → P N
⊢ P N

Tactic:
haveI : DecidableEq M := Classical.decEq M
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n
this : DecidableEq M
a :
  (N' : Submodule R M) →
    N' ≤ ⊥ → (x : M) → Membership.mem (γ := Submodule R M) ⊥ x → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
⊢ P ⊥

Tactic:
apply ih
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N_1 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N_1), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N_1) ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a : N ≤ ⊥ → (x : M) → Membership.mem (γ := Submodule R M) ⊥ x → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N
⊢ N ≤ ⊥ → (x : M) → Membership.mem (γ := Submodule R M) ⊥ x → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N_1 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N_1), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N_1) ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
h : N ≤ ⊥
x : M
x_mem : Membership.mem (γ := Submodule R M) ⊥ x
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
a : False
⊢ P N

Tactic:
exfalso
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N_1 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N_1), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N_1) ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
h : N ≤ ⊥
x : M
x_mem : Membership.mem (γ := Submodule R M) ⊥ x
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ x = 0

Tactic:
rw [mem_bot] at x_mem

Premises used: Submodule.mem_bot
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N_1 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N_1), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N_1) ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
h : N ≤ ⊥
x : M
x_mem : Membership.mem (γ := Submodule R M) ⊥ x
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
x_mem₁ : x = 0
⊢ ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0

Tactic:
rw [mem_bot] at x_mem

Premises used: Submodule.mem_bot
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N_1 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N_1), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N_1) ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
h : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False

Tactic:
simpa [x_mem] using x_ortho 1 0 N.zero_mem

Premises used: Submodule.zero_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n
this : DecidableEq M
have : (Pbot : P ⊥) → P N
⊢ P N

Tactic:
have Pbot : P ⊥ := by
    apply ih
    intro N _ x x_mem x_ortho
    exfalso
    rw [mem_bot] at x_mem
    simpa [x_mem] using x_ortho 1 0 N.zero_mem
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this_1 : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ 0
this : N = ⊥
rwa rwa₁ rwa₂ rwa₃ : P ⊥
⊢ P N

Tactic:
rwa [this]
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ 0
zero : N = ⊥
⊢ P N

Tactic:
suffices N = ⊥ by rwa [this]
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ 0
⊢ N = ⊥

Tactic:
apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)

Premises used: Nat.le_zero, Module.Basis.eq_bot_of_rank_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n) →
      P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n + 1
succ : (N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
⊢ P N

Tactic:
apply ih
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n) →
      P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
succ : ∀ {m : ℕ} (v : Fin m → ↥N'), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) → m ≤ n
⊢ P N'

Tactic:
apply rank_ih
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n) →
      P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v)
⊢ m ≤ n

Tactic:
Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)

Premises used: Fin.cons, Subtype.mk, Nat.succ_le_succ_iff, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n) →
      P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v)
succ :
  LinearIndependent.{0, u_3, u_5} (ι := Fin m.succ) R (M := M)
    (comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N))
      (Fin.cons (α := fun (a : Fin m.succ) ↦ ↥N) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) x x_mem) fun (i : Fin m) ↦
        Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑(v i) : M) ⋯))
⊢ m ≤ n

Tactic:
refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)

Premises used: Fin.cons, Subtype.mk, Nat.succ_le_succ_iff, Iff.mp, Subtype.val, Subtype.property