mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
hab : q < b
⊢ q.insertNth x f q < q.insertNth x f b

Tactic:
cases b using succAboveCases q

Goal state after:
case refine_4.x.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
hab : q < q
⊢ q.insertNth x f q < q.insertNth x f q

case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q < q.succAbove j✝
⊢ q.insertNth x f q < q.insertNth x f (q.succAbove j✝)
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
j✝ : Fin n
hab : q.succAbove j✝ < b
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f b

Tactic:
cases b using succAboveCases q

Goal state after:
case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q.succAbove j✝ < q
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f q

case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case elim0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i, i.elim0 = n

Tactic:
cases n

Goal state after:
case elim0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 0 ↔ ∑ i, i.elim0 = 0

case elim0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i, i.elim0 = n✝ + 1
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case zero
n : ℕ
⊢ (antidiagonalTuple 0 n).Nodup

Tactic:
cases n

Goal state after:
case zero.zero
⊢ (antidiagonalTuple 0 0).Nodup

case zero.succ
n✝ : ℕ
⊢ (antidiagonalTuple 0 (n✝ + 1)).Nodup
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_2
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
x : ι
hx : x ∈ s
⊢ (Finsupp.erase a f) x = f x

Tactic:
Finsupp.erase_ne (ne_of_mem_of_not_mem hx h)

Goal state after:
case mp.refine_2
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
x : ι
hx : x ∈ s
⊢ f x = f x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ a + ((↑p).parts.erase a).sum = n

Tactic:
simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2)

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

Goal state before:
pp: case refine_2
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ ((↑p).parts.erase a).sum = n - a

Tactic:
have hs : a + (p.1.parts.erase a).sum = n := by
        simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2)

Goal state after:
case refine_2
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
hs : a + ((↑p).parts.erase a).sum = n
⊢ ((↑p).parts.erase a).sum = n - a
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
⊢ f x = g x

Tactic:
replace hf := mt (hf.2 ·) h
            replace hg := mt (hg.2 ·) h
            rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ n) (f x) = x

Tactic:
hfx,

Goal state after:
α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ n) x = x
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).pt ≅
    (F.mapCone c).pt

Tactic:
by dsimp; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅ (F.mapBinaryBicone b).toCone.pt

Tactic:
by dsimp; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).pt ≅
    (F.mapCocone c).pt

Tactic:
by dsimp; rfl

Goal state after:
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
  simp only [mem_support, ne_eq, Finset.mem_map, Function.Embedding.coe_subtype, Subtype.exists,
    exists_and_right, exists_eq_right, not_iff_comm, not_exists, not_not]
  by_cases hx : p x
  · simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]
  · simp only [forall_prop_of_false hx, ofSubtype_apply_of_not_mem u hx]

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

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

Tactic:
by_cases hfa : f a = a

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

case neg
α : 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)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
rw [hn] at hk

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : (hd :: tl).formPerm hd = hd
⊢ (hd :: tl).formPerm = 1

Tactic:
simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h

Goal state after:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : tl = []
⊢ (hd :: tl).formPerm = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
⊢ f.IsCycle → (g * f * g⁻¹).IsCycle

Tactic:
rintro ⟨x, hx, h⟩
  refine ⟨g x, by simp [coe_mul, hx], fun y hy => ?_⟩
  simpa using (h <| eq_inv_iff_eq.not.2 hy).conj (g := g)

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x

Tactic:
rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi

Goal state after:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : x = y
⊢ f x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle

Tactic:
cases n

Goal state after:
case ofNat
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.ofNat a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a✝).support
⊢ f.IsCycle

case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ (f.cycleOf x ^ (n + 1)) x = (f ^ (n + 1)) x

Tactic:
rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]

Goal state after:
case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ (τ * 1 * τ⁻¹).cycleType = cycleType 1

Tactic:
| base_one =>

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).sum = #(support 1)

Tactic:
| base_one =>

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sign 1 = (Multiset.map (fun n ↦ -(-1) ^ n) (cycleType 1)).prod

Tactic:
| base_one =>

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).lcm = orderOf 1

Tactic:
| base_one =>

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

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = ↑((decomposeFin.symm (1, finRotate n)) i)

Tactic:
cases n

Goal state after:
case zero
i : Fin (Nat.succ 0)
⊢ ↑((finRotate (Nat.succ 0)) i) = ↑((decomposeFin.symm (1, finRotate 0)) i)

case succ
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) i) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
| base_one =>

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

Goal state before:
pp: case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2)) ((finRotate (n + 2) ^ x) 0)) = ↑⟨x + 1, hx⟩

Tactic:
coe_finRotate_of_ne_last,

Goal state after:
case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2) ^ x) 0) + 1 = ↑⟨x + 1, hx⟩

case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ (finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

Tactic:
cycleRange_of_le h

Goal state after:
case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(if i = j then 0 else i + 1) = if i = j then 0 else ↑i + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint.refine_1
α : 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
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
Finset.mem_def

Goal state after:
case induction_disjoint.refine_1
α : 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
⊢ σ' ∈ τ.cycleFactorsFinset.val
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
cases n

Goal state after:
case zero
i j : Fin 0
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
| base_one =>

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

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

Tactic:
by
  rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]

Goal state after:
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 α
⊢ Fintype.card α < 2 * orderOf σ

Tactic:
rw [← one_mul (Fintype.card α), ← h2, 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: case refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
hg' : g = 1
⊢ v = v₀

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, hg, hg', v.1.2]
    simp only [v₀, List.Vector.replicate]

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

Goal state before:
pp: case refine_3.inl
α : 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 : α
⊢ τ x = x ∨ (σ * f⁻¹) x = x

Tactic:
rcases hd.symm x with hx | hx

Goal state after:
case refine_3.inl.inl
α : 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
⊢ τ x = x ∨ (σ * f⁻¹) x = x

case refine_3.inl.inr
α : 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
⊢ τ x = x ∨ (σ * f⁻¹) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos.inr.inr
α : 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 (g a)) = (swap a (g a)) ((swap (g a) (g (g a))) (g (g a)))

Tactic:
· simp only [swap_apply_right]
      suffices (g ^ 3) a = a by simpa
      simp [← hg3.orderOf]

Goal state after:
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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : ∃ a, q a ≠ p a
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = 0

Tactic:
obtain ⟨i, hpqi⟩ := hpq

Goal state after:
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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = 0
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₂
g : M₂ →ₗ[R] M
⊢ compLinearMap 0 g = 0

Tactic:
ext
  simp only [compLinearMap_apply, zero_apply]

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ f (update v i (g j • v j)) = 0

Tactic:
rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]

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

Tactic:
simpa using detp_eq_of_row_eq_zero (A := Aᵀ) s hcol

Goal state after:
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:
by
      simp only [(· + ·), (· * ·), Add.add]
      exact Quot.sound (Relation.left_distrib _ _ _)

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:
by
      simp only [(· + ·), (· * ·), Add.add]
      exact Quot.sound (Relation.left_distrib _ _ _)

Goal state after: