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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none)

case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (term WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ ∀ {X Y : WalkingSpan} (f : X ⟶ Y), F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id none) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none)

case none.some.left.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.left) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.left)

case none.some.right.init
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (init WalkingPair.right) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (init WalkingPair.right)

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
unfold prodComparison

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) =
    G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
desc : (s : PushoutCocone f g) → t.pt ⟶ s.pt
fac_left : ∀ (s : PushoutCocone f g), t.inl ≫ desc s = s.inl
fac_right : ∀ (s : PushoutCocone f g), t.inr ≫ desc s = s.inr
uniq : ∀ (s : PushoutCocone f g) (m : t.pt ⟶ s.pt), (∀ (j : WalkingSpan), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (span f g)
j : WalkingSpan
⊢ t.ι.app none ≫ desc s = s.ι.app none

Tactic:
by simp [← s.w fst, ← t.w fst, fac_left s]

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
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
⊢ Epi (Hom.right k)

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

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
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ (post F).map (homMk a ⋯) = f

Tactic:
ext; simpa

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inl f g ≫ 𝟙 (pushout f g)

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inr f g ≫ 𝟙 (pushout f g)

Tactic:
· simp [← pushout.condition]

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inr f g ≫ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = pushout.inr f g ≫ 𝟙 (pushout f g)
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
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
⊢ t.fst ≫ x ≫ h = t.snd ≫ y ≫ h

Tactic:
by  -- Porting note: reassoc workaround
      rw [← Category.assoc, ← Category.assoc]
      apply congrArg (· ≫ h) t.condition

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
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)
⊢ g = 𝟙 (image f) ≫ g

Tactic:
rw [Category.id_comp]

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 C
X : C
⊢ Mono (zeroIsInitial.to X)

Tactic:
by infer_instance

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
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)
⊢ 𝟙 (image f) ≫ h = h

Tactic:
rw [Category.id_comp]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
⊢ ∀ (s_1 : Fork (h ≫ f) (h ≫ g)), liftPrecomp h hs hc s_1 ≫ (precompFork h s c).ι = s_1.ι

Tactic:
simp [liftPrecomp, precompFork]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0 = 0

Tactic:
· simp only [id_obj, Adjunction.unit_naturality_assoc, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -f ≫ g = -f ≫ g'
⊢ g = g'

Tactic:
← comp_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : f ≫ (-g) = -f ≫ g'
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : f ≫ (-g) = -f ≫ g'
⊢ g = g'

Tactic:
← comp_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : f ≫ (-g) = f ≫ (-g')
⊢ g = g'
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteLimits C
⊢ HasEqualizers C

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
⊢ HasCoequalizers C

Tactic:
by infer_instance

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

Goal state before:
pp: case intro
C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
val✝ : Fintype J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
exact HasFiniteColimits.out _

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✝ : HasFiniteWidePullbacks C
⊢ HasPullbacks C

Tactic:
by infer_instance

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✝ : HasFiniteWidePushouts C
⊢ HasPushouts C

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
J : ℕ
⊢ HasColimitsOfShape (Discrete (Fin J)) C

Tactic:
by infer_instance

Goal state after:
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

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:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : ObjectProperty C
X : C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ (P ⊔ Q).IsClosedUnderIsomorphisms

Tactic:
by
  simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self, isoClosure_sup, isoClosure_eq_self]

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
inst✝¹ : HasCokernel f
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst✝ : Epi k
Z : C
g g' : W ⟶ Z
w : k ≫ g = k ≫ g'
⊢ g = g'

Tactic:
exact (cancel_epi k).1 w

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

Goal state before:
pp: case mp
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
n : ℕ
hn : n ≠ 0
f : ι → ℕ
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ s.sum (n • f) = n * s.sum f ∧ (∀ (i : ι), (n • f) i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ (n • f) i

Tactic:
simpa [← mul_sum, hn] using hf

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

Goal state before:
pp: n : ℕ
p : n.Partition
⊢ ∀ ⦃a₂ : n.Partition⦄,
    (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) p =
        (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) a₂ →
      p = a₂

Tactic:
q

Goal state after:
n : ℕ
p q : n.Partition
⊢ (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) p =
      (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) q →
    p = q
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ (∀ (x : α), (σ * τ) x = 1 x) ↔ (∀ (x : α), σ x = 1 x) ∧ ∀ (x : α), τ x = 1 x

Tactic:
one_apply,

Goal state after:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ (∀ (x : α), (σ * τ) x = x) ↔ (∀ (x : α), σ x = x) ∧ ∀ (x : α), τ x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ c.blocks = (ones n).blocks

Tactic:
A,

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ replicate c.blocks.length 1 = (ones n).blocks
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ f x = x ∧ g x = x → f (g x) = x

Tactic:
rintro ⟨hf, hg⟩

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f (g x) = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ ofFn c.blocksFun
i_blocks : 1 < i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i

Tactic:
mem_ofFn' c.blocksFun,

Goal state after:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ Set.range c.blocksFun
i_blocks : 1 < i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ ↑(l.toFinset ⊔ l.tail.toFinset) ⊆ ↑l.toFinset

Tactic:
simpa [Finset.subset_iff] using! tail_subset l

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

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑((d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩) = ↑(c.boundary ⟨i, i_lt''⟩)

Tactic:
A,

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑((c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩) = ↑(c.boundary ⟨i, i_lt''⟩)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f a = a ∨ f a = a
⊢ f a = 1 a

Tactic:
or_self_iff

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f a = a
⊢ f a = 1 a
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case intro.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α), (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (g * l.prod)

Tactic:
hxy.2

Goal state after:
case intro.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α), (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (swap x y * l.prod)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_1
α : 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
⊢ (g.extendDomain f) ↑(f a) ≠ ↑(f a)

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
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Tactic:
· rw [extendDomain_apply_image]
    exact Subtype.coe_injective.ne (f.injective.ne ha)

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
⊢ (g.extendDomain f).SameCycle (↑(f a)) b
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

Tactic:
ofSubtype_apply_of_not_mem u hx

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : (prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : (prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (a₁, b₁).2 = (a₂, b₂).2
⊢ (a₁, b₁) = (a₂, b₂)

Tactic:
simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h

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

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, (f ^ n) a)

Tactic:
exact ⟨_, _, hx.1, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro.hcomm
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
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)

Tactic:
intro _ _ hj
    apply hcomm
    exact hj ∘ Subtype.ext

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : w✝.IsCycle
⊢ 2 ≤ #w✝.support

Tactic:
exact hc.two_le_card_support

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ g (c x) = c (g x)

Tactic:
by_cases hx : x ∈ c.support

Goal state after:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
⊢ g (c x) = c (g x)

case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g (c x) = c (g x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
    rcases k with - | k
    · refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
      simp only [pow_zero, coe_one, id_eq] at hk'
      subst hk'
      rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : g x = x
y : α
hy : g y ≠ y
h : y = x
⊢ g y = y

Tactic:
by rwa [h]

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

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)

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 ⋯)
⊢ ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)

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

Goal state before:
pp: case comm.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
a : ↥f.cycleFactorsFinset
a✝¹ : a ∈ ↑univ
b : ↥f.cycleFactorsFinset
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) a ∈ Subgroup.zpowers ↑a

Tactic:
simp only [Subgroup.coe_subtype, SetLike.coe_mem]

Goal state after: