Theorem: MulAction.is_two_pretransitive_iff (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
have : ∀ i : Fin 2, i = 0 ∨ i = 1 := by
  rintro ⟨i, hi⟩
  by_cases hi' : i = 0
  apply Or.intro_left
  apply Fin.eq_of_val_eq
  simp only [Fin.val_zero, hi']
  apply Or.intro_right
  apply Fin.eq_of_val_eq
  simp only [Fin.val_one]
  apply Nat.eq_of_lt_succ_of_not_lt
  exact hi; simp only [lt_one_iff]; exact hi'
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
let f : ∀ (a b : α) (_ : a ≠ b), Fin 2 ↪ α := fun a b hab =>
  ⟨fun i => ite (i = 0) a b, by
    intro i j hij
    by_cases hi : i = 0
    by_cases hj : j = 0
    rw [hi, hj]
    simp only [if_pos hi, if_neg hj] at hij ; exfalso; exact hab hij
    by_cases hj : j = 0
    simp only [if_neg hi, if_pos hj] at hij ; exfalso; exact hab hij.symm
    rw [Or.resolve_left (this i) hi, Or.resolve_left (this j) hj]⟩
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 ↔ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
constructor
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 → ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ (∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d) → IsMultiplyPretransitive M α 2

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (i : Fin 2), i = 0 ∨ i = 1
Tactic:
rintro ⟨i, hi⟩
State after:
case mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

State before:
case mk
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
by_cases hi' : i = 0
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
apply Or.intro_left
State after:
case pos.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ { val := i, isLt := hi } = 0

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

State before:
case pos.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ { val := i, isLt := hi } = 0

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
apply Fin.eq_of_val_eq
State after:
case pos.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ ↑{ val := i, isLt := hi } = ↑0

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

State before:
case pos.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : i = 0
⊢ ↑{ val := i, isLt := hi } = ↑0

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
simp only [Fin.val_zero, hi']
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 0 ∨ { val := i, isLt := hi } = 1
Tactic:
apply Or.intro_right
State after:
case neg.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 1

State before:
case neg.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ { val := i, isLt := hi } = 1
Tactic:
apply Fin.eq_of_val_eq
State after:
case neg.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ↑{ val := i, isLt := hi } = ↑1

State before:
case neg.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ↑{ val := i, isLt := hi } = ↑1
Tactic:
simp only [Fin.val_one]
State after:
case neg.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ i = 1

State before:
case neg.h.a
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ i = 1
Tactic:
apply Nat.eq_of_lt_succ_of_not_lt
State after:
case neg.h.a.hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ i < 1 + 1

case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i < 1

State before:
case neg.h.a.hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ i < 1 + 1

case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i < 1
Tactic:
exact hi
State after:
case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i < 1

State before:
case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i < 1
Tactic:
simp only [lt_one_iff]
State after:
case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i = 0

State before:
case neg.h.a.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
i : ℕ
hi : i < 2
hi' : ¬i = 0
⊢ ¬i = 0
Tactic:
exact hi'
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
⊢ Function.Injective fun i => if i = 0 then a else b
Tactic:
intro i j hij
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
⊢ i = j

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
⊢ i = j
Tactic:
by_cases hi : i = 0
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
by_cases hj : j = 0
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
rw [hi, hj]
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : i = 0
hj : ¬j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
simp only [if_pos hi, if_neg hj] at hij
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : i = 0
hj : ¬j = 0
hij : a = b
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : i = 0
hj : ¬j = 0
hij : a = b
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
exfalso
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : i = 0
hj : ¬j = 0
hij : a = b
⊢ False

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : i = 0
hj : ¬j = 0
hij : a = b
⊢ False

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
exact hab hij
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j
Tactic:
by_cases hj : j = 0
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : j = 0
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j
Tactic:
simp only [if_neg hi, if_pos hj] at hij
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ i = j

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j
Tactic:
exfalso
State after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ False

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j

State before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ False

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j
Tactic:
exact hab hij.symm
State after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j

State before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
a b : α
hab : a ≠ b
i j : Fin 2
hij : (fun i => if i = 0 then a else b) i = (fun i => if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ i = j
Tactic:
rw [Or.resolve_left (this i) hi, Or.resolve_left (this j) hj]
State after:
no goals

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ IsMultiplyPretransitive M α 2 → ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
intro h
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
⊢ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
⊢ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
let h' := h.exists_smul_eq
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
Tactic:
intro a b c d hab hcd
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
⊢ ∃ m, m • a = c ∧ m • b = d

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
⊢ ∃ m, m • a = c ∧ m • b = d
Tactic:
obtain ⟨m, hm⟩ := h' (f a b hab) (f c d hcd)
State after:
case mp.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : m • f a b hab = f c d hcd
⊢ ∃ m, m • a = c ∧ m • b = d

State before:
case mp.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : m • f a b hab = f c d hcd
⊢ ∃ m, m • a = c ∧ m • b = d
Tactic:
rw [← Function.Embedding.ext_iff] at hm
State after:
case mp.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ ∃ m, m • a = c ∧ m • b = d

State before:
case mp.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ ∃ m, m • a = c ∧ m • b = d
Tactic:
use m
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • a = c ∧ m • b = d

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • a = c ∧ m • b = d
Tactic:
constructor
State after:
case h.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • a = c

case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • b = d

State before:
case h.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • a = c

case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • b = d
Tactic:
simpa only [smul_apply, coeFn_mk, eq_self_iff_true, if_true] using hm 0
State after:
case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • b = d

State before:
case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : IsMultiplyPretransitive M α 2
h' : ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
a b c d : α
hab : a ≠ b
hcd : c ≠ d
m : M
hm : ∀ (x : Fin 2), (m • f a b hab) x = (f c d hcd) x
⊢ m • b = d
Tactic:
simpa only [smul_apply, coeFn_mk, eq_self_iff_true, if_true] using hm 1
State after:
no goals

State before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
⊢ (∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d) → IsMultiplyPretransitive M α 2
Tactic:
intro h
State after:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ IsMultiplyPretransitive M α 2

State before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ IsMultiplyPretransitive M α 2
Tactic:
apply IsPretransitive.mk
State after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ ∀ (x y : Fin 2 ↪ α), ∃ g, g • x = y
Tactic:
intro u v
State after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
u v : Fin 2 ↪ α
⊢ ∃ g, g • u = v

State before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
h : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
u v : Fin 2 ↪ α
⊢ ∃ g, g • u = v
Tactic:
specialize h (u 0) (u 1) (v 0) (v 1)
State after:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v

State before:
case mpr.exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Tactic:
obtain ⟨m, hm⟩ := h
  (by rw [Ne.def, Function.Embedding.apply_eq_iff_eq]; exact zero_ne_one)
  (by rw [Ne.def, Function.Embedding.apply_eq_iff_eq]; exact zero_ne_one)
State after:
case mpr.exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v

State before:
case mpr.exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ∃ g, g • u = v
Tactic:
use m
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ m • u = v

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ m • u = v
Tactic:
ext x
State after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
⊢ (m • u) x = v x

State before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
⊢ (m • u) x = v x
Tactic:
cases' this x with hx hx
State after:
case h.h.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 0
⊢ (m • u) x = v x

case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x

State before:
case h.h.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 0
⊢ (m • u) x = v x

case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Tactic:
simpa only [hx] using hm.left
State after:
case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x

State before:
case h.h.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
m : M
hm : m • u 0 = v 0 ∧ m • u 1 = v 1
x : Fin 2
hx : x = 1
⊢ (m • u) x = v x
Tactic:
simpa only [hx] using hm.right
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ u 0 ≠ u 1
Tactic:
rw [Ne.def, Function.Embedding.apply_eq_iff_eq]
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1
Tactic:
exact zero_ne_one
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ v 0 ≠ v 1
Tactic:
rw [Ne.def, Function.Embedding.apply_eq_iff_eq]
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
this : ∀ (i : Fin 2), i = 0 ∨ i = 1
f : (a b : α) → a ≠ b → Fin 2 ↪ α := fun a b hab => { toFun := fun i => if i = 0 then a else b, inj' := ⋯ }
u v : Fin 2 ↪ α
h : u 0 ≠ u 1 → v 0 ≠ v 1 → ∃ m, m • u 0 = v 0 ∧ m • u 1 = v 1
⊢ ¬0 = 1