mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_1
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this : IsLimit
  ((Cone.postcompose (Discrete.functorComp f ⇑g).inv).obj
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone)) :=
  hc.isLimit.ofIsoLimit (c.whiskerToCone g)
⊢ IsLimit c.toCone

Tactic:
let := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this

Goal state after:
case refine_1
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this✝ : IsLimit
  ((Cone.postcompose (Discrete.functorComp f ⇑g).inv).obj
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone)) :=
  hc.isLimit.ofIsoLimit (c.whiskerToCone g)
this : IsLimit (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone) :=
  (IsLimit.postcomposeHomEquiv (Discrete.functorComp f ⇑g).symm
      (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone))
    this✝
⊢ IsLimit c.toCone
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv) =
    G.map (F.map f') + G.map ((F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv)

Tactic:
← hg',

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map f') + G.map (F.map g')
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : BinaryBicone P Q
f : X✝ ⟶ Y✝
⊢ { pt := F.obj X✝.pt, fst := F.map X✝.fst, snd := F.map X✝.snd, inl := F.map X✝.inl, inr := F.map X✝.inr, inl_fst := ⋯,
          inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inl ≫
      F.map f.hom =
    { pt := F.obj Y✝.pt, fst := F.map Y✝.fst, snd := F.map Y✝.snd, inl := F.map Y✝.inl, inr := F.map Y✝.inr,
        inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inl

Tactic:
simp [-BinaryBiconeMorphism.winl, ← f.winl]

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

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

Tactic:
simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        ← Equiv.eq_symm_apply, h]

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

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : ¬g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

Tactic:
simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        ← Equiv.eq_symm_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl

Tactic:
intro h
    exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case hnc
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ

Tactic:
· exact not_not.mpr k.2

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
x✝² x✝¹ : R
x✝ : ↑(mkOfSMul' φ)
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by simp; rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s) →
    f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s

Tactic:
rintro ⟨n1, n2, rfl, g, rfl, rfl, hgsupp⟩

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ (g.update a n1) a + ∑ x ∈ s, (g.update a n1) x = n1 + s.sum ⇑g ∧ (g.update a n1).support ⊆ insert a s
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
hf : x ∉ f.support
hg : x ∉ g.support
⊢ 0 = g x

Tactic:
notMem_support_iff.mp hg

Goal state after:
case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
hf : x ∉ f.support
hg : x ∉ g.support
⊢ 0 = 0
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s

Tactic:
· rw [notMem_support.mp hx']

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n✝ n : ℕ
c : CompositionAsSet (n + 1)
k : Fin n
i_mem : k.castSucc.succ ∈ c.boundaries
i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)
⊢ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑k.castSucc.succ = ↑j + 1

Tactic:
use k

Goal state after:
case h
n✝ n : ℕ
c : CompositionAsSet (n + 1)
k : Fin n
i_mem : k.castSucc.succ ∈ c.boundaries
i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)
⊢ ⟨↑k + 1, ⋯⟩ ∈ c.boundaries ∧ ↑k.castSucc.succ = ↑k + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ k % ↑(orderOf f) < ↑(orderOf f)

Tactic:
exact Int.emod_lt_of_pos _ h₀

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (swap x y).signAux = -1

Tactic:
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]

Goal state after:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
h₁ : ∀ (x : α), x ∈ ⟦l₁⟧
h₂ : ∀ (x : α), x ∈ ⟦l₂⟧
x✝ : h₁ ≍ h₂
⊢ signAux2 l₁ f ≍ signAux2 l₂ f

Tactic:
← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
h₁ : ∀ (x : α), x ∈ ⟦l₁⟧
h₂ : ∀ (x : α), x ∈ ⟦l₂⟧
x✝ : h₁ ≍ h₂
⊢ signAux ((e.symm.trans f).trans e) ≍ signAux2 l₂ f
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : (a :: l).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
List.nodup_cons

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ l.Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
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
⊢ IsConj σ τ

Tactic:
refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_
  intro x hx
  simp only [Equiv.trans_apply]
  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
  simp [← Perm.mul_apply, ← pow_succ']

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ Finset.univ.noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y

Tactic:
rw [← Finset.insert_erase (Finset.mem_univ i)]

Goal state after:
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ (insert i (Finset.univ.erase i)).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f⁻¹.cycleOf x ^ (z + 1)) x = (f⁻¹ ^ (z + 1)) x

Tactic:
cycleOf_pow_apply_self

Goal state after:
case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f⁻¹ ^ (z + 1)) x = (f⁻¹ ^ (z + 1)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = τ.cycleType
⊢ IsConj 1 τ

Tactic:
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]

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

Goal state before:
pp: M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst✝⁶ : SMul M β
inst✝⁵ : SMul M' β
inst✝⁴ : SMul M F
inst✝³ : SMul M' F
inst✝² : IsSMulApply M F α β
inst✝¹ : IsSMulApply M' F α β
inst✝ : SMulCommClass M M' β
x✝² : M
x✝¹ : M'
x✝ : F
⊢ x✝² • x✝¹ • x✝ = x✝¹ • x✝² • x✝

Tactic:
by apply DFunLike.ext; simp [smul_comm]

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

Goal state before:
pp: 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
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
by simp [hik]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
⊢ ∃ x, orderOf x = p

Tactic:
have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
⊢ ∃ x, orderOf x = p
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i = j
⊢ j.cycleIcc i = 1

Tactic:
rw [hij, ← cycleIcc_eq]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
intro g k c

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
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' : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ : ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update m i (c • x)) = c • f (update m i x)
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) = c • f (update m i x)

Tactic:
by convert! h₂ m i c x

Goal state after:
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
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (v ∘ ⇑(Equiv.swap i j)) + f v = 0

Tactic:
by
  rw [Equiv.comp_swap_eq_update]
  convert! f.map_update_update v hij (v i + v j)
  simp [f.map_update_self _ hij, f.map_update_self _ hij.symm,
    Function.update_comm hij (v i + v j) (v _) v, Function.update_comm hij.symm (v i) (v i) v]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)

Tactic:
classical
  let O := Finset.univ.image F.obj
  let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
    Finset.univ.biUnion fun X : J => Finset.univ.biUnion fun Y : J =>
      Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp [O], by simp [O], F.map f⟩
  obtain ⟨Z, f, w⟩ := sup_exists O H
  refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
  intro j j' g
  dsimp
  simp only [Category.comp_id]
  apply w
  simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq,
    true_and, exists_and_left]
  exact ⟨j, rfl, j', g, by simp⟩

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
⊢ B * A = 1

Tactic:
replace h := congr(B * $(detp_smul_adjp hAB))

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 • adjp (-1) B + detp (-1) A • adjp 1 B)) = B * (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ B * A = 1
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 : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
x : M₁ (σ.symm (σ i))
⊢ (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (c • x)) =
    c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x)

Tactic:
simp only [Function.comp, piCongrLeft'_update, f.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
⊢ ∀ b ∈ preserving_snd, ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = b

pp: case refine_4
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,
    ∏ x, ↑↑(sign (a x ⋯)) * ∏ x_1, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign (prodCongrLeft fun k ↦ a k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ a k ⋯) i) i

Tactic:
· intro σ hσ
      rw [mem_preserving_snd] at hσ
      have hσ' x : (σ.symm x).snd = x.snd := by simpa [eq_comm] using hσ (σ.symm x)
      have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by
        intro k x
        ext
        · simp only
        · simp only [hσ]
      have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind
      refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
      · intro x
        simp [mk_apply_eq]
      · intro x
        simp [mk_inv_apply_eq]
      · apply Finset.mem_univ
      · ext ⟨k, x⟩
        · simp only [coe_fn_mk, prodCongrLeft_apply]
        · simp only [prodCongrLeft_apply, hσ]

Goal state after:
case refine_4
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,
    ∏ x, ↑↑(sign (a x ⋯)) * ∏ x_1, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign (prodCongrLeft fun k ↦ a k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ a k ⋯) i) i
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
f₁ : M₁ i →ₗ[R] M₁' i
⊢ ∀ (y : M₁ i →ₗ[R] M₁' i),
    compLinearMapₗ (update f i (f₁ + y)) = compLinearMapₗ (update f i f₁) + compLinearMapₗ (update f i y)

Tactic:
f₂

Goal state after:
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
f₁ f₂ : M₁ i →ₗ[R] M₁' i
⊢ compLinearMapₗ (update f i (f₁ + f₂)) = compLinearMapₗ (update f i f₁) + compLinearMapₗ (update f i f₂)