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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f) ↔ f 0 + ∑ i, f i.succ = n

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f) → f 0 + ∑ i, f i.succ = n

case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ f 0 + ∑ i, f i.succ = n → ∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
constructor

Goal state after:
case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) → s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) → ∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.piAntidiag 0 = {0}

Tactic:
ext

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a✝ : ι → μ
⊢ a✝ ∈ ∅.piAntidiag 0 ↔ a✝ ∈ {0}
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f

case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
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 : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s ↔
    ∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s →
    ∃ a_2 b, a_2 + b = n ∧ ∃ g, f = g.update a a_2 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s) →
    f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
ext

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid μ
inst✝³ : PartialOrder μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
a✝ : ι → μ
⊢ a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: n k : ℕ
⊢ univ.piAntidiag n = Nat.antidiagonalTuple k n

Tactic:
ext

Goal state after:
n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
constructor

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

case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ (s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i) →
    ∃ y, s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

case mpr
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
    ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.blocks = [] ↔ n = 0

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : Composition n
⊢ c.blocks = [] → n = 0

case mpr
n : ℕ
c : Composition n
⊢ n = 0 → c.blocks = []
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ → j ∈ Set.range ⇑(c.embedding i)
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
⊢ ofSym s = indiscrete 1

Tactic:
ext

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
a✝ : ℕ
⊢ count a✝ (ofSym s).parts = count a✝ (indiscrete 1).parts
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: case refine_2
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ ((↑p).parts.erase a).sum = n - a

Tactic:
have hs : a + (p.1.parts.erase a).sum = n := by
        simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2)
      lia

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) ↔ i = c.index j

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → i = c.index j

case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)
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)
⊢ PreservesBiproduct f F

Tactic:
have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert! piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]

Goal state after:
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
⊢ PreservesBiproduct f F
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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ ((mapRange ⇑e ⋯ g).sum fun x x_1 ↦ x_1) = e n ∧ (mapRange ⇑e ⋯ g).support ⊆ s

Tactic:
constructor

Goal state after:
case left
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ ((mapRange ⇑e ⋯ g).sum fun x x_1 ↦ x_1) = e n

case right
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (mapRange ⇑e ⋯ g).support ⊆ s
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:
ext

Goal state after:
α : Type u_1
p : Perm α
x✝ : α
⊢ x✝ ∈ {x | (Equiv.symm p) x ≠ x} ↔ x✝ ∈ {x | p x ≠ x}
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
simp [eq_symm_apply, eq_comm]

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:
ext

Goal state after:
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ↑(((ones n).embedding i) ⟨0, h⟩) = ↑⟨↑i, ⋯⟩
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1

case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n
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 : μ
f : ι →₀ μ'
⊢ f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ↔ f ∈ s.finsuppAntidiag (e n)

Tactic:
constructor

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

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

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

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x✝ : α
⊢ x✝ ∈ ↑f.support ↔ x✝ ∈ {x | f x ≠ x}
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:
ext

Goal state after:
case h₁
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 ≫ prod.fst =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.fst

case h₂
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 ≫ prod.snd =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.snd
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → c.length = n

case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
ext

Goal state after:
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(((single n h).embedding 0) i) = ↑i
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
constructor

Goal state after:
case mp
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h → c.length = 1

case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
constructor

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

case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) ↔
    c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) →
    c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
constructor

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ⊆ s

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ (∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
⊢ f.toEquivRange = Equiv.ofInjective ⇑f ⋯

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
x✝ : α
⊢ ↑(f.toEquivRange x✝) = ↑((Equiv.ofInjective ⇑f ⋯) x✝)
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
⊢ ↑(s \ t) ≃ ↑(t \ s)
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
⊢ spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
x✝ : α
⊢ x✝ ∈ spᶜ ↔ x✝ ∈ sq \ sp ∪ (sp ∪ sq)ᶜ
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
⊢ sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x✝ : α
⊢ x✝ ∈ sqᶜ ↔ x✝ ∈ sp \ sq ∪ (sp ∪ sq)ᶜ
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
by
  simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]

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

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1) ↔ i ∈ c.boundaries

Tactic:
constructor

Goal state after:
case mp
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1) → i ∈ c.boundaries

case mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries → i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
constructor

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries
Module: Mathlib.GroupTheory.Perm.Finite

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

Tactic:
constructor

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

case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (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 neg
α : 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:
· 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: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ⊆ f.support
hg : y.support ⊆ g.support
⊢ x.Disjoint y

Tactic:
disjoint_iff_disjoint_support

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : _root_.Disjoint f.support g.support
hf : x.support ⊆ f.support
hg : y.support ⊆ g.support
⊢ _root_.Disjoint x.support y.support
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 2 → f.IsSwap

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsSwap → #f.support = 2