Theorem: MulAction.IsBlock.def (Jordan/Blocks.lean)

State before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
constructor
State after:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)

case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → IsBlock G B

State before:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro hB g g'
State after:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)

State before:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
by_cases h : g • B = g' • B
State after:
case pos
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)

case neg
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)

State before:
case pos
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
refine' Or.intro_left _ h
State after:
no goals

State before:
case neg
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_right
State after:
case neg.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ Disjoint (g • B) (g' • B)

State before:
case neg.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ Disjoint (g • B) (g' • B)
Tactic:
exact hB (Set.mem_range_self g) (Set.mem_range_self g') h
State after:
no goals

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → IsBlock G B
Tactic:
intro hB
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ IsBlock G B

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ IsBlock G B
Tactic:
unfold IsBlock
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ Set.PairwiseDisjoint (Set.range fun g => g • B) id

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ Set.PairwiseDisjoint (Set.range fun g => g • B) id
Tactic:
intro C hC C' hC'
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C : Set X
hC : C ∈ Set.range fun g => g • B
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
⊢ C ≠ C' → (Disjoint on id) C C'

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C : Set X
hC : C ∈ Set.range fun g => g • B
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
⊢ C ≠ C' → (Disjoint on id) C C'
Tactic:
obtain ⟨g, rfl⟩ := hC
State after:
case mpr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
g : G
⊢ (fun g => g • B) g ≠ C' → (Disjoint on id) ((fun g => g • B) g) C'

State before:
case mpr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
g : G
⊢ (fun g => g • B) g ≠ C' → (Disjoint on id) ((fun g => g • B) g) C'
Tactic:
obtain ⟨g', rfl⟩ := hC'
State after:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
⊢ (fun g => g • B) g ≠ (fun g => g • B) g' → (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')

State before:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
⊢ (fun g => g • B) g ≠ (fun g => g • B) g' → (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
intro hgg'
State after:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')

State before:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
cases hB g g' with
| inl h => exfalso; exact hgg' h
| inr h => exact h
State after:
no goals

State before:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
exfalso
State after:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ False

State before:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ False
Tactic:
exact hgg' h
State after:
no goals

State before:
case mpr.intro.intro.inr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : Disjoint (g • B) (g' • B)
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
exact h
State after:
no goals