awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hA : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
hA₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ Eq.{u_1 + 1} (α := R) (∑ i : n, (M *ᵥ x) i) (∑ i : n, x i)

Tactic:
apply sum_mulVec_of_mem_colStochastic

Premises used: Matrix.sum_mulVec_of_mem_colStochastic
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hA : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
constructor :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
mpr :
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M'
⊢ (∀ (i j : n), 0 ≤ M' i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M' i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M' i j) 1

Tactic:
rw [mem_doublyStochastic_iff_sum] at hM'

Premises used: mem_doublyStochastic_iff_sum
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' :
  (∀ (i j : n), 0 ≤ M' i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M' i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M' i j) 1
simp : (∀ (i j : n), 0 ≤ s * M' i j) ∧ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s

Tactic:
simp only [smul_apply, smul_eq_mul, ← mul_sum]

Premises used: Finset.mul_sum, Matrix.smul_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' :
  (∀ (i j : n), 0 ≤ M' i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M' i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M' i j) 1
⊢ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s

Tactic:
simp [hM']
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' :
  (∀ (i j : n), 0 ≤ M' i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M' i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M' i j) 1
⊢ (∀ (i j : n), 0 ≤ s * M' i j) ∧ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s

Tactic:
exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩

Premises used: Finset.mul_sum, mem_doublyStochastic_iff_sum, Matrix.smul_apply, smul_eq_mul, rfl
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
rcases :
  ∀ (hs : LE.le.{u_1} (α := R) 0 0),
    ((∀ (i j : n), 0 ≤ M i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
      ∃ (M' : Matrix n n R),
        Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
mpr :
  ∀ (hs : 0 < s),
    ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
      ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
simp :
  (∀ (i j : n), 0 ≤ M i j) →
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) →
      (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
        (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧
      (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
    ∃ (M' : Matrix n n R),
      Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'

Tactic:
simp only [zero_smul, exists_and_right, and_imp]

Premises used: and_imp, exists_and_right, zero_smul
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
_ :
  (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
    (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0
⊢ (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
    (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0

Tactic:
_
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
⊢ (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0

Tactic:
⟨⟨1, Submonoid.one_mem _⟩, ?_⟩

Premises used: Submonoid.one_mem, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
refine : M = 0
⊢ (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0

Tactic:
refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
a : ∀ (i j : n), M i j = 0 i j
⊢ M = 0

Tactic:
ext i j
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
i j : n
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0

Tactic:
specialize h₂ i
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
i j : n
h₂ : Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
⊢ ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → 0 ≤ M i i_1

Tactic:
simp [h₁ i]
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
i j : n
h₂ : Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
⊢ ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → M i i_1 = 0

Tactic:
rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂

Premises used: Finset.sum_eq_zero_iff_of_nonneg
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
i j : n
h₂ : ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → M i i_1 = 0
⊢ Membership.mem (γ := Finset n) univ j

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0
i j : n
h₂ : ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → M i i_1 = 0
⊢ M i j = 0 i j

Tactic:
exact h₂ _ (by simp)
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hs : LE.le.{u_1} (α := R) 0 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧
      (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
    ∃ (M' : Matrix n n R),
      Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'

Tactic:
case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)

Premises used: and_imp, Finset.sum_eq_zero_iff_of_nonneg, exists_and_right, zero_smul
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs_1 : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j : n, M i j = s
hM₃ : ∀ (j : n), ∑ i : n, M i j = s
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) (s⁻¹ • M) ∧ M = s • s⁻¹ • M

Tactic:
simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]

Premises used: Finset.mul_sum, mem_doublyStochastic_iff_sum, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs_1 : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j : n, M i j = s
hM₃ : ∀ (j : n), ∑ i : n, M i j = s
⊢ ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'

Tactic:
exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
case :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
mpr mpr₁ :
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
case₁ :
  ∀ (hs : LE.le.{u_1} (α := R) 0 0),
    ((∀ (i j : n), 0 ≤ M i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
      ∃ (M' : Matrix n n R),
        Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
mpr₂ mpr₃ :
  ∀ (hs : 0 < s),
    ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
      ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
mpr₄ :
  ∀ (hs : 0 < s) (hM₁ : ∀ (i j : n), 0 ≤ M i j) (hM₂ : ∀ (i : n), ∑ j : n, M i j = s)
    (hM₃ : ∀ (j : n), ∑ i : n, M i j = s),
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

Tactic:
classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩

Premises used: Finset.mul_sum, mem_doublyStochastic_iff_sum, and_imp, Finset.sum_eq_zero_iff_of_nonneg, Matrix.smul_apply, exists_and_right, eq_or_lt_of_le, zero_smul, smul_eq_mul, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s : Set E
E' : Type u_3
F : Type u_4
inst_2 : SMul 𝕜 E'
inst_3 : FunLike F E E'
inst_4 : MulActionHomClass F 𝕜 E E'
f : F
t : Set E'
h : MapsTo (⇑f : (a : E) → E') s t
x : E
⊢ egauge 𝕜 t ((f : (a : E) → E') x) ≤ egauge 𝕜 s x

Tactic:
iInf_mono fun c ↦ iInf_mono' fun hc ↦ ⟨h.smul_set c hc, le_rfl⟩

Premises used: le_rfl, iInf_mono, Set.MapsTo.smul_set, Exists.intro, egauge, iInf_mono'
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s t : Set E
h : s ⊆ t
x : E
⊢ egauge 𝕜 t x ≤ egauge 𝕜 s x

Tactic:
MapsTo.egauge_le _ (MulActionHom.id ..) h _

Premises used: MulActionHom.id, Set.MapsTo.egauge_le
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
x : E
⊢ egauge 𝕜 ∅ x = ∞

Tactic:
simp [egauge]

Premises used: egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
c : 𝕜
s : Set E
x : E
h : x ∈ c • s
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ

Tactic:
iInf₂_le c h

Premises used: iInf₂_le, egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s : Set E
x : E
r : ℝ≥0∞
⊢ r ≤ egauge 𝕜 s x ↔ ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ

Tactic:
le_iInf₂_iff

Premises used: le_iInf₂_iff, egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s : Set E
x : E
⊢ egauge 𝕜 s x = ∞ ↔ ∀ (c : 𝕜), x ∉ c • s

Tactic:
simp [egauge]

Premises used: egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s : Set E
x : E
r : ℝ≥0∞
⊢ egauge 𝕜 s x < r ↔ ∃ (c : 𝕜), x ∈ c • s ∧ ‖c‖ₑ < r

Tactic:
simp [egauge, iInf_lt_iff]

Premises used: iInf_lt_iff, egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s t : Set E
x : E
⊢ Eq (α := ℝ≥0∞) (⨅ (c : 𝕜), ⨅ (_ : x ∈ c • (s ∪ t)), ‖c‖ₑ)
    (min (⨅ (c : 𝕜), ⨅ (_ : x ∈ c • s), ‖c‖ₑ) (⨅ (c : 𝕜), ⨅ (_ : x ∈ c • t), ‖c‖ₑ))

Tactic:
simp [smul_set_union, iInf_or, iInf_inf_eq]

Premises used: Set.smul_set_union, iInf_or, iInf_inf_eq
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
s t : Set E
x : E
⊢ max (egauge 𝕜 s x) (egauge 𝕜 t x) ≤ egauge 𝕜 (s ∩ t) x

Tactic:
max_le (egauge_anti _ inter_subset_left _) (egauge_anti _ inter_subset_right _)

Premises used: Set.inter_subset_left, max_le, egauge_anti, Set.inter_subset_right
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
ι : Type u_3
E : ι → Type u_4
inst_1 : (i : ι) → SMul.{u_1, u_4} 𝕜 (E i)
I : Set ι
i : ι
hi : i ∈ I
s : (i : ι) → Set (E i)
x_1 x : (i : ι) → E i
hx : x ∈ I.pi (α := E) s
⊢ Membership.mem (α := E i) (s i) ((Pi.evalMulActionHom (X := E) i : (a : (i : ι) → E i) → E i) x : E i)

Tactic:
hx i hi

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
ι : Type u_3
E : ι → Type u_4
inst_1 : (i : ι) → SMul.{u_1, u_4} 𝕜 (E i)
I : Set ι
i : ι
hi : i ∈ I
s : (i : ι) → Set (E i)
x_1 x : (i : ι) → E i
hx : x ∈ I.pi (α := E) s
⊢ Membership.mem (α := E i) (s i) ((Pi.evalMulActionHom (X := E) i : (a : (i : ι) → E i) → E i) x : E i)

Tactic:
exact hx i hi
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
E : Type u_2
inst_1 : SMul 𝕜 E
F : Type u_3
inst_2 : SMul 𝕜 F
s : Set E
t : Set F
a : E
b : F
⊢ max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b)

Tactic:
max_le (mapsTo_fst_prod.egauge_le 𝕜 (MulActionHom.fst 𝕜 E F) (a, b))
    (MapsTo.egauge_le 𝕜 (MulActionHom.snd 𝕜 E F) mapsTo_snd_prod (a, b))

Premises used: MulActionHom.fst, Prod.mk, Set.MapsTo.egauge_le, max_le, Set.mapsTo_fst_prod, Set.mapsTo_snd_prod, MulActionHom.snd
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NNNorm 𝕜
inst_1 : Nonempty 𝕜
E : Type u_2
inst_2 : Zero E
inst_3 : SMulZeroClass 𝕜 E
x : E
⊢ egauge 𝕜 0 x = ∞ ↔ x ≠ 0

Tactic:
simp [egauge_eq_top]

Premises used: egauge_eq_top
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
rw : egauge 𝕜 s x ≤ (↑‖c⁻¹‖₊ : ℝ≥0∞)
⊢ egauge 𝕜 s x ≤ (↑‖c‖₊⁻¹ : ℝ≥0∞)

Tactic:
rw [← nnnorm_inv]

Premises used: nnnorm_inv
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑‖c⁻¹‖₊ : ℝ≥0∞)

Tactic:
egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

Premises used: Iff.mpr, Set.mem_inv_smul_set_iff₀, egauge_le_of_mem_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑‖c⁻¹‖₊ : ℝ≥0∞)

Tactic:
exact egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

Premises used: Iff.mpr, Set.mem_inv_smul_set_iff₀, egauge_le_of_mem_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
inl : ∀ (h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x ∈ s), egauge 𝕜 s x ≤ (enorm.{u_1} (E := 𝕜) 0)⁻¹
inr : ∀ (hc : c ≠ 0), egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x ∈ s
⊢ egauge 𝕜 s x ≤ (enorm.{u_1} (E := 𝕜) 0)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
(egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

Premises used: ENNReal.coe_inv_le, LE.le.trans, egauge_le_of_smul_mem_of_ne
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
exact (egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

Premises used: ENNReal.coe_inv_le, LE.le.trans, egauge_le_of_smul_mem_of_ne
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
hs : Balanced 𝕜 s
hc : egauge 𝕜 s x < ‖c‖ₑ
a : 𝕜
hxa : x ∈ a • s
ha : ‖a‖ₑ < ‖c‖ₑ
⊢ ‖a‖ ≤ ‖c‖

Tactic:
simpa [enorm] using ha.le

Premises used: LT.lt.le, ENorm.enorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
hs : Balanced 𝕜 s
hx : egauge 𝕜 s x < 1
⊢ egauge 𝕜 s x < enorm.{u_1} (E := 𝕜) 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
⊢ egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
(iInf₂_eq_bot _).trans ?_

Premises used: Iff.trans, iInf₂_eq_bot, egauge
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
refine : (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s
⊢ egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
refine (iInf₂_eq_bot _).trans ?_

Premises used: Iff.trans, iInf₂_eq_bot