mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  ↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective ⇑g
g_ker : g.ker = Submodule.map f.rangeRestrict p
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
⊢ (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  ↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective ⇑g
g_ker : g.ker = Submodule.map f.rangeRestrict p
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
⊢ (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = Module.rank K (ι → K)

pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ lift.{v, u} #K ≤ Module.rank K (ι → K)

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ lift.{v, u} #K ≤ Module.rank K (ι → K)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
]

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(ι → Kᵐᵒᵖ)

Tactic:
]

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(ι → Kᵐᵒᵖ)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
this :
  Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
e : (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
this :
  Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
⊢ Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(ι → K)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι

Tactic:
]

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{u, v} (Module.rank R (M' ⧸ f.range)) +
      lift.{u, v} (Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{u, v} (Module.rank R (M' ⧸ f.range)) +
      lift.{u, v} (Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ Nontrivial K

Tactic:
]

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ Nontrivial K
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
]

Goal state after:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ p ≤ p ⊔ f.rangeRestrict.ker

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ p ≤ p ⊔ f.rangeRestrict.ker
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = Module.rank K V

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = Module.rank K V

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M ⧸ p →ₗ[R] ↥f.range ⧸ Submodule.map f.rangeRestrict p :=
  p.mapQ (Submodule.map f.rangeRestrict p) f.rangeRestrict ⋯
⊢ Submodule.map (Submodule.map f.rangeRestrict p).mkQ f.rangeRestrict.range = ⊤

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M ⧸ p →ₗ[R] ↥f.range ⧸ Submodule.map f.rangeRestrict p :=
  p.mapQ (Submodule.map f.rangeRestrict p) f.rangeRestrict ⋯
⊢ Submodule.map (Submodule.map f.rangeRestrict p).mkQ f.rangeRestrict.range = ⊤
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : 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₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ ⊤ ≤ db.range ⊔ eb.range

Tactic:
]

Goal state after:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : 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₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ ⊤ ≤ db.range ⊔ eb.range
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ X Xᘁ ≫ η_ Y Yᘁ ▷ (X ⊗ Xᘁ)) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ Xᘁ) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ X Xᘁ ≫ η_ Y Yᘁ ▷ (X ⊗ Xᘁ)) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ Xᘁ) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
⊢ s ∩ sec '' t ⊆ ∅

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
⊢ s ∩ sec '' t ⊆ ∅
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ sec x ∈ span R s

Tactic:
]

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ sec x ∈ span R s
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s ≠ ⊤
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)

Tactic:
]

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s ≠ ⊤
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : Nontrivial (V ⧸ s)
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)

Tactic:
]

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : Nontrivial (V ⧸ s)
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ (𝟙_ C ◁ f ▷ Xᘁ ≫ η_ Y Yᘁ ▷ (Y ⊗ Xᘁ)) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ (𝟙_ C ◁ f ▷ Xᘁ ≫ η_ Y Yᘁ ▷ (Y ⊗ Xᘁ)) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Module.rank R (M ⧸ span R s) + #↑s = Module.rank R (M ⧸ span R s) + #↑s

pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id t

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id t
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ ⊗𝟙.hom ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ ⊗𝟙.hom ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t