awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f y
⊢ deriv f y ≤ slope f x y

Tactic:
hfc.le_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, ConcaveOn.le_slope_of_hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), derivWithin f S x ≤ derivWithin f S x
inr : ∀ (hxy' : x < y), derivWithin f S y ≤ derivWithin f S x
⊢ derivWithin f S y ≤ derivWithin f S x

Tactic:
rcases eq_or_lt_of_le hxy with rfl | hxy'

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S y ≤ derivWithin f S x

Tactic:
(hfc.derivWithin_le_slope hx hy hxy' (hfd y hy)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd x hx))

Premises used: ConcaveOn.slope_le_derivWithin, ConcaveOn.derivWithin_le_slope, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S y ≤ derivWithin f S x

Tactic:
exact (hfc.derivWithin_le_slope hx hy hxy' (hfd y hy)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd x hx))

Premises used: ConcaveOn.slope_le_derivWithin, ConcaveOn.derivWithin_le_slope, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ AntitoneOn (deriv f) S

Tactic:
simpa using (hfc.neg.monotoneOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

Premises used: MonotoneOn.neg, DifferentiableAt.neg, ConvexOn.monotoneOn_deriv, ConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

Premises used: neg_lt_neg, neg_neg, HasDerivWithinAt.neg, slope_neg, StrictConcaveOn.neg, StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ slope f x y < derivWithin f (Ioi x) x

Tactic:
hfc.slope_lt_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConcaveOn.slope_lt_of_hasDerivWithinAt_Ioi
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivWithinAt f f' S x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.lt_slope_of_hasDerivWithinAt hx hy hxy hfd.neg)

Premises used: neg_lt_neg, neg_neg, HasDerivWithinAt.neg, slope_neg, StrictConvexOn.lt_slope_of_hasDerivWithinAt, StrictConcaveOn.neg, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S x
⊢ slope f x y < derivWithin f S x

Tactic:
hfc.slope_lt_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConcaveOn.slope_lt_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivAt f f' x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.lt_slope_of_hasDerivAt hx hy hxy hfd.neg)

Premises used: StrictConvexOn.lt_slope_of_hasDerivAt, HasDerivAt.neg, neg_lt_neg, neg_neg, slope_neg, StrictConcaveOn.neg, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f x
⊢ slope f x y < deriv f x

Tactic:
hfc.slope_lt_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, StrictConcaveOn.slope_lt_of_hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' < slope f x y

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

Premises used: neg_lt_neg, neg_neg, StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio, HasDerivWithinAt.neg, slope_neg, StrictConcaveOn.neg, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f (Iio y) y
⊢ derivWithin f (Iio y) y < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

Premises used: StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ f' < slope f x y

Tactic:
simpa only [neg_neg, Pi.neg_def, slope_neg] using
    neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt hx hy hxy hf'.neg)

Premises used: neg_lt_neg, neg_neg, HasDerivWithinAt.neg, slope_neg, StrictConcaveOn.neg, StrictConvexOn.slope_lt_of_hasDerivWithinAt, Pi.neg_def
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableWithinAt ℝ f S y
⊢ derivWithin f S y < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, StrictConcaveOn.lt_slope_of_hasDerivWithinAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivAt f f' y
⊢ f' < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivWithinAt_Iio hx hy hxy hf'.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
x y : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : DifferentiableAt ℝ f y
⊢ deriv f y < slope f x y

Tactic:
hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt

Premises used: StrictConcaveOn.lt_slope_of_hasDerivAt, DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x

Tactic:
(hfc.derivWithin_lt_slope hx hy hxy (hfd y hy)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd x hx))

Premises used: StrictConcaveOn.slope_lt_derivWithin, StrictConcaveOn.derivWithin_lt_slope, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd y hy)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd x hx))

Premises used: StrictConcaveOn.slope_lt_derivWithin, StrictConcaveOn.derivWithin_lt_slope, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Deriv
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictAntiOn (deriv f) S

Tactic:
simpa using (hfc.neg.strictMonoOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

Premises used: StrictConvexOn.strictMonoOn_deriv, DifferentiableAt.neg, StrictMonoOn.neg, StrictConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
    (M * N)

Tactic:
⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩

Premises used: mul_nonneg, Set.Mem, setOf, Finset.sum_nonneg, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
refine : (M * N) *ᵥ 1 = 1
refine₁ : 1 ᵥ* (M * N) = 1
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
    (M * N)

Tactic:
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
rw : M *ᵥ N *ᵥ 1 = 1
rw₁ : M *ᵥ 1 = 1
rw₂ rw₃ : Eq (α := n → R) 1 1
⊢ (M * N) *ᵥ 1 = 1

Tactic:
rw [← mulVec_mulVec, hN.2.1, hM.2.1]

Premises used: And.right, And.left, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
⊢ (M * N) *ᵥ 1 = 1

Tactic:
next => rw [← mulVec_mulVec, hN.2.1, hM.2.1]

Premises used: And.right, And.left, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
rw : 1 ᵥ* M ᵥ* N = 1
rw₁ : 1 ᵥ* N = 1
rw₂ rw₃ : Eq (α := n → R) 1 1
⊢ 1 ᵥ* (M * N) = 1

Tactic:
rw [← vecMul_vecMul, hM.2.2, hN.2.2]

Premises used: And.right, Matrix.vecMul_vecMul
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} N
next : 1 ᵥ* M ᵥ* N = 1
next₁ : 1 ᵥ* N = 1
next₂ next₃ : Eq (α := n → R) 1 1
⊢ 1 ᵥ* (M * N) = 1

Tactic:
next => rw [← vecMul_vecMul, hM.2.2, hN.2.2]

Premises used: And.right, Matrix.vecMul_vecMul
-- Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M : Matrix n_1 n_1 R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1} 1

Tactic:
simp [zero_le_one_elem]

Premises used: Matrix.zero_le_one_elem
-- 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
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
⊢ 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:
simp [funext_iff, doublyStochastic, mulVec, vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul, funext_iff, doublyStochastic, Matrix.mulVec
-- 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
h :
  ∀ (M : Matrix n n R),
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M ↔
      Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n ⊓ colStochastic R n) M
⊢ Eq (α := Submonoid (Matrix n n R)) (doublyStochastic R n) (rowStochastic R n ⊓ colStochastic R n)

Tactic:
ext M
-- 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
⊢ (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1 ↔
    ((∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1) ∧ (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1

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 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
rw :
  Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n ⊓ colStochastic R n) M ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ∧
      Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₁ rw₂ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ∧
      Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ∧
      Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ∧
      Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M

Tactic:
rw [doublyStochastic_eq_rowStochastic_inf_colStochastic, Submonoid.mem_inf]

Premises used: doublyStochastic_eq_rowStochastic_inf_colStochastic, Submonoid.mem_inf
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
i j : n
⊢ 0 ≤ M i j

Tactic:
hM.1 _ _

Premises used: And.left
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
i : n
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 1

Tactic:
(mem_doublyStochastic_iff_sum.1 hM).2.1 _

Premises used: mem_doublyStochastic_iff_sum, And.right, And.left, Iff.mp
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
j : n
⊢ Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 1

Tactic:
(mem_doublyStochastic_iff_sum.1 hM).2.2 _

Premises used: mem_doublyStochastic_iff_sum, And.right, Iff.mp
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
⊢ M *ᵥ 1 = 1

Tactic:
(mem_doublyStochastic.1 hM).2.1

Premises used: And.right, And.left, mem_doublyStochastic, Iff.mp
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
⊢ 1 ᵥ* M = 1

Tactic:
(mem_doublyStochastic.1 hM).2.2

Premises used: And.right, mem_doublyStochastic, Iff.mp
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
i j : n
rw : M i j ≤ ∑ j : n, M i j
⊢ M i j ≤ 1

Tactic:
rw [← sum_row_of_mem_doublyStochastic hM i]

Premises used: sum_row_of_mem_doublyStochastic
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
i j : n
⊢ M i j ≤ ∑ j : n, M i j

Tactic:
single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
i j : n
⊢ M i j ≤ ∑ j : n, M i j

Tactic:
exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- 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
x : Matrix n n R
hx : x ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
y : Matrix n n R
hy : y ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
simp :
  ∀
    (hx :
      (∀ (i j : n), 0 ≤ x i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, x i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, x i j) 1)
    (hy :
      (∀ (i j : n), 0 ≤ y i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, y i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, y i j) 1),
    (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧
      (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, (a • x + b • y) i j) 1) ∧
        ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, (a • x + b • y) i j) 1
⊢ a • x + b • y ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
simp only [SetLike.mem_coe, mem_doublyStochastic_iff_sum] at hx hy ⊢

Premises used: mem_doublyStochastic_iff_sum, SetLike.mem_coe
-- 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
x y : Matrix n n R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
hx :
  (∀ (i j : n), 0 ≤ x i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, x i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, x i j) 1
hy :
  (∀ (i j : n), 0 ≤ y i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, y i j) 1) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, y i j) 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧
    (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, (a • x + b • y) i j) 1) ∧
      ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, (a • x + b • y) i j) 1

Tactic:
simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

Premises used: Finset.mul_sum, mul_nonneg, Finset.sum_add_distrib, add_nonneg
-- 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
σ : Equiv.Perm n
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) (Equiv.Perm.permMatrix R σ)

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 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) Mᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic 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 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
m : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (doublyStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)

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 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
m : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (doublyStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M

Tactic:
grind