awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
u v : m ⊕ n
a :
  ∀ (i : m),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) v = fromBlocks A B 0 D (Sum.inl i) v
a₁ :
  ∀ (j : n),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) v = fromBlocks A B 0 D (Sum.inr j) v
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e u v = fromBlocks A B 0 D u v

Tactic:
cases u with
  | inl i =>
    cases v with
    | inl k =>
      simp only [b, sumQuot_inl, Matrix.fromBlocks_apply₁₁, A, LinearMap.toMatrix_apply]
      apply sumQuot_repr_inl_of_mem
    | inr l => simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]
  | inr j =>
    cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp

Premises used: Matrix.fromBlocks_apply₁₁, Submodule.mapQ_apply, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, LinearMap.inl, Module.Basis.sumQuot_repr_inl_of_mem, LinearMap.mem_ker, Submodule.ker_mkQ, LinearMap.inr, Module.Basis.sumQuot_inl, LinearMap.toMatrix_apply, Module.Basis.sumQuot_repr_inr
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
⊢ LinearIndependent (ι := ι₁ ⊕ ι₂) R (Sum.elim (fun (x : ι₁) ↦ (↑(f x) : M)) g)

Tactic:
.sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_

Premises used: LinearIndependent.sum_type, Submodule.ker_subtype, LinearIndependent.map', LinearIndependent.of_comp, Submodule.subtype, Submodule.mkQ
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
refine : Disjoint (α := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) (span R (range g))
⊢ LinearIndependent (ι := ι₁ ⊕ ι₂) R (Sum.elim (fun (x : ι₁) ↦ (↑(f x) : M)) g)

Tactic:
refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
⊢ Disjoint (α := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) (span R (range g))

Tactic:
disjoint_def.mpr fun x h₁ h₂ ↦ ?_

Premises used: Iff.mpr, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
refine :
  ∀ (x : M) (h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x)
    (h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x), x = 0
⊢ Disjoint (α := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) (span R (range g))

Tactic:
refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_

Premises used: Iff.mpr, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
x : M
h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x
⊢ x ∈ M'

Tactic:
have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
x : M
h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x
this : x ∈ M'
obtain :
  ∀ (c : ι₂ →₀ R)
    (h₁ :
      Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
        (c.sum fun (i : ι₂) (a : R) ↦ a • g i))
    (h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i))
    (this : (c.sum fun (i : ι₂) (a : R) ↦ a • g i) ∈ M'), Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂

Premises used: Finsupp.mem_span_range_iff_exists_finsupp, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ :
  Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
    (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
this : (c.sum fun (i : ι₂) (a : R) ↦ a • g i) ∈ M'
⊢ Eq.{v + 1} (α := M ⧸ M') (c.sum fun (a : ι₂) (b : R) ↦ HSMul.hSMul (β := M ⧸ M') b (Submodule.Quotient.mk (g a))) 0

Tactic:
simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this

Premises used: Submodule.mkQ_apply, map_finsuppSum, Submodule.Quotient.mk_eq_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ :
  Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
    (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
this :
  Eq.{v + 1} (α := M ⧸ M') (c.sum fun (a : ι₂) (b : R) ↦ HSMul.hSMul (β := M ⧸ M') b (Submodule.Quotient.mk (g a))) 0
rw : Eq.{v + 1} (α := M) (Finsupp.sum 0 fun (i : ι₂) (a : R) ↦ a • g i) 0
rw₁ rw₂ : Eq.{v + 1} (α := M) 0 0
⊢ Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0

Tactic:
rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]

Premises used: linearIndependent_iff, Iff.mp, Finsupp.sum_zero_index
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
apply : Disjoint (α := Submodule R M) (span R (f '' s)) (span R (f '' t))
⊢ LinearIndepOn R f (s ∪ t)

Tactic:
apply hs.union ht.of_comp

Premises used: LinearIndepOn.union, LinearIndepOn.of_comp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ Disjoint (α := Submodule R M)
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
    (span R (range fun (x : (↑t : Type w)) ↦ f (↑x : ι)))

Tactic:
(Submodule.range_ker_disjoint ht).symm

Premises used: Disjoint.symm, Submodule.range_ker_disjoint
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
h :
  Eq (α := Submodule R M) (span R (f '' s))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
h₁ : f '' t = range fun (x : (↑t : Type w)) ↦ f (↑x : ι)
⊢ Disjoint (α := Submodule R M) (span R (f '' s)) (span R (f '' t))

Tactic:
convert! (Submodule.range_ker_disjoint ht).symm

Premises used: Disjoint.symm, Submodule.range_ker_disjoint
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ Eq (α := Submodule R M) (span R (f '' s))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ f '' t = range fun (x : (↑t : Type w)) ↦ f (↑x : ι)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ (↑M' : Set M)
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (M := M ⧸ M') (⇑M'.mkQ : (a : M) → M ⧸ M') t
rw :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ id) t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (id '' s)))
    ((⇑(mkQ (span R (id '' s))) : (a : M) → M ⧸ span R (id '' s)) ∘ id) t

Tactic:
rw [image_id]

Premises used: Set.image_id
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ (↑M' : Set M)
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (M := M ⧸ M') (⇑M'.mkQ : (a : M) → M ⧸ M') t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ id) t

Tactic:
ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))

Premises used: Iff.mpr, LinearMap.id, Submodule.mapQ, Submodule.span, LinearIndepOn.of_comp, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ (↑M' : Set M)
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (M := M ⧸ M') (⇑M'.mkQ : (a : M) → M ⧸ M') t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ id) t

Tactic:
exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
⊢ LinearIndepOn R f (s ∪ t) ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, LinearIndepOn.union_of_quotient
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
refine_1 : ∀ (h : LinearIndepOn R f (s ∪ t)), LinearIndepOn R f s
refine_2 :
  ∀ (h : LinearIndepOn R f (s ∪ t)),
    LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ LinearIndepOn R f (s ∪ t) ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R f s

Tactic:
h.mono subset_union_left

Premises used: Set.subset_union_left, LinearIndepOn.mono
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R f s

Tactic:
exact h.mono subset_union_left

Premises used: Set.subset_union_left, LinearIndepOn.mono
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
refine_2 :
  Disjoint (α := Submodule R M) (span R (range fun (x : (↑t : Type w)) ↦ f (↑x : ι)))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t

Tactic:
apply (h.mono subset_union_right).map

Premises used: Set.subset_union_right, LinearIndepOn.mono, LinearIndependent.map
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ Disjoint (α := Submodule R M) (span R (range fun (x : (↑t : Type w)) ↦ f (↑x : ι)))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))

Tactic:
simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm

Premises used: Set.image_eq_range, linearIndepOn_union_iff, Disjoint.symm, And.right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
rw :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
rw₁ rw₂ :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R f (s ∪ t)

Tactic:
rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]

Premises used: and_iff_right, linearIndepOn_union_iff_quotient
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
simp :
  HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
    (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v))
| Module.rank R (M ⧸ M') + Module.rank R ↥M'

Tactic:
simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
conv_lhs :
  HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
      (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v)) ≤
    Module.rank R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M

Tactic:
conv_lhs => simp only [Module.rank_def]

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
rw :
  ⨆ (i : { s : Set (M ⧸ M') // LinearIndepOn R id s }),
      ⨆ (j : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑i : Set (M ⧸ M')) : Type v) + #(↑(↑j : Set ↥M') : Type v) ≤
    Module.rank R M
⊢ HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
      (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v)) ≤
    Module.rank R M

Tactic:
rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]

Premises used: Cardinal.bddAbove_of_small, Cardinal.ciSup_add_ciSup
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
⊢ ⨆ (i : { s : Set (M ⧸ M') // LinearIndepOn R id s }),
      ⨆ (j : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑i : Set (M ⧸ M')) : Type v) + #(↑(↑j : Set ↥M') : Type v) ≤
    Module.rank R M

Tactic:
ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Premises used: _private.0.rank_quotient_add_rank_le.match_1, iSup, Cardinal.mk, Set.Elem, LE.le, Subtype.mk, _private.0.rank_quotient_add_rank_le.match_2, HAdd.hAdd, Module.rank, Subtype.val, ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
refine :
  ∀ (x : { s : Set (M ⧸ M') // LinearIndepOn R id s }) (s : Set (M ⧸ M')) (hs : LinearIndepOn R id s)
    (x : { s : Set ↥M' // LinearIndepOn R id s }) (t : Set ↥M') (ht : LinearIndepOn R id t),
    #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
        #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
      Module.rank R M
⊢ ⨆ (i : { s : Set (M ⧸ M') // LinearIndepOn R id s }),
      ⨆ (j : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑i : Set (M ⧸ M')) : Type v) + #(↑(↑j : Set ↥M') : Type v) ≤
    Module.rank R M

Tactic:
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
x : { s : Set (M ⧸ M') // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x_1 : { s : Set ↥M' // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
choose :
  ∀ (f : (b : M ⧸ M') → M) (hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b),
    #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
        #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
      Module.rank R M
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
      #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
    Module.rank R M

Tactic:
choose f hf using Submodule.Quotient.mk_surjective M'

Premises used: Submodule.Quotient.mk_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
x : { s : Set (M ⧸ M') // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x_1 : { s : Set ↥M' // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : (b : M ⧸ M') → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ LinearIndependent.{v, u, v} (ι := (↑s : Type v)) R (M := M ⧸ M')
    (Submodule.Quotient.mk ∘ fun (i : (↑s : Type v)) ↦ f (↑i : M ⧸ M'))

Tactic:
simpa [Function.comp_def, hf] using hs

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
x : { s : Set (M ⧸ M') // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x_1 : { s : Set ↥M' // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : (b : M ⧸ M') → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
      #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
    Module.rank R M

Tactic:
simpa [add_comm] using (LinearIndependent.sumElim_of_quotient ht (fun (i : s) ↦ f i)
    (by simpa [Function.comp_def, hf] using hs)).cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, add_comm, LinearIndependent.sumElim_of_quotient, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ Module.rank R (M ⧸ p) ≤ Module.rank R M

Tactic:
(mkQ p).rank_le_of_surjective Quot.mk_surjective

Premises used: LinearMap.rank_le_of_surjective, Submodule.mkQ, Quot.mk_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
s : Submodule R M
⊢ finrank.{u, v} R (M ⧸ s) ≤ finrank R M

Tactic:
toNat_le_toNat ((Submodule.mkQ s).rank_le_of_surjective Quot.mk_surjective)
    (rank_lt_aleph0 _ _)

Premises used: Cardinal.toNat_le_toNat, LinearMap.rank_le_of_surjective, Submodule.mkQ, Quot.mk_surjective, Module.rank_lt_aleph0, Module.finrank