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

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelCommMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
⊢ p = q ↔ p.2 = q.2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
⊢ mulAntidiagonal 1 = {(1, 1)}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ ⋃ i ∈ range (n + 1), disjointed f i = (partialSups f) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.1 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ (∏ k ∈ range m, f k) / ∏ k ∈ range n, f k = ∏ k ∈ range m with n ≤ k, f k

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.2 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (partialSups t) n

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n] i0)
⊢ toZ i0 (pred^[n] i0) = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ {x ∈ antidiagonal n | x.1 = m} ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ StrictMono (toZ i0)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ Iio (succ i) = Iic i

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
⊢ ∀ {a b : ι}, (Equiv.ofInjective (toZ hι.some) ⋯) a ≤ (Equiv.ofInjective (toZ hι.some) ⋯) b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ {x ∈ antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ Countable ι

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
⊢ ∀ i < m, i ≤ n

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ {x ∈ antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
⊢ LeftInverse (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) fun x ↦ ↑x.snd

Tactic:
by

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

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid A
inst✝³ : PartialOrder A
inst✝² : CanonicallyOrderedMul A
inst✝¹ : LocallyFiniteOrderBot A
inst✝ : DecidableEq A
n : A
a : A × A
⊢ a ∈ {uv ∈ Iic n ×ˢ Iic n | uv.1 * uv.2 = n} ↔ a.1 * a.2 = n

Tactic:
by

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

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : Multiplicative A
x✝¹ x✝ : A × A
h : (fun p ↦ (ofAdd p.1, ofAdd p.2)) x✝¹ = (fun p ↦ (ofAdd p.1, ofAdd p.2)) x✝
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
by

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

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : Multiplicative A
p : Multiplicative A × Multiplicative A
⊢ p ∈ map { toFun := fun p ↦ (ofAdd p.1, ofAdd p.2), inj' := ⋯ } (antidiagonal (toAdd a)) ↔ p.1 * p.2 = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ n + 1 - k ≤ n + 1 - m

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ p ∈ mulAntidiagonal (ofAdd a) ↔ (toAdd p.1, toAdd p.2) ∈ antidiagonal a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ (Ioc n m).sup (disjointed f) = f m \ f n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
ι : Type u_4
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → Set α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ ⋃ i ∈ Ioc n m, disjointed f i = f m \ f n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal n).length = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id Nat.succ) (antidiagonal n) ++ [(n + 1, 0)]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map Prod.swap (antidiagonal n) = (antidiagonal n).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ (∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ i ∈ range n, (n - 1 - i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
⊢ f = f' ∘ ⇑R

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal n).card = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
⊢ ∀ {a b : ι},
    { toFun := toZ hι.some, invFun := fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
            left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := toZ hι.some, invFun := fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i : ι
⊢ (fun n ↦ succ^[n] ⊥) ((fun i ↦ (toZ ⊥ i).toNat) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m ↦ range (n - m), f x.fst x.snd

Tactic:
refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1), ⟨a.snd, a.fst - a.snd⟩ ∈ (range n).sigma fun m ↦ range (n - m)

case refine_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m), ⟨a.fst + a.snd, a.fst⟩ ∈ (range n).sigma fun m ↦ range (m + 1)

case refine_3
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    ⟨⟨a.snd, a.fst - a.snd⟩.fst + ⟨a.snd, a.fst - a.snd⟩.snd, ⟨a.snd, a.fst - a.snd⟩.fst⟩ = a

case refine_4
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m),
    ⟨⟨a.fst + a.snd, a.fst⟩.snd, ⟨a.fst + a.snd, a.fst⟩.fst - ⟨a.fst + a.snd, a.fst⟩.snd⟩ = a

case refine_5
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    f a.snd (a.fst - a.snd) = f ⟨a.snd, a.fst - a.snd⟩.fst ⟨a.snd, a.fst - a.snd⟩.snd
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (fun i ↦ (toZ ⊥ i).toNat) ((fun n ↦ succ^[n] ⊥) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : CompleteBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i ⊓ ⨅ j, ⨅ (_ : j < i), (f j)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
⊢ (fun x ↦ Nat.find ⋯) ⁻¹' {n} = disjointed s n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∏ i ∈ Icc a b, f i = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ ↑((fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩) ((fun n ↦ succ^[↑n] ⊥) n)) = ↑n

Tactic:
simp only

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (toZ ⊥ (succ^[↑n] ⊥)).toNat = ↑n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∉ range (↑a + 1) →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Iic a then f ⟨a_1, h⟩.succ / f ⟨a_1, h⟩.castSucc else 1 else 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range (↑a + 1),
    a_1 ∉ range n →
      ((if hi : a_1 + 1 < n + 1 then f ⟨a_1 + 1, hi⟩ else 1) / if hi : a_1 < n + 1 then f ⟨a_1, hi⟩ else 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ range (↑a + 1) →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Iic a then f ⟨a_1, h⟩.succ / f ⟨a_1, h⟩.castSucc else 1 else 1) =
        (if hi : a_1 + 1 < n + 1 then f ⟨a_1 + 1, hi⟩ else 1) / if hi : a_1 < n + 1 then f ⟨a_1, hi⟩ else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ≤ a, f i.succ / f i.castSucc = f a.succ / f 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ ∏ i ∈ Icc a b, f i.succ / f i.castSucc = f b.succ / f a.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩) ((fun n ↦ succ^[↑n] ⊥) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
xy : ℕ × ℕ
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ } ↔ xy.1 + xy.2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = image (fun i ↦ (i, n - i)) (range (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = image (fun i ↦ (n - i, i)) (range (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ #(antidiagonal n) = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 1) ∉ map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) =
    cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (n + 1, 0) ∉ map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (n + 2, 0) ∉
    map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
      (antidiagonal n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 2) ∉
    cons (n + 2, 0)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n))
      ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ {a ∈ antidiagonal n | a.2 ≤ k} ↔
    (i, j) ∈ map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | a.2 ≤ k} =
    map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
by

Goal state after: