awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ LinearIndependent.{0, u_3, u_5} (ι := Fin (m + 1)) R (M := M)
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))

Tactic:
hli.finCons' x _ ?_

Premises used: LinearIndependent.finCons'
-- 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)
h :
  Eq.{u_5 + 1} (α := Fin m.succ → 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) ⋯))
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))
succ :
  ∀ (c : R) (y : M),
    Membership.mem (γ := Submodule R M) (span R (range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))) y →
      c • x + y = 0 → c = 0
⊢ 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) ⋯))

Tactic:
convert! hli.finCons' x _ ?_

Premises used: LinearIndependent.finCons'
-- 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)
h :
  ∀ (i : Fin m.succ),
    Eq.{u_5 + 1} (α := 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) ⋯)
          i :
        M)
      (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) i : M)
⊢ Eq.{u_5 + 1} (α := Fin m.succ → 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) ⋯))
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))

Tactic:
ext i
-- 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)
i : Fin m.succ
⊢ Eq.{u_5 + 1} (α := 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) ⋯)
        i :
      M)
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) i : M)

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- 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)
i : Fin m.succ
h :
  Eq.{u_5 + 1} (α := M)
    (comp (α := Fin m.succ) (β := ↥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) ⋯)
        0 :
      M)
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) 0 : M)
h₁ :
  ∀ (i : Fin m),
    Eq.{u_5 + 1} (α := 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) ⋯)
          i.succ :
        M)
      (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) i.succ : M)
⊢ Eq.{u_5 + 1} (α := 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) ⋯)
        i :
      M)
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) i : M)

Tactic:
refine Fin.cases ?_ ?_ i
-- 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)
i : Fin m.succ
⊢ Eq.{u_5 + 1} (α := M)
    (comp (α := Fin m.succ) (β := ↥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) ⋯)
        0 :
      M)
    (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) 0 : M)

Tactic:
simp
-- 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)
i : Fin m.succ
⊢ ∀ (i : Fin m),
    Eq.{u_5 + 1} (α := 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) ⋯)
          i.succ :
        M)
      (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) i.succ : M)

Tactic:
simp
-- 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)
c : R
y : M
hy : Membership.mem (γ := Submodule R M) (span R (range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))) y
hc : c • x + y = 0
⊢ c = 0

Tactic:
x_ortho c y (Submodule.span_le.mpr ?_ hy) hc

Premises used: Iff.mpr, Submodule.span_le
-- 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)
c : R
y : M
hy : Membership.mem (γ := Submodule R M) (span R (range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))) y
hc : c • x + y = 0
succ : range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) ⊆ (↑N' : Set M)
⊢ c = 0

Tactic:
refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc

Premises used: Iff.mpr, Submodule.span_le
-- 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)
c : R
y : M
hy : Membership.mem (γ := Submodule R M) (span R (range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))) y
hc : c • x + y = 0
z : Fin m
⊢ (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) z ∈ (↑N' : Set M)

Tactic:
(v z).2

Premises used: Set.Mem, 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)
c : R
y : M
hy : Membership.mem (γ := Submodule R M) (span R (range (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v))) y
hc : c • x + y = 0
z : Fin m
⊢ (Subtype.val (p := fun (x : M) ↦ x ∈ N') ∘ v) z ∈ (↑N' : Set M)

Tactic:
exact (v z).2

Premises used: 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
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
Pbot : P ⊥
zero :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ 0) →
      P N
succ :
  (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) →
          P N
⊢ P N

Tactic:
induction n generalizing N with
  | zero =>
    suffices N = ⊥ by rwa [this]
    apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
  | succ n rank_ih =>
    apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert! hli.finCons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2

Premises used: Submodule.zero, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
mp :
  z ∈ center A →
    (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
      ∀ (i j : ι),
        z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
            HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
          HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
            HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
mpr :
  ((∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
      ∀ (i j : ι),
        z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
            HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
          HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
            HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)) →
    z ∈ center A
⊢ z ∈ center A ↔
    (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
      ∀ (i j : ι),
        z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
            HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
          HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
            HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
mp : ∀ (i : ι), Commute ((b : (a : ι) → A) i) z
mp₁ :
  ∀ (i j : ι),
    z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
        HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
      HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
        HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
⊢ (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
i : ι
⊢ Commute ((b : (a : ι) → A) i) z

Tactic:
apply (h.1 (b i)).symm

Premises used: IsMulCentral.comm, Commute.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
i j : ι
⊢ z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
      HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
    HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
      HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)

Tactic:
⟨h.2 _ _, h.3 _ _⟩

Premises used: And.intro, IsMulCentral.left_assoc, IsMulCentral.right_assoc
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
i j : ι
⊢ z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
      HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
    HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
      HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)

Tactic:
exact ⟨h.2 _ _, h.3 _ _⟩
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
constructor : ∀ (a : A), Commute z a
constructor₁ : ∀ (b c : A), z * (b * c) = z * b * c
constructor₂ : ∀ (a b : A), a * b * z = a * (b * z)
⊢ IsMulCentral z

Tactic:
constructor