awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
⊢ IsEmpty κ

Tactic:
haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this : IsEmpty κ
⊢ Subsingleton.{u_2 + 1} ↥⊥

Tactic:
haveI := b.repr.toEquiv.subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this_1 : IsEmpty κ
this : Subsingleton.{u_2 + 1} ↥⊥
⊢ False

Tactic:
one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

Premises used: congrArg, Subalgebra.val, id, Bot.bot, Subsingleton.elim, one_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this_1 : IsEmpty κ
this : Subsingleton.{u_2 + 1} ↥⊥
⊢ False

Tactic:
exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

Premises used: congrArg, Subalgebra.val, id, Bot.bot, Subsingleton.elim, one_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
rw : finrank.{u_1, u_2} F ↥S = 1 ↔ Module.rank F ↥S = 1
⊢ finrank.{u_1, u_2} F ↥S = 1 ↔ S = ⊥

Tactic:
rw [← Subalgebra.rank_eq_one_iff]

Premises used: Subalgebra.rank_eq_one_iff
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
⊢ finrank.{u_1, u_2} F ↥S = 1 ↔ Module.rank F ↥S = 1

Tactic:
toNat_eq_iff one_ne_zero

Premises used: Cardinal.toNat_eq_iff, one_ne_zero, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
⊢ finrank.{u_1, u_2} F ↥S = 1 ↔ Module.rank F ↥S = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Premises used: Cardinal.toNat_eq_iff, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
⊢ Free.{u_1, u_2} F ↥⊤

Tactic:
haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F ↥⊤ = 1
rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F E = 1

Tactic:
rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]

Premises used: eq_comm, Subalgebra.rank_eq_one_iff, Subalgebra.rank_top
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
rw₂ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
rw₃ rw₄ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1

Tactic:
rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]

Premises used: eq_comm, finrank_top, subalgebra_top_finrank_eq_submodule_top_finrank, Subalgebra.finrank_eq_one_iff
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
⊢ finrank F E = 1 ↔ Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
⟨?_, Module.finrank_of_bijective_algebraMap⟩

Premises used: Module.finrank_of_bijective_algebraMap, Iff.intro
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
refine : finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
⊢ finrank F E = 1 ↔ Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
refine ⟨?_, Module.finrank_of_bijective_algebraMap⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h : Nontrivial E
⊢ finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
fun h ↦ ⟨FaithfulSMul.algebraMap_injective F E, ?_⟩

Premises used: FaithfulSMul.algebraMap_injective, And.intro, Function.Bijective
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h : Nontrivial E
refine :
  ∀ (h : finrank F E = 1), Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
⊢ finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
refine fun h ↦ ⟨FaithfulSMul.algebraMap_injective F E, ?_⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h_1 : Nontrivial E
h : finrank F E = 1
rwa : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
rwa₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : finrank F E = 1
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
rwa [Algebra.surjective_algebraMap_iff, eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one]

Premises used: eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one, Algebra.surjective_algebraMap_iff
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
⊢ f.rank ≤ Module.rank K V'

Tactic:
Submodule.rank_le _

Premises used: Submodule.rank_le
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V V₁ : Type v
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
f : V →ₗ[K] V₁
⊢ f.rank ≤ Module.rank K V

Tactic:
rank_range_le _

Premises used: Set.Mem, rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : Nontrivial K
rw : Module.rank K ↥(range.{u, u, v, v'} (R := K) (M := V) (τ₁₂ := RingHom.id K) 0) = 0
rw₁ : Module.rank K ↥⊥ = 0
rw₂ rw₃ : Eq.{v' + 2} (α := Cardinal.{v'}) 0 0
⊢ rank.{u, v, v'} (K := K) (V := V) (V' := V') 0 = 0

Tactic:
rw [rank, LinearMap.range_zero, rank_bot]

Premises used: rank_bot, LinearMap.range_zero, LinearMap.rank
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ (f ∘ₗ g).rank ≤ f.rank

Tactic:
Submodule.rank_mono ?_

Premises used: Submodule.rank_mono
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
refine : (f ∘ₗ g).range ≤ f.range
⊢ (f ∘ₗ g).rank ≤ f.rank

Tactic:
refine Submodule.rank_mono ?_

Premises used: Submodule.rank_mono
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
rw : Submodule.map f g.range ≤ f.range
⊢ (f ∘ₗ g).range ≤ f.range

Tactic:
rw [LinearMap.range_comp]

Premises used: LinearMap.range_comp
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ Submodule.map f g.range ≤ f.range

Tactic:
LinearMap.map_le_range

Premises used: Set.Mem, LinearMap.map_le_range
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ Submodule.map f g.range ≤ f.range

Tactic:
exact LinearMap.map_le_range

Premises used: LinearMap.map_le_range
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
rw : lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)
⊢ lift.{v', v''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank

Tactic:
rw [rank, rank, LinearMap.range_comp]

Premises used: LinearMap.range_comp, LinearMap.rank
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)

Tactic:
lift_rank_map_le _ _

Premises used: lift_rank_map_le, Set.Mem
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)

Tactic:
exact lift_rank_map_le _ _

Premises used: lift_rank_map_le
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring 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''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (f ∘ₗ g).rank ≤ min (lift.{v', v''} f.rank) (lift.{v'', v'} g.rank)

Tactic:
le_min (Cardinal.lift_le.mpr <| rank_comp_le_left _ _) (lift_rank_comp_le_right _ _)

Premises used: Iff.mpr, LinearMap.lift_rank_comp_le_right, LinearMap.rank_comp_le_left, le_min, Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' V'₁ : Type v'
inst : Ring 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'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ g.rank

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f

Premises used: LinearMap.lift_rank_comp_le_right, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' V'₁ : Type v'
inst : Ring 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'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ min f.rank g.rank

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_comp_le g f

Premises used: Cardinal.lift_id, LinearMap.lift_rank_comp_le
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f g : V →ₗ[K] V'
⊢ (f + g).rank ≤ Module.rank K ↥(f.range ⊔ g.range)

Tactic:
Submodule.rank_mono ?_

Premises used: Set.Mem, Submodule.rank_mono
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f g : V →ₗ[K] V'
refine : (f + g).range ≤ f.range ⊔ g.range
⊢ (f + g).rank ≤ Module.rank K ↥(f.range ⊔ g.range)

Tactic:
refine Submodule.rank_mono ?_

Premises used: Submodule.rank_mono
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f g : V →ₗ[K] V'
⊢ (f + g).range ≤ f.range ⊔ g.range

Tactic:
LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun x =>
        show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩

Premises used: Iff.mpr, Submodule.eq_top_iff', LinearMap.range_le_iff_comap, And.intro, Exists.intro, Submodule.mem_sup, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f g : V →ₗ[K] V'
⊢ (f + g).range ≤ f.range ⊔ g.range

Tactic:
exact LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun x =>
        show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩

Premises used: Iff.mpr, Submodule.eq_top_iff', LinearMap.range_le_iff_comap, And.intro, Exists.intro, Submodule.mem_sup, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
η : Type u_1
s : Finset η
f : η → V →ₗ[K] V'
x : η
x_1 : V →ₗ[K] V'
x_2 : Cardinal.{v'}
h : (fun (a : V →ₗ[K] V') (b : Cardinal.{v'}) ↦ a.rank ≤ b) x_1 x_2
⊢ (f x).rank + x_1.rank ≤ (fun (d : η) ↦ (f d).rank) x + x_2

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
rcases :
  ∀ (g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V) (hg : f.rangeRestrict ∘ₗ g = id),
    c ≤ f.rank ↔
      ∃ (s : Set V),
        lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s

Tactic:
rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩

Premises used: LinearMap.exists_rightInverse_of_surjective, LinearMap.range_rangeRestrict, LinearMap.rangeRestrict
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
⊢ LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)

Tactic:
have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
refine_1 :
  ∀ (h : c ≤ f.rank),
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
refine_2 :
  (∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) →
    c ≤ f.rank
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
h : c ≤ f.rank
refine_1 :
  ∀ (s : Set ↥f.range) (si : LinearIndepOn K _root_.id s) (h : #(↑s : Type v') ≤ f.rank),
    ∃ (s_1 : Set V),
      lift.{v', v} #(↑s_1 : Type v) = lift.{v, v'} #(↑s : Type v') ∧
        LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1
⊢ ∃ (s : Set V),
    lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s

Tactic:
rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩

Premises used: le_rank_iff_exists_linearIndependent, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
⊢ ∃ (s_1 : Set V),
    lift.{v', v} #(↑s_1 : Type v) = lift.{v, v'} #(↑s : Type v') ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1

Tactic:
⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩

Premises used: Function.LeftInverse.injective, Cardinal.mk_image_eq_lift, And.intro, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
refine_1 : LinearIndepOn.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)
⊢ ∃ (s_1 : Set V),
    lift.{v', v} #(↑s_1 : Type v) = lift.{v, v'} #(↑s : Type v') ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1

Tactic:
refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
x : ↥f.range
⊢ (↑(((f.rangeRestrict : LinearMap.{u, u, v, v'} (RingHom.id K) V ↥f.range) : (a : V) → ↥f.range)
          ((g : (a : ↥f.range) → V) x)) :
      V') =
    (↑x : V')

Tactic:
congr_arg Subtype.val (fg x)

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
x : ↥f.range
⊢ (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')

Tactic:
convert! congr_arg Subtype.val (fg x)

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type 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'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
⊢ ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')

Tactic:
replace fg : ∀ x, f (g x) = x := by
      intro x
      convert! congr_arg Subtype.val (fg x)