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

Goal state before:
pp: α : Type u_1
f : Perm α
h : f.Disjoint f
⊢ f = 1

Tactic:
ext x

Goal state after:
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
⊢ f x = 1 x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1

Tactic:
by
  constructor
  · rintro rfl
    exact fun i => eq_of_mem_replicate
  · intro H
    ext1
    have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
    have : c.blocks.length = n := by
      conv_rhs => rw [← c.blocks_sum, A]
      simp
    rw [A, this, ones_blocks]

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
i_blocks : 1 < i
j : Fin c.length
hj : c.blocksFun j = i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i

Tactic:
← hj

Goal state after:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
j : Fin c.length
i_blocks : 1 < c.blocksFun j
hj : c.blocksFun j = i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
⊢ (ofSubtype u).support = map (Embedding.subtype p) u.support

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ x ∈ (ofSubtype u).support ↔ x ∈ map (Embedding.subtype p) u.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
⊢ f.extendSubtype * σ = τ * f.extendSubtype

Tactic:
ext x

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
⊢ (f.extendSubtype * σ) x = (τ * f.extendSubtype) x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks = c.blocks

Tactic:
have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
⊢ d.blocks = c.blocks
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].formPerm x ∈ []

Tactic:
simp at h

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ∈ []
hl : List.Pairwise Disjoint []
⊢ ∀ x ∈ f.support, f x = [].prod x

Tactic:
simp at h

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f

Tactic:
· rw [← mul_assoc, mul_def (Equiv.swap a (f a)) (Equiv.swap a (f a)), Equiv.swap_swap,
      ← Perm.one_def, one_mul]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb]

Goal state after:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
⊢ (l.rotate 1).formPerm = l.formPerm

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
⊢ (l.rotate 1).formPerm x = l.formPerm x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
h : x = y
f : Perm α
⊢ f.SameCycle x y

Tactic:
by rw [h]

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

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

Tactic:
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp

Goal state after:
case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : (swap 0 1) 0 = 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ ∃ i, (f ^ i) x = y

Tactic:
exact
      ⟨(n % orderOf f).toNat, by
        {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm ^ l.length = 1

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
⊢ (l.formPerm ^ l.length) x = 1 x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
⊢ s f = sign f

Tactic:
let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
    have hsl : ∀ a ∈ l.map s, a = (-1 : ℤˣ) := fun a ha =>
      let ⟨g, hg⟩ := List.mem_map.1 ha
      hg.2 ▸ this (hl₂ _ hg.1)
    rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]

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

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + -(↑y * ↑b) = ↑d

Tactic:
← sub_eq_add_neg,

Goal state after:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a - ↑y * ↑b = ↑d
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
by
  rw [SameCycle.cycleOf_apply]
  · rw [add_comm, zpow_add, zpow_one, mul_apply]
  · exact ⟨k, rfl⟩

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

Goal state before:
pp: case mpr
α : 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'
⊢ Commute g c

Tactic:
ext x

Goal state after:
case mpr
α : 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 : α
⊢ (g * c) x = (c * g) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
⊢ c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
ext x

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
⊢ (c ^ n) x = (ofSubtype (g.subtypePerm hg)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = c * (l.erase c).prod

Tactic:
← List.prod_cons,

Goal state after:
case mp.mk.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = (c :: l.erase c).prod
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
mul_lt_mul_iff_left₀ (orderOf_pos σ)

Goal state after:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 < 2
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ (↑v).head * (↑v).tail.toList.prod = 1

Tactic:
← List.prod_cons,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ ((↑v).head :: (↑v).tail.toList).prod = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
⊢ cycleIcc 0 i = i.cycleRange

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
inst✝ : NeZero n
x : Fin n
⊢ ↑((cycleIcc 0 i) x) = ↑(i.cycleRange x)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
⊢ ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)

Tactic:
ext x

Goal state after:
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr.inr
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)

Tactic:
rcases lt_or_ge x j with ch2 | ch2

Goal state after:
case inr.inr.inl
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)

case inr.inr.inr
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset

Tactic:
· rintro ⟨hc, hd, hp⟩
    refine List.toFinset_eq_of_perm _ _ ?_
    refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
    rw [hp, hp']

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
s : Finset (Perm α)
⊢ σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hl : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔
    (∀ f ∈ l.toFinset, f.IsCycle) ∧ ∃ (h : (↑l.toFinset).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : (↑σ).IsCycle
hσ3 : (↑σ).support = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ ↑σ ∈ ↑H ∧ τ ∈ ↑H

Tactic:
exact ⟨Subtype.mem σ, h2⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsSwap → σ.cycleType = {2}

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = {2} → σ.IsSwap

Tactic:
· intro h
    simpa [h.isCycle.cycleType, card_support_eq_two] using h

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = {2} → σ.IsSwap
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
⊢ Commute c c'

Tactic:
by_cases hcc' : c = c'

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
⊢ f = g

Tactic:
ext x

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ f x = g x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
⊢ g = swap a (g a) * swap (g a) (g (g a))

Tactic:
ext x

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
⊢ g x = (swap a (g a) * swap (g a) (g (g a))) x
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case inr
ι : 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)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ ((dfinsuppFamily (Pi.single p f)) x) p' = (DFinsupp.single p (f fun i ↦ (x i) (p i))) p'

Tactic:
simp [hp]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommSemiring R
M : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
b' : Basis ι' R N
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), Finite (κ i)
i : ((i : ι) → κ i) × ι'
⊢ (multilinearMap b b') i =
    (LinearMap.id.smulRight (b' i.2)).compMultilinearMap
      ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun i' ↦ (b i').coord (i.1 i'))

Tactic:
ext x

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommSemiring R
M : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
b' : Basis ι' R N
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), Finite (κ i)
i : ((i : ι) → κ i) × ι'
x : (i : ι) → M i
⊢ ((multilinearMap b b') i) x =
    ((LinearMap.id.smulRight (b' i.2)).compMultilinearMap
        ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun i' ↦ (b i').coord (i.1 i')))
      x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ ↑((g.subtypePerm ⋯) ⟨x, hx⟩) = ↑(c.subtypePermOfSupport ⟨x, hx⟩)

Tactic:
simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g x = c x
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✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
⊢ (fun f ↦ { toFun := fun x ↦ f (x i), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((fun f ↦ { toFun := fun x ↦ f fun x_1 ↦ x, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f

Tactic:
ext x

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✝¹¹ : 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✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
x : ι → M₂
⊢ ((fun f ↦ { toFun := fun x ↦ f (x i), map_update_add' := ⋯, map_update_smul' := ⋯ })
        ((fun f ↦ { toFun := fun x ↦ f fun x_1 ↦ x, map_add' := ⋯, map_smul' := ⋯ }) f))
      x =
    f x
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
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A (some i) none = detp (-s) (A.submatrix some (Function.update some i none))

Tactic:
by
  rw [adjp_none_right]; congr
  · simp
  · ext1; aesop

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ ⇑(ConcreteCategory.hom (c.ι.app j'✝)) ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (c.ι.app j✝))

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (fun X ↦ X) (F.obj j✝)
⊢ (⇑(ConcreteCategory.hom (c.ι.app j'✝)) ∘ ⇑(ConcreteCategory.hom (F.map f))) x = (ConcreteCategory.hom (c.ι.app j✝)) x
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
j : J
⊢ ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x) = s.ι.app j

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
j : J
x : F.obj j
⊢ (ConcreteCategory.hom ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x)).toFun x =
    (ConcreteCategory.hom (s.ι.app j)).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
m : (F.coconeTypesEquiv c).pt ⟶ s.pt
hm : ∀ (j : J), (F.coconeTypesEquiv c).ι.app j ≫ m = s.ι.app j
⊢ m = ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
m : (F.coconeTypesEquiv c).pt ⟶ s.pt
hm : ∀ (j : J), (F.coconeTypesEquiv c).ι.app j ≫ m = s.ι.app j
x : (F.coconeTypesEquiv c).pt
⊢ (ConcreteCategory.hom m).toFun x = (ConcreteCategory.hom (↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x)).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ f ∘ F.descColimitType c = F.descColimitType c'

Tactic:
ext x

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
x : F.ColimitType
⊢ (f ∘ F.descColimitType c) x = F.descColimitType c' x