Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
⊢ IsPreprimitive M α
Tactic:
by_cases hα : Subsingleton α
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : Subsingleton α
⊢ IsPreprimitive M α

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ IsPreprimitive M α

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ IsPreprimitive M α
Tactic:
have hα' : 2 ≤ PartENat.card α := by
  rw [← PartENat.card_le_one_iff_subsingleton, not_le] at hα
  exact PartENat.coe_succ_le_iff.mpr hα
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPreprimitive M α

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPreprimitive M α
Tactic:
have : IsPretransitive M α := by
  rw [isPretransitive_iff_is_one_pretransitive]
  apply isMultiplyPretransitive_of_higher M α h2
  norm_num
  exact hα'
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ IsPreprimitive M α

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
State after:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B

State before:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
State after:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B

State before:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
cases' B.subsingleton_or_nontrivial with h h
State after:
case neg.has_trivial_blocks'.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ IsTrivialBlock B

case neg.has_trivial_blocks'.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ IsTrivialBlock B

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : Subsingleton α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.on_subsingleton
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ 2 ≤ PartENat.card α
Tactic:
rw [← PartENat.card_le_one_iff_subsingleton, not_le] at hα
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : 1 < PartENat.card α
⊢ 2 ≤ PartENat.card α

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : 1 < PartENat.card α
⊢ 2 ≤ PartENat.card α
Tactic:
exact PartENat.coe_succ_le_iff.mpr hα
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPretransitive M α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α 1

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α 1
Tactic:
apply isMultiplyPretransitive_of_higher M α h2
State after:
case hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ 1 ≤ 2

case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α

State before:
case hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ 1 ≤ 2

case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Tactic:
norm_num
State after:
case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α

State before:
case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Tactic:
exact hα'
State after:
no goals

State before:
case neg.has_trivial_blocks'.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ IsTrivialBlock B
Tactic:
left
State after:
case neg.has_trivial_blocks'.inl.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ Set.Subsingleton B

State before:
case neg.has_trivial_blocks'.inl.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ Set.Subsingleton B
Tactic:
exact h
State after:
no goals

State before:
case neg.has_trivial_blocks'.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ IsTrivialBlock B
Tactic:
right
State after:
case neg.has_trivial_blocks'.inr.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ B = ⊤

State before:
case neg.has_trivial_blocks'.inr.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ B = ⊤
Tactic:
obtain ⟨a, ha, b, hb, h⟩ := h
State after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = ⊤

State before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = ⊤
Tactic:
rw [eq_top_iff]
State after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ ⊤ ≤ B

State before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ ⊤ ≤ B
Tactic:
intro c _
State after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
⊢ c ∈ B

State before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
⊢ c ∈ B
Tactic:
by_cases h' : a = c
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ c ∈ B

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ c ∈ B
Tactic:
rw [← h']
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ a ∈ B

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ a ∈ B
Tactic:
exact ha
State after:
no goals

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
rw [IsBlock.mk_subset] at hB
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
rw [is_two_pretransitive_iff] at h2
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
obtain ⟨g, hga, hgb⟩ := h2 a b a c h h'
State after:
case neg.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ B

State before:
case neg.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ B
Tactic:
apply hB ha
State after:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ a ∈ ?m.235992 • B

case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M

State before:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ a ∈ ?m.235992 • B
Tactic:
rw [← hga]
State after:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M

State before:
case neg.intro.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ ?m.235992 • B

M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ M
Tactic:
exact Set.smul_mem_smul_set ha
State after:
no goals

State before:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ g • B
Tactic:
rw [← hgb]
State after:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B

State before:
case neg.intro.intro.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ g • b ∈ g • B
Tactic:
exact Set.smul_mem_smul_set hb
State after:
no goals