internlm/Lean-Github huggingface dataset:
Theorem: verus_lemma_mul_ordering
Proof state before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
rw [mul_comm]
Proof state after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ y * x ≥ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ y * x ≥ y
Tactic:
exact h' y x h2 h1 h3
Proof state after:
no goals
Theorem: verus_lemma_div_basics
Proof state before:
n : ℤ
h : n > 0
⊢ n / n = 1 ∧
    (-(-n / n) == 1) = true ∧
      (∀ (x : ℤ), 0 ≤ x ∧ x < n ↔ x / n = 0) ∧ (∀ (x : ℤ), (x + n) / n = x / n + 1) ∧ ∀ (x : ℤ), (x - n) / n = x / n - 1
Tactic:
sorry
Proof state after:
no goals
Theorem: verus_lemma_mul_induction
Proof state before:
f : ℤ → Bool
h1 : f 0 = true
h2 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + 1) = true
h3 : ∀ (i : ℤ), i ≤ 0 ∧ f i = true → f (i - 1) = true
⊢ ∀ (i : ℤ), f i = true
Tactic:
sorry
Proof state after:
no goals
Theorem: verus_lemma_mul_successor
Proof state before:
⊢ (∀ (x y : ℤ), (x + 1) * y = x * y + y) ∧ ∀ (x y : ℤ), (x - 1) * y = x * y - y
Tactic:
exact ⟨add_one_mul, sub_one_mul⟩
Proof state after:
no goals
Theorem: verus_lemma_mul_distributes
Proof state before:
⊢ (∀ (x y z : ℤ), (x + y) * z = x * z + y * z) ∧ ∀ (x y z : ℤ), (x - y) * z = x * z - y * z
Tactic:
exact ⟨Int.add_mul, Int.sub_mul⟩
Proof state after:
no goals
Theorem: verus_lemma_induction_helper_pos
Proof state before:
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : x ≥ 0
h2 : n > 0
h3 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h4 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h5 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
⊢ f x = true
Tactic:
sorry
Proof state after:
no goals
Theorem: verus_lemma_induction_helper_neg
Proof state before:
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : x < 0
h2 : n > 0
h3 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h4 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h5 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
⊢ f x = true
Tactic:
sorry
Proof state after:
no goals
Theorem: verus_lemma_induction_helper
Proof state before:
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
⊢ f x = true
Tactic:
by_cases h0 : x ≥ 0
Proof state after:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true

case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Theorem: verus_lemma_induction_helper
Proof state before:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true

case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
. exact verus_lemma_induction_helper_pos n f x h0 h1 h2 h3 h4
Proof state after:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Theorem: verus_lemma_induction_helper
Proof state before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
. simp only [ge_iff_le, not_le] at h0
  exact verus_lemma_induction_helper_neg n f x h0 h1 h2 h3 h4
Proof state after:
no goals
Theorem: verus_lemma_induction_helper
Proof state before:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true
Tactic:
exact verus_lemma_induction_helper_pos n f x h0 h1 h2 h3 h4
Proof state after:
no goals
Theorem: verus_lemma_induction_helper
Proof state before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
simp only [ge_iff_le, not_le] at h0
Proof state after:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x < 0
⊢ f x = true
Theorem: verus_lemma_induction_helper
Proof state before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x < 0
⊢ f x = true
Tactic:
exact verus_lemma_induction_helper_neg n f x h0 h1 h2 h3 h4
Proof state after:
no goals
Theorem: verus_lemma_small_div
Proof state before:
⊢ ∀ (x d : ℤ), 0 ≤ x ∧ x < d ∧ d > 0 → x / d = 0
Tactic:
intro x d h
Proof state after:
x d : ℤ
h : 0 ≤ x ∧ x < d ∧ d > 0
⊢ x / d = 0
Theorem: verus_lemma_small_div
Proof state before:
x d : ℤ
h : 0 ≤ x ∧ x < d ∧ d > 0
⊢ x / d = 0
Tactic:
exact Int.ediv_eq_zero_of_lt h.1 h.2.1
Proof state after:
no goals
Theorem: verus_lemma_mod_of_zero_is_zero
Proof state before:
m : ℤ
h : 0 < m
⊢ 0 % m = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: verus_lemma_0_mod_any
Proof state before:
⊢ ∀ m > 0, 0 % m = 0
Tactic:
intros
Proof state after:
m✝ : ℤ
a✝ : m✝ > 0
⊢ 0 % m✝ = 0
Theorem: verus_lemma_0_mod_any
Proof state before:
m✝ : ℤ
a✝ : m✝ > 0
⊢ 0 % m✝ = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
⊢ ↑x % ↑m = ↑x
Tactic:
have h1 : 0 ≤ (x : Int) := by simp only [Nat.cast_nonneg]
Proof state after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ ↑x % ↑m = ↑x
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ ↑x % ↑m = ↑x
Tactic:
have h2 : 0 ≤ (m : Int) := by simp only [Nat.cast_nonneg]
Proof state after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑x % ↑m = ↑x
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑x % ↑m = ↑x
Tactic:
rw [← Int.mod_eq_emod h1 h2, ← Int.ofNat_mod x m]
Proof state after:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑(x % m) = ↑x
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
h2 : 0 ≤ ↑m
⊢ ↑(x % m) = ↑x
Tactic:
exact ((fun a b => (Mathlib.Tactic.Zify.nat_cast_eq a b).mp) x (x % m) (Nat.mod_eq_of_lt h).symm).symm
Proof state after:
no goals
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
⊢ 0 ≤ ↑x
Tactic:
simp only [Nat.cast_nonneg]
Proof state after:
no goals
Theorem: verus_lemma_small_mod
Proof state before:
x m : ℕ
h : x < m
h' : 0 < m
h1 : 0 ≤ ↑x
⊢ 0 ≤ ↑m
Tactic:
simp only [Nat.cast_nonneg]
Proof state after:
no goals
Theorem: verus_lemma_mod_range
Proof state before:
x m : ℤ
h : m > 0
⊢ 0 ≤ x % m ∧ x % m < m
Tactic:
have h' : m ≠ 0 := Int.ne_of_gt h
Proof state after:
x m : ℤ
h : m > 0
h' : m ≠ 0
⊢ 0 ≤ x % m ∧ x % m < m
Theorem: verus_lemma_mod_range
Proof state before:
x m : ℤ
h : m > 0
h' : m ≠ 0
⊢ 0 ≤ x % m ∧ x % m < m
Tactic:
exact ⟨Int.emod_nonneg x h', Int.emod_lt_of_pos x h⟩
Proof state after:
no goals
Theorem: BrownCs22.Nat.quotient_remainder
Proof state before:
a b c : ℕ
h : a % b = c
⊢ ∃ q, a = q * b + c
Tactic:
use a/b
Proof state after:
case h
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c
Theorem: BrownCs22.Nat.quotient_remainder
Proof state before:
case h
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c
Tactic:
rw [← h, mul_comm, Nat.div_add_mod]
Proof state after:
no goals
Theorem: Set.ncard_pigeonhole
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ Set.Nonempty (s ∩ t)
Tactic:
rw [← compl_ne_univ]
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ (s ∩ t)ᶜ ≠ univ
Theorem: Set.ncard_pigeonhole
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ (s ∩ t)ᶜ ≠ univ
Tactic:
intro h'
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ False
Theorem: Set.ncard_pigeonhole
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ False
Tactic:
apply not_le.mpr h
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard s + ncard t ≤ Fintype.card α
Theorem: Set.ncard_pigeonhole
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard s + ncard t ≤ Fintype.card α
Tactic:
rw [← Set.ncard_union_add_ncard_inter]
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) ≤ Fintype.card α
Theorem: Set.ncard_pigeonhole
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) ≤ Fintype.card α
Tactic:
apply Nat.le_of_add_le_add_right
Proof state after:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) + ?b ≤ Fintype.card α + ?b

case b
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ℕ
Theorem: Set.ncard_pigeonhole
Proof state before:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) + ?b ≤ Fintype.card α + ?b

case b
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ℕ
Tactic:
rw [add_assoc, Set.ncard_add_ncard_compl, h', Set.ncard_univ, ← Nat.card_eq_fintype_card, add_le_add_iff_right, ← Set.ncard_univ]
Proof state after:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) ≤ ncard univ
Theorem: Set.ncard_pigeonhole
Proof state before:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) ≤ ncard univ
Tactic:
apply Set.ncard_le_ncard (subset_univ _)
Proof state after:
no goals
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Set.Nonempty (sᶜ ∩ tᶜ)
Tactic:
apply Set.ncard_pigeonhole
Proof state after:
case h
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Fintype.card α < ncard sᶜ + ncard tᶜ
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Fintype.card α < ncard sᶜ + ncard tᶜ
Tactic:
apply Nat.lt_of_add_lt_add_left
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.n + Fintype.card α < ?h.n + (ncard sᶜ + ncard tᶜ)

case h.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.n + Fintype.card α < ?h.n + (ncard sᶜ + ncard tᶜ)

case h.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Tactic:
rw [← add_assoc, Set.ncard_add_ncard_compl]
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + Fintype.card α < Nat.card α + ncard tᶜ
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + Fintype.card α < Nat.card α + ncard tᶜ
Tactic:
simp only [Nat.card_eq_fintype_card, add_comm, add_lt_add_iff_left]
Proof state after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s < ncard tᶜ
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s < ncard tᶜ
Tactic:
apply Nat.lt_of_add_lt_add_left
Proof state after:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.a.n + ncard s < ?h.a.n + ncard tᶜ

case h.a.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.a.n + ncard s < ?h.a.n + ncard tᶜ

case h.a.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl, Nat.card_eq_fintype_card, add_comm]
Proof state after:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + ncard t < Fintype.card α
Theorem: Set.ncard_pigeonhole_compl
Proof state before:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + ncard t < Fintype.card α
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.ncard_pigeonhole_compl'
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ s ∪ t ≠ ⊤
Tactic:
intro h'
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ False
Theorem: Set.ncard_pigeonhole_compl'
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ False
Tactic:
apply not_le.mpr h
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ Fintype.card α ≤ ncard s + ncard t
Theorem: Set.ncard_pigeonhole_compl'
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ Fintype.card α ≤ ncard s + ncard t
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_univ, ← top_eq_univ, ← h']
Proof state after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
Theorem: Set.ncard_pigeonhole_compl'
Proof state before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
Tactic:
exact ncard_union_le s t
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
rw [Ne.def, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne.def, ← Set.nonempty_iff_ne_empty] at ha
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : Set.Nonempty (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : Set.Nonempty (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
obtain ⟨a, ha⟩ := ha
Proof state after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have ha' : a ∈ (s ∩ g • s)ᶜ := by
  rw [Set.compl_inter]
  apply Set.mem_union_left
  rw [Set.compl_union] at ha
  apply Set.mem_of_mem_inter_left ha
Proof state after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
apply (IsPretransitive.mk_base_iff (⟨a, ha'⟩ : SubMulAction.ofFixingSubgroup G (s ∩ g • s))).mpr
Proof state after:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ ∀ (x : ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))), ∃ g_1, g_1 • { val := a, property := ha' } = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ ∀ (x : ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))), ∃ g_1, g_1 • { val := a, property := ha' } = x
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx }
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx
Proof state after:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s ∨ x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s ∨ x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
cases' hx with hx hx
Proof state after:
case intro.mk.inl
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }

case intro.mk.inr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
⊢ ∃ g_1, g_1 • { val := a, property := ha' } = { val := x, property := hx✝ }
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ
Tactic:
rw [Set.compl_inter]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ
Tactic:
apply Set.mem_union_left
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ a ∈ sᶜ
Tactic:
rw [Set.compl_union] at ha
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ
Tactic:
apply Set.mem_of_mem_inter_left ha
Proof state after:
no goals