mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.repr x) i = (b.repr y) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : b.toDual m = 0
⊢ b.toDual m = b.toDual 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) (Finsupp.equivFunOnFinite.symm fun i ↦ f (b i)))) (b i) = f (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
⊢ ∑ x, f (b x) • b.coord x = f

Tactic:
by

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

Goal state before:
pp: 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 ↦ bK i.1 i.2)
⊢ #↥L < #K

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ (b.dualBasis i) (b j) = if j = i then 1 else 0

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ▷ (X₁ ⊗ X₂) ≫
      (α_ (X₁ ⊗ X₂) (Y₂ ⊗ Y₁) (X₁ ⊗ X₂)).hom ≫ (X₁ ⊗ X₂) ◁ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) =
    η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫ (X₁ ⊗ X₂) ◁ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ (b.dualBasis.repr l) i = l (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ ⇑b.dualBasis = b.coord

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ b.dualBasis.equivFun l i = l (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ Injective ⇑(Dual.eval R M)

Tactic:
by

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

Goal state before:
pp: 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 ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
⊢ ℵ₀ ≤ #ιL

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ (Dual.eval R M).range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i : ι
f : M
⊢ (b.dualBasis.coord i) (b.toDualEquiv f) = (b.coord i) f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i : ι
f : Dual R M
⊢ (b.coord i) (b.toDualEquiv.symm f) = (b.dualBasis.coord i) f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ i ∈ ⋯.toFinset ↔ (ε i) m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (lc e l) = l i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
⊢ h.coeffs (lc e l) = l

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
⊢ ∀ (i : ι), (ε i) (lc e (h.coeffs m)) = (ε i) 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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫ (X₁ ⊗ X₂) ◁ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ =
    η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ (Y₁ ⊗ X₁) ≫ (X₂ ⊗ Y₂) ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
⊢ h.coeffs (v + w) = h.coeffs v + h.coeffs w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
⊢ h.coeffs (c • v) = (RingHom.id R) c • h.coeffs 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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ (Y₁ ⊗ X₁) ≫ (X₂ ⊗ Y₂) ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ =
    η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (𝟙_ C ◁ ε_ X₁ Y₁ ≫ η_ X₂ Y₂ ▷ 𝟙_ C) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ 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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (𝟙_ C ◁ ε_ X₁ Y₁ ≫ η_ X₂ Y₂ ▷ 𝟙_ C) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ =
    𝟙 (𝟙_ C ⊗ X₁ ⊗ X₂) ⊗≫
      (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ 𝟙_ C)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
⊢ ⇑h.basis = e

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 (𝟙_ C ⊗ X₁ ⊗ X₂) ⊗≫
      (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ 𝟙_ C) =
    (λ_ (X₁ ⊗ X₂)).hom ≫ (ρ_ (X₁ ⊗ X₂)).inv

Tactic:
rw [evaluation_coevaluation'', evaluation_coevaluation'']; monoidal

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

Goal state before:
pp: 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 ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
⊢ False

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 (𝟙_ C ⊗ X₁ ⊗ X₂) ⊗≫
      (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ 𝟙_ C) =
    (λ_ (X₁ ⊗ X₂)).hom ≫ (ρ_ (X₁ ⊗ X₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
⊢ ∀ (i : ι), (ε i) x ≠ 0 → i ∈ H

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ▷ (X₁ ⊗ X₂) ≫
      (α_ (X₁ ⊗ X₂) (Y₂ ⊗ Y₁) (X₁ ⊗ X₂)).hom ≫ (X₁ ⊗ X₂) ◁ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) =
    (λ_ (X₁ ⊗ X₂)).hom ≫ (ρ_ (X₁ ⊗ X₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
i j : ι
⊢ (h.basis.dualBasis i) (h.basis j) = (ε i) (h.basis j)

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 : C
inst✝ : HasRightDual X
⊢ 𝟙 Xᘁ = 𝟙 Xᘁ

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 : C
inst✝ : HasLeftDual X
⊢ (ᘁ𝟙 X) = 𝟙 ᘁX

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

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
⊢ Nontrivial R

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.{u, u_1} R
f : M →ₗ[R] M'
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
⊢ Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M

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.{u, u_1} R
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R M = Module.rank R M₁ + Module.rank R ↥f.ker

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.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
⊢ ∀ x ∈ comap f p, f x ∈ p

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.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
x : M
hx : x ∈ Submodule.map (comap f p).subtype f'.ker
⊢ x ∈ f.ker

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.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
⊢ Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker

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.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
⊢ Module.rank R ↥f'.range ≤ Module.rank R ↥p

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.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

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' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ Submodule.map (Submodule.map f p).mkQ f.range = f'.ker

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' ⧸ 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
⊢ Surjective ⇑g

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

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)

Tactic:
by

Goal state after:
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)
⊢ Infinite ιK

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' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
by

Goal state after:
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
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
by

Goal state after:
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
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

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
⊢ 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:
by

Goal state after:
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
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
by

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

Goal state after:
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 →ₗ[K] K)

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
⊢ p ≤ comap f.rangeRestrict (Submodule.map f.rangeRestrict p)

Tactic:
by

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 →ₗ[K] K)

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
⊢ η_ Y Yᘁ ≫ (g ⊗ₘ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommHopfAlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

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
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

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 : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after: