internlm/Lean-Github huggingface dataset:
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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']
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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]
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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]
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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'
Proof state after:
no goals
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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]
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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]
Proof state after:
no goals
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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)
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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
Theorem: MulAction.is_two_pretransitive_iff
Proof 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
Proof 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