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

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

Tactic:
rw [hwz]

Goal state after:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))

Tactic:
(rw [trans_apply])

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle

Tactic:
simp only [zpow_negSucc, Perm.support_inv] at h1 h2

Goal state after:
case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ (a✝ + 1))⁻¹.IsCycle
h2 : f.support ⊆ (f ^ (a✝ + 1)).support
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ sign (↑l).prod = sign (List.map ⇑ofSubtype ↑l).prod

Tactic:
rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]

Goal state after:
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)

Tactic:
by rw [mul_assoc, mul_self_zpow]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
x : α
hx : x ∈ ↑σ.support
⊢ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ x, ⋯⟩))) =
    τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨x, hx⟩)))

Tactic:
obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
n : ℕ
hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support
⊢ ↑(hτ.zpowersEquivSupport
        ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ ((σ ^ n) (Classical.choose hσ)), ⋯⟩))) =
    τ
      ↑(hτ.zpowersEquivSupport
          ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), hx⟩)))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
rw [prodExtendRight_apply_ne _ ha']

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
sum_smul_sum,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ i ∈ s, ∑ j ∈ s, f i • g j = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Tactic:
exact ⟨k, rfl⟩

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

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ (if f.SameCycle x y then f y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
split_ifs with hy

Goal state after:
case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : f.SameCycle x y
⊢ f y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : ¬f.SameCycle x y
⊢ y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Tactic:
exact hσ.ne_one

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : i < j
⊢ i.cycleRange j = j

Tactic:
rw [cycleRange, Perm.extendDomain_apply_not_subtype]
  simpa using h

Goal state after:
Module: Mathlib.Data.FunLike.Group

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
⊢ Function.Injective ⇑(coeMulHom F α β)

Tactic:
rw [coe_coeMulHom]
  exact DFunLike.coe_injective

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

Goal state before:
pp: case intro.mp
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ σ ∈ l → ∀ (a : α), σ a ≠ a → σ a = l.prod a

pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ (∀ (a : α), σ a ≠ a → σ a = l.prod a) → σ ∈ l

Tactic:
· intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ (∀ (a : α), σ a ≠ a → σ a = l.prod a) → σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ v.toList.prod⁻¹ * v.toList.prod = 1

Tactic:
inv_mul_cancel

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ 1 = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
inst✝ : NeZero n
⊢ (j.cycleIcc i).cycleType = ∅

Tactic:
simpa using cycleIcc_ge hij

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 : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) → x ∈ f.support

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support → (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a

Tactic:
· rintro ⟨hc, _⟩
    contrapose hc
    rw [notMem_support, ← cycleOf_eq_one_iff] at hc
    simp [hc]

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

Goal state before:
pp: G : Type u_3
inst✝² : AddGroup G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card (Multiplicative G)

Tactic:
convert! hdvd

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ ↑c = g.cycleOf ((g ^ m) x) ↔ x ∈ (↑c).support

Tactic:
cycleOf_self_apply_zpow,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ ↑c = g.cycleOf x ↔ x ∈ (↑c).support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ 3 ≤ #{g a, g (g a)} + 1

Tactic:
rw [Finset.card_insert_eq_ite, if_neg]
        · simp
        · simpa using Ne.symm ha

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

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp 1 B + detp (-1) B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1

Tactic:
mul_adjp_add_detp,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B + detp 1 B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: 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
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩

Tactic:
obtain ⟨s, α, β, h₁, h₂⟩ := IsFiltered.bowtie (IsFiltered.leftToMax j₁ j₂) f
    (IsFiltered.rightToMax j₁ j₂) g

Goal state after:
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 ≫ β
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
x y : ↑(M F)
⊢ x * y = y * x

Tactic:
obtain ⟨i, x, rfl⟩ := x.mk_surjective
      obtain ⟨j, y, rfl⟩ := y.mk_surjective
      let k := max' i j
      let f := IsFiltered.leftToMax i j
      let g := IsFiltered.rightToMax i j
      rw [colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ ⟨j, y⟩ k f g,
        colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ ⟨i, x⟩ k g f]
      dsimp
      rw [mul_comm]

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
x y : ↑(M F)
⊢ x * y = y * x

Tactic:
by
      obtain ⟨i, x, rfl⟩ := x.mk_surjective
      obtain ⟨j, y, rfl⟩ := y.mk_surjective
      let k := max' i j
      let f := IsFiltered.leftToMax i j
      let g := IsFiltered.rightToMax i j
      rw [colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ ⟨j, y⟩ k f g,
        colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ ⟨i, x⟩ k g f]
      dsimp
      rw [mul_comm]

Goal state after:
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 : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with #x_1 = 0 ∨ #x_1 = 1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)

Tactic:
filter_or,

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ {a ∈ Finset.univ.powerset | #a = 0} ∪ {a ∈ Finset.univ.powerset | #a = 1}, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
⊢ IsLimit ((forget₂ CommGrpCat GrpCat).mapCone c)

Tactic:
have : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat) := by
      rw [GrpCat.hasLimit_iff_small_sections]
      change Small.{u} (F ⋙ forget CommGrpCat).sections
      rw [← CommGrpCat.hasLimit_iff_small_sections]
      exact ⟨_, hc⟩

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
this : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
⊢ IsLimit ((forget₂ CommGrpCat GrpCat).mapCone c)
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
simp only [← id_tensorHom, ← tensorHom_id]
  rw [← assoc, ← associator_naturality]
  simp

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

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
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
E' : Type u₄
inst✝⁶ : Category.{v₄, u₄} E'
inst✝⁵ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁴ : F₁.LaxMonoidal
inst✝³ : F₂.LaxMonoidal
inst✝² : F₃.LaxMonoidal
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (Functor.whiskerRight τ G₁)

Tactic:
← Functor.hcomp_id

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
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
E' : Type u₄
inst✝⁶ : Category.{v₄, u₄} E'
inst✝⁵ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁴ : F₁.LaxMonoidal
inst✝³ : F₂.LaxMonoidal
inst✝² : F₃.LaxMonoidal
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (τ ◫ 𝟙 G₁)
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
j : J
⊢ ((coconeOfConeLeftOp c).ι.app j ≫ (hc.lift (coneLeftOpOfCocone s)).op).unop = (s.ι.app j).unop

Tactic:
by
      simp only [coconeOfConeLeftOp_ι_app, unop_comp, Quiver.Hom.unop_op, IsLimit.fac,
        coneLeftOpOfCocone_π_app, unop_op]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g : Y✝ ⟶ Z✝
x✝ : C
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ 𝟙 x✝)

Tactic:
rwa [Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
hf₀ : W f✝
⊢ W f✝

Tactic:
exact hf₀

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
← mono_iff_injective

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Mono ((forget C).map f)
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
← mono_iff_injective

Goal state after:
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.unop g.unop ↔ HasPullback f g

Tactic:
rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.unop g.unop ↔ HasPushout f g

Tactic:
rw [HasPullback, hasLimit_iff_of_iso (cospanUnop f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_leftOp_iff_hasColimit]

Goal state after: