mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ curry f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
⊢ ∀ (f : Y ⟶ (ihom X).obj Z),
    uncurry f =
      (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
        (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
          (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫ (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫ (ρ_ x).hom ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
triangle_assoc_comp_right_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫ x ◁ (λ_ ((ihom x).obj y)).hom ≫ (ihom.ev x).app y = uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ (λ_ ((ihom x).obj y)).inv ≫ id x ▷ (ihom x).obj y ≫ comp x x y = 𝟙 ((ihom x).obj y)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ρ_ ((ihom x).obj y)).inv ≫ (ihom x).obj y ◁ id y ≫ comp x y y = 𝟙 ((ihom x).obj y)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫ comp w x y ▷ (ihom y).obj z ≫ comp w y z =
    (ihom w).obj x ◁ comp x y z ≫ comp w x z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
g : 𝟙_ C ⟶ (ihom X).obj Y
⊢ curry' (uncurry' g) = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ uncurry' (curry' f) = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : X ⟶ Y
⊢ uncurry' (curry' x✝) = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : 𝟙_ C ⟶ (ihom X).obj Y
⊢ curry' (uncurry' x✝) = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry' (𝟙 X) = id X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ (ρ_ X).hom ▷ (ihom Y).obj Z ≫ f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
triangle_assoc_comp_right_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫ X ◁ (λ_ ((ihom Y).obj Z)).hom ≫ f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (λ_ ((ihom Y).obj Z)).hom ≫ (pre f).app Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫ (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f

Tactic:
whiskerLeft_rightUnitor_inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ ((ρ_ (X ⊗ (ihom X).obj Y)).inv ≫ (α_ X ((ihom X).obj Y) (𝟙_ C)).hom) ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
inst✝ : Closed X
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' f ≫ (ihom X).map g = curry' (f ≫ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ₘ curry' g) ≫ comp X Y Z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ (fun f ↦ (β_ M N).hom ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
      ((fun f ↦ ofHom₂ ((TensorProduct.mk R ↑N ↑M).compr₂ (Hom.hom ((β_ N M).hom ≫ f)))) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ ∀ {X' X Y : ModuleCat R} (f : X' ⟶ X) (g : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y),
    (M.monoidalClosedHomEquiv X' Y).symm (f ≫ g) =
      (MonoidalCategory.tensorLeft M).map f ≫ (M.monoidalClosedHomEquiv X Y).symm g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (ihom.ev M).app N =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : DivisionSemiring R
inst✝ : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
⊢ ∃ y, f y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : DivisionSemiring R
inst✝ : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
y : M
hy : f y ≠ 0
⊢ f ((z * (f y)⁻¹) • y) = z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : DivisionSemiring R
inst✝ : Module R M
f : M →ₗ[R] R
⊢ Function.Surjective ⇑f ↔ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Semiring R
inst✝¹ : Module R M
inst✝ : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective ⇑f
x z : M₁
⊢ z ∈ (f.smulRight x).range ↔ z ∈ R ∙ x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
s : Multiset α
⊢ decodeMultiset (encodeMultiset s) = some s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
s : Multiset α
⊢ (fun n ↦ Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s ↦ encode (lower ((Multiset.map encode s).sort fun a b ↦ a ≤ b) 0)) s) =
    s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ (fun s ↦ encode (lower ((Multiset.map encode s).sort fun a b ↦ a ≤ b) 0))
      ((fun n ↦ Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0)) n) =
    n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ lower' (raise' (m :: l) n) n = m :: l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: head✝¹ head✝ : ℕ
tail✝ : List ℕ
x✝ : ℕ
⊢ head✝¹ + x✝ < head✝ + (head✝¹ + x✝ + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (m :: raise' l n)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: α : Type ?u.3
inst✝ : Denumerable α
s : Finset α
⊢ ((fun n ↦ Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0))
        ((fun s ↦ encode (lower' ((Finset.map (eqv α).toEmbedding s).sort fun a b ↦ a ≤ b) 0)) s)).val =
    s.val

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: α : Type ?u.3
inst✝ : Denumerable α
n : ℕ
⊢ (fun s ↦ encode (lower' ((Finset.map (eqv α).toEmbedding s).sort fun a b ↦ a ≤ b) 0))
      ((fun n ↦ Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0)) n) =
    n

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
⊢ #((a : α) × (β a → WType β)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType β
a₂ : α
f₂ : β a₂ → WType β
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
κ : Cardinal.{max u v}
hκ : (sum fun a ↦ κ ^ lift.{u, v} #(β a)) ≤ κ
⊢ #(WType β) ≤ κ

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
x✝ : IsEmpty α
⊢ #(WType β) ≤ max (lift.{v, u} #α) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ Order.succ 0 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
⊢ (sum fun a ↦ #(WType β) ^ lift.{u, u} #(β a)) = sum fun a ↦ #(WType β) ^ #(β a)

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun a ↦ κ ^ lift.{u, u} #(β a)) ≤ κ

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
⊢ 𝟙_ C ◁ (ρ_ (𝟙_ C)).inv ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).inv ≫ (ρ_ (𝟙_ C)).hom ▷ 𝟙_ C = (ρ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
⊢ ¬Finite (WType β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ max (lift.{u, u} #α) ℵ₀ = max #α ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth

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
⊢ (ρ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ (𝟙_ C)).hom = (λ_ (𝟙_ C)).hom ≫ (ρ_ (𝟙_ C)).inv

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType' β 0 → Empty :=
  fun x ↦
    match x with
    | ⟨val, h⟩ => ⋯.elim
⊢ Empty → WType' β 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : t.depth ≤ n + 1
⊢ (a : α) × (β a → WType' β n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
x✝ : Encodable (WType' β n)
⊢ ∀ (b : WType' β (n + 1)), finv n (f n b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
⊢ Encodable (WType β)

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₂
⊢ (Y₂ ⊗ Y₁) ◁ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ≫
      (α_ (Y₂ ⊗ Y₁) (X₁ ⊗ X₂) (Y₂ ⊗ Y₁)).inv ≫ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ (Y₂ ⊗ Y₁) ◁ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ (Y₂ ◁ ε_ X₁ Y₁ ▷ X₂) ▷ (Y₂ ⊗ Y₁) ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) (WType.mk (Sum.inl 1) fun t ↦ Bool.rec x y t) =
    WType.elim (↥(closure s)) (operate s) x * WType.elim (↥(closure s)) (operate s) y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {a b : ↥(closure s)},
    a ∈ Set.range (WType.elim (↥(closure s)) (operate s)) →
      b ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → a * b ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) (WType.mk (Sum.inl 0) fun t ↦ Bool.rec x y t) =
    WType.elim (↥(closure s)) (operate s) x + WType.elim (↥(closure s)) (operate s) y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {a b : ↥(closure s)},
    a ∈ Set.range (WType.elim (↥(closure s)) (operate s)) →
      b ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → a + b ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {x : ↥(closure s)},
    x ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → -x ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ x ∈ Set.range (WType.elim (↥(closure s)) (operate s)), x⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ rangeOfWType s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Function.Surjective (WType.elim (↥(closure s)) (operate s))

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₂
⊢ (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ (Y₂ ⊗ Y₁) ◁ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ (Y₂ ◁ ε_ X₁ Y₁ ▷ X₂) ▷ (Y₂ ⊗ Y₁) ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ ((Y₁ ⊗ X₁) ◁ η_ X₂ Y₂ ≫ ε_ X₁ Y₁ ▷ (X₂ ⊗ Y₂)) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ 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₂
⊢ (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ ((Y₁ ⊗ X₁) ◁ η_ X₂ Y₂ ≫ ε_ X₁ Y₁ ▷ (X₂ ⊗ Y₂)) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁)

Tactic:
whisker_exchange

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁)
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #(WType (Operands s)) ≤ max #↑s ℵ₀

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

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

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
i j : ι
⊢ (b.toDual (b i)) (b j) = if i = j then 1 else 0

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
⊢ Function.Injective ⇑Finsupp.lcoeFun

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
f : ι →₀ R
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) 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
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = 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
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.repr m) 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
i : ι
m : M
⊢ (b.toDual (b i)) m = (b.repr m) 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
i : ι
⊢ b.toDual (b i) = b.coord 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 ι
m : M
i : ι
⊢ (b.toDual m) (b i) = b.equivFun m i

Tactic:
by

Goal state after: