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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({c ∈ σ.cycleFactorsFinset.attach | #(↑c).support = n})

Tactic:
Finset.filter_attach',

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #(Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ }
        {x ∈ σ.cycleFactorsFinset | ∃ (h : x ∈ σ.cycleFactorsFinset), #(↑⟨x, h⟩).support = n}.attach)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∈ f.support
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun f ↦ Classical.decRel f.SameCycle
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∈ f.support
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun f ↦ Classical.decRel f.SameCycle
i : ℕ
hixy : i < #(f.cycleOf x).support
hi : (f ^ i) x = y
⊢ ∃ m < Fintype.card α, (f ^ m) x = y
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
this : (g ^ m) x = x ↔ g ^ m = 1
⊢ (g ^ m) x = x ↔ m = 0

Tactic:
rw [this]

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
this : (g ^ m) x = x ↔ g ^ m = 1
⊢ g ^ m = 1 ↔ m = 0
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ

Tactic:
Fin.lt_def

Goal state after:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p i : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) i = (x ∘ ⇑(Equiv.symm p.cycleRange)) i

Tactic:
cases i using Fin.cons

Goal state after:
case x
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) 0 = (x ∘ ⇑(Equiv.symm p.cycleRange)) 0

case p
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
i✝ : Fin n
⊢ cons (x p) (p.removeNth x) i✝.succ = (x ∘ ⇑(Equiv.symm p.cycleRange)) i✝.succ
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
b : α
⊢ b ∈ σ.supportᶜ ↔ σ b = b

Tactic:
rw [Finset.mem_compl, mem_support, Classical.not_not]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ 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
i j : Fin n
hij : j < i
⊢ min (σ i) (σ j) ≠ max (σ i) (σ j)

Tactic:
by simp [hij.ne.symm]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn✝ : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : n ∈ σ.cycleType
⊢ 0 < n

pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn✝ : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : n ∈ Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ 0 < n

Tactic:
· exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn✝ : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
hn : n ∈ Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ 0 < n
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support

Tactic:
· intro h
    use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h
    rw [mem_support_cycleOf_iff]
    exact ⟨SameCycle.refl g x, h⟩

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
by
  rw [disjoint_iff_disjoint_support] at h
  rw [Finset.disjoint_left]
  intro x hx hy
  simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
  obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
  have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
  tauto

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType

Tactic:
rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : (n ::ₘ 0).sum = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

Tactic:
cons_zero,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : {n}.sum = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
rw [this]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = c.cycleOf a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset

Tactic:
· exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))

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

Goal state before:
pp: case pos
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₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
h : j = i
⊢ update (t.piecewise (m + m') m') i (m i) i = t.piecewise (m + m'') m'' i

Tactic:
simp [m'', hit]

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

Goal state before:
pp: case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp (-1) A

Tactic:
rw [this]

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

Goal state before:
pp: case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp 1 A

Tactic:
rw [this]

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

Goal state before:
pp: case e_a
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₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
this : (insert i s).piecewise m m' = s.piecewise m m''
⊢ f (s.piecewise m m'') = f ((insert i s).piecewise m m')

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.add zero) = descFunLift F s x

Tactic:
| add_zero x =>

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.add zero) = descFunLift F s x

Tactic:
| add_zero x =>

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

Goal state before:
pp: case pos
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₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
this : A i₀ = B i₀ ∪ C i₀
⊢ ∑ j ∈ A i₀, g i₀ j = ∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j

Tactic:
rw [this]

Goal state after:
case pos
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₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
this : A i₀ = B i₀ ∪ C i₀
⊢ ∑ j ∈ B i₀ ∪ C i₀, g i₀ j = ∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
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₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝¹ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
this✝ : A i₀ = B i₀ ∪ C i₀
j : α i₀
hj : j ∈ C i₀
this : j = j₂
⊢ j ∉ B i₀

Tactic:
rw [this]

Goal state after:
case pos
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₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝¹ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
this✝ : A i₀ = B i₀ ∪ C i₀
j : α i₀
hj : j ∈ C i₀
this : j = j₂
⊢ j₂ ∉ B i₀
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
i j j' : C
f : j ⟶ i
f' : j' ⟶ i
K : C
G : K ⟶ j
G' : K ⟶ j'
h✝ : True
k : C
e : k ⟶ K
he : e ≫ G ≫ f = e ≫ G' ≫ f'
⊢ (e ≫ G) ≫ f = (e ≫ G') ≫ f'

Tactic:
by simpa only [Category.assoc] using he

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map ij)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map (li ≫ ij)))

Tactic:
F.map_comp

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map ij)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map li ≫ F.map ij))
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map kj)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map (lk ≫ kj)))

Tactic:
F.map_comp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map kj)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map lk ≫ F.map kj))
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i : J) (x y : (fun X ↦ X) (F.obj i)),
    (hom (t.ι.app i)) x = (hom (t.ι.app i)) y → ∃ k f, (hom (F.map f)) x = (hom (F.map f)) y
i j : J
xi : (fun X ↦ X) (F.obj i)
xj : (fun X ↦ X) (F.obj j)
h : (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj
⊢ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj

Tactic:
obtain ⟨k, g, hg⟩ := hinj (IsFiltered.max i j) (F.map (IsFiltered.leftToMax i j) xi)
      (F.map (IsFiltered.rightToMax i j) xj)
      (by set_option backward.isDefEq.respectTransparency true in simp_all)
    exact ⟨k, IsFiltered.leftToMax i j ≫ g, IsFiltered.rightToMax i j ≫ g, by simpa using hg⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, ((prodCongrLeft fun k ↦ a₁ k ⋯) = prodCongrLeft fun k ↦ a₂ k ⋯) → a₁ = a₂

Tactic:
intro σ _ σ' _ eq

Goal state after:
case refine_2
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k ↦ σ k ⋯) = prodCongrLeft fun k ↦ σ' k ⋯
⊢ σ = σ'
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ↑(G F)

Tactic:
refine Quot.lift (colimitInvAux.{v, u} F) ?_ x
    intro x y h
    apply colimitInvAux_eq_of_rel
    apply Types.FilteredColimit.rel_of_colimitTypeRel
    exact h

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

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
this : ∀ (c_1 : Cone F) (y : c_1.pt), ∃! x, ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j
x : (c_1 : Cone F) → c_1.pt → c.pt
hx :
  ∀ (c_1 : Cone F) (y : c_1.pt),
    (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j) (x c_1 y) ∧
      ∀ (y_1 : c.pt), (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j) y_1 → y_1 = x c_1 y
⊢ IsLimit c

Tactic:
exact ⟨fun d ↦ ↾(x d), fun c j ↦ by ext y; exact (hx c y).1 j,
      fun c f hf ↦ by ext y; exact (hx c y).2 (f y) (fun j ↦ congr_hom (hf j) y)⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
ext x
    apply Subtype.ext
    funext j
    exact congr_hom (w j) x

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
pow_add,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ x, (-1) ^ ↑i * (-1) ^ ↑x * A i x * (A.submatrix i.succAbove x.succAbove).det
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso i.inv
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso i.hom
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ (evaluation C (Type v)).obj K)

Tactic:
change PreservesLimitsOfSize (yoneda.obj K)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda.obj K)
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
⊢ ∀ (c_1 : R) (x : ↑(((Functor.const J).obj c.pt).obj j)),
    ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1 * x =
      x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1

Tactic:
by
    intro r x
    obtain ⟨k, hjk, y, rfl⟩ := Concrete.exists_hom_ι_eq_of_isColimit _ hc x j
    simp [← dsimp% c.w hjk, ← dsimp% (c.ι.app k).hom.map_mul, Algebra.commutes']

Goal state after: