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

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

Tactic:
]

Goal state after:
case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∑ i, f (e ⟨↑i, ⋯⟩) = ∑ i, f i ∧ ∀ (i : ι), (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ 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 μ
s : Finset ι
n : μ
f : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum ⇑f = n ↔ ∑ x ∈ s, f x = n

Tactic:
]

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

Goal state before:
pp: case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i, (f ∘ Subtype.val ∘ ⇑e.symm) i = ∑ x ∈ s.attach, f ↑x

Tactic:
]

Goal state after:
case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i, (f ∘ Subtype.val ∘ ⇑e.symm) i = ∑ x ∈ s.attach, f ↑x
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False

Tactic:
]

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h :
  (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint
    (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k b.2))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

Tactic:
]

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h :
  (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint
    (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k b.2))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k : ℕ
⊢ [Fin.cons (0, 0).1 0] = [0]

Tactic:
]

Goal state after:
k : ℕ
⊢ [Fin.cons (0, 0).1 0] = [0]
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
ext; simp [Nat.mem_antidiagonalTuple]

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ 0

Tactic:
]

Goal state after:
case neg
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case e_a
x m : ℕ
hx : x < x + m + 1
⊢ [] = []

Tactic:
]

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f = f

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) (antidiagonal n) =
    map (fun i ↦ ![i.1, i.2]) (antidiagonal n)

Tactic:
]

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) (antidiagonal n) =
    map (fun i ↦ ![i.1, i.2]) (antidiagonal n)
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∑ i ∈ s, f i / n = m ∧ (∀ (i : ι), (fun i ↦ f i / n) i ≠ 0 → i ∈ s) ∧ (n • fun i ↦ f i / n) = f

Tactic:
simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]

Goal state after:
case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∀ (i : ι), n ≤ f i → i ∈ s
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun x ↦ n • x, inj' := ⋯ }) (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun x ↦ n • x, inj' := ⋯ }) (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = flatMap (fun x ↦ [![x.1, x.2]]) (antidiagonal n)

Tactic:
]

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = flatMap (fun x ↦ [![x.1, x.2]]) (antidiagonal n)
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_2
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
x : ι
hx : x ∈ s
⊢ f x = f x

Tactic:
]

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

Goal state before:
pp: case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    [(0, 0)]

Tactic:
]

Goal state after:
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    [(0, 0)]
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
c : Composition n
⊢ n = n

Tactic:
]

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

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : (filter (fun a ↦ ¬a = 0) l).sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
]

Goal state after:
n : ℕ
l : Multiset ℕ
hl : (filter (fun a ↦ ¬a = 0) l).sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (↑s).card = n

Tactic:
]

Goal state after:
n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (↑s).card = n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun a ↦ count a ↑s) (↑s).dedup

Tactic:
]

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun a ↦ count a ↑s) (↑s).dedup
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_3
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f.support ⊆ insert a s

Tactic:
]

Goal state after:
case mp.refine_3
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f.support ⊆ insert a s
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
i : σ
⊢ count (e i) (map ⇑e ↑s) = count (e i) (map ⇑e ↑s)

Tactic:
]

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

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ c.blocks.sum

Tactic:
]

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
c : Composition 0
⊢ c.blocks.length ≤ 0

Tactic:
]

Goal state after:
case mpr
c : Composition 0
⊢ c.blocks.length ≤ 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
h : p.parts.toFinset = q.parts.toFinset ∧ (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p = q

Tactic:
]

Goal state after:
n : ℕ
p q : n.Partition
h : p.parts.toFinset = q.parts.toFinset ∧ (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p = q
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ ∀ (a : ℕ), count a p.parts = count a q.parts

Tactic:
]

Goal state after:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ ∀ (a : ℕ), count a p.parts = count a q.parts
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take i c.blocks).sum + c.blocks[i] = (take i c.blocks).sum + c.blocks[i]

Tactic:
]

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

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]

Tactic:
]

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case a.a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl ≫ f ≫ biprod.fst

pp: case a.a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl

pp: case a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| inv f

pp: case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.fst

Tactic:
rw [a₁]

Goal state after:
case a.a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| 0

case a.a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl

case a.a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| inv f

case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.fst
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hx
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ n1 = n1

Tactic:
]

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo (↑(c.index j) + 1)

pp: n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
]

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo (↑(c.index j) + 1)

n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∑ m ∈ p.parts.toFinset, count m p.parts • m = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m

Tactic:
]

Goal state after:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∑ m ∈ p.parts.toFinset, count m p.parts • m = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j - c.sizeUpTo ↑(c.index j) < c.blocksFun (c.index j)

Tactic:
rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
    · exact lt_sizeUpTo_index_succ _ _
    · exact sizeUpTo_index_le _ _

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j

Tactic:
]

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ g x = g x

Tactic:
]

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

Goal state before:
pp: 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

Tactic:
rintro ⟨n1, n2, rfl, g, rfl, rfl, hgsupp⟩
    refine ⟨?_, (support_update_subset _ _).trans (insert_subset_insert a hgsupp)⟩
    simp only [coe_update]
    apply congr_arg₂
    · rw [Function.update_self]
    · apply sum_congr rfl
      intro x hx
      rw [update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g]

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

Goal state before:
pp: p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
⊢ {1} = {1}

Tactic:
]

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

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : ↑((c.embedding i) k) = ↑j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
]

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : ↑((c.embedding i) k) = ↑j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1

Tactic:
]

Goal state after:
n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : c.sizeUpTo ↑i + ↑k = ↑j
⊢ c.sizeUpTo ↑i ≤ c.sizeUpTo ↑i + ↑k ∧ c.sizeUpTo ↑i + ↑k < c.sizeUpTo (↑i).succ

Tactic:
]

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : c.sizeUpTo ↑i + ↑k = ↑j
⊢ c.sizeUpTo ↑i ≤ c.sizeUpTo ↑i + ↑k ∧ c.sizeUpTo ↑i + ↑k < c.sizeUpTo (↑i).succ
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo (↑i + 1)

pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j

Tactic:
]

Goal state after:
case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo (↑i + 1)

case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (∑ j, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (∑ j, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
hf : x ∉ f.support
hg : x ∉ g.support
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f x = x ∨ g x = x

Tactic:
]

Goal state after:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
⊢ f.Disjoint g ↔ f.Disjoint g

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f

Tactic:
]

Goal state after:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)

Tactic:
]

Goal state after:
case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ x = x

Tactic:
]

Goal state after: