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

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle

Tactic:
exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ (List.map (⇑sign ∘ fun a ↦ prodExtendRight a (σ a)) l).prod =
    (List.map (fun k ↦ sign (prodExtendRight k (σ k))) l).prod

Tactic:
Function.comp_def

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

Goal state before:
pp: α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ (prodComm β α✝) ((prodCongrLeft σ) (b, α)) = (prodCongrRight σ) ((prodComm β α✝) (b, α))

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ (noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range

Tactic:
let := Classical.decEq ι
  apply le_antisymm
  · rintro x ⟨f, rfl⟩
    refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_
    intro i _hi
    apply Subgroup.mem_sSup_of_mem
    · use i
    simp
  · refine iSup_le ?_
    rintro i x ⟨y, rfl⟩
    exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

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

Goal state before:
pp: case zero
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ (f.cycleOf x ^ 0) x = (f ^ 0) x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Tactic:
grind

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support

Tactic:
· exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
iff_true_left (fun b ↦ (ha b).elim),

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) 0).prod = (-1) ^ (Multiset.sum 0 + card 0)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ orderOf σ

Tactic:
by
  rw [← lcm_cycleType]
  exact dvd_lcm h

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))
⊢ iSupIndep H

Tactic:
by
  simpa using
    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
      (commute_subtype_of_commute hcomm) hcoprime

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝
l : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, g x ≠ x → x ∈ []
⊢ [].prod = g ∧ (∀ g' ∈ [], g'.IsCycle) ∧ List.Pairwise Disjoint []

Tactic:
{ simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}

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

Goal state before:
pp: case zero
n : ℕ
hx : 0 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨0, hx⟩) 0) = ↑⟨0, hx⟩

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
⊢ (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩

Tactic:
rfl

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 (σ' * τ * σ'⁻¹) τ
⊢ {(Finset.card ∘ support) σ'} = {#σ'.support}

Tactic:
rfl

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) 0, ⋯⟩ = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
h' : i = j
⊢ ↑0 = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : j = i
⊢ i.cycleRange j = 0

pp: case neg
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ i.cycleRange j = j

Tactic:
· exact cycleRange_of_eq h₂

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
i j : Fin n
h₁ : ¬j < i
h₂ : ¬j = i
⊢ i.cycleRange j = j
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:
by
          rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]
          exact v.2

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : f.SameCycle x y
⊢ f y = f y

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ (-1) ^ ({3}.sum + {3}.card) = 1

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x ∈ {a, b, c}
⊢ (⇑(swap a b) ∘ ⇑(swap a c)) x ≠ x

Tactic:
grind

Goal state after:
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
⊢ a ∈ g.support → g.support = {a, g a, g (g a)}

Tactic:
intro ha
    symm
    apply Finset.eq_of_subset_of_card_le
    · apply Finset.insert_subset ha
      apply Finset.insert_subset
      · rwa [Perm.apply_mem_support]
      simpa only [Finset.singleton_subset_iff, Perm.apply_mem_support]
    · 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.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : [a, g a, g (g a)].Nodup
⊢ g a ≠ a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
this : #g.support = 3
⊢ [a, g a, g (g a)].Nodup

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : 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 (g a) ≠ a

Tactic:
grind

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

Goal state before:
pp: α : 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 (g a) ≠ g a

Tactic:
grind

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

Goal state before:
pp: α : 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 : α
h : x ∉ g.support
⊢ x ≠ g a

Tactic:
grind

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

Goal state before:
pp: α : 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 : α
h : x ∉ g.support
⊢ x ≠ g (g a)

Tactic:
grind

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

Goal state before:
pp: α : 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 : α
h : x ∉ g.support
⊢ x ≠ a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ z ≠ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ x ≠ y

Tactic:
grind

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

Goal state before:
pp: case mk.mk.refl
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₂
toFun✝ : ((i : ι) → M₁ i) → M₂
map_update_add'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
⊢ { toFun := toFun✝, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ } =
    { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }

Tactic:
rfl

Goal state after:
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✝² : DistribSMul S M₂
inst✝¹ : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ c • f (update m i (x + y)) = c • f (update m i x) + c • f (update m i y)

Tactic:
by simp [smul_add]

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
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k, diagonal d k (σ k) = 0

Tactic:
exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

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
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k, diagonal d k (σ k) = 0

Tactic:
exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

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

Goal state before:
pp: case inl.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp 1 A

Tactic:
rfl

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

Goal state before:
pp: case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp (-1) A

Tactic:
rfl

Goal state after:
case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp (-1) A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp 1 A

Tactic:
rfl

Goal state after:
case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp 1 A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp (-1) A

Tactic:
rfl

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

Goal state before:
pp: case pos
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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
let g' := Equiv.ofBijective g <| (Fintype.bijective_iff_injective_and_card _).mpr
    ⟨hg, (Fintype.card_le_of_injective g hg).antisymm le⟩

Goal state after:
case pos
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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
g' : m ≃ n := ofBijective g ⋯
⊢ (A.submatrix f g).IsDetpBalanced a b
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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
g' : m ≃ n := ofBijective g ⋯
⊢ f = ⇑f'

Tactic:
rfl

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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
g' : m ≃ n := ofBijective g ⋯
⊢ g = ⇑g'

Tactic:
rfl

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 = ∅
i : ι
hi : ∑ j ∈ A i, g i j = 0
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
have hpi : piFinset A = ∅ := by simpa

Goal state after:
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 = ∅
i : ι
hi : ∑ j ∈ A i, g i j = 0
hpi : piFinset A = ∅
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝

Tactic:
rfl

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

Goal state before:
pp: case e'_2.a
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
x✝¹ : Perm n
a✝¹ : x✝¹ ∈ ofSign (sign (swap none i) * s)
x✝ : n
a✝ : x✝ ∈ univ
⊢ A.submatrix some (⇑(swap none i) ∘ some) x✝ (x✝¹ x✝) = A (some x✝) ((decomposeOption.symm (i, x✝¹)) (some x✝))

Tactic:
rfl

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) ⋯ (Quot.mk (⇑(colimitSetoid F)) (a.add b)) = descFunLift F s a + descFunLift F s b

Tactic:
rfl

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

Goal state before:
pp: case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝

Tactic:
rfl

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1, A i_1 (i i_1) * B (i i_1) (x i_1) +
      ∑ x ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯, ∑ x_1 ∈ ofSign s, ∏ i, A i (ι x i) * B (ι x i) (x_1 i) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))

Tactic:
sum_disjUnion

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1, A i_1 (i i_1) * B (i i_1) (x i_1) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ i, A i (ι x i) * B (ι x i) (x_1 i) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ i, A i (ι x i) * B (ι x i) (x_1 i)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) ⋯ (Quot.mk (⇑(colimitSetoid F)) (a.add b)) = descFunLift F s a + descFunLift F s b

Tactic:
rfl

Goal state after: