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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ i₁ ≫ j₁ ≫ g'' = (i₁ ≫ j₁) ≫ g''

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ i₁ ≫ j₁ ≫ g'' = i₁ ≫ j₁ ≫ g''
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
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ (m ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom

Tactic:
Category.assoc

Goal state after:
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
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ m ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
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✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ f.hom ≫ Hom.right k ≫ m = (f.hom ≫ Hom.right k) ≫ m

Tactic:
Category.assoc

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ f.hom ≫ Hom.right k ≫ m = f.hom ≫ Hom.right k ≫ m
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
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt

Tactic:
apply PullbackCone.IsLimit.hom_ext ht

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = v ≫ q ≫ ι f

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ v ≫ q ≫ ι f = v ≫ q ≫ ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ (v ≫ q) ≫ g = v ≫ q ≫ g

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ g = v ≫ q ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ preComp f g ≫
      lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } =
    𝟙 (image (f ≫ g))

Tactic:
ext
        simp [image.preComp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ } ≫
      preComp f g =
    𝟙 (image g)

Tactic:
ext
        simp [image.preComp]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ (imageMap sq1).map ≫ (imageMap sq2).map ≫ image.ι h.hom = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)

Tactic:
ImageMap.map_ι,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ (imageMap sq1).map ≫ image.ι g.hom ≫ Arrow.Hom.right sq2 = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ hO.from_ X ≫ hO.to_ Y ≫ f = hO.from_ X ≫ hO.to_ Z
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ (default ≫ default) ≫ f = default ≫ default

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ default ≫ default ≫ f = default ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso 0

Tactic:
exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))

Tactic:
apply fun s m => (Cocone.functoriality K F).map_injective _
              intro s m
              rw [Functor.map_preimage]
              apply t.uniq_cocone_morphism

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ : CancelMonoid M
⊢ ∀ ⦃a₂ : CancelMonoid M⦄, m₁.toRightCancelMonoid = a₂.toRightCancelMonoid → m₁ = a₂

Tactic:
m₂

Goal state after:
M : Type u
m₁ m₂ : CancelMonoid M
⊢ m₁.toRightCancelMonoid = m₂.toRightCancelMonoid → m₁ = m₂
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
⊢ g₁ = g₂

Tactic:
have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)

Goal state after:
G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
h₁ : One.one = One.one
⊢ g₁ = g₂
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
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
⊢ f ≫ e.inv ≫ s = 0

Tactic:
rw [iff, e.hom_inv_id_assoc, hs]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasCokernels C
f g : Arrow C
u : f ⟶ g
⊢ f.hom ≫ Arrow.Hom.right u ≫ cokernel.π g.hom = 0

Tactic:
simp [← Arrow.w_assoc u]

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
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
have hₗ := h ⟨.left⟩
        have hᵣ := h ⟨.right⟩
        dsimp at hₗ hᵣ
        simpa [← hₗ, ← hᵣ] using total.symm =≫ m

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.inl = BinaryFan.IsLimit.lift ht (𝟙 X) 0

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

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

Goal state before:
pp: case neg
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
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
h : ¬(p j)ᶜ
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
          simpa using w.symm

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

Goal state before:
pp: k : ℕ
⊢ antidiagonalTuple (k + 1) 0 = [0]

Tactic:
rw [antidiagonalTuple, antidiagonal_zero, List.flatMap_singleton,
      antidiagonalTuple_zero_right k, List.map_singleton]
    exact congr_arg (fun x => [x]) Matrix.cons_zero_zero

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s

Tactic:
by
  simp_rw [Equiv.Perm.coe_pow]; exact SurjOn.iterate

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

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

Tactic:
rw [← Composition.ext_iff] at hc

Goal state after:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
· rw [reverse_append, reverse_single]
      apply cast_heq

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

Goal state before:
pp: case mpr
n✝ n : ℕ
c : CompositionAsSet n
j : Fin n
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last n
⊢ ∃ j_1, ⟨↑j_1 + 1, ⋯⟩ ∈ c.boundaries ∧ ↑j.succ = ↑j_1 + 1

Tactic:
rcases Nat.exists_add_one_eq.mpr j.pos with ⟨n, rfl⟩

Goal state after:
case mpr
n✝ n : ℕ
c : CompositionAsSet (n + 1)
j : Fin (n + 1)
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last (n + 1)
⊢ ∃ j_1, ⟨↑j_1 + 1, ⋯⟩ ∈ c.boundaries ∧ ↑j.succ = ↑j_1 + 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
← perm_symm_mapsTo_iff_mapsTo

Goal state after:
case mp
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
← perm_symm_mapsTo_iff_mapsTo

Goal state after:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : 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
hx : x ∈ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
rw [formPerm_cons_cons, mul_apply, swap_apply_def]

Goal state after:
case pos
α : 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
hx : x ∈ z :: l
⊢ (if (z :: l).formPerm x = y then z else if (z :: l).formPerm x = z then y else (z :: l).formPerm x) ∈ y :: z :: l
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ 1 * f = f

Tactic:
one_mul

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ f = f
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:
simp_rw [one_lt_card_iff, mem_support, ← not_or]
  contrapose! h
  ext a
  specialize h (f a) a
  rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : ¬f a = a
⊢ f a = (swap x y) a

Tactic:
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : ¬f a = a
ha' : f a = x ∨ f a = y
⊢ f a = (swap x y) a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 2 ↔ f.IsSwap

Tactic:
by
  constructor <;> intro h
  · obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
    obtain ⟨y, rfl⟩ := card_eq_one.1 ht
    rw [mem_singleton] at hmem
    refine ⟨x, y, hmem, ?_⟩
    ext a
    have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
    by_cases ha : f a = a
    · have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
      rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
    · have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
      obtain rfl | rfl := (key a).mp ha
      · rw [Or.resolve_left ha' ha, swap_apply_left]
      · rw [Or.resolve_right ha' ha, swap_apply_right]
  · obtain ⟨x, y, hxy, rfl⟩ := h
    exact card_support_swap hxy

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ #l.prod.support = (List.map (card ∘ support) l).sum

Tactic:
by
  induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ 1 * f = f

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ f = f
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
hxa : ¬(Equiv.symm f) a₂ < (Equiv.symm f) a₁
h : (Equiv.symm f) a₁ = (Equiv.symm f) a₂
⊢ False

Tactic:
simp [mem_finPairsLT, f⁻¹.injective h] at ha

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
this : l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]

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

Goal state before:
pp: case mpr
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
⊢ g ∈ ofSubtype.range

Tactic:
refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩

Goal state after:
case mpr
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
⊢ p (g x) ↔ p x
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: l : List ℕ
k : ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

Tactic:
induction l <;> simp [Nat.coprime_mul_iff_left, *]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ Equiv.trans f (swap x (f x)) = Equiv.refl α

Tactic:
hf.eq_swap_of_apply_apply_eq_self hx.1 h1,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ Equiv.trans (swap x (f x)) (swap x ((swap x (f x)) x)) = Equiv.refl α
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ #f.support

Tactic:
hf.eq_swap_of_apply_apply_eq_self hx.1 h1,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ #(swap x (f x)).support
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]

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

Goal state before:
pp: d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ x.gcd y = d

Tactic:
rw [← Int.gcd_natCast_natCast]
  apply int_gcd_helper' a (-b)
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hu))
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hv))
  rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
  exact mod_cast h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Tactic:
refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ (decomposeFin.symm (p, e)) x.succ = (swap 0 p) (e x).succ

Tactic:
by
  refine Fin.cases ?_ ?_ p
  · simp [Equiv.Perm.decomposeFin]
  · intro i
    by_cases h : i = e x
    · simp [h, Equiv.Perm.decomposeFin]
    · simp [Equiv.Perm.decomposeFin, swap_apply_def, Ne.symm h]

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

Goal state before:
pp: case neg
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
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑k - ↑i + 1 + (n - (n - ↑i)) = (↑k + 1) % n

Tactic:
Nat.mod_eq_of_lt (by lia)

Goal state after:
case neg
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
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑k - ↑i + 1 + (n - (n - ↑i)) = ↑k + 1