awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
⊢ f' < slope f x y
have this₁ : slope f x u < slope f x y
Tactic: simp only [← slope_def_field] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y < f'
have obtain : ∀ (u : ℝ) (hxu : x < u) (huy : u < y), slope f x y < f'
Tactic: obtain ⟨u, hxu, huy⟩ := exists_between hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
⊢ slope f x y < f'
have hu : u ∈ S
Tactic: have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ slope f x y < f'
have this : (f x - f y) / (x - y) < (f u - f y) / (u - y)
Tactic: have := hfc.secant_strict_mono hy hx hu hxy.ne huy.ne hxu
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f x - f y) / (x - y) < (f u - f y) / (u - y)
⊢ slope f x y < f'
have this₁ : slope f x y < slope f u y
Tactic: simp_rw [← slope_def_field, slope_comm _ y] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ 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
have inl : ∀ (hy : x ∈ S) (hxy : x ≤ x), derivWithin f S x ≤ derivWithin f S x
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
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
⊢ derivWithin f S y ≤ derivWithin f S x
have inr : ∀ (hxy' : x < y), derivWithin f S y ≤ derivWithin f S x
Tactic: rcases eq_or_lt_of_le hxy with rfl | hxy'
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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)
have refine : (M * N) *ᵥ 1 = 1
Tactic: refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 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)
have refine₁ : 1 ᵥ* (M * N) = 1
Tactic: refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
have rw : M *ᵥ N *ᵥ 1 = 1
Tactic: rw [← mulVec_mulVec, hN.2.1, hM.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ (M * N) *ᵥ 1 = 1
have rw₁ : M *ᵥ 1 = 1
Tactic: rw [← mulVec_mulVec, hN.2.1, hM.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ (M * N) *ᵥ 1 = 1
have rw₂ : Eq (α := n → R) 1 1
Tactic: rw [← mulVec_mulVec, hN.2.1, hM.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have rw : 1 ᵥ* M ᵥ* N = 1
Tactic: rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have rw₁ : 1 ᵥ* N = 1
Tactic: rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have rw₂ : Eq (α := n → R) 1 1
Tactic: rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have next : 1 ᵥ* M ᵥ* N = 1
Tactic: next => rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have next₁ : 1 ᵥ* N = 1
Tactic: next => rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have next₂ : Eq (α := n → R) 1 1
Tactic: next => rw [← vecMul_vecMul, hM.2.2, hN.2.2]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ Eq (α := Submonoid (Matrix n n R)) (doublyStochastic R n) (rowStochastic R n ⊓ colStochastic R n)
have 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
Tactic: ext M
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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)) (rowStochastic R n) M ∧
      Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
have 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
Tactic: rw [doublyStochastic_eq_rowStochastic_inf_colStochastic, Submonoid.mem_inf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ 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
have 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
Tactic: rw [doublyStochastic_eq_rowStochastic_inf_colStochastic, Submonoid.mem_inf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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 ≤ 1
have rw : M i j ≤ ∑ j : n, M i j
Tactic: rw [← sum_row_of_mem_doublyStochastic hM i]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ a • x + b • y ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
have 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
Tactic: simp only [SetLike.mem_coe, mem_doublyStochastic_iff_sum] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i : n, (M *ᵥ x) i) (∑ i : n, x i)
have hA₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
Tactic: apply sum_mulVec_of_mem_colStochastic
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ (∃ (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
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (hypothesis)
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 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s
have 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
Tactic: rw [mem_doublyStochastic_iff_sum] at hM'
Cleared hypotheses: hM'
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s
have 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
Tactic: simp only [smul_apply, smul_eq_mul, ← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ ((∀ (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'
have 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'
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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'
⊢ ((∀ (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'
have 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'
Tactic: rcases eq_or_lt_of_le hs with rfl | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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'
have 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
Tactic: simp only [zero_smul, exists_and_right, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
have refine : M = 0
Tactic: refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
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
⊢ M = 0
have a : ∀ (i j : n), M i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (hypothesis)
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
⊢ M i j = 0 i j
have h₃ : Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0
Tactic: specialize h₂ i
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (hypothesis)
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
⊢ M i j = 0 i j
have h₃ : ∀ (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₂
Cleared hypotheses: h₂