mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
by
  ext
  simp [mem_smul, mem_smul_finset, h]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
a b : Fin n
hab : a < b
⊢ f a < f b

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
a b : Fin n
hab : a < b
⊢ f a < f b
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
this : q.succAbove i < q
⊢ f i < x

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
this : q.succAbove i < q
⊢ f i < x
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
this : q < q.succAbove i
⊢ x < f i

Tactic:
simpa using

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
this : q < q.succAbove i
⊢ x < f i
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ m - f = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ m - g = 0
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q < q.succAbove j
⊢ q ≤ j.castSucc

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q < q.succAbove j
⊢ q ≤ j.castSucc
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q < q.succAbove j
this : q ≤ j.castSucc
⊢ q.insertNth x f q < q.insertNth x f (q.succAbove j)

Tactic:
simpa using

Goal state after:
case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q < q.succAbove j
this : q ≤ j.castSucc
⊢ x < f j
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
⊢ j.castSucc < q

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
⊢ j.castSucc < q
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
this : j.castSucc < q
⊢ q.insertNth x f (q.succAbove j) < q.insertNth x f q

Tactic:
simpa using

Goal state after:
case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
this : j.castSucc < q
⊢ f j < x
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)

Tactic:
simpa using

Goal state after:
case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ f j✝¹ < f j✝
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
g : Fin (n + 1) → Fin (n + 1)
hg : StrictMono g
x : Fin (n + 1)
⊢ g x ≤ id x

Tactic:
simpa using

Goal state after:
n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
g : Fin (n + 1) → Fin (n + 1)
hg : StrictMono g
x : Fin (n + 1)
⊢ g x ≤ x
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
key : ∀ (g : Fin (n + 1) → Fin (n + 1)), StrictMono g → g = id
⊢ f i = i.succ

Tactic:
simpa using

Goal state after:
n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
key : ∀ (g : Fin (n + 1) → Fin (n + 1)), StrictMono g → g = id
⊢ f i = i.succ
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Tactic:
simpa using

Goal state after:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ ↑x = p.succAbove ((p.castLT ⋯).predAbove ↑x)
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 μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
f : ↥(s.piAntidiag n)
⊢ ∀ (a : ι), a ∈ {x ∈ s | ↑f x ≠ 0} ↔ ↑f a ≠ 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
f : ↥(s.piAntidiag n)
⊢ ∀ (a : ι), ¬↑f a = 0 → a ∈ s
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
f g : Fin #s → μ
hfg : (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) = fun i ↦ if hi : i ∈ s then g (e ⟨i, hi⟩) else 0
i : Fin #s
⊢ f i = g i

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
f g : Fin #s → μ
hfg : (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) = fun i ↦ if hi : i ∈ s then g (e ⟨i, hi⟩) else 0
i : Fin #s
⊢ f i = g i
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 a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j ↦ if j = i then c else 0) = f + fun j ↦ if j = i then a else 0
⊢ s.sum f = s.sum g

Tactic:
simpa using

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j ↦ if j = i then c else 0) = f + fun j ↦ if j = i then a else 0
⊢ s.sum f = s.sum g
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 using

Goal state after:
case mp
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
n : ℕ
hn : n ≠ 0
f : ι → ℕ
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∀ (i : ι), ¬f i = 0 → i ∈ s
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ n • univ.piAntidiag m = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ n • univ.piAntidiag m = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun x ↦ n • x, inj' := ⋯ } (univ.piAntidiag m) = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∑ a ∈ s, f a • {a}).card = s.sum f ∧ ∀ (x : ι), Multiset.count x (∑ a ∈ s, f a • {a}) = f x

Tactic:
simpa using

Goal state after:
case mpr.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∀ x ∉ s, f x = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ 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)
    (antidiagonal n)

Tactic:
induction n with
    | zero =>
      rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    | succ n n_ih =>
      simp
      grind

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

Goal state before:
pp: n : ℕ
p : n.Partition
m : ℕ
h : m ∈ p.parts
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
n : ℕ
p : n.Partition
m : ℕ
h : m ∈ p.parts
⊢ m ≤ n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ b.sum = n

Tactic:
simpa using

Goal state after:
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ b.sum = n
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
← c.blocks_sum

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: n : ℕ
c : Composition n
| n

Tactic:
← c.blocks_sum

Goal state after:
n : ℕ
c : Composition n
| c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
simpa using

Goal state after:
case mp
n : ℕ
c : Composition n
h : c.blocks = []
⊢ n = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

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

Tactic:
simpa using

Goal state after:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts.card = 1
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

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

Tactic:
simpa using

Goal state after:
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ a + ((↑p).parts.erase a).sum = n
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

Tactic:
simpa using

Goal state after:
case inr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x
x : ι
hx : x ≠ a
⊢ f x = g x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ c.sizeUpTo ↑i + ↑j - c.sizeUpTo ↑i = ↑j

Tactic:
add_tsub_cancel_left

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

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

Tactic:
rwa [Fin.ext_iff]

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:
simpa using

Goal state after:
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ↑i ≤ n
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:
rw [A, this, ones_blocks]

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

Goal state before:
pp: case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get ⟨0, ⋯⟩].sum = n
⊢ [c.blocks.get ⟨0, ⋯⟩] = (single n h).blocks

Tactic:
simpa using

Goal state after:
case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get ⟨0, ⋯⟩].sum = n
⊢ c.blocks[0] = n
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
simpa using

Goal state after:
case mpr
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
this : ∀ (j : Fin c.length), j = i
⊢ c.length = 1
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✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a ↦ ↑a = ↑x) y
⊢ y = x

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a ↦ ↑a = ↑x) y
⊢ ↑y = ↑x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = n + ns.sum - n

Tactic:
add_tsub_cancel_left

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = ns.sum
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∩ g.support

Tactic:
mem_inter,

Goal state after:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∧ g x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x ↦ f i) x hx
y2 : α
hy2 : y2 ∈ s
hy : (fun i x ↦ f i) y2 hy2 ∈ s
⊢ (Equiv.symm f) ((fun i x ↦ f i) y2 hy2) ∈ s

Tactic:
simpa using

Goal state after:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x ↦ f i) x hx
y2 : α
hy2 : y2 ∈ s
hy : (fun i x ↦ f i) y2 hy2 ∈ s
⊢ y2 ∈ s
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
this : Finite ↑{x | p x}
⊢ p ((Equiv.symm f) x)

Tactic:
simpa using

Goal state after:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
this : Finite ↑{x | p x}
⊢ p ((Equiv.symm f) x)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.blocks.sum = n

Tactic:
have : c.blocks.take c.length = c.blocks := take_of_length_le (by simp [blocks])

Goal state after:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ c.blocks.sum = n
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith Equiv.swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith Equiv.swap l l').prod x = x
⊢ (Equiv.swap a b) x ≠ x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith Equiv.swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith Equiv.swap l l').prod x = x
⊢ ¬(Equiv.swap a b) x = x
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 < d.boundaries.card

Tactic:
simpa using

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 < d.length + 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
x✝ : α
h : x✝ ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x✝ ∈ ↑(l.toFinset ⊔ l'.toFinset)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
x✝ : α
h : x✝ ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x✝ ∈ l ∨ x✝ ∈ l'
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
⊢ x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
⊢ ¬(zipWith Equiv.swap l l').prod x = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
hx' : x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
hx' : x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x ∈ l ∨ x ∈ l'
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ ¬l.formPerm x = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l.toFinset

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
h : x ∈ [y]
⊢ [y].formPerm x ∈ [y]

Tactic:
simpa using

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
h : x ∈ [y]
⊢ x = y
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
hn : 0 + 1 < xs.length
⊢ xs.formPerm xs[0] = xs[0 + 1]

Tactic:
simpa using

Goal state after:
case zero
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
hn : 0 + 1 < xs.length
⊢ xs.formPerm xs[0] = xs[1]