mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ b.fst ≫ q = 0

Tactic:
← Category.id_comp q,

Goal state after:
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)
⊢ b.fst ≫ 𝟙 X ≫ q = 0
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨
      ∃ i,
        ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)

Tactic:
simp [and_assoc, exists_and_left]

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.inlCokernelCofork
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 : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.snd ≫ q = 0

Tactic:
← Category.id_comp q,

Goal state after:
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.inlCokernelCofork
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 : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.snd ≫ 𝟙 Y ≫ q = 0
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
g : Fin (n + 1) → Fin (n + 1)
hg : StrictMono g
⊢ g = id

Tactic:
refine funext fun x ↦ le_antisymm ?_ (hg.id_le x)

Goal state after:
n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
g : Fin (n + 1) → Fin (n + 1)
hg : StrictMono g
x : Fin (n + 1)
⊢ g x ≤ id x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl

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

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo (i + 1)

Tactic:
by
  rw [c.sizeUpTo_succ h]
  simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
⊢ Function.Injective toFinsuppAntidiag

Tactic:
by
  unfold toFinsuppAntidiag
  intro p q h
  rw [Finsupp.mk.injEq] at h
  obtain ⟨hfinset, hcount⟩ := h
  rw [Nat.Partition.ext_iff, Multiset.ext]
  intro m
  obtain rfl | h0 := Nat.eq_zero_or_pos m
  · grind [Multiset.count_eq_zero]
  · exact Nat.eq_of_mul_eq_mul_right h0 <| funext_iff.mp hcount m

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

Goal state before:
pp: α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
⊢ (f * g) x = x ∨ h x = x

Tactic:
cases H1 x <;> cases H2 x

Goal state after:
case inl.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

case inl.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

case inr.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : h x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

case inr.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
⊢ False

Tactic:
have A : (i₁ : ℕ).succ ≤ i₂ := Nat.succ_le_of_lt h'

Goal state after:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ False
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ (∀ (x : α), (σ * τ) x = x) ↔ (∀ (x : α), σ x = x) ∧ ∀ (x : α), τ x = x

Tactic:
hστ.mul_apply_eq_iff,

Goal state after:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ (∀ (x : α), σ x = x ∧ τ x = x) ↔ (∀ (x : α), σ x = x) ∧ ∀ (x : α), τ x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ support 1 = ∅

Tactic:
support_eq_empty_iff

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 1 = 1
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
this✝¹ : IsIso (F.biprodComparison X Y)
this✝ : IsIso (prodComparison F X Y)
this : PreservesLimit (pair X Y) F
⊢ PreservesBinaryBiproduct X Y F

Tactic:
apply preservesBinaryBiproduct_of_preservesBinaryProduct

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support

Tactic:
by
  simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
⊢ spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
ext; simp; tauto

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
⊢ sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
ext; simp; tauto

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

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []

Tactic:
simp only [not_mem_nil] at h
    exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
⊢ (swap x (f x) * f).support = f.support \ {x}

Tactic:
by_cases hx : f x = x
  · simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem, pull_end]
  ext z
  by_cases hzx : z = x
  · simp [hzx]
  by_cases hzf : z = f x
  · simp [hzf, hx, h, swap_apply_of_ne_of_ne]
  by_cases hzfx : f z = x
  · simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
  · simp [hzx, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.support = ∅ ↔ f = 1

Tactic:
support_eq_empty_iff

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f = 1 ↔ f = 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ¬(f * σ * f⁻¹) (f x) = f x

Tactic:
· rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l' = [] ∨ l'.length ≤ 1 → l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x] ~r l' ∨ l'.length ≤ 1 → l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ¬(g * τ * g⁻¹) (g (τ x)) = g (τ x)

Tactic:
· rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
⊢ closure {σ, swap x (σ x)} = ⊤

Tactic:
have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
⊢ closure {σ, swap x (σ x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : x.support = ∅
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥

Tactic:
support_eq_empty_iff

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : x = 1
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Tactic:
by
  induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

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
⊢ #τ.support = orderOf τ

Tactic:
hτ.orderOf

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ #τ.support = #τ.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty
  exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g.support = ∅

Tactic:
support_eq_empty_iff

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f.cycleOf x ^ i) x = y

Tactic:
by rw [cycleOf_zpow_apply_self, hi]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ g (c x) = c (g x)

Tactic:
hi' x hx,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ g (c x) = c ((c ^ i) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
a✝ : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType

Tactic:
| induction_disjoint σ π hd _ hσ hπ =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val ≤
    Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
hf'.left.cycleFactorsFinset_eq_singleton

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ Multiset.map (Finset.card ∘ support) {f}.val ≤ Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
α : Type u_1
a : α
x : Fin n → α
p j : Fin (n + 1)
⊢ cons a x (p.cycleRange j) = p.insertNth a x j

Tactic:
rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x ∈ f.cycleFactorsFinset
hy : x ∈ g.cycleFactorsFinset
⊢ False

Tactic:
simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = f a
hy : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = g a
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g * g).IsThreeCycle

Tactic:
← pow_two,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g ^ 2).IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : 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.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
hfx : f x = x
⊢ (σ * f⁻¹) x = x

Tactic:
rw [← hfx]
            simpa [hx] using hfx.symm

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

Goal state before:
pp: case pos
α : 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.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : f x = x
⊢ (τ * f⁻¹) x = x

Tactic:
rw [← hfx]
            simpa [hx] using hfx.symm

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) = DFinsupp.single p ((f p) m)

Tactic:
ext q
  obtain rfl | hpq := eq_or_ne q p
  · simp
  · rw [DFinsupp.single_eq_of_ne hpq]
    rw [Function.ne_iff] at hpq
    obtain ⟨i, hpqi⟩ := hpq
    apply (f q).map_coord_zero i
    simp_rw [DFinsupp.single_eq_of_ne hpqi]

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

Goal state before:
pp: case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ ∀ b ∈ ofSign 1, b ≠ 1 → ∏ k, diagonal d k (b k) = 0

Tactic:
rintro σ - hσ1

Goal state after:
case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
⊢ ∏ k, diagonal d k (σ k) = 0
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
⊢ ∏ k, diagonal d k (σ k) = 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Goal state after:
case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k, diagonal d k (σ k) = 0
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
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
⊢ ∏ k, diagonal d k (σ k) = 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k, diagonal d k (σ k) = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
by
  ext
  apply Quot.sound
  apply Relation.map

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
by
  ext
  apply Quot.sound
  apply Relation.map

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₂}
i : ι
hi : i = i₀
⊢ B i₀ ⊆ A i₀

Tactic:
simp only [B, Finset.sdiff_subset, update_self]

Goal state after: