-- Mathlib/GroupTheory/GroupAction/Pointwise.lean
theorem preimage_smul_setₛₗ'
    (hc : Function.Surjective (fun (m : M) ↦ c • m))
    (hc' : Function.Injective (fun (n : N) ↦ σ c • n)) :
    h ⁻¹' (σ c • t) = c • h ⁻¹' t

Proof state:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = σ c • h m'
⊢ n ∈ t

Tactic:
exact hn

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
⊢ ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
⊢ ⇑h ⁻¹' (σ c • t) ≤ c • ⇑h ⁻¹' t

case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
⊢ c • ⇑h ⁻¹' t ≤ ⇑h ⁻¹' (σ c • t)

Proof state:
case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
⊢ ⇑h ⁻¹' (σ c • t) ≤ c • ⇑h ⁻¹' t

Tactic:
intro m

Result:
case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m : M
⊢ m ∈ ⇑h ⁻¹' (σ c • t) → m ∈ c • ⇑h ⁻¹' t

Proof state:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = h ((fun m => c • m) m')
⊢ m' ∈ ⇑h ⁻¹' t

Tactic:
rw [map_smulₛₗ] at hn'

Result:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = σ c • h m'
⊢ m' ∈ ⇑h ⁻¹' t

Proof state:
case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
⊢ c • ⇑h ⁻¹' t ≤ ⇑h ⁻¹' (σ c • t)

Tactic:
exact smul_preimage_set_leₛₗ M N σ h c t

Result:
no goals

Proof state:
case a
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m : M
⊢ m ∈ ⇑h ⁻¹' (σ c • t) → m ∈ c • ⇑h ⁻¹' t

Tactic:
obtain ⟨m', rfl⟩ := hc m

Result:
case a.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
⊢ (fun m => c • m) m' ∈ ⇑h ⁻¹' (σ c • t) → (fun m => c • m) m' ∈ c • ⇑h ⁻¹' t

Proof state:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = h ((fun m => c • m) m')
⊢ (fun m => c • m) m' ∈ c • ⇑h ⁻¹' t

Tactic:
refine ⟨m', ?_, rfl⟩

Result:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = h ((fun m => c • m) m')
⊢ m' ∈ ⇑h ⁻¹' t

Proof state:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = σ c • h m'
⊢ m' ∈ ⇑h ⁻¹' t

Tactic:
rw [mem_preimage, ← hc' hn']

Result:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = σ c • h m'
⊢ n ∈ t

Proof state:
case a.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
⊢ (fun m => c • m) m' ∈ ⇑h ⁻¹' (σ c • t) → (fun m => c • m) m' ∈ c • ⇑h ⁻¹' t

Tactic:
rintro ⟨n, hn, hn'⟩

Result:
case a.intro.intro.intro
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : Function.Surjective fun m => c • m
hc' : Function.Injective fun n => σ c • n
m' : M
n : N
hn : n ∈ t
hn' : (fun x => σ c • x) n = h ((fun m => c • m) m')
⊢ (fun m => c • m) m' ∈ c • ⇑h ⁻¹' t