mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

pp: case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅

Tactic:
· cases j <;> simp

Goal state after:
case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j' ↦ {Hom.init j'}) fun j_1 ↦
      if h : some j_1 = j then ⋯.mpr {Hom.id j} else ∅

pp: case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅

Tactic:
· cases j <;> simp

Goal state after:
case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_2
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
⊢ IsColimit c.toCocone

pp: case refine_3
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsLimit (c.whisker g).toCone

pp: case refine_4
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit (c.whisker g).toCocone

Tactic:
· let := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
    let := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
    exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this

Goal state after:
case refine_3
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsLimit (c.whisker g).toCone

case refine_4
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit (c.whisker g).toCocone
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ lift b.fst b.snd ≫ desc b.inl b.inr = 𝟙 b.pt

Tactic:
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (binaryBiconeOfIsSplitMonoOfCokernel i).fst ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      (binaryBiconeOfIsSplitMonoOfCokernel i).snd ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inr =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt

Tactic:
simp only [binaryBiconeOfIsSplitMonoOfCokernel_fst,
        binaryBiconeOfIsSplitMonoOfCokernel_inr,
        binaryBiconeOfIsSplitMonoOfCokernel_snd,
        splitEpiOfIdempotentOfIsColimitCofork_section_]
      dsimp only [binaryBiconeOfIsSplitMonoOfCokernel_pt]
      rw [isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]
      simp only [binaryBiconeOfIsSplitMonoOfCokernel_inl, Cofork.IsColimit.π_desc,
        cokernelCoforkOfCofork_π, Cofork.π_ofπ, add_sub_cancel]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j)

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, true_and]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range (n + 1))) =
    [![n]]

Tactic:
List.range_succ,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range n ++ [n])) =
    [![n]]
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s →
    ∃ a_2 b, a_2 + b = n ∧ ∃ g, f = g.update a a_2 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

Tactic:
rintro ⟨rfl, hsupp⟩

Goal state after:
case mp
ι : 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
⊢ ∃ a_1 b, a_1 + b = f a + ∑ x ∈ s, f x ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
    Set.mem_range_self _

Goal state after:
n : ℕ
c : Composition n
j : Fin n
this : (c.embedding (c.index j)) (c.invEmbedding j) ∈ Set.range ⇑(c.embedding (c.index j))
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin c₁.length
i₂ : Fin c₂.length
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
by
  cases hn
  rw [← Composition.ext_iff] at hc
  cases hc
  congr
  rwa [Fin.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ g x ∈ c.support ↔ x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not, ← mul_apply]
  rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.blocks.length ≤ c.length

Tactic:
simp [blocks]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ l.formPerm.support = l.toFinset

Tactic:
by
  rw [← Finset.coe_inj]
  convert! support_formPerm_of_nodup' _ h h'
  simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : (x :: y :: l).formPerm = (x' :: y' :: l').formPerm
⊢ x :: y :: l ~r x' :: y' :: l'

Tactic:
rw [Equiv.Perm.ext_iff] at h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ x :: y :: l ~r x' :: y' :: l'
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ ↑(finPairsLT n)
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩ ∈ ↑(finPairsLT n)
h : f.signBijAux ⟨a₁, a₂⟩ = f.signBijAux ⟨b₁, b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
dsimp [signBijAux] at h

Goal state after:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ ↑(finPairsLT n)
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩ ∈ ↑(finPairsLT n)
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
ha₂ : ⟨a₁, 1⟩ ∉ {⟨1, 0⟩}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 1 then -1 else 1) = 1

pp: case inr.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
· rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]

Goal state after:
case inr.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

pp: case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
· exact ⟨0, hfxb⟩

Goal state after:
case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support ↔ ¬orderOf f ∣ n

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support ↔ ¬f ^ n = 1
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

Tactic:
pow_apply_eq_self_of_apply_eq_self hz,

Goal state after:
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
⊢ z = 1 z
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ d ≠ 0

Tactic:
by simpa using hi.ne_zero

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 2 ≤ #(f.cycleOf x).support ↔ f x ≠ x

Tactic:
refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : 2 ≤ #(f.cycleOf x).support
⊢ f x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ sign f = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Tactic:
rw [sign_of_cycleType']
  induction f.cycleType using Multiset.induction_on with
  | empty => rfl
  | cons a s ihs =>
    rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

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

Goal state before:
pp: case pos.succ
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩

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

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

Tactic:
apply hσ.isConj hτ

Goal state after:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ #σ.support = #τ.support
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (m + 2)).IsCycle

Tactic:
exact isCycle_finRotate

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

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

Tactic:
rw [(List.perm_cons_erase cl).pairwise_iff symm] at hld

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

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

Tactic:
· exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
obtain ⟨b, hb1, hb2⟩ := Finset.exists_mem_ne (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
        ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a

Goal state after:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
b : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ b, σ b = b ∧ b ≠ a
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
⊢ Perm.sign (i.cycleIcc j) = (-1) ^ (↑j - ↑i)

Tactic:
by
  simp [hij, sub_val_of_le hij]

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

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h✝¹ : x = j
h✝ : x = k
⊢ ↑i = ↑i

pp: case neg
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h✝¹ : x = j
h✝ : ¬x = k
⊢ ↑i = ↑(x + 1)

pp: case pos
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h✝¹ : ¬x = j
h✝ : x = k
⊢ ↑(x + 1) = ↑i

pp: case neg
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h✝¹ : ¬x = j
h✝ : ¬x = k
⊢ ↑(x + 1) = ↑(x + 1)

Tactic:
repeat lia

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

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

Tactic:
intro g

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k c g : Perm α
⊢ ∀ {k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
apply g.cycleFactorsFinset_mem_commute hc hc'; exact hcc'

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)) z +
      Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]
      exact Quot.sound (Relation.right_distrib _ _ _)

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)
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
⊢ ∑ j ∈ ofSign t, (∏ k, A k (σ k)) * ∏ k, B k (j k) = ∑ x ∈ ofSign (t * s), (∏ x, A x (σ x)) * ∏ x_1, B (σ x_1) (x x_1)

Tactic:
hf hσ,

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)
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
⊢ ∑ j ∈ ofSign t, (∏ k, A k (σ k)) * ∏ k, B k (j k) =
    ∑ x ∈ Finset.map (mulRightEmbedding σ) (ofSign t), (∏ k, A k (σ k)) * ∏ x_1, B (σ x_1) (x x_1)
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]
      exact Quot.sound (Relation.right_distrib _ _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j

Tactic:
push Not at H

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ∃ a₁ a₂, p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

Tactic:
have h₂ := c.ι.naturality ⟨WalkingParallelPairHom.right⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
h₂ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.right } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.right }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case neg
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
hi'i : ¬i' = i
⊢ c i' = 0

Tactic:
· exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c z) = f z
⊢ f x = f y

Tactic:
rw [← this x, h, ← this y]

Goal state after:
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₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (f.linearDeriv x) y = ∑ i, f (update x i (y i))

Tactic:
unfold linearDeriv

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₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (∑ i, f.toLinearMap x i ∘ₗ LinearMap.proj i) y = ∑ i, f (update x i (y i))