Theorem: Finset.le_card_mul_add_card_mulStab_mul (LeanCamCombi/Kneser/KneserRuzsa.lean)

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
have :
  ∀ b : t,
    ∃ n s' t',
      ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card :=
  fun b => ⟨_, s, t, b.2, Subset.rfl, Subset.rfl, rfl, rfl⟩
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
choose s' t' hbt' hs' hst' hstcard ht' using fun b => Nat.find_spec (this b)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
have : s * t = univ.sup fun b => s' b * t' b := by
  refine' le_antisymm _ (Finset.sup_le_iff.2 fun _ _ => hst' _)
  exact
    mul_subset_iff_right.2 fun b hb =>
      (smul_finset_subset_smul_finset $ hs' ⟨b, hb⟩).trans $
        (op_smul_finset_subset_mul $ hbt' ⟨b, hb⟩).trans $
          @le_sup _ _ _ _ _ (fun b => s' b * t' b) _ $ mem_univ _
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card
Tactic:
rw [this]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
⊢ s.card + t.card ≤ (univ.sup fun b => s' b * t' b).card + (univ.sup fun b => s' b * t' b).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
⊢ s.card + t.card ≤ (univ.sup fun b => s' b * t' b).card + (univ.sup fun b => s' b * t' b).mulStab.card
Tactic:
refine' (le_inf' ht.attach _ fun b _ => _).trans (le_card_sup_add_card_mulStab_sup _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ s.card + t.card ≤ (s' b * t' b).card + (s' b * t' b).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ s.card + t.card ≤ (s' b * t' b).card + (s' b * t' b).mulStab.card
Tactic:
rw [← hstcard b]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ (s' b).card + (t' b).card ≤ (s' b * t' b).card + (s' b * t' b).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ (s' b).card + (t' b).card ≤ (s' b * t' b).card + (s' b * t' b).mulStab.card
Tactic:
refine'
  add_le_add (card_le_card_mul_right _ ⟨_, hbt' _⟩)
    ((card_mono $ subset_mulStab_mul_left ⟨_, hbt' _⟩).trans' _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ (t' b).card ≤ (s' b).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ (t' b).card ≤ (s' b).mulStab.card
Tactic:
rw [← card_smul_finset (b : α)⁻¹ (t' _)]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ ((↑b)⁻¹ • t' b).card ≤ (s' b).mulStab.card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ ((↑b)⁻¹ • t' b).card ≤ (s' b).mulStab.card
Tactic:
refine' card_mono ((mul_subset_left_iff $ hs.mono $ hs' _).1 _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ s' b * (↑b)⁻¹ • t' b ⊆ s' b

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ s' b * (↑b)⁻¹ • t' b ⊆ s' b
Tactic:
refine' mul_subset_iff_left.2 fun c hc => _
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ c • (↑b)⁻¹ • t' b ⊆ s' b

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ c • (↑b)⁻¹ • t' b ⊆ s' b
Tactic:
rw [← mul_smul]
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ (c * (↑b)⁻¹) • t' b ⊆ s' b

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ (c * (↑b)⁻¹) • t' b ⊆ s' b
Tactic:
refine'
  smul_finset_subset_iff.2
    (inter_eq_left.1 $ eq_of_subset_of_card_le inter_subset_left _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ (t' b).card ≤ (t' b ∩ (c * (↑b)⁻¹)⁻¹ • s' b).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ (t' b).card ≤ (t' b ∩ (c * (↑b)⁻¹)⁻¹ • s' b).card
Tactic:
rw [← ht']
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ Nat.find ⋯ ≤ (t' b ∩ (c * (↑b)⁻¹)⁻¹ • s' b).card

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ Nat.find ⋯ ≤ (t' b ∩ (c * (↑b)⁻¹)⁻¹ • s' b).card
Tactic:
refine'
  Nat.find_min' _
    ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans subset_union_left,
      (mulDysonETransform.subset _ (s' b, t' b)).trans $ hst' _,
      (mulDysonETransform.card _ _).trans $ hstcard _, rfl⟩
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ ↑b ∈ (c * (↑b)⁻¹)⁻¹ • (s' b, t' b).1

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this✝ :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
b : { x // x ∈ t }
x✝ : b ∈ t.attach
c : α
hc : c ∈ s' b
⊢ ↑b ∈ (c * (↑b)⁻¹)⁻¹ • (s' b, t' b).1
Tactic:
rwa [mem_inv_smul_finset_iff, smul_eq_mul, inv_mul_cancel_right]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ s * t = univ.sup fun b => s' b * t' b
Tactic:
refine' le_antisymm _ (Finset.sup_le_iff.2 fun _ _ => hst' _)
State after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ s * t ≤ univ.sup fun b => s' b * t' b

State before:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
s' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ s * t ≤ univ.sup fun b => s' b * t' b
Tactic:
exact
  mul_subset_iff_right.2 fun b hb =>
    (smul_finset_subset_smul_finset $ hs' ⟨b, hb⟩).trans $
      (op_smul_finset_subset_mul $ hbt' ⟨b, hb⟩).trans $
        @le_sup _ _ _ _ _ (fun b => s' b * t' b) _ $ mem_univ _
State after:
no goals