internlm/Lean-Github huggingface dataset:
Theorem: inversions_comp
Proof state before:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
cases' (le_of_not_lt h).eq_or_lt with h' h'
Proof state after:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [h', not_mem_inversions_diag]
Proof state after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
  exact this f g _ _ h'
Proof state after:
no goals
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [h', not_mem_inversions_diag]
Proof state after:
no goals
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
Proof state after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f
Tactic:
exact this f g _ _ h'
Proof state after:
no goals
Theorem: inversions_comp
Proof state before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
Proof state after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [mem_inversions', Set.mem_symmDiff, h, hgab, hgab.not_le]
Proof state after:
no goals
Theorem: inversions_comp
Proof state before:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [mem_inversions', Set.mem_symmDiff, h, hgba, hgba.not_lt]
Proof state after:
no goals
Theorem: mem_stdinversions
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
p : α × α
⊢ p ∈ StdInversions g ↔ p.1 < p.2 ∧ g p.2 ≤ g p.1
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_stdinversions'
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ StdInversions g ↔ a < b ∧ g b ≤ g a
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_stdinversions''
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ StdInversions g ↔ a < b ∧ g b < g a
Tactic:
rw [mem_stdinversions']
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Theorem: mem_stdinversions''
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
by_cases h : a = b
Proof state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a

case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Theorem: mem_stdinversions''
Proof state before:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a

case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
. simp [h]
Proof state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Theorem: mem_stdinversions''
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
. have h' : g a ≠ g b := fun hg => h (g.injective hg)
  simp [h, h'.symm.le_iff_lt]
Proof state after:
no goals
Theorem: mem_stdinversions''
Proof state before:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
simp [h]
Proof state after:
no goals
Theorem: mem_stdinversions''
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
have h' : g a ≠ g b := fun hg => h (g.injective hg)
Proof state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
h' : g a ≠ g b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Theorem: mem_stdinversions''
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : ¬a = b
h' : g a ≠ g b
⊢ a < b ∧ g b ≤ g a ↔ a < b ∧ g b < g a
Tactic:
simp [h, h'.symm.le_iff_lt]
Proof state after:
no goals
Theorem: not_mem_stdinversions_diag
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a : α
⊢ (a, a) ∉ StdInversions g
Tactic:
simp [mem_stdinversions']
Proof state after:
no goals
Theorem: stdinversions_inversions
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
⊢ Inversions g = StdInversions g ∪ Prod.swap ⁻¹' StdInversions g
Tactic:
ext ⟨a, b⟩
Proof state after:
case h.mk
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∪ Prod.swap ⁻¹' StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case h.mk
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∪ Prod.swap ⁻¹' StdInversions g
Tactic:
simp only [Set.mem_union, Set.mem_preimage, Prod.swap_prod_mk]
Proof state after:
case h.mk
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case h.mk
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
by_cases hab : a = b
Proof state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g

case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g

case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
. subst b
  simp [not_mem_stdinversions_diag, not_mem_inversions_diag]
Proof state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
. push_neg at hab
  obtain (hab | hba) := hab.lt_or_lt
  . simp [mem_stdinversions', mem_inversions, hab, hab.not_lt]
  . rw [mem_inversions_symm]
    simp [mem_stdinversions', mem_inversions, hba, hba.not_lt]
Proof state after:
no goals
Theorem: stdinversions_inversions
Proof state before:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
subst b
Proof state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a : α
⊢ (a, a) ∈ Inversions g ↔ (a, a) ∈ StdInversions g ∨ (a, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case pos
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a : α
⊢ (a, a) ∈ Inversions g ↔ (a, a) ∈ StdInversions g ∨ (a, a) ∈ StdInversions g
Tactic:
simp [not_mem_stdinversions_diag, not_mem_inversions_diag]
Proof state after:
no goals
Theorem: stdinversions_inversions
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬a = b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
push_neg at hab
Proof state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case neg
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
obtain (hab | hba) := hab.lt_or_lt
Proof state after:
case neg.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g

case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case neg.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g

case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
. simp [mem_stdinversions', mem_inversions, hab, hab.not_lt]
Proof state after:
case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
. rw [mem_inversions_symm]
  simp [mem_stdinversions', mem_inversions, hba, hba.not_lt]
Proof state after:
no goals
Theorem: stdinversions_inversions
Proof state before:
case neg.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
simp [mem_stdinversions', mem_inversions, hab, hab.not_lt]
Proof state after:
no goals
Theorem: stdinversions_inversions
Proof state before:
case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (a, b) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
rw [mem_inversions_symm]
Proof state after:
case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (b, a) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Theorem: stdinversions_inversions
Proof state before:
case neg.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a ≠ b
hba : b < a
⊢ (b, a) ∈ Inversions g ↔ (a, b) ∈ StdInversions g ∨ (b, a) ∈ StdInversions g
Tactic:
simp [mem_stdinversions', mem_inversions, hba, hba.not_lt]
Proof state after:
no goals
Theorem: perm_conj
Proof state before:
α : Type u_1
f g : Equiv.Perm α
a b : α
hab : f a = b
⊢ g (f (g.symm (g a))) = g b
Tactic:
rw [Equiv.symm_apply_apply, hab]
Proof state after:
no goals
Theorem: swap_conj
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap ((Equiv.swap a b) c) ((Equiv.swap a b) d)
Tactic:
rw [Equiv.swap_apply_apply]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap a b * Equiv.swap c d * (Equiv.swap a b)⁻¹
Theorem: swap_conj
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
a b c d : α
⊢ Equiv.swap a b * Equiv.swap c d * Equiv.swap a b = Equiv.swap a b * Equiv.swap c d * (Equiv.swap a b)⁻¹
Tactic:
rfl
Proof state after:
no goals
Theorem: inversions_mul
Proof state before:
f g : Equiv.Perm ℕ
⊢ Inversions (f * g) = Prod.map ⇑g.symm ⇑g.symm '' Inversions f ∩ Inversions g
Tactic:
sorry
Proof state after:
no goals
Theorem: truncate_apply_of_le
Proof state before:
f : ℕ → ℕ
n x : ℕ
hx : n ≤ x
⊢ ¬x < n
Tactic:
simpa
Proof state after:
no goals
Theorem: card_lehmer_eq_factorial
Proof state before:
n : ℕ
⊢ Fintype.card { g // ⇑g ≤ ⇑(truncate id n) } = n !
Tactic:
rw [Fintype.card_of_bijective (le_truncate_equiv_prod_fin _ _).bijective]
Proof state after:
n : ℕ
⊢ Fintype.card ((i : Fin n) → Fin (id ↑i + 1)) = n !
Theorem: card_lehmer_eq_factorial
Proof state before:
n : ℕ
⊢ Fintype.card ((i : Fin n) → Fin (id ↑i + 1)) = n !
Tactic:
simp only [id_eq, Fintype.card_pi, Fintype.card_fin]
Proof state after:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = n !
Theorem: card_lehmer_eq_factorial
Proof state before:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = n !
Tactic:
rw [← Finset.prod_range_add_one_eq_factorial n]
Proof state after:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = Finset.prod (Finset.range n) fun x => x + 1
Theorem: card_lehmer_eq_factorial
Proof state before:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = Finset.prod (Finset.range n) fun x => x + 1
Tactic:
exact Fin.prod_univ_eq_prod_range Nat.succ n
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
apply le_antisymm ?right ?left
Proof state after:
case right
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' ≤ 0

case left
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'
Tactic:
case left =>
  sorry
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' ≤ 0
Tactic:
have hf : Tendsto (fun x ↦ (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f') := by
  rw [hasDerivAt_iff_tendsto_slope] at hf
  apply hf.mono_left (nhds_right'_le_nhds_ne a)
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ f' ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ f' ≤ 0
Tactic:
suffices ∀ᶠ x in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0 from le_of_tendsto hf this
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
have ha : ∀ᶠ x in 𝓝[>] a, a < x := eventually_nhdsWithin_of_forall fun x hx ↦ hx
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
have h : ∀ᶠ x in 𝓝[>] a, f x ≤ f a := h.filter_mono nhdsWithin_le_nhds
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, (f x - f a) / (x - a) ≤ 0
Tactic:
filter_upwards [ha, h]
Proof state after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ (a_1 : ℝ), a < a_1 → f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
⊢ ∀ (a_1 : ℝ), a < a_1 → f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≤ 0
Tactic:
intro x ha h
Proof state after:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≤ 0
Tactic:
apply div_nonpos_of_nonpos_of_nonneg
Proof state after:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ f x - f a ≤ 0

case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ 0 ≤ x - a
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
Tactic:
rw [hasDerivAt_iff_tendsto_slope] at hf
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
Tactic:
apply hf.mono_left (nhds_right'_le_nhds_ne a)
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ f x - f a ≤ 0
Tactic:
linarith only [h]
Proof state after:
no goals