internlm/Lean-Github huggingface dataset:
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n • ↑m)|) ≥ (↑(|f ↑m|) - ↑bound) * ↑(|↑n|) - ↑bound
Tactic:
norm_cast
Proof state after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat |f ↑m| bound * ↑n - ↑bound
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat |f ↑m| bound * ↑n - ↑bound
Tactic:
rewrite [Int.abs_eq_natAbs,
         Int.subNatNat_of_le <|
           show bound ≤ |f m| from Int.ofNat_le.mp <|
           calc (bound:ℤ) ≤ bound * 2 := by linarith
                        _ ≤ f m       := Int.le_of_lt h
                        _ ≤ |f m|     := Int.le_natAbs]
Proof state after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ ↑(|f ↑m| - bound) * ↑n - ↑bound
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ ↑(|f ↑m| - bound) * ↑n - ↑bound
Tactic:
norm_cast
Proof state after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Tactic:
rewrite [Int.abs_eq_natAbs]
Proof state after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Tactic:
apply Int.le_trans (Int.subNatNat_le_sub ..)
Proof state after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑((|f ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑((|f ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)
Tactic:
exact_mod_cast h_bound.linear_growth_lower_bound n m
Proof state after:
no goals
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof state before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑bound ≤ ↑bound * 2
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
unfold Function.BddAboveOn Function.BddAboveOnBy at h
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬∃ b, ∀ {a : ℤ}, a ∈ Set.Ici 0 → toFun f a ≤ b
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬∃ b, ∀ {a : ℤ}, a ∈ Set.Ici 0 → toFun f a ≤ b
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
push_neg at h
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
let ⟨m, h_nonneg, h⟩ := h (bound * 2)
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h✝ : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
m : ℤ
h_nonneg : m ∈ Set.Ici 0
h : ↑bound * 2 < toFun f m
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h✝ : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
m : ℤ
h_nonneg : m ∈ Set.Ici 0
h : ↑bound * 2 < toFun f m
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
exact ⟨m.toNat, Int.toNat_of_nonneg h_nonneg ▸ h⟩
Proof state after:
no goals
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
⊢ toFun f n ≥ R
Tactic:
let n' := n.toNat
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
⊢ toFun f n ≥ R
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
⊢ toFun f n ≥ R
Tactic:
have : ↑n' = n :=
  Int.toNat_of_nonneg <| Int.le_trans (Int.ofNat_zero_le ..) h_ge
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
this : ↑n' = n
⊢ toFun f n ≥ R
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
this : ↑n' = n
⊢ toFun f n ≥ R
Tactic:
rewrite [←this] at h_ge ⊢
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
⊢ toFun f ↑n' ≥ R
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
⊢ toFun f ↑n' ≥ R
Tactic:
let h_ge : n' ≥ R.toNat + (m + 3) * bound := Int.ofNat_le.mp h_ge
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ toFun f ↑n' ≥ R
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ toFun f ↑n' ≥ R
Tactic:
calc f n' ≥ n' - ↑((m + 3) * bound)
              := positive_linear_growth_of_large_enough_value h_a h n'
        _ ≥ ↑(R.toNat + (m + 3) * bound) - ↑((m + 3) * bound)
              := Int.sub_le_sub_right (c := _) <| Int.ofNat_le.mpr h_ge
        _ ≥ R.toNat := by custom_zify; linarith
        _ ≥ R       := Int.self_le_toNat ..
Proof state after:
no goals
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R + (m + 3) * bound) - ↑((m + 3) * bound) ≥ ↑(Int.toNat R)
Tactic:
custom_zify
Proof state after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R) + (↑m + (1 + 1 + 1)) * ↑bound - (↑m + (1 + 1 + 1)) * ↑bound ≥ ↑(Int.toNat R)
Theorem: AlmostHom.diverges_nonneg_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R) + (↑m + (1 + 1 + 1)) * ↑bound - (↑m + (1 + 1 + 1)) * ↑bound ≥ ↑(Int.toNat R)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostHom.diverges_nonpos_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f n - -toFun f (-n) ≤ ↑bound
Tactic:
conv in f n => rw [←neg_neg n]
Proof state after:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f (- -n) - -toFun f (-n) ≤ ↑bound
Theorem: AlmostHom.diverges_nonpos_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f (- -n) - -toFun f (-n) ≤ ↑bound
Tactic:
exact Int.le_trans (Int.le_natAbs ..) (Int.ofNat_le.mpr <| h_a (-n))
Proof state after:
no goals
Theorem: AlmostHom.diverges_nonpos_of_nonneg_of_not_bddAbove_on_nonneg
Proof state before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
this : toFun f n - -toFun f (-n) ≤ ↑bound
⊢ toFun f n ≤ R
Tactic:
linarith [this, h (-n) (Int.le_neg_of_le_neg h_le)]
Proof state after:
no goals
Theorem: AlmostHom.nonneg_total_integers
Proof state before:
G : Type ?u.74532
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ 0
a b : ℕ
h' : ∀ (n : ℤ), |toFun f n| ≤ a * |n| + b
n : ℤ
h_nonneg : n ≥ 0
h_comp : ¬n ≥ ↑N
⊢ n ≤ ↑N
Tactic:
linarith [h_comp]
Proof state after:
no goals
Theorem: liftedSet.index_mem
Proof state before:
F α : Type
x : α
ρ : SPL.Config F
s : vset F α
⊢ (x ∈ s | ρ) = ((x, ρ) ∈ s)
Tactic:
simp [vset.Variational, Set.mem_def]
Proof state after:
no goals
Theorem: liftedSet.fun_comp_correct
Proof state before:
⊢ (∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ) →
    (∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ) →
      ∀ (a : vset F α) (ρ : SPL.Config F), (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ
Tactic:
intros h₁ h₂ a ρ
Proof state after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ
Theorem: liftedSet.fun_comp_correct
Proof state before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ
Tactic:
simp
Proof state after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁ (a | ρ)) = f₂' (f₁' a) | ρ
Theorem: liftedSet.fun_comp_correct
Proof state before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁ (a | ρ)) = f₂' (f₁' a) | ρ
Tactic:
rw [h₁]
Proof state after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁' a | ρ) = f₂' (f₁' a) | ρ
Theorem: liftedSet.fun_comp_correct
Proof state before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁' a | ρ) = f₂' (f₁' a) | ρ
Tactic:
rw [←h₂]
Proof state after:
no goals
Theorem: liftedSet.index_union
Proof state before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ ((s₁ | ρ) ∪ s₂ | ρ) = (s₁ ∪ s₂) | ρ
Tactic:
simp [Set.union_def]
Proof state after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a ∈ s₁ | ρ) ∨ a ∈ s₂ | ρ} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Theorem: liftedSet.index_union
Proof state before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a ∈ s₁ | ρ) ∨ a ∈ s₂ | ρ} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Tactic:
simp [index_mem]
Proof state after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Theorem: liftedSet.index_union
Proof state before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Tactic:
simp [vset.Variational]
Proof state after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = vset.index {a | a ∈ s₁ ∨ a ∈ s₂} ρ
Theorem: liftedSet.index_union
Proof state before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = vset.index {a | a ∈ s₁ ∨ a ∈ s₂} ρ
Tactic:
unfold vset.index
Proof state after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = fun x => {a | a ∈ s₁ ∨ a ∈ s₂} (x, ρ)
Theorem: liftedSet.index_union
Proof state before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = fun x => {a | a ∈ s₁ ∨ a ∈ s₂} (x, ρ)
Tactic:
simp [vset.index, Set.union, Set.union_def, Set.mem_def, setOf]
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof state before:
F : Type
p : ConfigPartition
pc : PC F
⊢ disjointPCs (Set.split (PC F) p.pcs fun p => (pc &&& p, ~~~pc &&& p))
Tactic:
simp[disjointPCs, Set.split]
Proof state after:
F : Type
p : ConfigPartition
pc : PC F
⊢ ∀ (c : Config F) (a : PC F),
    ((∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a) →
      ∀ (a_1 : PC F), ((∃ x ∈ p.pcs, pc &&& x = a_1) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a_1) → c ∈ ⦃a⦄ → c ∈ ⦃a_1⦄ → a = a_1
Theorem: SPL.splitDisjoint
Proof state before:
F : Type
p : ConfigPartition
pc : PC F
⊢ ∀ (c : Config F) (a : PC F),
    ((∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a) →
      ∀ (a_1 : PC F), ((∃ x ∈ p.pcs, pc &&& x = a_1) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a_1) → c ∈ ⦃a⦄ → c ∈ ⦃a_1⦄ → a = a_1
Tactic:
intros c a h₀ b h₁ h₂ h₃
Proof state after:
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ a = b
Theorem: SPL.splitDisjoint
Proof state before:
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ a = b
Tactic:
apply Or.elim h₀
Proof state after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b

case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Theorem: SPL.splitDisjoint
Proof state before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b

case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Tactic:
{
    intros h₄
    apply Exists.elim h₄
    intros x h₅
    simp [←h₅.right, semantics] at h₂
    apply Or.elim h₁
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
        simp at h₈
        simp[←h₅.right, ←h₇.right, h₈]
    }
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        apply Not.elim h₃.left h₂.left
    }
}
Proof state after:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Theorem: SPL.splitDisjoint
Proof state before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Tactic:
{
    intros h₄
    apply Exists.elim h₄
    intros x h₅
    simp [←h₅.right, semantics] at h₂
    apply Or.elim h₁
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        apply Not.elim h₂.left h₃.left
    }
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
        simp at h₈
        simp[←h₅.right, ←h₇.right, h₈]
    }
}
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof state before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b
Tactic:
intros h₄
Proof state after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ a = b
Theorem: SPL.splitDisjoint
Proof state before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ a = b
Tactic:
apply Exists.elim h₄
Proof state after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = a → a = b
Theorem: SPL.splitDisjoint
Proof state before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = a → a = b
Tactic:
intros x h₅
Proof state after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
⊢ a = b
Theorem: SPL.splitDisjoint
Proof state before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
⊢ a = b
Tactic:
simp [←h₅.right, semantics] at h₂
Proof state after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ a = b