Theorem: Weight.dom_perm (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp w σ ≤ Weight.comp w' σ ↔ w ≤ w'
Tactic:
simp [E_perm, pair_perm']
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ (∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)) ↔
    ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' a + pair w a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ (∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)) ↔
    ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' a + pair w a
Tactic:
refine ⟨fun h a ha ↦ ?_, fun h a ha ↦ h (a.comp σ⁻¹) (testvecs_perm ha σ⁻¹)⟩
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
h : ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w ≤ E w' - pair w' a + pair w a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
h : ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w ≤ E w' - pair w' a + pair w a
Tactic:
specialize h (a.comp σ) (testvecs_perm ha σ)
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
a : Weight n d
ha : a ∈ testvecs n d
h : E w ≤ E w' - pair w' (Weight.comp (Weight.comp a σ) σ⁻¹) + pair w (Weight.comp (Weight.comp a σ) σ⁻¹)
⊢ E w ≤ E w' - pair w' a + pair w a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
a : Weight n d
ha : a ∈ testvecs n d
h : E w ≤ E w' - pair w' (Weight.comp (Weight.comp a σ) σ⁻¹) + pair w (Weight.comp (Weight.comp a σ) σ⁻¹)
⊢ E w ≤ E w' - pair w' a + pair w a
Tactic:
rwa [comp_comp, mul_right_inv, Weight.comp, Equiv.Perm.coe_one, Function.comp_id] at h
State after:
no goals