mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : rightExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
by
    simp only [rightExactFunctor_iff] at h
    exact Functor.additive_of_preservesBinaryBiproducts F

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
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inr = BinaryFan.IsLimit.lift ht 0 (𝟙 Y)

Tactic:
by
  apply ht.uniq (BinaryFan.mk 0 (𝟙 Y)); rintro ⟨⟨⟩⟩ <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s

Tactic:
by
  simp [finsuppAntidiag, ← DFunLike.coe_fn_eq, subset_iff]

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

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
suffices m ∈ p.parts → m ≠ 0 by simpa

Goal state after:
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts → m ≠ 0
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

Goal state after:
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
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
hf : x ∉ f.support
⊢ f x = g x
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case inr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
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
hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x
x : ι
hx : x ≠ a
⊢ f x = g x

Tactic:
simpa only [coe_update, Function.update, dif_neg hx] using hfg x

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
rw [List.pairwise_cons] at h

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
⊢ (Equiv.symm f) y ∈ s

Tactic:
have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
    Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
      (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge

Goal state after:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x ↦ f i) x hx
⊢ (Equiv.symm f) y ∈ s
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ∈ l
⊢ x ∈ l

Tactic:
contrapose h
  rwa [formPerm_apply_of_notMem h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (swap x y).support = { val := x ::ₘ y ::ₘ 0, nodup := ⋯ }

Tactic:
simp [support_swap hxy, *, Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * Equiv.swap a b

Tactic:
by
    simpa [mul_assoc] using formPerm_append_pair (y::l) a b

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

Goal state before:
pp: case intro.refine_2.inl.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ↑⟨x, ⋯⟩ ∈ ↑σ.support

Tactic:
rwa [Subtype.coe_mk, mem_coe, mem_support]

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

Goal state before:
pp: case pos
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ ∈ finPairsLT n

pp: case neg
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : ¬f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩ ∈ finPairsLT n

Tactic:
· exact mem_finPairsLT.2 h

Goal state after:
case neg
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : ¬f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩ ∈ finPairsLT n
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
left; rw [ofSubtype_apply_of_not_mem u hx]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ n) ((Equiv.symm f) x) = (Equiv.symm f) b

Tactic:
rw [← mul_apply, ← pow_succ]

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ (n + 1)) x = (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹) (((swap x (f x) * f) ^ (-i)) (f x)) = (swap x (f⁻¹ x) * f⁻¹) b

Tactic:
convert! hi using 1

Goal state after:
case e'_2
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹) (((swap x (f x) * f) ^ (-i)) (f x)) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)

case e'_3
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹) b = (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)

Tactic:
refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
      rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case insert.inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
s : Finset ι
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1S : s.noncommProd f hcomm = 1
i : ι
hnotMem : i ∉ s
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
heq1 : f i * s.noncommProd f ⋯ = 1
hnotMem' : i ∉ ↑s
heq1i : f i = 1
⊢ f i = 1

Tactic:
exact heq1i

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x).SameCycle x y

pp: case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y

Tactic:
· exact ⟨1, by rw [zpow_one, swap_apply_right]⟩

Goal state after:
case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
this : sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb
⊢ sign (σa.sumCongr σb) = sign σa * sign σb

Tactic:
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.gcd y' = d
⊢ x.gcd y = d

Tactic:
by subst_vars; rw [Int.gcd_def]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

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

Tactic:
Int.cast_id

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ ∅.Countable

pp: case inr
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Tactic:
· exact Set.countable_empty

Goal state after:
case inr
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
x : α
hx : x ∈ s.toList.formPerm.support
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ orderOf f ∣ 1

Tactic:
use c

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := ⋯
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

Tactic:
· by_cases hx : i = x
    · simp only [hx, optionCongr_apply, Option.map_some, swap_apply_left,
             Option.some.injEq]
    by_cases hy : i = y <;> simp [hx, hy, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))

Tactic:
cases h : σ (some _)

Goal state after:
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : σ (some x) = none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) none

case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (some val✝)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x ^ (m - n)) x = x ↔ ↑(#(g.cycleOf x).support) ∣ m - n

Tactic:
cycle_zpow_mem_support_iff

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(#(g.cycleOf x).support) = 0 ↔ ↑(#(g.cycleOf x).support) ∣ m - n

case hg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x).IsCycle

case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x → g ^ m = 1

pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x

Tactic:
· intro hgm
      simp only [IsCycle.pow_eq_one_iff hg]
      use x

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x
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
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = 0

pp: case neg
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
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = i + 1

Tactic:
· have : ((castLEEmb (by lia)).toEquivRange.symm ⟨i, iin⟩) = last j := by
      simpa only [coe_castLEEmb, ← this, symm_apply_apply] using eq_of_val_eq (by simp [ch])
    rw [this, finRotate_last]
    rfl

Goal state after:
case neg
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
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = i + 1
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
simp [hij]

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

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

Tactic:
simp [hij]

Goal state after:
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 ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ ↑i ≤ ↑(Fin.cast ⋯ j)

Tactic:
simp [hij]

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

Goal state before:
pp: case inl
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i < j
⊢ j.cycleIcc i = 1

Tactic:
simp [hij]

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

Goal state before:
pp: case inr.inr.inr
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 : j ≤ x
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)

Tactic:
simp only [Function.comp_apply, cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]
    split_ifs with h
    · exact val_eq_of_eq (cycleIcc_of_last hij)
    · simp [cycleIcc_of_gt (lt_of_le_of_lt ch2 (lt_add_one_of_succ_lt (by lia)))]

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

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

Tactic:
simp [hij]

Goal state after:
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
⊢ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D

Tactic:
ext ⟨x1, x2⟩

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
x1 x2 : Fin n
⊢ ⟨x1, x2⟩ ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D ↔ ⟨x1, x2⟩ ∈ D
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
x1 x2 : Fin n
⊢ (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) ↔ x2 < x1

Tactic:
refine ⟨?_, fun hlt ↦ ?_⟩

Goal state after:
case refine_1
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
x1 x2 : Fin n
⊢ (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) → x2 < x1

case refine_2
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
x1 x2 : Fin n
hlt : x2 < x1
⊢ ∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ ∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle

pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset)).Pairwise Disjoint

pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g

Tactic:
· simp [or_imp, mem_cycleFactorsFinset_iff, forall_comm]

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset)).Pairwise Disjoint

case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
cycleFactorsFinset_noncommProd

Goal state after:
case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ f * g = f * g
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ #g.support ≤ #{a, g a, g (g a)}

Tactic:
hg3.card_support

Goal state after:
case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ 3 ≤ #{a, g a, g (g a)}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
hτ : τ.IsSwap
a b : α
ab : a ≠ b
⊢ swap a b * τ ∈ closure {σ | σ.IsThreeCycle}

Tactic:
obtain ⟨c, d, cd, rfl⟩ := hτ

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
⊢ swap a b * swap c d ∈ closure {σ | σ.IsThreeCycle}
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₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Tactic:
ext
  simp only [compLinearMap_apply, add_apply]

Goal state after: