Theorem: Finset.mulImpact_map_of_infinite (LeanCamCombi/Impact.lean)

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Infinite β := sorry
State after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this : Infinite β
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this : Infinite β
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Nonempty {t : Finset α // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
State after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝ : Infinite β
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝ : Infinite β
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Nonempty {t : Finset β // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
State after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
refine' le_antisymm _ _
State after:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ s.mulImpact n

case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s).mulImpact n

State before:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ s.mulImpact n
Tactic:
refine' le_ciInf fun t => _
State after:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ (s * ↑t).card

State before:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ (s * ↑t).card
Tactic:
sorry
State after:
no goals

State before:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s).mulImpact n
Tactic:
refine' le_ciInf fun t => _
State after:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s * ↑t).card

State before:
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s * ↑t).card
Tactic:
sorry
State after:
no goals