mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
⊢ f x = g x

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

Goal state after:
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
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
⊢ f x = g x
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)
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
⊢ 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
⊢ c.sizeUpTo ↑i ≤ ↑j
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.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:
·

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.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : MulAction (Perm α) β
i j : α
x : β
⊢ swap i j • swap i j • x = x

Tactic:
simp [smul_smul]

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

pp: n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
·

Goal state after:
case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
Module: Mathlib.Combinatorics.Enumerative.Composition

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

pp: case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)

Tactic:
·

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
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
·

Goal state after:
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.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ Int.negSucc n) x = x ∨ (f ^ Int.negSucc n) x = f x

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm,
      inv_eq_iff_eq, ← mul_apply, ← pow_succ, @eq_comm _ x, or_comm]

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = x ∨ (f ^ (n + 1 + 1)) x = f x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e_3
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i) y) = i

pp: case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.invEmbedding ((c.embedding i) y) ≍ y

Tactic:
·

Goal state after:
case e_3
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i) y) = i
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) y)) = ↑y

pp: case e_4.h
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i) y)) = c.blocksFun i

Tactic:
·

Goal state after:
case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) y)) = ↑y
Module: Mathlib.GroupTheory.Perm.Support

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

pp: case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a

Tactic:
·

Goal state after:
case inl
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hσ : σ a = a
⊢ σ a = a ∧ τ a = a
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e_4.h
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i) y)) = c.blocksFun i

Tactic:
·

Goal state after:
case e_4.h
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i) y)) = c.blocksFun i
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

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

Tactic:
·

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
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

Tactic:
·

Goal state after:
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.Combinatorics.Enumerative.Composition

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

pp: case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Tactic:
·

Goal state after:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

pp: 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)

Tactic:
·

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)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Tactic:
·

Goal state after:
case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

Tactic:
·

Goal state after:
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.Combinatorics.Enumerative.Composition

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

pp: case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n

Tactic:
·

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n

Tactic:
·

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

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

pp: case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h

Tactic:
·

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

Goal state before:
pp: case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ f ∈ f :: l

pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ ∀ f ∈ l, f x = x

Tactic:
·

Goal state after:
case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ f ∈ f :: l
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
·

Goal state after:
case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h
Module: Mathlib.GroupTheory.Perm.Support

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

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∈ c.support
⊢ c x ∈ s ↔ x ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

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

pp: case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn

Tactic:
·

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

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

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn

Tactic:
·

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

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

Tactic:
·

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)
Module: Mathlib.GroupTheory.Perm.Support

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

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

Tactic:
·

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
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
intro a ha
      by_contra ha'
      rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
      exact ha rfl

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

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

Tactic:
·

Goal state after:
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.GroupTheory.Perm.Support

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

Tactic:
·

Goal state after:
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.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e'_1
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ k + 1 + n = n + (k + 1)

pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
·

Goal state after:
case e'_1
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ k + 1 + n = n + (k + 1)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
·

Goal state after:
case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)
Module: Mathlib.GroupTheory.Perm.Support

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

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
·

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