-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
/-- Arithmetic progressions are preserved under 2-Freiman isos. -/
@[to_additive "Arithmetic progressions are preserved under 2-Freiman isos."]
lemma IsMulFreimanIso.mulRothNumber_congr (hf : IsMulFreimanIso 2 A B f) :
    mulRothNumber A = mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
rw [← hcard, ← Finset.card_image_of_injOn hfs]

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ #(image f s) ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : s ⊆ A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
rw [← coe_subset] at hsA

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree (f '' ↑s)
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
rw [← coe_image] at this

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
⊢ mulRothNumber A = mulRothNumber B

Tactic:
refine le_antisymm ?_ (hf.isMulFreimanHom.mulRothNumber_mono hf.bijOn)

Result:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ image f s ⊆ B

Tactic:
rw [← coe_subset, coe_image]

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ f '' ↑s ⊆ ↑B

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
obtain ⟨s, hsA, hcard, hs⟩ := mulRothNumber_spec A

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : s ⊆ A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
have := (hf.subset hsA hfs.bijOn_image).threeGPFree_congr.1 hs

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree (f '' ↑s)
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Tactic:
have hfs : Set.InjOn f s := hf.bijOn.injOn.mono hsA

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
⊢ mulRothNumber A ≤ mulRothNumber B

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ f '' ↑s ⊆ ↑B

Tactic:
exact (hf.bijOn.mapsTo.mono hsA Subset.rfl).image_subset

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ #(image f s) ≤ mulRothNumber B

Tactic:
refine this.le_mulRothNumber ?_

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ image f s ⊆ B