awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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
rwa : (db.coprod eb).range = ⊤
rwa₁ : db.range ⊔ eb.range = ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : ⊤ ≤ db.range ⊔ eb.range
⊢ Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)

Tactic:
rwa [← range_eq_top, range_coprod, eq_top_iff]

Premises used: eq_top_iff, LinearMap.range_eq_top, LinearMap.range_coprod
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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
⊢ Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)

Tactic:
have hf : Surjective (coprod db eb) := by
    rwa [← range_eq_top, range_coprod, eq_top_iff]
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
rhs : Module.rank K V₂ + Module.rank K V₃
| Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
rhs
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
rw : Module.rank K V + Module.rank K ↥(db.coprod eb).ker
| Module.rank K V₂ + Module.rank K V₃

Tactic:
rw [← rank_prod', rank_eq_of_surjective hf]

Premises used: LinearMap.rank_eq_of_surjective, rank_prod'
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
rw : Module.rank K V + Module.rank K ↥(db.coprod eb).ker
| Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
rhs
    rw [← rank_prod', rank_eq_of_surjective hf]

Premises used: LinearMap.rank_eq_of_surjective, rank_prod'
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
conv : Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(db.coprod eb).ker
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
conv =>
    rhs
    rw [← rank_prod', rank_eq_of_surjective hf]

Premises used: LinearMap.rank_eq_of_surjective, rank_prod'
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
e_a : Module.rank K V₁ = Module.rank K ↥(db.coprod eb).ker
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(db.coprod eb).ker

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
e_a : V₁ ≃ₗ[K] ↥(db.coprod eb).ker
⊢ Module.rank K V₁ = Module.rank K ↥(db.coprod eb).ker

Tactic:
apply LinearEquiv.rank_eq

Premises used: LinearEquiv.rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
⊢ ∀ (c : V₁), Membership.mem (α := V₂ × V₃) (db.coprod eb).ker ((cd.prod (-ce) : (a : V₁) → V₂ × V₃) c : V₂ × V₃)

Tactic:
simpa [add_eq_zero_iff_eq_neg] using LinearMap.ext_iff.1 eq

Premises used: add_eq_zero_iff_eq_neg, LinearMap.ext_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
e_a₁ : Surjective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker

Tactic:
refine LinearEquiv.ofBijective L ⟨?_, ?_⟩

Premises used: And.intro, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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 = ⊥
e_a₄ e_a₅ : Eq.{v + 1} (α := Submodule K V₁) ⊥ ⊥
⊢ Injective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)

Tactic:
rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]

Premises used: LinearMap.ker_eq_bot, LinearMap.ker_codRestrict, LinearMap.ker_prod, bot_inf_eq
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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 : (db.coprod eb).ker ≤ (cd.prod (-ce)).range
⊢ Surjective (α := V₁) (β := ↥(db.coprod eb).ker) (⇑L : (a : V₁) → ↥(db.coprod eb).ker)

Tactic:
rw [← range_eq_top, eq_top_iff, LinearMap.range_codRestrict, ← map_le_iff_le_comap,
      Submodule.map_top, range_subtype]

Premises used: eq_top_iff, Submodule.map_top, LinearMap.range_eq_top, Submodule.map_le_iff_le_comap, LinearMap.range_codRestrict, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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₃
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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
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
⊢ (d, e) ∈ (db.coprod eb).ker → (d, e) ∈ (cd.prod (-ce)).range

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 ⊢

Premises used: Prod.mk_inj, LinearMap.coprod_apply, LinearMap.neg_apply, add_eq_zero_iff_eq_neg, map_neg, LinearMap.mem_ker, LinearMap.mem_range, Function.prod_apply, LinearMap.prod_apply
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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
⊢ 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:
grind
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
⊢ Function.Injective.{u + 1, u + 1} (α := ℕ →₀ K) (β := ℕ → K) (⇑Finsupp.lcoeFun : (a : ℕ →₀ K) → ℕ → K)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
⊢ Function.Injective.{u + 1, u + 1} (α := ℕ →₀ K) (β := ℕ → K) (⇑Finsupp.lcoeFun : (a : ℕ →₀ K) → ℕ → K)

Tactic:
exact DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
⊢ ℵ₀ ≤ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)

Tactic:
max_le aleph0_le ?_

Premises used: max_le
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
refine : #K ≤ Module.rank K (ℕ → K)
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)

Tactic:
refine max_le aleph0_le ?_

Premises used: max_le
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
inl : ∀ (card_K : #K ≤ ℵ₀), #K ≤ Module.rank K (ℕ → K)
inr : ∀ (card_K : ℵ₀ < #K), #K ≤ Module.rank K (ℕ → K)
⊢ #K ≤ Module.rank K (ℕ → K)

Tactic:
obtain card_K | card_K := le_or_gt #K ℵ₀

Premises used: Cardinal.mk, Cardinal.aleph0, le_or_gt
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : #K ≤ ℵ₀
⊢ #K ≤ Module.rank K (ℕ → K)

Tactic:
card_K.trans aleph0_le

Premises used: LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : #K ≤ ℵ₀
⊢ #K ≤ Module.rank K (ℕ → K)

Tactic:
exact card_K.trans aleph0_le

Premises used: LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
inr : ∀ (this : Module.rank K (ℕ → K) < #K), False
⊢ #K ≤ Module.rank K (ℕ → K)

Tactic:
by_contra!
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
inr : ∀ (ιK : Type u) (bK : Module.Basis ιK K (ℕ → K)), False
⊢ False

Tactic:
obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ℕ → K)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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

Tactic:
(Subfield.cardinalMk_closure_le_max _).trans_lt
      (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)

Premises used: Iff.mpr, Subfield.cardinalMk_closure_le_max, Set.Mem, max_lt_iff, Cardinal.mk_range_le, And.intro, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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)
refine : #(ιK × ℕ) < #K
⊢ #↥L < #K

Tactic:
refine (Subfield.cardinalMk_closure_le_max _).trans_lt
      (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)

Premises used: Iff.mpr, Subfield.cardinalMk_closure_le_max, max_lt_iff, Cardinal.mk_range_le, And.intro, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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
rwa₃ : Module.rank K (ℕ → K) * ℵ₀ < #K
rwa₄ rwa₅ rwa₆ rwa₇ : Module.rank K (ℕ → K) < #K
⊢ #(ιK × ℕ) < #K

Tactic:
rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]

Premises used: Cardinal.mul_aleph0_eq, Cardinal.aleph0, Cardinal.lift_uzero, Module.Basis.mk_eq_rank'', Cardinal.mk_prod
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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

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]
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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)
inr : ∀ (ιL : Type u) (bL : Module.Basis ιL (↥L)ᵐᵒᵖ K), False
⊢ False

Tactic:
obtain ⟨⟨ιL, bL⟩⟩ := Module.Free.exists_basis (R := Lᵐᵒᵖ) (M := K)

Premises used: MulOpposite, Membership.mem, Subtype, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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
contrapose! : ∀ (hLK : #ιL < ℵ₀), #K ≤ #↥L
⊢ ℵ₀ ≤ #ιL

Tactic:
contrapose! hLK
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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 < ℵ₀
haveI : ∀ (this : Fintype ιL), #K ≤ #↥L
⊢ #K ≤ #↥L

Tactic:
haveI := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK)
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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
rw :
  ∀ (bL : Module.Basis ιL (↥L)ᵐᵒᵖ K) (hLK : #ιL < ℵ₀) (this : Fintype ιL) (card_K : ℵ₀ < #↥L ^ Fintype.card ιL),
    #↥L ^ Fintype.card ιL ≤ #↥L
⊢ #K ≤ #↥L

Tactic:
rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
        ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢

Premises used: MulOpposite.opEquiv, Module.Basis.repr, Cardinal.mk_finsupp_of_fintype, LinearEquiv.toEquiv, Equiv.cardinal_eq
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
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
h : ℵ₀ ≤ #↥L
⊢ #↥L ^ Fintype.card ιL ≤ #↥L

Tactic:
apply power_nat_le

Premises used: Cardinal.power_nat_le