mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
hxp : f ∈ ↑(noncommPiCoprod (fun x ↦ ϕ ↑x) ?intro.hcomm).range
⊢ f ∈ ⊥

pp: case intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)

Tactic:
rotate_left

Goal state after:
case intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)

case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
hxp : f ∈ ↑(noncommPiCoprod (fun x ↦ ϕ ↑x) ?intro.hcomm).range
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Tactic:
refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩
  rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ (decomposeFin.symm (0, e)) x.succ = (swap 0 0) (e x).succ

pp: case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
· simp [Equiv.Perm.decomposeFin]

Goal state after:
case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
i j : Fin 0
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

pp: case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

Tactic:
· exact absurd le_rfl j.pos.not_ge

Goal state after:
case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c

Tactic:
(List.perm_cons_erase cl).pairwise_iff symm

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ c_1 τ, l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
b : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
exact ⟨b, (h b).mp hb1, hb2⟩

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
⊢ cycleIcc 0 i = i.cycleRange

Tactic:
ext x
  rcases lt_trichotomy x i with ch | ch | ch
  · simp [-cycleIcc_def_le, cycleIcc_of_ge_of_lt (zero_le x) ch, cycleRange_of_lt ch]
  · simp [-cycleIcc_def_le, ch]
  · simp [-cycleIcc_def_le, cycleIcc_of_gt ch, cycleRange_of_gt ch]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
⊢ ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)

Tactic:
by
  ext x
  rcases lt_or_ge x i with ch | ch
  · simp [cycleIcc_of_lt (lt_of_lt_of_le ch hij), cycleIcc_of_lt ch]
  rcases lt_or_ge k x with ch | ch1
  · simp [cycleIcc_of_gt (lt_of_le_of_lt hjk ch), cycleIcc_of_gt ch]
  rcases lt_or_ge x j with ch2 | ch2
  · simp [cycleIcc_of_lt ch2, cycleIcc_of_le_of_le ch ch1, cycleIcc_of_le_of_le ch (le_of_lt ch2)]
    split_ifs
    repeat lia
  · simp only [Function.comp_apply, cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]
    split_ifs with h
    · exact val_eq_of_eq (cycleIcc_of_last hij)
    · simp [cycleIcc_of_gt (lt_of_le_of_lt ch2 (lt_add_one_of_succ_lt (by lia)))]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (c • x) i_1).support') }
      p =
    (c •
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') })
      p

Tactic:
dsimp
    simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))

Tactic:
rw [← hσ, ← hτ, ← sign_inv] at h

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
h : sign σ⁻¹ ≠ sign τ
hτ : sign τ = t
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case neg
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : ¬i' = i
⊢ B i' j' + c i' * B k j' = B i' j' + c i' * B.updateRow i (A i) k j'

Tactic:
updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s

Goal state after:
case neg
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : ¬i' = i
⊢ B i' j' + c i' * B k j' = B i' j' + c i' * B k j'
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
⊢ ∀ (c : Fin n → R),
    (∀ (i : Fin n), 0 < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det

Tactic:
intro c hc M N h0 hsucc

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
⊢ M.det = N.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
⊢ ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.succ < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det

Tactic:
intro c hc M N h0 hsucc

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
⊢ M.det = N.det
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (f.linearDeriv x) y = ∑ i, f (update x i (y i))

Tactic:
by
  unfold linearDeriv
  simp only [LinearMap.coe_sum, LinearMap.coe_comp, LinearMap.coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, toLinearMap_apply]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩

Tactic:
colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ ⟨j, y⟩ k f g,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map f)) ⟨i, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map g)) ⟨j, y⟩.snd⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X✝ Y✝ : C
f : X✝ ⟶ Y✝
g : ((evaluation Cᵒᵖ (Type w)).obj Y).obj (shrinkYoneda.{w, v, u}.obj X✝)
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v, u} ⋙ (evaluation Cᵒᵖ (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
            (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom)).toFun
      { down := g } =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
            (coyoneda.obj Y ⋙ uliftFunctor.{w, v}).map f)).toFun
      { down := g }

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X✝ Y✝ : C
f : X✝ ⟶ Y✝
g : unop Y ⟶ X✝
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v, u} ⋙ (evaluation Cᵒᵖ (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
            (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom)).toFun
      { down := shrinkYonedaObjObjEquiv.symm g } =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
            (coyoneda.obj Y ⋙ uliftFunctor.{w, v}).map f)).toFun
      { down := shrinkYonedaObjObjEquiv.symm g }
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv

Tactic:
rw [← assoc, ← leftUnitor_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (𝟙 X ▷ Y) = F.map (𝟙 (X ⊗ Y))

Tactic:
simp [fData.whiskerRight_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
X✝ Y✝ : D
x✝ : X✝ ⟶ Y✝
⊢ ∀ (X' : D), F.map x✝ ▷ F.obj X' ≫ (fData.μIso Y✝ X').hom = (fData.μIso X✝ X').hom ≫ F.map (x✝ ▷ X')

Tactic:
simp [fData.whiskerRight_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j = X ◁ biproduct.π f j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j = X ◁ biproduct.π f j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j ↦ X ⊗ f j) j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j ↦ X ⊗ f j) j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j ↦ X ⊗ f j) j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j ↦ X ⊗ f j) j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y : C
f : J → C
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y : C
f : J → C
val✝ : Fintype J
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j ↦ f j ⊗ X) j = biproduct.π f j ▷ X

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
val✝ : Fintype J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j ↦ f j ⊗ X) j = biproduct.π f j ▷ X
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
⊢ biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j ↦ f j ⊗ X) j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
val✝ : Fintype J
⊢ biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j ↦ f j ⊗ X) j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j ↦ f j ⊗ X) j

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
val✝ : Fintype J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j ↦ f j ⊗ X) j
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j ↦ f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
val✝ : Fintype J
⊢ biproduct.ι (fun j ↦ f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
⊢ (rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ (f x) X Y).symm

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
val✝ : Fintype J
⊢ (rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ (f x) X Y).symm