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

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
by

Goal state after:
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
⊢ ∃ s, #↑s = Module.rank K V ∧ LinearIndepOn K id s

Tactic:
by

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
⊢ Surjective ⇑(db.coprod eb)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommHopfAlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : HopfAlgebra R X
inst✝³ : CommRing Y
inst✝² : HopfAlgebra R Y
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : HopfAlgebra R X
inst✝³ : CommRing Y
inst✝² : HopfAlgebra R Y
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : HopfAlgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : HopfAlgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
X Y : CommHopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommHopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
by

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 ⋯
⊢ Surjective ⇑f'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : HopfAlgebra R A
⊢ CartesianMonoidalCategory.lift (ofHom (antipodeAlgHom R A)).op (𝟙 (Opposite.op (of R A))) ≫ MonObj.mul =
    SemiCartesianMonoidalCategory.toUnit (Opposite.op (of R A)) ≫ MonObj.one

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : HopfAlgebra R A
⊢ CartesianMonoidalCategory.lift (𝟙 (Opposite.op (of R A))) (ofHom (antipodeAlgHom R A)).op ≫ MonObj.mul =
    SemiCartesianMonoidalCategory.toUnit (Opposite.op (of R A)) ≫ MonObj.one

Tactic:
by

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
⊢ lift.{u, v} (Module.rank R (M' ⧸ Submodule.map f p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))

Tactic:
by

Goal state after:
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) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (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:
by

Goal state after:
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
⊢ Disjoint s (sec '' t)

Tactic:
by

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
hf : Surjective ⇑(db.coprod eb)
⊢ ∀ (c : V₁), (cd.prod (-ce)) c ∈ (db.coprod eb).ker

Tactic:
by

Goal state after:
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 V

Tactic:
by

Goal state after:
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ᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ 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:
by

Goal state after:
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, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
by

Goal state after:
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ Set.range v ≠ t

Tactic:
by

Goal state after:
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R (Fin.cons x v)

Tactic:
by

Goal state after:
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ᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ

Tactic:
by

Goal state after:
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R (Fin.snoc v x)

Tactic:
by

Goal state after:
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✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ Fin.snoc ![x] y = ![x, y]

Tactic:
by

Goal state after:
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
⊢ (f ≫ g)ᘁ = gᘁ ≫ fᘁ

Tactic:
by

Goal state after:
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✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
by

Goal state after:
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ Module.rank R (M ⧸ N) ≠ 0

Tactic:
by

Goal state after:
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ₘ g) =
    𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
whisker_exchange

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (η_ (ᘁX) X ▷ 𝟙_ C ≫ (ᘁX ⊗ X) ◁ η_ (ᘁY) Y) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g
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
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g

Tactic:
whisker_exchange

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ((ᘁX ◁ f) ▷ 𝟙_ C ≫ (ᘁX ⊗ Y) ◁ η_ (ᘁY) Y) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g
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
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
by

Goal state after:
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
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥s + finrank K ↥t

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsStablyFiniteRing R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective ⇑f
⊢ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ toMatrixRight' ↑e * toMatrixRight' ↑e.symm = 1

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g = η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ toMatrixRight' ↑e.symm * toMatrixRight' ↑e = 1

Tactic:
by

Goal state after:
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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ᘁf ≫ g) = (ᘁg) ≫ ᘁf

Tactic:
by

Goal state after:
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 t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥s + finrank K ↥t ≤ finrank K V

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
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
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
whisker_exchange

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ 𝟙 (Y' ⊗ X) ⊗≫ Y' ◁ η_ Y Y' ▷ X ⊗≫ (ε_ Y Y' ▷ (Y' ⊗ X) ≫ 𝟙_ C ◁ f) ⊗≫ 𝟙 Z =
    𝟙 (Y' ⊗ X) ⊗≫ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ▷ X ⊗≫ f
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
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
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ (fun f ↦ Y' ◁ f ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom)
      ((fun f ↦ (λ_ X).inv ≫ η_ Y Y' ▷ X ≫ (α_ Y Y' X).hom ≫ Y ◁ f) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
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
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N = finrank R M

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
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 t : Submodule K V
hdim : finrank K V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊓ t) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R M - finrank R ↥N

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Y ⊗ Z
⊢ (fun f ↦ (λ_ X).inv ≫ η_ Y Y' ▷ X ≫ (α_ Y Y' X).hom ≫ Y ◁ f)
      ((fun f ↦ Y' ◁ f ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ RankCondition Rᵐᵒᵖ ↔ RankCondition R

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ Disjoint L f.ker

Tactic:
by

Goal state after:
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 t : Submodule K V
hdim : finrank K V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
⊢ s ⊔ t = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by

Goal state after:
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✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
⊢ v ≠ 0

Tactic:
by

Goal state after: