awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
exact nsmul_piAntidiag _ _ hn

Premises used: Finset.nsmul_piAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
classical classical₁ classical₂ classical₃ :
  image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
⊢ map { toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn

Premises used: Finset.map_eq_image, Finset.nsmul_piAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Finset (ι → ℕ)) (SMul.smul n (piAntidiag univ m))
    ({f ∈ piAntidiag univ (n * m) | ∀ (i : ι), n ∣ f i})

Tactic:
simpa using nsmul_piAntidiag (univ : Finset ι) m hn

Premises used: Finset.univ, Finset.nsmul_piAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Finset ((x : ι) → ℕ))
    (map (α := (x : ι) → ℕ) { toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } (piAntidiag univ m))
    ({f ∈ piAntidiag univ (n * m) | ∀ (i : ι), n ∣ f i})

Tactic:
simpa using map_nsmul_piAntidiag (univ : Finset ι) m hn

Premises used: Finset.univ, Finset.map_nsmul_piAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
h :
  ∀ (f : (a : ι) → ℕ),
    f ∈
        map
          { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := ⋯ : Sym ι n ↪ (a : ι) → ℕ }
          (s.sym n) ↔
      f ∈ s.piAntidiag n
⊢ map { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := ⋯ : Sym ι n ↪ (a : ι) → ℕ }
      (s.sym n) =
    s.piAntidiag n

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : (a : ι) → ℕ
h :
  (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ f ∈
      map { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := ⋯ : Sym ι n ↪ (a : ι) → ℕ }
        (s.sym n) ↔
    f ∈ s.piAntidiag n

Tactic:
simp only [Sym.val_eq_coe, mem_map, mem_sym_iff, Embedding.coeFn_mk, funext_iff, Sym.exists,
    Sym.mem_mk, Sym.coe_mk, exists_and_left, exists_prop, mem_piAntidiag, ne_eq]

Premises used: Sym.val_eq_coe, Finset.mem_sym_iff, Sym.exists, Sym.mem_mk, funext_iff, Sym.coe_mk, exists_and_left, Finset.mem_piAntidiag, exists_prop, ne_eq, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : (a : ι) → ℕ
h :
  (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
h₁ :
  (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
    ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x
⊢ (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
m : Multiset ι
hm : ∀ a ∈ m, a ∈ s
hf : ∀ (x : ι), Multiset.count x m = f x
⊢ s.sum f = m.card ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
simpa [← hf, Multiset.sum_count_eq_card hm]

Premises used: Multiset.sum_count_eq_card
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩

Premises used: And.intro, Exists.intro, HSMul.hSMul, Finset.sum
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
h : ∀ (a : ι), Membership.mem (γ := Multiset ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) a → a ∈ s
h₁ :
  Multiset.card (α := ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = s.sum f ∧
    ∀ (x : ι), Multiset.count x (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = f x
⊢ ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∀ (a : ι), Membership.mem (γ := Multiset ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) a → a ∈ s

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ Multiset.card (α := ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = s.sum f ∧
    ∀ (x : ι), Multiset.count x (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = f x

Tactic:
simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

Premises used: not_imp_comm, eq_comm, Multiset.count_sum', Multiset.count_singleton
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddMonoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 + a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 + a.2 = n
e_antidiagonal : ∀ (n : A) (xy : A × A), xy ∈ a n ↔ xy ∈ b n
⊢ { antidiagonal := a, mem_antidiagonal := @ha : HasAntidiagonal A } = { antidiagonal := b, mem_antidiagonal := @hb }

Tactic:
congr with n xy
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddMonoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 + a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 + a.2 = n
n : A
xy : A × A
e_antidiagonal : xy.1 + xy.2 = n ↔ xy ∈ b n
e_antidiagonal₁ e_antidiagonal₂ : xy.1 + xy.2 = n ↔ xy.1 + xy.2 = n
⊢ xy ∈ a n ↔ xy ∈ b n

Tactic:
rw [ha, hb]
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_2
inst : AddMonoid A
H1 H2 : HasAntidiagonal A
h : H1 = H2
⊢ Eq.{u_2 + 1} (α := A → Finset (A × A)) (@antidiagonal _ inst _) (@antidiagonal _ inst _)

Tactic:
congr!
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_2
inst : AddMonoid A
H1 H2 : HasAntidiagonal A
⊢ H1 = H2

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
n : A
xy : A × A
⊢ xy.swap ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n ↔ xy ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
n : A
x : A × A
a b : A
⊢ (a, b) ∈ map (Equiv.prodComm A A).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) ↔
    (a, b) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
n : A
⊢ map { toFun := Prod.swap, inj' := ⋯ : A × A ↪ A × A } (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) =
    @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
map_prodComm_antidiagonal

Premises used: Prod.swap, Finset.map_prodComm_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
⊢ p = q ↔ p.1 = q.1

Tactic:
⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩

Premises used: Prod.fst, congr_arg, Prod.ext, Iff.intro, Iff.mp, add_right_inj
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
refine : ∀ (h : p.1 = q.1), q.1 + p.2 = q.1 + q.2
⊢ p = q ↔ p.1 = q.1

Tactic:
refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
h : p.1 = q.1
⊢ p.1 + p.2 = n

Tactic:
rw [mem_antidiagonal] at hp hq

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
h : p.1 = q.1
hp₁ : p.1 + p.2 = n
⊢ q.1 + q.2 = n

Tactic:
rw [mem_antidiagonal] at hp hq

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
h : p.1 = q.1
hp₁ : p.1 + p.2 = n
hq₁ : q.1 + q.2 = n
⊢ p.1 = q.1

Tactic:
rw [mem_antidiagonal] at hp hq

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p.1 + p.2 = n
hq : q.1 + q.2 = n
h : p.1 = q.1
rw : q.1 + p.2 = n
rw₁ : p.1 + p.2 = n
rw₂ rw₃ : n = n
⊢ q.1 + p.2 = q.1 + q.2

Tactic:
rw [hq, ← h, hp]
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
n : A
p q : ↥(@antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n)
h : (↑p : A × A).1 = (↑q : A × A).1
⊢ p = q

Tactic:
Subtype.ext ((antidiagonal_congr p.prop q.prop).mpr h)

Premises used: Iff.mpr, Finset.antidiagonal_congr, Subtype.prop, Subtype.ext
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelCommMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
rw : p.swap = q.swap ↔ p.2 = q.2
⊢ p = q ↔ p.2 = q.2

Tactic:
rw [← Prod.swap_inj]

Premises used: Prod.swap_inj
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelCommMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ p.swap = q.swap ↔ p.2 = q.2

Tactic:
antidiagonal_congr (swap_mem_antidiagonal.2 hp) (swap_mem_antidiagonal.2 hq)

Premises used: Iff.mpr, Finset.antidiagonal_congr, Finset.swap_mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCancelCommMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ p.swap = q.swap ↔ p.2 = q.2

Tactic:
exact antidiagonal_congr (swap_mem_antidiagonal.2 hp) (swap_mem_antidiagonal.2 hq)

Premises used: Iff.mpr, Finset.antidiagonal_congr, Finset.swap_mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
h :
  ∀ (x y : A),
    Membership.mem (γ := Finset (A × A)) (@antidiagonal _ AddCommMonoid.toAddMonoid _ 0) (x, y) ↔
      Membership.mem (γ := Finset (A × A)) {(0, 0)} (x, y)
⊢ Eq (α := Finset (A × A)) (@antidiagonal _ AddCommMonoid.toAddMonoid _ 0) {(0, 0)}

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
x y : A
⊢ Membership.mem (γ := Finset (A × A)) (@antidiagonal _ AddCommMonoid.toAddMonoid _ 0) (x, y) ↔
    Membership.mem (γ := Finset (A × A)) {(0, 0)} (x, y)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
rw : ∃ (c : A), n = kl.1 + c
⊢ kl.1 ≤ n

Tactic:
rw [le_iff_exists_add]

Premises used: le_iff_exists_add
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : n = kl.1 + kl.2
⊢ ∃ (c : A), n = kl.1 + c

Tactic:
use kl.2

Premises used: Prod.snd
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.1 + kl.2
h₁ h₂ h₃ h₄ : ∀ (hlk : n = kl.1 + kl.2), n = kl.1 + kl.2
⊢ n = kl.1 + kl.2

Tactic:
rwa [mem_antidiagonal, eq_comm] at hlk

Premises used: eq_comm, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
rw : ∃ (c : A), n = kl.2 + c
⊢ kl.2 ≤ n

Tactic:
rw [le_iff_exists_add]

Premises used: le_iff_exists_add
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : n = kl.2 + kl.1
⊢ ∃ (c : A), n = kl.2 + c

Tactic:
use kl.1

Premises used: Prod.fst
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.2 + kl.1
h₁ : ∀ (hlk : n = kl.1 + kl.2), n = kl.2 + kl.1
h₂ h₃ h₄ h₅ : ∀ (hlk : n = kl.2 + kl.1), n = kl.2 + kl.1
⊢ n = kl.2 + kl.1

Tactic:
rwa [mem_antidiagonal, eq_comm, add_comm] at hlk

Premises used: eq_comm, add_comm, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
h :
  ∀ (a b : A),
    (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
      Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)
⊢ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
rw :
  (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔
    m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ Membership.mem (γ := Finset (A × A)) ∅ (a, b)
⊢ (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
    Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)

Tactic:
rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]

Premises used: Finset.mem_singleton, Prod.mk_inj, Membership.mem, apply_ite, Prod.mk, Finset.HasAntidiagonal.mem_antidiagonal, Finset.mem_filter, ite_prop_iff_or
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔
    m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ Membership.mem (γ := Finset (A × A)) ∅ (a, b)

Tactic:
simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]

Premises used: and_congr_left_iff, and_assoc, and_right_comm
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
a b : A
h : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
    Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)

Tactic:
suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
    rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n a b : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ n)
h : a + b = n → a ≤ n ∧ b = n - a
h₁ : a ≤ n ∧ b = n - a → a + b = n
⊢ a + b = n ↔ a ≤ n ∧ b = n - a

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
a b : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ a + b)
⊢ a ≤ a + b ∧ b = a + b - a

Tactic:
⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩

Premises used: le_rfl, add_tsub_cancel_left, And.intro, Eq.symm, le_add_right
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
a b : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ a + b)
⊢ a ≤ a + b ∧ b = a + b - a

Tactic:
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n a : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n

Tactic:
add_tsub_cancel_of_le h

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n a : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n

Tactic:
exact add_tsub_cancel_of_le h

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
rw :
  map { toFun := Prod.swap, inj' := ⋯ : A × A ↪ A × A }
      (filter ((fun (x : A × A) ↦ x.2 = m) ∘ (⇑{ toFun := Prod.swap, inj' := ⋯ : A × A ↪ A × A } : (a : A × A) → A × A))
        (@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) =
    if m ≤ n then {(n - m, m)} else ∅
⊢ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅

Tactic:
rw [← map_swap_antidiagonal, filter_map]

Premises used: Finset.map_swap_antidiagonal, Finset.filter_map
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
⊢ map { toFun := Prod.swap, inj' := ⋯ : A × A ↪ A × A }
      (filter ((fun (x : A × A) ↦ x.2 = m) ∘ (⇑{ toFun := Prod.swap, inj' := ⋯ : A × A ↪ A × A } : (a : A × A) → A × A))
        (@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) =
    if m ≤ n then {(n - m, m)} else ∅

Tactic:
simp [filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]

Premises used: Finset.filter_fst_eq_antidiagonal, Finset.map, apply_ite
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddMonoid A
inst_1 : HasAntidiagonal A
n k l : A
h : (k, l) ∈ @antidiagonal _ inst _ n
⊢ (k, l).1 + (k, l).2 = n

Tactic:
rw [mem_antidiagonal] at h

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddMonoid A
inst_1 : HasAntidiagonal A
n k l : A
h_1 : (k, l) ∈ @antidiagonal _ inst _ n
h : (k, l).1 + (k, l).2 = n
⊢ Eq (α := (n : A) × ↥(@antidiagonal _ inst _ n))
    ((fun (x : A × A) ↦
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) (x.1 + x.2)
            (Subtype.mk (p := fun (x_1 : A × A) ↦ x_1 ∈ @antidiagonal _ inst _ (x.1 + x.2)) x ⋯) :
          (n : A) × ↥(@antidiagonal _ inst _ n)))
      ((fun (x : (n : A) × ↥(@antidiagonal _ inst _ n)) ↦
          (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n))) : A × A))
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
          (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h_1))))
    (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
      (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h_1))

Tactic:
Sigma.subtype_ext h rfl

Premises used: Sigma.subtype_ext, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A : Type u_1
inst : AddMonoid A
inst_1 : HasAntidiagonal A
n k l : A
h_1 : (k, l) ∈ @antidiagonal _ inst _ n
h : (k, l).1 + (k, l).2 = n
⊢ Eq (α := (n : A) × ↥(@antidiagonal _ inst _ n))
    ((fun (x : A × A) ↦
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) (x.1 + x.2)
            (Subtype.mk (p := fun (x_1 : A × A) ↦ x_1 ∈ @antidiagonal _ inst _ (x.1 + x.2)) x ⋯) :
          (n : A) × ↥(@antidiagonal _ inst _ n)))
      ((fun (x : (n : A) × ↥(@antidiagonal _ inst _ n)) ↦
          (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n))) : A × A))
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
          (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h_1))))
    (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
      (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h_1))

Tactic:
exact Sigma.subtype_ext h rfl

Premises used: Sigma.subtype_ext, rfl