mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
⊢ Function.LeftInverse (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩

Tactic:
by intro x; simp

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

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
⊢ Function.RightInverse (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩

Tactic:
by intro x; simp

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

Goal state before:
pp: β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), σ ↑a = ↑((Finset.equivOfCardEq h) a)
⊢ ∃ σ, Finset.map (Equiv.toEmbedding σ) s = t

Tactic:
refine ⟨σ, Finset.eq_of_subset_of_card_le (fun b hb => ?_) (by simp [h])⟩

Goal state after:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), σ ↑a = ↑((Finset.equivOfCardEq h) a)
b : β
hb : b ∈ Finset.map (Equiv.toEmbedding σ) s
⊢ b ∈ t
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support

Tactic:
by
  refine le_antisymm (support_mul_le _ _) fun a => ?_
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  exact
    (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
      ⟨(congr_arg f hg).symm.trans h, hg⟩

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

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ (take (↑i) c.blocks).sum = ↑j

Tactic:
← hi,

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ (take (↑i) c.blocks).sum = ↑((c.boundaries.orderEmbOfFin ⋯) i)
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case pos
α : 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
⊢ f ∈ permsOfList (a :: l)

Tactic:
refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))
    rintro rfl
    exact hx hfa

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ (x :: y :: tl).formPerm (x :: y :: tl)[0] = (x :: y :: tl)[1]

Tactic:
rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ f y = y

Tactic:
← hi,

Goal state after:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ f ((f ^ i) x) = (f ^ i) x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l
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
  by_cases hx : x ∈ l
  · obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]
  · have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
    simpa using this

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:
by
  ext x
  by_cases hx : x ∈ l
  · obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]
  · have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
    simpa using this

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans 1).trans e) = signAux2 [] 1

Tactic:
one_def,

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : f z = z
⊢ (f ^ n) z = 1 z

pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬f z = z
⊢ (f ^ n) z = 1 z

Tactic:
· rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬f z = z
⊢ (f ^ n) z = 1 z
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
a : α
ha : f a ≠ a ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle a y
⊢ {x | f x ≠ x}.Nontrivial

Tactic:
exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn {a}
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

Tactic:
isCycleOn_singleton

Goal state after:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f a = a
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n
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
⊢ (ϕ i) y * ?m ^ (Finset.univ.erase i).card = (ϕ i) y

Tactic:
rw [one_pow]
    exact mul_one _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType

Tactic:
hc.cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ {#σ.support} = σ'.cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ'.Disjoint (τ * σ'⁻¹)

Tactic:
· exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm

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

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

Tactic:
obtain ⟨π, rfl⟩ := isConj_iff.1 h
    rw [cycleType_conj]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ (g.extendDomain f).cycleType = g.cycleType

Tactic:
induction g using cycle_induction_on with

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.IsCycle

Tactic:
cases i

Goal state after:
case zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.IsCycle

case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.IsCycle
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.cycleType = {↑⟨i, hi⟩ + 1}

Tactic:
cases i

Goal state after:
case zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.cycleType = {↑⟨0, hi⟩ + 1}

case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
⊢ c.cycleType + g'.cycleType = {#c.support}

Tactic:
hc.cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
⊢ {#c.support} + g'.cycleType = {#c.support}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
· rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: 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)

Tactic:
rcases lt_or_ge x i with ch | ch

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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ ≠ 1

Tactic:
by
  rintro rfl
  simpa using h.cycleType

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

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

Tactic:
simp only [mem_cycleFactorsFinset_iff]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (c.IsCycle ∧ ∀ a ∈ c.support, c a = g a) →
    (k * c * k⁻¹).IsCycle ∧ ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ {f : Perm α}, f ∈ cycleFactorsFinset 1 → (1 * f⁻¹).cycleFactorsFinset = cycleFactorsFinset 1 \ {f}

case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    σ.IsCycle → ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}

case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}
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 : a ∈ g.support
⊢ #g.support ≤ #{a, g a, g (g a)}

Tactic:
· rw [hg3.card_support]
      simp only [mem_support, ne_eq] at ha
      rw [Finset.card_insert_eq_ite, if_neg]
      · rw [Finset.card_insert_eq_ite, if_neg]
        · simp
        · simpa using Ne.symm ha
      · simp only [Finset.mem_insert, Finset.mem_singleton]
        contrapose ha
        rcases ha with ha | ha
        · exact ha.symm
        · suffices (g ^ 3) a = a by simpa [pow_succ, ← ha] using this
          simp [← hg3.orderOf]

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

Goal state before:
pp: case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)

Tactic:
have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp

Goal state after:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i ↦ e (v i)
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y + Quot.mk (⇑(colimitSetoid F)) z) =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y +
      Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x)
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F)) y) (Quot.mk (⇑(colimitSetoid F)) z)) =
    Quotient.map₂ add ⋯ (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) y))
      (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) z))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ (Quot.mk (⇑(colimitSetoid F)) x + Quot.mk (⇑(colimitSetoid F)) y) * Quot.mk (⇑(colimitSetoid F)) z =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z +
      Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul ⋯ ⋯ (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) y))
      (Quot.mk (⇑(colimitSetoid F)) z) =
    Quotient.map₂ add ⋯ (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) z))
      (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) y) (Quot.mk (⇑(colimitSetoid F)) z))
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 : ι) → 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
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
Ai_card : ∀ (i : ι), #(A i) = 1
⊢ ∀ r ∈ piFinset A, (f fun i ↦ g i (r i)) = f fun i ↦ ∑ j ∈ A i, g i j

Tactic:
intro r hr

Goal state after:
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
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
Ai_card : ∀ (i : ι), #(A i) = 1
r : (i : ι) → α i
hr : r ∈ piFinset A
⊢ (f fun i ↦ g i (r i)) = f fun i ↦ ∑ j ∈ A i, g i j
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e_A.e_c
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
⊢ ⇑(swap none (some i)) ∘ some = Function.update some i none

Tactic:
· ext1; aesop

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y + Quot.mk (⇑(colimitSetoid F)) z) =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y +
      Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x)
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F)) y) (Quot.mk (⇑(colimitSetoid F)) z)) =
    Quotient.map₂ add ⋯ (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) y))
      (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) z))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ (Quot.mk (⇑(colimitSetoid F)) x + Quot.mk (⇑(colimitSetoid F)) y) * Quot.mk (⇑(colimitSetoid F)) z =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z +
      Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul ⋯ ⋯ (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) y))
      (Quot.mk (⇑(colimitSetoid F)) z) =
    Quotient.map₂ add ⋯ (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) x) (Quot.mk (⇑(colimitSetoid F)) z))
      (Quot.map₂ mul ⋯ ⋯ (Quot.mk (⇑(colimitSetoid F)) y) (Quot.mk (⇑(colimitSetoid F)) z))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ (M.submatrix ⇑(e.trans e'.symm).symm ⇑(Equiv.refl m)).det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
Equiv.coe_refl,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ (M.submatrix (⇑(e.trans e'.symm).symm) id).det = ↑↑(sign (e'.trans e.symm)) * M.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝³ : DecidableEq m
inst✝² : Fintype m
R : Type v
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ det A.col ≠ 0

Tactic:
simpa [Matrix.col]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h0 :
  detp 1 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) 1 + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

Tactic:
detp_one_one,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h0 :
  1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) 1 + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B