Theorem: SubMulAction.image_inclusion (Jordan/SubMulActions.lean)

State before:
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
⊢ Set.range ⇑(inclusion s) = s.carrier
Tactic:
ext a
State after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ Set.range ⇑(inclusion s) ↔ a ∈ s.carrier

State before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ Set.range ⇑(inclusion s) ↔ a ∈ s.carrier
Tactic:
simp only [Set.mem_range, Subtype.exists, mem_carrier, SetLike.mem_coe]
State after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) ↔ a ∈ s

State before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) ↔ a ∈ s
Tactic:
constructor
State after:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) → a ∈ s

case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ s → ∃ a_2, ∃ (b : a_2 ∈ s), (inclusion s) { val := a_2, property := b } = a

State before:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ (∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a) → a ∈ s
Tactic:
intro ha
State after:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
⊢ a ∈ s

State before:
case h.mp
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
⊢ a ∈ s
Tactic:
obtain ⟨a, h, rfl⟩ := ha
State after:
case h.mp.intro.intro
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } ∈ s

State before:
case h.mp.intro.intro
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } ∈ s
Tactic:
exact h
State after:
no goals

State before:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
⊢ a ∈ s → ∃ a_2, ∃ (b : a_2 ∈ s), (inclusion s) { val := a_2, property := b } = a
Tactic:
intro h
State after:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a

State before:
case h.mpr
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), (inclusion s) { val := a_1, property := b } = a
Tactic:
use a
State after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ (b : a ∈ s), (inclusion s) { val := a, property := b } = a

State before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ ∃ (b : a ∈ s), (inclusion s) { val := a, property := b } = a
Tactic:
use h
State after:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } = a

State before:
case h
M : Type u_1
N : Type ?u.2410
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
h : a ∈ s
⊢ (inclusion s) { val := a, property := h } = a
Tactic:
rfl
State after:
no goals