awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
rw : ¬n ≤ #t
⊢ (mulRothNumber : (a : Finset α) → ℕ) s < n

Tactic:
rw [← hcard, ← not_le]

Premises used: not_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
hn : n ≤ #t
obtain : ∀ (u : Finset α) (hut : u ⊆ t) (h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree (↑t : Set α)) (hn : #u ≤ #t), False
⊢ False

Tactic:
obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn

Premises used: Finset.exists_subset_card_eq, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
u : Finset α
hut : u ⊆ t
h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree (↑t : Set α)
hn : #u ≤ #t
⊢ False

Tactic:
h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)

Premises used: Iff.mpr, HasSubset.Subset.trans, Finset.mem_powersetCard, ThreeGPFree.mono, And.intro, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
hts : t ⊆ s
hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s
ht : ThreeGPFree (↑t : Set α)
u : Finset α
hut : u ⊆ t
h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree (↑t : Set α)
hn : #u ≤ #t
⊢ False

Tactic:
exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)

Premises used: Iff.mpr, HasSubset.Subset.trans, Finset.mem_powersetCard, ThreeGPFree.mono, And.intro, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
obtain :
  ∀ (s : Finset β) (hsB : s ⊆ B) (hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B) (hs : ThreeGPFree (↑s : Set β)),
    LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)

Tactic:
obtain ⟨s, hsB, hcard, hs⟩ := mulRothNumber_spec B

Premises used: mulRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
⊢ invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)

Tactic:
have hsA : invFunOn f A '' s ⊆ A :=
    (hf'.surjOn.mapsTo_invFunOn.mono (coe_subset.2 hsB) Subset.rfl).image_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
⊢ Set.SurjOn f (↑A : Set α) (↑s : Set β)

Tactic:
have hfsA : Set.SurjOn f A s := hf'.surjOn.mono Subset.rfl (coe_subset.2 hsB)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
rw : #(image (invFunOn f (↑A : Set α)) s) ≤ (mulRothNumber : (a : Finset α) → ℕ) A
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ)

Tactic:
rw [← hcard, ← s.card_image_of_injOn ((invFunOn_injOn_image f _).mono hfsA)]

Premises used: Function.invFunOn_injOn_image, Set.InjOn.mono, Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
⊢ #(image (invFunOn f (↑A : Set α)) s) ≤ (mulRothNumber : (a : Finset α) → ℕ) A

Tactic:
ThreeGPFree.le_mulRothNumber ?_ (mod_cast hsA)

Premises used: SetLike.coe_subset_coe._simp_1, congrArg, cast, Finset.coe_image._simp_1, ThreeGPFree.le_mulRothNumber, HasSubset.Subset, SetLike.coe, congrFun', Eq.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
refine : ThreeGPFree (↑(image (invFunOn f (↑A : Set α)) s) : Set α)
⊢ #(image (invFunOn f (↑A : Set α)) s) ≤ (mulRothNumber : (a : Finset α) → ℕ) A

Tactic:
refine ThreeGPFree.le_mulRothNumber ?_ (mod_cast hsA)

Premises used: ThreeGPFree.le_mulRothNumber
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
rw : ThreeGPFree (invFunOn f (↑A : Set α) '' (↑s : Set β))
⊢ ThreeGPFree (↑(image (invFunOn f (↑A : Set α)) s) : Set α)

Tactic:
rw [coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A : Set α) (↑B : Set β) f
hf' : Set.BijOn f (↑A : Set α) (↑B : Set β)
s : Finset β
hsB : s ⊆ B
hcard : #s = (mulRothNumber : (a : Finset β) → ℕ) B
hs : ThreeGPFree (↑s : Set β)
hsA : invFunOn f (↑A : Set α) '' (↑s : Set β) ⊆ (↑A : Set α)
hfsA : Set.SurjOn f (↑A : Set α) (↑s : Set β)
⊢ ThreeGPFree (invFunOn f (↑A : Set α) '' (↑s : Set β))

Tactic:
simpa using (hf.subset hsA hfsA.bijOn_subset.mapsTo).threeGPFree (hf'.injOn.mono hsA) hs

Premises used: Set.BijOn.injOn, Set.BijOn.mapsTo, Set.InjOn.mono, IsMulFreimanHom.subset, IsMulFreimanHom.threeGPFree, Set.SurjOn.bijOn_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)

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

Premises used: IsMulFreimanIso.bijOn, IsMulFreimanHom.mulRothNumber_mono, le_antisymm, IsMulFreimanIso.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
refine : LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)

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

Premises used: IsMulFreimanIso.bijOn, IsMulFreimanHom.mulRothNumber_mono, le_antisymm, IsMulFreimanIso.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
obtain :
  ∀ (s : Finset α) (hsA : s ⊆ A) (hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A) (hs : ThreeGPFree (↑s : Set α)),
    LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)

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

Premises used: mulRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : s ⊆ A
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
⊢ (↑s : Set α) ⊆ (↑A : Set α)

Tactic:
rw [← coe_subset] at hsA

Premises used: Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : s ⊆ A
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hsA₁ : (↑s : Set α) ⊆ (↑A : Set α)
⊢ #s = (mulRothNumber : (a : Finset α) → ℕ) A

Tactic:
rw [← coe_subset] at hsA

Premises used: Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : s ⊆ A
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hsA₁ : (↑s : Set α) ⊆ (↑A : Set α)
hcard₁ : #s = (mulRothNumber : (a : Finset α) → ℕ) A
⊢ ThreeGPFree (↑s : Set α)

Tactic:
rw [← coe_subset] at hsA

Premises used: Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
⊢ Set.InjOn f (↑s : Set α)

Tactic:
have hfs : Set.InjOn f s := hf.bijOn.injOn.mono hsA
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
⊢ ThreeGPFree (f '' (↑s : Set α))

Tactic:
have := (hf.subset hsA hfs.bijOn_image).threeGPFree_congr.1 hs
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (f '' (↑s : Set α))
⊢ ThreeGPFree (↑(image f s) : Set β)

Tactic:
rw [← coe_image] at this

Premises used: Finset.coe_image
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
rw : #(image f s) ≤ (mulRothNumber : (a : Finset β) → ℕ) B
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) A : ℕ) ((mulRothNumber : (a : Finset β) → ℕ) B : ℕ)

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

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ #(image f s) ≤ (mulRothNumber : (a : Finset β) → ℕ) B

Tactic:
this.le_mulRothNumber ?_

Premises used: ThreeGPFree.le_mulRothNumber
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
refine : image f s ⊆ B
⊢ #(image f s) ≤ (mulRothNumber : (a : Finset β) → ℕ) B

Tactic:
refine this.le_mulRothNumber ?_

Premises used: ThreeGPFree.le_mulRothNumber
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
rw : f '' (↑s : Set α) ⊆ (↑B : Set β)
⊢ image f s ⊆ B

Tactic:
rw [← coe_subset, coe_image]

Premises used: Finset.coe_image, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ f '' (↑s : Set α) ⊆ (↑B : Set β)

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

Premises used: Finset.Subset.rfl, IsMulFreimanIso.bijOn, Set.MapsTo.mono, Set.BijOn.mapsTo, Set.MapsTo.image_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : CommMonoid α
inst_2 : CommMonoid β
inst_3 : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A : Set α) (↑B : Set β) f
s : Finset α
hsA : (↑s : Set α) ⊆ (↑A : Set α)
hcard : #s = (mulRothNumber : (a : Finset α) → ℕ) A
hs : ThreeGPFree (↑s : Set α)
hfs : Set.InjOn f (↑s : Set α)
this : ThreeGPFree (↑(image f s) : Set β)
⊢ f '' (↑s : Set α) ⊆ (↑B : Set β)

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

Premises used: Finset.Subset.rfl, IsMulFreimanIso.bijOn, Set.MapsTo.mono, Set.BijOn.mapsTo, Set.MapsTo.image_subset
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
refine_1 :
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
refine_2 :
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
refine_1 :
  ∀ (u : Finset α) (hus : u ⊆ map (mulLeftEmbedding a) s)
    (hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)) (hu : ThreeGPFree (↑u : Set α)),
    LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
      ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

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

Premises used: mulRothNumber_spec, Finset.map, mulLeftEmbedding
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
⊢ ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1

Tactic:
rw [subset_map_iff] at hus

Premises used: Finset.subset_map_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
hus₁ : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
⊢ #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)

Tactic:
rw [subset_map_iff] at hus

Premises used: Finset.subset_map_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
hus₁ : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
hcard₁ : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
⊢ ThreeGPFree (↑u : Set α)

Tactic:
rw [subset_map_iff] at hus

Premises used: Finset.subset_map_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 ⊆ s, u = map (mulLeftEmbedding a) u_1
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑u : Set α)
refine_1 :
  ∀ (u : Finset α) (hus : u ⊆ s)
    (hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s))
    (hu : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)),
    LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
      ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
⊢ ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))

Tactic:
rw [coe_map] at hu

Premises used: Finset.coe_map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
refine_1 : #u ≤ (mulRothNumber : (a : Finset α) → ℕ) s
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

Tactic:
rw [← hcard, card_map]

Premises used: Finset.card_map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
⊢ #u ≤ (mulRothNumber : (a : Finset α) → ℕ) s

Tactic:
(threeGPFree_smul_set.1 hu).le_mulRothNumber hus

Premises used: ThreeGPFree.le_mulRothNumber, Iff.mp, threeGPFree_smul_set
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #(map (mulLeftEmbedding a) u) = (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)
hu : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
⊢ #u ≤ (mulRothNumber : (a : Finset α) → ℕ) s

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

Premises used: ThreeGPFree.le_mulRothNumber, Iff.mp, threeGPFree_smul_set
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
refine_2 :
  ∀ (u : Finset α) (hus : u ⊆ s) (hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s) (hu : ThreeGPFree (↑u : Set α)),
    LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)

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

Premises used: mulRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
rw : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
⊢ ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)

Tactic:
rw [coe_map]

Premises used: Finset.coe_map