Theorem: Subgroup.map_iff_mono_of_injective (Jordan/AlternatingMaximal.lean)

State before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' ↔ map f K ≤ map f K'
Tactic:
constructor
State after:
case mp
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' → map f K ≤ map f K'

case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'

State before:
case mp
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' → map f K ≤ map f K'

case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Tactic:
exact Subgroup.map_mono
State after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'

State before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Tactic:
intro h
State after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
⊢ K ≤ K'

State before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
⊢ K ≤ K'
Tactic:
intro x hx
State after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ x ∈ K'

State before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ x ∈ K'
Tactic:
suffices f x ∈ Subgroup.map f K' by
  simp only [Subgroup.mem_map] at this
  obtain ⟨y, hy, hx⟩ := this
  rw [← hf hx]; exact hy
State after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K'

State before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K'
Tactic:
apply h
State after:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K

State before:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K
Tactic:
rw [Subgroup.mem_map]
State after:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ ∃ x_1 ∈ K, f x_1 = f x

State before:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ ∃ x_1 ∈ K, f x_1 = f x
Tactic:
exact ⟨x, hx, rfl⟩
State after:
no goals

State before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : f x ∈ map f K'
⊢ x ∈ K'
Tactic:
simp only [Subgroup.mem_map] at this
State after:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : ∃ x_1 ∈ K', f x_1 = f x
⊢ x ∈ K'

State before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : ∃ x_1 ∈ K', f x_1 = f x
⊢ x ∈ K'
Tactic:
obtain ⟨y, hy, hx⟩ := this
State after:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ x ∈ K'

State before:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ x ∈ K'
Tactic:
rw [← hf hx]
State after:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ y ∈ K'

State before:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ y ∈ K'
Tactic:
exact hy
State after:
no goals