-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_map_mul_left :
    mulRothNumber (s.map <| mulLeftEmbedding a) = mulRothNumber s

Proof state:
case h.e'_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
h : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber s = #(map (mulLeftEmbedding a) u)

Tactic:
rw [card_map, hcard]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑u
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
rw [subset_map_iff] at hus

Result:
case refine_1.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
hcard : #u = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑u
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ ThreeGPFree ↑(map (mulLeftEmbedding a) u)

Tactic:
rw [coe_map]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)

Proof state:
case refine_2.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Tactic:
have h : ThreeGPFree (u.map <| mulLeftEmbedding a : Set α) := by rw [coe_map]; exact hu.smul_set

Result:
case refine_2.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
h : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Proof state:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ #u ≤ mulRothNumber s

Tactic:
exact (threeGPFree_smul_set.1 hu).le_mulRothNumber hus

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s.map <| mulLeftEmbedding a)

Result:
case refine_1.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑u
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Proof state:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
rw [← hcard, card_map]

Result:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ #u ≤ mulRothNumber s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) = mulRothNumber s

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Proof state:
case refine_2.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
h : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Tactic:
convert h.le_mulRothNumber (map_subset_map.2 hus) using 1

Result:
case h.e'_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
h : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber s = #(map (mulLeftEmbedding a) u)

Proof state:
case refine_1.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
hcard : #u = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑u
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
obtain ⟨u, hus, rfl⟩ := hus

Result:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Tactic:
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s

Result:
case refine_2.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Proof state:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Tactic:
rw [coe_map] at hu

Result:
case refine_1.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = mulRothNumber (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)
⊢ mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ ThreeGPFree (⇑(mulLeftEmbedding a) '' ↑u)

Tactic:
exact hu.smul_set

Result:
no goals