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

Goal state before:
pp: case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ castSucc 0 < i.succ

Tactic:
· rw [Fin.castSucc_zero]
      apply Fin.succ_pos

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

Goal state before:
pp: case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Tactic:
simpa using

Goal state after:
case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i < j
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Tactic:
simpa [Fin.le_iff_val_le_val] using hgt

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:
by
  induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]

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

Goal state before:
pp: case refine_3
ι : 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
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x (g y)
⊢ ¬(m.erase g').prod y = y

Tactic:
simpa using

Goal state after:
case refine_3
ι : 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
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x (g y)
⊢ ¬y = g' y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (i.cycleIcc j) k = k

Tactic:
simpa using

Goal state after:
case pos
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (((j - i).castLT ⋯).cycleRange.extendDomain (natAdd_castLEEmb ⋯).toEquivRange) k = k
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
simpa using

Goal state after:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ k = Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i)))
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
simpa using

Goal state after:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ k = Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i)))
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
n : ℕ
i j : Fin n
hij✝ : i ≤ j
hij : i < j
⊢ Perm.sign (j.cycleIcc i) = 1

Tactic:
simp [Fin.not_le.mpr hij]

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ (i.cycleIcc j).IsCycle

Tactic:
simpa using

Goal state after:
n : ℕ
i j : Fin n
hij : i < j
⊢ (((j - i).castLT ⋯).cycleRange.extendDomain (natAdd_castLEEmb ⋯).toEquivRange).IsCycle
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ (i.cycleIcc j).cycleType = {↑j - ↑i + 1}

Tactic:
simpa using

Goal state after:
n : ℕ
i j : Fin n
hij : i < j
⊢ ↑(j - i) = ↑j - ↑i
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
inst✝ : NeZero n
⊢ (j.cycleIcc i).cycleType = ∅

Tactic:
simpa using

Goal state after:
n : ℕ
i j : Fin n
hij : i ≤ j
inst✝ : NeZero n
⊢ j.cycleIcc i = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l ↔ p.IsCycle ∧ ∀ (a : α), ¬p a = a → p a = l.prod a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f.cycleFactorsFinset.noncommProd id ⋯ = g

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ g.cycleFactorsFinset.noncommProd (fun x ↦ x) ⋯ = g
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ σ.IsSwap
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : IsThreeCycle 1
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : IsThreeCycle 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : ⟨x₁, x₂⟩ ∈ D
⊢ x₂ < x₁

Tactic:
simpa using

Goal state after:
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : ⟨x₁, x₂⟩ ∈ D
⊢ x₂ < x₁
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ g a ∉ {g (g a)}

Tactic:
simpa using

Goal state after:
case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ ¬a = g a
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 (g a)
this : (g ^ 3) a = a
⊢ g a = a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = g (g a)
this : (g ^ 3) a = a
⊢ g a = a
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⁻¹) (f x) = f x

Tactic:
simpa using

Goal state after:
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
⊢ x = f x
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⁻¹) (f x) = f x

Tactic:
simpa using

Goal state after:
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
⊢ x = f x
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
M : Type u_2
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
N : Type u_3
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
P : Type u_4
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
M' : Type u_5
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
N' : Type u_6
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
S : Type u_10
inst✝² : Monoid S
inst✝¹ : DistribMulAction S N
inst✝ : SMulCommClass R S N
c : S
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (c • ↑f).toFun v = 0

Tactic:
by simp [f.map_eq_zero_of_eq v h hij]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
f : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (-↑f).toFun v = 0

Tactic:
by simp [f.map_eq_zero_of_eq v h hij]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_3
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type u_4
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type u_5
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
S : Type u_10
N₂ : Type u_11
inst✝¹ : AddCommMonoid N₂
inst✝ : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (g.compMultilinearMap ↑f).toFun v = 0

Tactic:
by simp [f.map_eq_zero_of_eq v h hij]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective ⇑f
g₁ g₂ : M [⋀^ι]→ₗ[R] N
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : ι → M
⊢ g₁ x = g₂ x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective ⇑f
g₁ g₂ : M [⋀^ι]→ₗ[R] N
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : ι → M
⊢ g₁ x = g₂ x
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_4
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type u_5
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
v : ι' → M
i j : ι'
hv : v i = v j
hij : i ≠ j
⊢ (v ∘ ⇑σ) (σ.symm i) = (v ∘ ⇑σ) (σ.symm j)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_4
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type u_5
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
v : ι' → M
i j : ι'
hv : v i = v j
hij : i ≠ j
⊢ v i = v j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
x y : M p
⊢ f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)

Tactic:
simpa using

Goal state after:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
x y : M p
⊢ f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
c : R
x : M p
⊢ f (p.insertNth (c • x) m) = c • f (p.insertNth x m)

Tactic:
simpa using

Goal state after:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
c : R
x : M p
⊢ f (p.insertNth (c • x) m) = c • f (p.insertNth x m)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ⇑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : (i : ι) → M₁' i
⊢ g₁ x = g₂ x

Tactic:
simpa using

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ⇑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : (i : ι) → M₁' i
⊢ g₁ x = g₂ x
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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp 1 A = b * detp 1 A + a * detp 1 A

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * detp (-1) A

Tactic:
· rw [add_comm]

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + 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
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * detp (-1) A

Tactic:
· rw [add_comm]

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
e₁ e₂ : m ≃ n
h : (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b
⊢ A.IsDetpBalanced a b

Tactic:
simpa using

Goal state after:
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b
⊢ A.IsDetpBalanced a b
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 : R
h : IsDetpBalanced 1 a b
⊢ a = b

Tactic:
simpa using

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
a b : R
h : IsDetpBalanced 1 a b
⊢ a = b
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 : Matrix n n R
p q : n
hpq : p ≠ q
hcol : A.col p = A.col q
s t : ℤˣ
⊢ detp s A = detp t A

Tactic:
simpa using

Goal state after:
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
hcol : A.col p = A.col q
s t : ℤˣ
⊢ detp s A = detp t A
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 : ℤˣ
A : Matrix n n R
p : n
hcol : A.col p = 0
⊢ detp s A = 0

Tactic:
simpa using

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
p : n
hcol : A.col p = 0
⊢ detp s A = 0
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₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m m' : (i : ι) → M₁ i
⊢ f (m + m') = ∑ s, f (s.piecewise m m')

Tactic:
simpa using

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₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m m' : (i : ι) → M₁ i
⊢ f (m + m') = ∑ s, f (s.piecewise m m')
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero

Tactic:
simp +instances

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

Goal state before:
pp: case a.one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one

Tactic:
simp +instances

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

Goal state before:
pp: case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (Prequotient.of j x).neg

Tactic:
simp +instances

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

Goal state before:
pp: case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s ((Prequotient.of j x).add (Prequotient.of j y))

Tactic:
simp +instances

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

Goal state before:
pp: case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s ((Prequotient.of j x).mul (Prequotient.of j y))

Tactic:
simp +instances

Goal state after: