mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : g x = x
⊢ ∀ {x : α}, g x ≠ x → x ∈ l

Tactic:
intro y

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : g x = x
y : α
⊢ g y ≠ y → y ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ r = 0

Tactic:
rw [← div_euc.1, zpow_add g]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ ↑m * g ^ (↑(orderOf g) * q)) x = x ↔ r = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
⊢ ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g) x_1 ≠ x_1 → x_1 ∈ l

Tactic:
intro y

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
⊢ ((g.cycleOf x)⁻¹ * g) y ≠ y → y ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x → g ^ m = 1

Tactic:
intro hgm

Goal state after:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : (g ^ m) x = x
⊢ g ^ m = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x

Tactic:
intro hgm

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ (g ^ m) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
⊢ ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g) x_1 ≠ x_1 → f.cycleOf x_1 = ((g.cycleOf x)⁻¹ * g).cycleOf x_1

Tactic:
intro y

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
⊢ ((g.cycleOf x)⁻¹ * g) y ≠ y → f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑i

Tactic:
have : subNat i.1 (j.cast (by lia)) (by simp [hij]) = (j - i).castLT (sub_val_lt_sub hij) :=
      eq_of_val_eq (by simp [sub_val_of_le hij])

Goal state after:
case pos
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
this : subNat (↑i) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑i
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr.inl
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
ch : k = i
⊢ ↑((i.cycleIcc i) k) = ↑k

Tactic:
simp [-cycleIcc_def_le, ch]

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

Goal state before:
pp: case inr.inl
n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
ch : x = i
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)

Tactic:
simp [-cycleIcc_def_le, ch]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
⊢ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Tactic:
intro y

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
⊢ y ∈ (f.cycleOf x).support → (f.cycleOf x) y = f y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
⊢ H = ⊤

Tactic:
by
  have : Fact (Fintype.card α).Prime := ⟨h0⟩
  obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
  have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
  have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
  have hσ3 : (σ : Perm α).support = ⊤ :=
    Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
  have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
  rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨Subtype.mem σ, h2⟩

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : ⟨x₁, x₂⟩ ∈ D
⊢ x₂ < x₁

Tactic:
simpa [hD] using hx

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ c_1 ∈ g.cycleFactorsFinset, Commute c c_1

Tactic:
intro c' hc'

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
⊢ Commute c c'
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
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)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) = DFinsupp.single p ((f p) m)

Tactic:
ext q

Goal state after:
ι : Type uι
κ : ι → Type uκ
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)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = (DFinsupp.single p ((f p) m)) q
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    rcases f with ⟨⟨_, _, _⟩, _⟩
    rcases g with ⟨⟨_, _, _⟩, _⟩
    congr

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h'' : ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T mY = T mX
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → f_1 ≫ T mY_1 = T mX_1

Tactic:
obtain ⟨S', T', w'⟩ := h''

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → f_1 ≫ T mY_1 = T mX_1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i : n
⊢ (A * adjp 1 A + detp (-1) A • 1) i i = (A * adjp (-1) A + detp 1 A • 1) i i

Tactic:
add_apply,

Goal state after:
case inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i : n
⊢ (A * adjp 1 A) i i + (detp (-1) A • 1) i i = (A * adjp (-1) A) i i + (detp 1 A • 1) i i
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (A * adjp 1 A + detp (-1) A • 1) i j = (A * adjp (-1) A + detp 1 A • 1) i j

Tactic:
add_apply,

Goal state after:
case inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (A * adjp 1 A) i j + (detp (-1) A • 1) i j = (A * adjp (-1) A) i j + (detp 1 A • 1) i j
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case h.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty (min Y S' ⟶ Y)

Tactic:
exact ⟨minToLeft _ _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h'' : ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T mX ≫ f = T mY
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → T mX_1 ≫ f_1 = T mY_1

Tactic:
obtain ⟨S', T', w'⟩ := h''

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → T mX_1 ≫ f_1 = T mY_1
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
⊢ Function.Bijective (F.descColimitType F.coconeTypes)

Tactic:
by
    convert! Function.bijective_id
    ext y
    obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h : (hom (F.map f)) x = (hom (F.map f)) y
⊢ ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y

Tactic:
exact ⟨j, f, f, h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesLimit F G
inst✝³ : HasLimit F
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (lim ⋙ G).map f ≫ (preservesLimitIso G Y).hom =
      (preservesLimitIso G X).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ lim).map f

Tactic:
intro _ _ f
      apply limit.hom_ext; intro j
      dsimp
      simp only [preservesLimitIso_hom_π, Functor.whiskerRight_app, limMap_π, Category.assoc,
        preservesLimitIso_hom_π_assoc, ← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (colim ⋙ G).map f ≫ (preservesColimitIso G Y✝).hom =
    (preservesColimitIso G X✝).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f

Tactic:
← Iso.inv_comp_eq,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f ≫ (preservesColimitIso G Y✝).hom =
    ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})

Tactic:
preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso.symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u}.obj (F ⋙ uliftFunctor.{v, w'}).reprX)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})

Tactic:
preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftCoyonedaCoreprXIso.symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (uliftCoyoneda.{u_1, v, u}.obj (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Cᵒᵖ ⥤ Type w
t : P.obj X
⊢ shrinkYonedaEquiv (shrinkYonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f.unop ≫ shrinkYonedaEquiv.symm t)

Tactic:
by
    obtain ⟨t, rfl⟩ := shrinkYonedaEquiv.surjective t
    rw [← shrinkYonedaEquiv_naturality]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    (colimitObjIsoColimitCompEvaluation F i).hom ≫ colimMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
← Iso.inv_comp_eq,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    colimMap (F.whiskerLeft ((evaluation K C).map f))
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)

Tactic:
← IsIso.eq_inv_comp,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  (R.associator L R).inv ≫ whiskerRight h.counit R = inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β

Tactic:
cases β

Goal state after:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝¹ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝¹
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝¹, isMonoidal := isMonoidal✝¹ }.hom = { hom := hom✝, isMonoidal := isMonoidal✝ }.hom
⊢ { hom := hom✝¹, isMonoidal := isMonoidal✝¹ } = { hom := hom✝, isMonoidal := isMonoidal✝ }
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
inst✝ : F.Monoidal
T : D
⊢ T ◁ ε F ≫ T ◁ η F = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
inst✝ : F.Monoidal
T : D
⊢ T ◁ (ε F ≫ η F) = 𝟙 (T ⊗ 𝟙_ D)
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
inst✝ : F.Monoidal
T : D
⊢ T ◁ η F ≫ T ◁ ε F = 𝟙 (T ⊗ F.obj (𝟙_ C))

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
inst✝ : F.Monoidal
T : D
⊢ T ◁ (η F ≫ ε F) = 𝟙 (T ⊗ F.obj (𝟙_ C))
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ (μ F X Y ≫ δ F X Y) = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ (δ F X Y ≫ μ F X Y) = 𝟙 (T ⊗ F.obj (X ⊗ Y))