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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ x ≫ f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ (i ≫ i') ≫ ⋯.lift = f

Tactic:
simp only [assoc, CommSq.fac_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := u } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := u }

Tactic:
by
    cases u
    · simp [Category.id_comp]
    · simp [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ m.right = (homMk (T.preimage c.pt.hom) ⋯).right

Tactic:
· apply T.map_injective
      simpa only [homMk_right, T.map_preimage, ← w m] using! (Category.id_comp _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
f : CostructuredArrow (toOver F X) Y
⊢ F.map (Iso.refl ((𝟭 (CostructuredArrow (toOver F X) Y)).obj f).left.left).hom ≫
      ((costructuredArrowToOverEquivalence.functor F Y ⋙ costructuredArrowToOverEquivalence.inverse F Y).obj
            f).left.hom =
    ((𝟭 (CostructuredArrow (toOver F X) Y)).obj f).left.hom

Tactic:
by simpa using f.hom.w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.snd i (f ≫ i))

Tactic:
by
  have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono (𝟙 _) f i⟩ WalkingCospan.right
  convert! (congrArg IsIso (show _ ≫ pullback.snd (𝟙 Z) f = _ from this)).mp inferInstance
  · exact (Category.id_comp _).symm
  · exact (Category.id_comp _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst

Tactic:
by
  refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩
  apply PullbackCone.IsLimit.hom_ext ht
  · simp
  · simp [fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := hF.iso hG
⊢ IsZero (F.obj X)

Tactic:
exact (isZero_zero _).of_iso (e.app X)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteLimits C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
cases nonempty_fintype J; exact HasFiniteLimits.out _

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure = ⨆ a, (P a).isoClosure

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure ≤ ⨆ a, (P a).isoClosure

case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ⨆ a, (P a).isoClosure ≤ (⨆ a, P a).isoClosure
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
← cancel_epi g,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ g ≫ f ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : f = 0
Z'✝ : C
x✝² : Y ⟶ Z'✝
x✝¹ : f ≫ x✝² = 0
x✝ : Y ⟶ Z'✝
hb : 𝟙 Y ≫ x✝ = x✝²
⊢ x✝ = x✝²

Tactic:
by simp only [← hb, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ coequalizer.π 0 0 ≫ cokernelZeroIsoTarget.hom = coequalizer.π 0 0 ≫ cokernel.desc 0 (𝟙 Y) ⋯

Tactic:
simp [cokernelZeroIsoTarget]

Goal state after:
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 P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ (Cone.postcompose (mapPairIso eP eQ).hom).obj b.toCone ≅ (b.ofIso eP eQ).toCone

Tactic:
exact BinaryFan.ext (Iso.refl _) (by simp [BinaryFan.fst])
      (by simp [BinaryFan.snd])

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
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) =
    𝟙 Y

Tactic:
rw [isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]

Goal state after:
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
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) =
    𝟙 Y
Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s : Finset β
a : α
x : β
⊢ x ∈ a • s ↔ ∃ y ∈ s, a • y = x

Tactic:
by
  simp only [Finset.smul_finset_def, mem_image]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ (f ≫ biprod.fst ≫ biprod.inl + f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst = 0

Tactic:
rw [comp_add_assoc, add_comp]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ x ≠ y

Tactic:
simp only [Ne, Subtype.ext_iff] at hxy
    exact hxy.1

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

Goal state before:
pp: case mp
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) → f ∈ s.finsuppAntidiag (e n)

pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ s.finsuppAntidiag (e n) → f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n)

Tactic:
· apply mapRange_finsuppAntidiag_subset

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ s.finsuppAntidiag (e n) → f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ c.blocksFun i

Tactic:
rintro rfl
    exact ⟨⟨0, by simp⟩, by simp⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
⊢ Fintype.card { x // x ∈ s } = ft.card

Tactic:
← Fintype.subtype_card ft ht

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
⊢ Fintype.card { x // x ∈ s } = Fintype.card { x // x ∈ t }
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
⊢ i < c.blocks.length

Tactic:
rw [c.card_boundaries_eq_succ_length] at h

Goal state after:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.length + 1
⊢ i < c.blocks.length
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
hx' : x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Tactic:
simpa using zipWith_swap_prod_support' _ _ hx'

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ a ∈ closure S, ↑a.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
apply closure_induction
  · exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl
  · simp
  · intro a b ha hb hc hd
    refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_
    rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]
    exact ⟨hc, hd⟩
  · simp only [support_inv, imp_self, implies_true]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ sign (Equiv.trans f g) = sign g * sign f

Tactic:
← mul_def,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ sign (g * f) = sign g * sign f
Module: Mathlib.Tactic.NormNum.GCD

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

Tactic:
simp_rw [Rat.mul_num, Rat.den_intCast, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.num_intCast, one_mul, mul_one, h, Nat.cast_one, Int.ediv_one, Int.cast_id]

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

Goal state before:
pp: case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : (f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

pp: case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

Tactic:
· obtain ⟨z, rfl⟩ := hxy
    rw [cycleOf_apply_apply_zpow_self]
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

Goal state after:
case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ (∃ m < Fintype.card α, (f ^ m) x = y) → f.SameCycle x y

Tactic:
rintro ⟨n, _, hn⟩
      exact ⟨n, hn⟩

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) ⋯
⊢ (i.cycleIcc j) k = if k = j then i else k + 1

Tactic:
simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this, Function.Embedding.trans_apply,
    addNatEmb_apply, coe_toEmbedding, finCongr_apply]

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 ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i))) =
    if k = j then i else k + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p

Tactic:
have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_gt hp.out.one_lt)
  have Scard :=
    calc
      p ∣ Fintype.card G ^ (p - 1) := hdvd.trans (dvd_pow (dvd_refl _) hp')
      _ = Fintype.card (vectorsProdEqOne G p) := (VectorsProdEqOne.card G p).symm
  let f : ℕ → vectorsProdEqOne G p → vectorsProdEqOne G p := fun k v =>
    VectorsProdEqOne.rotate v k
  have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero
  have hf2 : ∀ j k v, f k (f j v) = f (j + k) v := fun j k v =>
    VectorsProdEqOne.rotate_rotate v j k
  have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length
  let σ :=
    Equiv.mk (f 1) (f (p - 1)) (fun s => by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3])
      fun s => by rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
  have hσ : ∀ k v, (σ ^ k) v = f k v := fun k =>
    Nat.rec (fun v => (hf1 v).symm) (fun k hk v => by
      rw [pow_succ, Perm.mul_apply, hk (σ v), Nat.succ_eq_one_add, ← hf2 1 k]
      simp only [σ, coe_fn_mk]) k
  replace hσ : σ ^ p ^ 1 = 1 := Perm.ext fun v => by rw [pow_one, hσ, hf3, one_apply]
  let v₀ : vectorsProdEqOne G p :=
    ⟨List.Vector.replicate p 1, (List.prod_replicate p 1).trans (one_pow p)⟩
  have hv₀ : σ v₀ = v₀ := Subtype.ext (Subtype.ext (List.rotate_replicate (1 : G) p 1))
  obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀
  refine
    Exists.imp (fun g hg => orderOf_eq_prime ?_ fun hg' => hv2 ?_)
      (List.rotate_one_eq_self_iff_eq_replicate.mp (Subtype.ext_iff.mp (Subtype.ext_iff.mp hv1)))
  · rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
  · 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: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
h : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
x✝ : Perm α
⊢ x✝ = k⁻¹ * (k * x✝ * k⁻¹) * k

Tactic:
by group

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
⊢ P σ

Tactic:
by
  cases nonempty_fintype β
  suffices ∀ l : List (Perm β),
      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
    classical
      let x := σ.truncCycleFactors.out
      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
  intro l
  induction l with
  | nil => exact fun _ _ => base_one
  | cons σ l ih =>
    intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)

Goal state after:
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 : ¬g a = a
⊢ 3 ≤ #{a, g a, g (g a)}

Tactic:
rw [Finset.card_insert_eq_ite, if_neg]

Goal state after:
case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ 3 ≤ #{g a, g (g a)} + 1

case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ a ∉ {g a, g (g a)}
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 : ¬g a = a
⊢ 3 ≤ #{g a, g (g a)} + 1

Tactic:
rw [Finset.card_insert_eq_ite, if_neg]

Goal state after:
case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ 3 ≤ #{g (g a)} + 1 + 1

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)}
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 : q ≠ p
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = 0

Tactic:
Function.ne_iff

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
hpq : ∃ a, q a ≠ p a
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = 0
Module: Mathlib.LinearAlgebra.Multilinear.Basis

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
⊢ f = g

Tactic:
classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv (DFinsupp.single p r)) x = r • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by
  classical
  conv_lhs => rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]
  congr
  ext i
  obtain ⟨p, j⟩ := p
  rcases eq_or_ne j i with rfl | h
  · suffices ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i) by
      simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]
    exact fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm
  · simp [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
      fromDFinsuppEquiv_apply, h]

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 : ℤˣ
⊢ (∑ σ ∈ ofSign s, ∏ k, A k (σ k)) * ∑ σ ∈ ofSign t, ∏ k, B k (σ k) =
    ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)

Tactic:
sum_mul_sum,

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 : ℤˣ
⊢ ∑ i ∈ ofSign s, ∑ j ∈ ofSign t, (∏ k, A k (i k)) * ∏ k, B k (j k) =
    ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
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
⊢ ∑ σ, ∑ τ, (∏ i, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign τ)) * ∏ i, M (τ i) i = M.det * N.det

Tactic:
by
      simp only [det_apply', Finset.mul_sum, mul_comm, mul_left_comm, mul_assoc]

Goal state after: