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

Goal state before:
pp: case inl.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ τ = υ ∨ τ = swap i j * υ

Tactic:
hτυ,

Goal state after:
case inl.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ swap i j * υ = υ ∨ swap i j * υ = swap i j * υ
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ swap i j * τ = υ ∨ swap i j * τ = swap i j * υ

Tactic:
hτυ,

Goal state after:
case inr.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ swap i j * υ = υ ∨ swap i j * υ = swap i j * υ
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ swap i j * τ = υ ∨ swap i j * τ = swap i j * υ

Tactic:
hτυ,

Goal state after:
case inr.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ swap i j * (swap i j * υ) = υ ∨ swap i j * (swap i j * υ) = swap i j * υ
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ)
lts : i < j.castSucc
⊢ swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
exact mul_mem (mul_mem mem <| ih lts.ne lts) mem

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z

Tactic:
by
      rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
i : ℤ
hy : ¬σ ((σ ^ i) (Classical.choose hσ)) = (σ ^ i) (Classical.choose hσ)
⊢ (σ ^ i) ((σ ^ m) (Classical.choose hσ)) = (σ ^ i) ((σ ^ n) (Classical.choose hσ))

Tactic:
exact congr_arg _ (Subtype.ext_iff.mp h)

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

Goal state before:
pp: case intro.mpr.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
this : ∀ {a b : ℕ}, (f ^ a) x = (f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

Tactic:
exact (this hx'.symm (le_of_not_ge hab)).symm

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign p * sign (f.trans g)

Tactic:
rw [← sign_permCongr g, ← sign_mul]

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign (g.permCongr p * f.trans g)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr σb) = sign σa * sign σb

Tactic:
suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb
    by rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ ∅.Countable

Tactic:
exact Set.countable_empty

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

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 2)).support = Finset.univ

Tactic:
by
  ext
  simp

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

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

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_gt ch, cycleRange_of_gt ch]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : x ∉ f.support
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
rw [notMem_support, ← cycleOf_eq_one_iff] at hc

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle
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
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ⁻¹) * ∏ j, ∏ i < j, f i j

Tactic:
σ⁻¹.sign_eq_prod_prod_Iio,

Goal state after:
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
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(∏ j, ∏ i < j, if σ⁻¹ i < σ⁻¹ j then 1 else -1) * ∏ j, ∏ i < j, f i j
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]

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

Goal state before:
pp: case refine_3
α : 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 α
⊢ f ∈ σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset →
    (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

Tactic:
mem_union

Goal state after:
case refine_3
α : 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 α
⊢ f ∈ σ.cycleFactorsFinset ∨ f ∈ τ.cycleFactorsFinset →
    (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
x y : M p
⊢ f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)

Tactic:
by
  simpa using f.map_update_add (p.insertNth 0 m) p x y

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1, A i_1 (i i_1) * B (i i_1) (x i_1) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ i, A i (ι x i) * B (ι x i) (x_1 i) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ i, A i (ι x i) * B (ι x i) (x_1 i)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))

Tactic:
simp_rw [hι]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |↑↑(sign (e₁.symm.trans e₂)) * A.det| = |A.det|

Tactic:
abs_mul,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |↑↑(sign (e₁.symm.trans e₂))| * |A.det| = |A.det|
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
⊢ ∀ (i j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)

Tactic:
intro i j

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 : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2._hsucc
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' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ ∀ (i : Fin n) (j : Fin n.succ), M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j

Tactic:
intro i j

Goal state after:
case refine_2._hsucc
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' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
⊢ M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update z i (c • a) ⟨j, h⟩ else z✝ ⟨j, h⟩) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_smul]

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

Goal state before:
pp: case refine_3
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
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ

Tactic:
have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by
        intro k x
        ext
        · simp only
        · simp only [hσ]

Goal state after:
case refine_3
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
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂))) x) *
      (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂))) y) =
    (ConcreteCategory.hom (F.map γ)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₃ j₂))) x') *
      (ConcreteCategory.hom (F.map γ)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₃ j₂))) y)

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α)) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α)) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₃ j₂) ≫ F.map γ)) x' *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ)) y
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ ↑(↑(sumCongrHom m n).range).toFinset
⊢ σ ∈ (fun σ ↦ σ.1.sumCongr σ.2) '' ↑univ

Tactic:
rw [mem_coe, Set.mem_toFinset] at hσ

Goal state after:
case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ ↑(sumCongrHom m n).range
⊢ σ ∈ (fun σ ↦ σ.1.sumCongr σ.2) '' ↑univ
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂))) x) *
      (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂))) y) =
    (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map f)) x) *
      (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map g)) y)

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α)) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α)) y =
    (ConcreteCategory.hom (F.map f ≫ F.map β)) x * (ConcreteCategory.hom (F.map g ≫ F.map β)) y
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x ↦ R) M₂
⊢ MultilinearMap.mkPiRing R ι (f fun x ↦ 1) = f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Tactic:
simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂) ↔ z₁ = z₂
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) (id j) * (A.submatrix (⇑i.cycleRange⁻¹ ∘ Fin.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
Function.comp_def,

Goal state after:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) (id j) * (A.submatrix (fun x ↦ i.cycleRange⁻¹ x.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (c.π.app (Opposite.op 0)))

Tactic:
by
  let i := hc.conePointUniqueUpToIso (limitConeIsLimit F)
  have : c.π.app ⟨0⟩ = i.hom ≫ (limitCone F).π.app ⟨0⟩ := by simp [i]; rfl
  rw [this, types_comp]
  apply Function.Surjective.comp
  · exact surjective_π_app_zero_of_surjective_map_aux hF
  · rw [← epi_iff_surjective]
    infer_instance

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

Goal state before:
pp: case inr
J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
h✝ : Nonempty J
i : J
⊢ Nontrivial ↑c.pt

Tactic:
refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩

Goal state after:
case inr
J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
h✝ : Nonempty J
i : J
h : (ConcreteCategory.hom (c.ι.app i)) 0 = (ConcreteCategory.hom (c.ι.app i)) 1
⊢ False
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✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
by
  ext
  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
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
by
  ext
  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
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ f = g

Tactic:
apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1

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
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
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
g : X✝ ⟶ Y✝
⊢ uliftYoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkYoneda.{max w' v, v, u}.map g

Tactic:
by
      ext
      exact (shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm _ _).symm

Goal state after:
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
X : C
⊢ L.preimage (h.counit.app (L.obj X)) ≫ h.unit.app X = 𝟙 ((L ⋙ R).obj X)

Tactic:
simp [← h.unit_naturality (L.preimage (h.counit.app (L.obj X)))]

Goal state after: