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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor
  intro a b
  casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
  · rfl
  · rfl
  · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (ι F j✝ ≫ desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
colimit.ι_desc,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
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
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
⊢ Mono (Hom.left k)

Tactic:
by
  refine ⟨fun {Y : T} l m a => ?_⟩
  let l' : mk (m ≫ f.hom) ⟶ f := homMk l (by
        dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc])
  suffices l' = (homMk m : mk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left this
  rw [← cancel_mono k]
  ext
  apply a

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
  · cat_disch
  · cat_disch

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
Y : T
X : D
g : StructuredArrow X (proj Y F)
⊢ X ⟶ (proj X (proj Y F) ⋙ proj Y F).obj g

Tactic:
exact g.hom

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
Y : T
X : D
g : StructuredArrow Y (Under.forget X ⋙ F)
⊢ Y ⟶ F.obj ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).obj g)

Tactic:
exact g.hom

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 : T ⥤ D
Y : D
X : T
g : CostructuredArrow (proj F Y) X
⊢ (proj (proj F Y) X ⋙ proj F Y).obj g ⟶ X

Tactic:
exact g.hom

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 : T ⥤ D
Y : D
X : T
g : CostructuredArrow (Over.forget X ⋙ F) Y
⊢ F.obj ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).obj g) ⟶ Y

Tactic:
exact g.hom

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

Goal state before:
pp: case h₀
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂

pp: case h₁
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂

Tactic:
· simpa using congrArg (fun f => coprod.inl ≫ f) h

Goal state after:
case h₁
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default

Tactic:
· rw [← cancel_epi e.inv]
    apply hY.eq_of_src

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R X₂))) x✝

Tactic:
apply e.right_inv

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsIso 0 → IsZero X ∧ IsZero Y

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsZero X ∧ IsZero Y → IsIso 0

Tactic:
· intro h
    let h' := isIsoZeroEquivIsoZero _ _ h
    exact ⟨(isZero_zero _).of_iso h'.1, (isZero_zero _).of_iso h'.2⟩

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsZero X ∧ IsZero Y → IsIso 0
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ (P ⊔ Q).isoClosure X → P.isoClosure X ∨ Q.isoClosure X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X

Tactic:
· rintro ⟨Y, hY, ⟨e⟩⟩
    simp only [prop_sup_iff] at hY
    obtain hY | hY := hY
    · exact Or.inl ⟨Y, hY, ⟨e⟩⟩
    · exact Or.inr ⟨Y, hY, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

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

Tactic:
exact (le_iSup P a).trans (le_isoClosure _)

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
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
cc : CokernelCofork f
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ Arrow.Hom.left φ ≫ (Arrow.mk f').hom ≫ Cofork.π cc' = 0

Tactic:
condition,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
cc : CokernelCofork f
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ Arrow.Hom.left φ ≫ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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
F : J → C
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite J
⊢ HasBiproductsOfShape J C

Tactic:
by
  rcases Finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩
  have : HasBiproductsOfShape (Fin n) C := HasFiniteBiproducts.out n
  exact hasBiproductsOfShape_of_equiv C e

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
a✝ : j ∈ Finset.univ
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
have reassoced : m ≫ Bicone.π b j ≫ Bicone.ι b j = s.π.app ⟨j⟩ ≫ Bicone.ι b j := by
          simpa using eq_whisker (h ⟨j⟩) _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
a✝ : j ∈ Finset.univ
reassoced : m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
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 P' Q Q' X Y : C
b : BinaryBicone X Y
j j' : WalkingPair
⊢ WalkingPair.casesOn j b.inl b.inr ≫ WalkingPair.casesOn j' b.fst b.snd = if h : j = j' then eqToHom ⋯ else 0

Tactic:
rcases j with ⟨⟩ <;> rcases j' with ⟨⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j, g j ≫ h j

Tactic:
by
  classical
  simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

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

Goal state before:
pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : 𝟙 (X ⊞ Y) = fst ≫ inl
⊢ IsIso inl

Tactic:
exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

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

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
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ biproduct.fromSubtype f p ≫ biproduct.toSubtype f pᶜ = 0

Tactic:
by
        classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R X₂))) x✝

Tactic:
apply e.right_inv

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

Goal state before:
pp: k n : ℕ
⊢ Pairwise (Pi.Lex (fun x1 x2 ↦ x1 < x2) fun x x1 x2 ↦ x1 < x2) (antidiagonalTuple (k + 1) n)

Tactic:
simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2))
      (antidiagonal n)
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0

Tactic:
suffices ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0 by simpa

Goal state after:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_2
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ (c.embedding i) ⟨↑j - c.sizeUpTo ↑i, ⋯⟩ = j

Tactic:
rw [Fin.ext_iff]
      exact add_tsub_cancel_of_le h.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)

Tactic:
apply mapRange_finsuppAntidiag_subset

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

Goal state before:
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 : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ h.symm f ∈ s.finsuppAntidiag (e.symm (e 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 : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := ⋯
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ h.symm f ∈ map (mapRange.addEquiv e.symm).toEmbedding (s.finsuppAntidiag (e n))
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.extendDomain f.toEquivRange) (f a) = f (e a)

Tactic:
convert! Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.extendDomain f.toEquivRange) b = f (e (⋯.invOfMemRange ⟨b, h⟩))

Tactic:
Equiv.Perm.extendDomain_apply_subtype _ _ h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ ↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ i ∈ {i | ⟨↑i + 1, ⋯⟩ ∈ {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset}.toFinset ↔ i ∈ s

Tactic:
Fin.ext_iff,

Goal state after:
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ i ∈ {i | ⟨↑i + 1, ⋯⟩ ∈ {i | ↑i = ↑0 ∨ ↑i = ↑(Fin.last n) ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset}.toFinset ↔ i ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ c.boundary ⟨i, hi⟩ = j

Tactic:
Fin.ext_iff,

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ f x = (f :: tl).prod x

Tactic:
rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ g x ≠ x

Tactic:
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]
              split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ 1 < #f.support

Tactic:
one_lt_card_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ a b, a ∈ f.support ∧ b ∈ f.support ∧ a ≠ b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑u ^ 2 = 1

Tactic:
isUnit_sq u.isUnit

Goal state after:
u : ℤˣ
⊢ 1 = 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ f.signBijAux ⟨a₁, a₂⟩ ∈ finPairsLT n

Tactic:
unfold signBijAux

Goal state after:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ (if x : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst then ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ else ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩) ∈
    finPairsLT n
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
by_cases hg : g b < g a

Goal state after:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
hb : (g.extendDomain f) ↑(f (f.symm ⟨b, ⋯⟩)) ≠ ↑(f (f.symm ⟨b, ⋯⟩))
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
hb : g (f.symm ⟨b, ⋯⟩) ≠ f.symm ⟨b, ⋯⟩
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
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 a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'),

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 a₁ ≤ a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).IsSwap ↔ a ≠ b

Tactic:
by
  constructor
  · intro h hab
    apply h.isCycle.ne_one
    aesop
  · intro h; use a, b

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
intro a ha b hb

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
⊢ _root_.Disjoint a.support b.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign g

Tactic:
rw [hg, sign_symm_trans_trans]

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

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ n.Coprime (orderOf f)

Tactic:
have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ n.Coprime (orderOf f)