awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
| Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
have rw : Module.rank K V + Module.rank K ↥(db.coprod eb).ker
Tactic: rhs
    rw [← rank_prod', rank_eq_of_surjective hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
have conv : Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(db.coprod eb).ker
Tactic: conv =>
    rhs
    rw [← rank_prod', rank_eq_of_surjective hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(db.coprod eb).ker
have e_a : Module.rank K V₁ = Module.rank K ↥(db.coprod eb).ker
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
⊢ Module.rank K V₁ = Module.rank K ↥(db.coprod eb).ker
have e_a : V₁ ≃ₗ[K] ↥(db.coprod eb).ker
Tactic: apply LinearEquiv.rank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker
have e_a : Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
Tactic: refine LinearEquiv.ofBijective L ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
e_a : Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker
have e_a₁ : Surjective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
Tactic: refine LinearEquiv.ofBijective L ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a : L.ker = ⊥
Tactic: rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
e_a : L.ker = ⊥
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a₁ : (cd.prod (-ce)).ker = ⊥
Tactic: rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
e_a : L.ker = ⊥
e_a₁ : (cd.prod (-ce)).ker = ⊥
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a₂ : cd.ker ⊓ (-ce).ker = ⊥
Tactic: rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
e_a : L.ker = ⊥
e_a₁ : (cd.prod (-ce)).ker = ⊥
e_a₂ : cd.ker ⊓ (-ce).ker = ⊥
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a₃ : ⊥ ⊓ (-ce).ker = ⊥
Tactic: rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
e_a : L.ker = ⊥
e_a₁ : (cd.prod (-ce)).ker = ⊥
e_a₂ : cd.ker ⊓ (-ce).ker = ⊥
e_a₃ : ⊥ ⊓ (-ce).ker = ⊥
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a₄ : Eq.{v + 1} (α := Submodule K V₁) ⊥ ⊥
Tactic: rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Surjective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
have e_a : (db.coprod eb).ker ≤ (cd.prod (-ce)).range
Tactic: rw [← range_eq_top, eq_top_iff, LinearMap.range_codRestrict, ← map_le_iff_le_comap,
      Submodule.map_top, range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (hypothesis)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
d : V₂
e : V₃
⊢ (d, e) ∈ (db.coprod eb).ker → (d, e) ∈ (cd.prod (-ce)).range
have h : Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) (-e) : V) →
  ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = -e
Tactic: have h := eq₂ d (-e)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
d : V₂
e : V₃
h :
  Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) (-e) : V) →
    ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = -e
⊢ (d, e) ∈ (db.coprod eb).ker → (d, e) ∈ (cd.prod (-ce)).range
have e_a : ∀
  (h :
    Eq (α := V) ((db : (a : V₂) → V) d : V) (-(eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = -e),
  Eq (α := V) ((db : (a : V₂) → V) d : V) (-(eb : (a : V₃) → V) e : V) →
    ∃ (y : V₁), (cd : (a : V₁) → V₂) y = d ∧ -(ce : (a : V₁) → V₃) y = e
Tactic: simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker,
      Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range,
      Function.prod_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)
have aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
Tactic: have aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K) := (rank_finsupp_self K ℕ).symm.trans_le
    (Finsupp.lcoeFun.rank_le_of_injective <| by exact DFunLike.coe_injective)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)
have refine : #K ≤ Module.rank K (ℕ → K)
Tactic: refine max_le aleph0_le ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
⊢ #K ≤ Module.rank K (ℕ → K)
have inl : ∀ (card_K : #K ≤ ℵ₀), #K ≤ Module.rank K (ℕ → K)
Tactic: obtain card_K | card_K := le_or_gt #K ℵ₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
inl : ∀ (card_K : #K ≤ ℵ₀), #K ≤ Module.rank K (ℕ → K)
⊢ #K ≤ Module.rank K (ℕ → K)
have inr : ∀ (card_K : ℵ₀ < #K), #K ≤ Module.rank K (ℕ → K)
Tactic: obtain card_K | card_K := le_or_gt #K ℵ₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
⊢ #K ≤ Module.rank K (ℕ → K)
have inr : ∀ (this : Module.rank K (ℕ → K) < #K), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
⊢ False
have inr : ∀ (ιK : Type u) (bK : Module.Basis ιK K (ℕ → K)), False
Tactic: obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ℕ → K)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
⊢ #↥L < #K
have refine : #(ιK × ℕ) < #K
Tactic: refine (Subfield.cardinalMk_closure_le_max _).trans_lt
      (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
⊢ #(ιK × ℕ) < #K
have rwa : lift.{0, u} #ιK * lift.{u, 0} #ℕ < #K
Tactic: rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
rwa : lift.{0, u} #ιK * lift.{u, 0} #ℕ < #K
⊢ #(ιK × ℕ) < #K
have rwa₁ : lift.{0, u} #ιK * ℵ₀ < #K
Tactic: rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
rwa : lift.{0, u} #ιK * lift.{u, 0} #ℕ < #K
rwa₁ : lift.{0, u} #ιK * ℵ₀ < #K
⊢ #(ιK × ℕ) < #K
have rwa₂ : #ιK * ℵ₀ < #K
Tactic: rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
rwa : lift.{0, u} #ιK * lift.{u, 0} #ℕ < #K
rwa₁ : lift.{0, u} #ιK * ℵ₀ < #K
rwa₂ : #ιK * ℵ₀ < #K
⊢ #(ιK × ℕ) < #K
have rwa₃ : Module.rank K (ℕ → K) * ℵ₀ < #K
Tactic: rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
⊢ False
have hLK : #↥L < #K
Tactic: have hLK : #L < #K := by
    refine (Subfield.cardinalMk_closure_le_max _).trans_lt
      (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)
    rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
⊢ False
have inr : ∀ (ιL : Type u) (bL : Module.Basis ιL (↥L)ᵐᵒᵖ K), False
Tactic: obtain ⟨⟨ιL, bL⟩⟩ := Module.Free.exists_basis (R := Lᵐᵒᵖ) (M := K)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
⊢ ℵ₀ ≤ #ιL
have contrapose! : ∀ (hLK : #ιL < ℵ₀), #K ≤ #↥L
Tactic: contrapose! hLK
Cleared hypotheses: hLK
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
this : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
⊢ #K ≤ #↥L
have haveI : ∀ (this : Fintype ιL), #K ≤ #↥L
Tactic: haveI := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
⊢ #K ≤ #↥L
have rw : ∀ (bL : Module.Basis ιL (↥L)ᵐᵒᵖ K) (hLK : #ιL < ℵ₀) (this : Fintype ιL) (card_K : ℵ₀ < #↥L ^ Fintype.card ιL),
  #↥L ^ Fintype.card ιL ≤ #↥L
Tactic: rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
        ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢
Cleared hypotheses: card_K, bL, hLK, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #↥L ^ Fintype.card ιL
⊢ #↥L ^ Fintype.card ιL ≤ #↥L
have h : ℵ₀ ≤ #↥L
Tactic: apply power_nat_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #↥L ^ Fintype.card ιL
⊢ ℵ₀ ≤ #↥L
have h : ∀ (card_K : #↥L < ℵ₀), #↥L ^ Fintype.card ιL ≤ ℵ₀
Tactic: contrapose! card_K
Cleared hypotheses: card_K