mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
⊢ (insert a s).finsuppAntidiag n =
    (antidiagonal n).biUnion fun p ↦
      map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this✝ : HasProduct fun b ↦ F.obj (f b)
that :
  piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom
this : IsIso (F.biproductComparison f)
⊢ IsIso (piComparison F f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : σ a = a ∧ τ a = a
⊢ (σ * τ) a = a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
⊢ Epi (F.splitEpiBiproductComparison f).section_

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
⊢ s.finsuppAntidiag n ⊆ t.finsuppAntidiag n

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
x : (i : Fin c.length) × Fin (c.blocksFun i)
⊢ (fun j ↦ ⟨c.index j, c.invEmbedding j⟩) ((fun x ↦ (c.embedding x.fst) x.snd) x) = x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
⊢ PreservesBiproduct f F

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
⊢ ofSubtype (swap x y) = swap ↑x ↑y

Tactic:
by

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

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

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

Tactic:
by

Goal state after:
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⟩
⊢ ofSubtype f = swap x y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
      (F.mapCocone c).ι.app j

Tactic:
by

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

Goal state before:
pp: c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd.blocks = c'.snd.blocks

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (swap x (f x) * f) y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Perm α
⊢ {x | (Equiv.symm p) x ≠ x} = {x | p x ≠ x}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
        (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
      (F.mapBicone b).toCocone.ι.app j

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ n = n'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).pt ≅
    (F.mapCone c).pt

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Perm α
a : α
⊢ p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}

Tactic:
by

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

Goal state before:
pp: c c' : (n : ℕ) × Composition n
⊢ c = c' ↔ c.snd.blocks = c'.snd.blocks

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Perm α
n : ℤ
⊢ {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Type u_1
inst✝ : CommMonoid A
a : Fin n → A
x : Composition n
⊢ ∏ i, ∏ j, a ((x.embedding i) j) = ∏ i, a i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      j =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app j

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n i : ℕ
hi : i ∈ replicate n 1
⊢ 0 < i

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
⊢ (replicate n 1).sum = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p q : Perm α
⊢ {x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (ones n).length
⊢ (ones n).blocksFun i = 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅ (F.mapBinaryBicone b).toCone.pt

Tactic:
by

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

Goal state before:
pp: n i : ℕ
⊢ (ones n).sizeUpTo i = min i n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
by

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

Goal state before:
pp: ι : 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 : μ
⊢ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ((ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support ↔ f x ≠ x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app j

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑f.support = {x | f x ≠ x}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ.support = ∅ ↔ σ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ support 1 = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
⊢ f = g

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ g x ∈ c.support ↔ x ∈ c.support

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
j : ℕ
hj : j ∈ c.blocks
⊢ j = 1 ↔ j ≤ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
this : IsIso (F.biprodComparison X Y)
⊢ IsIso (prodComparison F X Y)

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n = ∑ i, 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ⊔ g.support

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ Epi (F.splitEpiBiprodComparison X Y).section_

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c = ones n ↔ c.length = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c = ones n ↔ n ≤ c.length

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).pt ≅
    (F.mapCocone c).pt

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ ∀ {i : ℕ}, i ∈ [n] → 0 < i

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ [n].sum = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
i : Fin (single n h).length
⊢ (single n h).blocksFun i = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
i : Fin n
⊢ ((single n h).embedding 0) i = i

Tactic:
by

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

Goal state before:
pp: ι : 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 : μ
⊢ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
x : α
hx : x ∈ l.prod.support
⊢ ∃ f ∈ l, x ∈ f.support

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : DecidableEq μ
inst✝³ : AddCommMonoid μ
inst✝² : PartialOrder μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
⊢ s.finsuppAntidiag 0 = {0}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h ↔ c.length = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ f x ∈ f.support ↔ x ∈ f.support

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ 0 < (single n hn).length

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ n ≤ (single n hn).blocksFun ⟨0, ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        j ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
⊢ c x ∈ s ↔ x ∈ s

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k, c.blocksFun k ≤ c.blocksFun i

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ ∀ (j : Fin c.length), j = i

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn ≍ c

Tactic:
by

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

Goal state before:
pp: n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn = cast ⋯ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
b : ↑(Set.range f)
⊢ ∀ (a : α), f a = ↑b ↔ a ∈ Finset.univ ∧ f a = ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
⊢ (Set.range f).domRestrict (invFun f) = hf.invOfMemRange

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ hf.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
⊢ (Set.range ⇑f).domRestrict (invFun ⇑f) = f.invOfMemRange

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
a : α
⊢ f.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ ∀ {i : ℕ}, i ∈ c₁.blocks ++ c₂.blocks → 0 < i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
hp : ∃! a, p a
⊢ ∃! a, a ∈ univ ∧ p a

Tactic:
by

Goal state after: