awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ False
have hm₁ : b = 0 ∧ a = 0
Tactic: rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ False
have hm₁ : b = 0 ∧ a = 0
Tactic: repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
⊢ False
have hm : LinearIndependent R m
Tactic: have hm : LinearIndependent R m := h.map' _ (ker_inclusion _ _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
⊢ False
have hn : Eq (α := S) ((mulLeftMap N m : (a : Fin 2 →₀ ↥N) → S) n : S) (0 : S)
Tactic: have hn : mulLeftMap N m n = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Eq (α := S) ((mulLeftMap N m : (a : Fin 2 →₀ ↥N) → S) n : S) (0 : S)
⊢ False
have hn₁ : n = 0
Tactic: rw [← LinearMap.mem_ker, H.linearIndependent_left_of_flat hm, mem_bot] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : n = 0
⊢ False
have hn₁ : Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) sorry = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) sorry = 0
Tactic: simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq,
    SetLike.coe_eq_coe, false_and, false_or, n] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ False
have hn₁ : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) sorry = 0
Tactic: rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ False
have hn₁ : b = 0 ∧ a = 0
Tactic: rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ False
have hn₁ : b = 0 ∧ a = 0
Tactic: repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
⊢ ¬LinearIndependent R ![a, b]
have inl : Flat.{u, v} R ↥M → ¬LinearIndependent R ![a, b]
Tactic: rcases hf with _ | _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
inl : Flat.{u, v} R ↥M → ¬LinearIndependent R ![a, b]
⊢ ¬LinearIndependent R ![a, b]
have inr : Flat.{u, v} R ↥N → ¬LinearIndependent R ![a, b]
Tactic: rcases hf with _ | _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥(M ⊓ N) ≤ 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h : Nontrivial R
⊢ Module.rank R ↥(M ⊓ N) ≤ 1
have refine : ∀ (s : Finset ↥(M ⊓ N)) (h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))), s.card ≤ 1
Tactic: refine _root_.rank_le fun s h ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
⊢ s.card ≤ 1
have by_contra : ∀ (hs : ¬s.card ≤ 1), False
Tactic: by_contra hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : ¬s.card ≤ 1
⊢ False
have hs₁ : Nontrivial.{v} ↥s
Tactic: rw [not_le, ← Fintype.card_coe, Fintype.one_lt_card_iff_nontrivial] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
⊢ False
have obtain : ∀ (a b : ↥s) (hab : a ≠ b), False
Tactic: obtain ⟨a, b, hab⟩ := hs.exists_pair_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
⊢ False
have refine : LinearIndependent R ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))]
Tactic: refine H.not_linearIndependent_pair_of_commute_of_flat hf a.1 b.1 (hc a.1 b.1) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
⊢ i = j
have 0 : ∀ (hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j),
  (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩ = j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
0 :
  ∀ (hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j),
    (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = j
⊢ i = j
have 1 : ∀ (hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j),
  (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩ = j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = j
have 0 : ∀
  (hij :
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
0 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = j
have 0₁ : ∀
  (hij :
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = j
have 1 : ∀
  (hij :
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
1 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = j
have 1₁ : ∀
  (hij :
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
⊢ LinearIndependent R ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))]
have this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
Tactic: have := h.comp ![a, b] fun i j hij ↦ by
    fin_cases i <;> fin_cases j
    · rfl
    · simp [hab] at hij
    · simp [hab.symm] at hij
    · rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
⊢ LinearIndependent R ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))]
have h₁ : ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] = (fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]
Tactic: convert! this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
⊢ ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] = (fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]
have h₁ : ∀ (i : Fin (Nat.succ 0).succ),
  (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] i) : S) = (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) i) : S)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
⊢ (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] i) : S) = (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) i) : S)
have h₁ : (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ))) : S) =
  (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)) : S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
h₁ :
  (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ))) :
      S) =
    (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) : S)
⊢ (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] i) : S) = (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) i) : S)
have h₂ : (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ))) : S) =
  (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)) : S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst_3 : Flat.{u, v} R ↥M
hc : ∀ (m n : ↥M), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥M ≤ 1
have rw : ∀ (hc : ∀ (m n : ↥(M ⊓ M)), Commute (↑m : S) (↑n : S)), Module.rank R ↥(M ⊓ M) ≤ 1
Tactic: rw [← inf_of_le_left (le_refl M)] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
⊢ Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have h : ∀ (x : ι) (x_1 : ι'),
  Eq.{u_4 + 1} (α := L) (((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') x x_1)
    (((⇑(algebraMap K L) : (a : K) → L) ∘ v x) x_1)
Tactic: ext