Theorem: ZMod.min_le_card_add' (LeanCamCombi/Archive/CauchyDavenportFromKneser.lean)

State before:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
haveI : Fact p.Prime := ⟨hp⟩
State after:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
⊢ min p (s.card + t.card - 1) ≤ (s + t).card

State before:
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
obtain h | h := eq_bot_or_eq_top (AddAction.stabilizer (ZMod p) (s + t))
State after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ min p (s.card + t.card - 1) ≤ (s + t).card

case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊤
⊢ min p (s.card + t.card - 1) ≤ (s + t).card

State before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
refine' min_le_of_right_le _
State after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ s.card + t.card - 1 ≤ (s + t).card

State before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊥
⊢ s.card + t.card - 1 ≤ (s + t).card
Tactic:
rw [← AddSubgroup.coe_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h
State after:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = 0
⊢ s.card + t.card - 1 ≤ (s + t).card

State before:
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = 0
⊢ s.card + t.card - 1 ≤ (s + t).card
Tactic:
simpa [*] using add_kneser s t
State after:
no goals

State before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : AddAction.stabilizer (ZMod p) (s + t) = ⊤
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
rw [← AddSubgroup.coe_eq_univ, ← coe_addStab (hs.add ht), coe_eq_univ] at h
State after:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).card

State before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
Tactic:
refine' card_addStab_le_card.trans' _
State after:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).addStab.card

State before:
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).addStab.card
Tactic:
simp [*, card_univ]
State after:
no goals