-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma image {F H : Type*} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F)
    (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup K (f '' A) where
  one_mem := ⟨1, hA.one_mem, map_one _⟩
  inv_eq_self

Proof state:
case intro.intro.refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F * A
⊢ ⇑f '' (A ^ 2) ⊆ ⇑f '' (↑F * A)

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ CovBySMul H K ((⇑f '' A) ^ 2) (⇑f '' A)

Tactic:
refine ⟨F.image f, ?_, ?_⟩

Result:
case intro.intro.refine_1
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ ↑(#(Finset.image (⇑f) F)) ≤ K

case intro.intro.refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ (⇑f '' A) ^ 2 ⊆ ↑(Finset.image (⇑f) F) • ⇑f '' A

Proof state:
case intro.intro.refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ (⇑f '' A) ^ 2 ⊆ ↑(Finset.image (⇑f) F) • ⇑f '' A

Tactic:
simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢

Result:
case intro.intro.refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F * A
⊢ ⇑f '' (A ^ 2) ⊆ ⇑f '' (↑F * A)

Proof state:
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ (⇑f '' A)⁻¹ = ⇑f '' A

Tactic:
simp [← Set.image_inv, hA.inv_eq_self]

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ CovBySMul H K ((⇑f '' A) ^ 2) (⇑f '' A)

Tactic:
obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul

Result:
case intro.intro
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ CovBySMul H K ((⇑f '' A) ^ 2) (⇑f '' A)

Proof state:
case intro.intro.refine_1
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ ↑(#(Finset.image (⇑f) F)) ≤ K

Tactic:
calc
  (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
  _ ≤ K := hF

Result:
no goals