harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ (n - ↑b + ↑a) % n = n + ↑a - ↑b ↔ ↑a < ↑b

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a = n + ↑a - ↑b ↔ ↑a < ↑b

n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ (n - ↑b + ↑a) % n = n + ↑a - ↑b ↔ ↑a < ↑b

Tactic:
rw [Nat.mod_eq_sub_of_lt_two_mul h]

Result:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a - n = n + ↑a - ↑b ↔ ↑a < ↑b

n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Proof state:
n : Nat
a b : Fin n
⊢ ↑⟨(n - ↑b + ↑a) % n, ⋯⟩ = n + ↑a - ↑b ↔ ↑a < ↑b

Tactic:
dsimp only

Result:
n : Nat
a b : Fin n
⊢ (n - ↑b + ↑a) % n = n + ↑a - ↑b ↔ ↑a < ↑b

Proof state:
n : Nat
a b : Fin n
⊢ ↑(a - b) = n + ↑a - ↑b ↔ a < b

Tactic:
rw [sub_def, lt_def]

Result:
n : Nat
a b : Fin n
⊢ ↑⟨(n - ↑b + ↑a) % n, ⋯⟩ = n + ↑a - ↑b ↔ ↑a < ↑b

Proof state:
n : Nat
a b : Fin n
⊢ (n - ↑b + ↑a) % n = n + ↑a - ↑b ↔ ↑a < ↑b

Tactic:
if h : n ≤ (n - b) + a then
  rw [Nat.mod_eq_sub_of_lt_two_mul h]
  all_goals omega
else
  rw [Nat.mod_eq_of_lt]
  all_goals omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a - n = n + ↑a - ↑b ↔ ↑a < ↑b

n : Nat
a b : Fin n
h : n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < 2 * n

Tactic:
all_goals omega

Result:
no goals

Proof state:
n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a = n + ↑a - ↑b ↔ ↑a < ↑b

n : Nat
a b : Fin n
h : ¬n ≤ n - ↑b + ↑a
⊢ n - ↑b + ↑a < n

Tactic:
all_goals omega

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
@[simp] lemma natCard_graphOn (s : Set α) (f : α → β) : Nat.card (s.graphOn f) = Nat.card s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card ↑(graphOn f s) = Nat.card ↑s

Tactic:
rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]

Result:
no goals
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Iio (a : ℕ) : (↑) '' Iio a = Ico (0 : ℤ) a

Proof state:
a : ℕ
⊢ Nat.cast '' Iio a = Ico 0 ↑a

Tactic:
rw [← Ico_bot, image_cast_int_Ico]

Result:
a : ℕ
⊢ Ico ↑⊥ ↑a = Ico 0 ↑a

Proof state:
a : ℕ
⊢ Ico ↑⊥ ↑a = Ico 0 ↑a

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isLeftDescent_iff {w : W} {i : B} :
    ¬cs.IsLeftDescent w i ↔ ℓ (s i * w) = ℓ w + 1

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
exact (cs.length_simple_mul w i).resolve_right (by omega)

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
intro _

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
unfold IsLeftDescent

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) = cs.length w + 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w
-- Mathlib/Algebra/Field/Equiv.lean
theorem isField {A : Type*} (B : Type*) [Semiring A] [Semiring B] (hB : IsField B)
    (e : A ≃* B) : IsField A where
  exists_pair_ne := have ⟨x, y, h⟩ := hB.exists_pair_ne; ⟨e.symm x, e.symm y, e.symm.injective.ne h⟩
  mul_comm := fun x y => e.injective <| by rw [map_mul, map_mul, hB.mul_comm]
  mul_inv_cancel := fun h => by
    obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
    exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : e a✝ * a' = 1
⊢ e (a✝ * e.symm a') = e 1

Tactic:
rw [map_mul, map_one, e.apply_symm_apply, he]

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
⊢ ∃ b, a✝ * b = 1

Tactic:
obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)

Result:
case intro
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : e a✝ * a' = 1
⊢ ∃ b, a✝ * b = 1

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : e a✝ * a' = 1
⊢ ∃ b, a✝ * b = 1

Tactic:
exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
x y : A
⊢ e (x * y) = e (y * x)

Tactic:
rw [map_mul, map_mul, hB.mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem jointly_surjective_of_isColimit {F : J ⥤ Type u} {t : Cocone F} (h : IsColimit t)
    (x : t.pt) : ∃ j y, t.ι.app j y = x

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ j y, t.ι.app j y = x

Tactic:
by_contra hx

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ¬∃ j y, t.ι.app j y = x
⊢ False

Proof state:
case h.h.a
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
j : J
y : F.obj j
⊢ ((t.ι.app j ≫ fun x => { down := True }) y).down ↔ ((t.ι.app j ≫ fun x_1 => { down := x_1 ≠ x }) y).down

Tactic:
exact (true_iff _).mpr (hx j y)

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
⊢ (fun x => { down := True }) ≠ fun x_1 => { down := x_1 ≠ x }

Tactic:
exact fun he ↦ of_eq_true (congr_arg ULift.down <| congr_fun he x).symm rfl

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ¬∃ j y, t.ι.app j y = x
⊢ False

Tactic:
simp_rw [not_exists] at hx

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
⊢ False

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
⊢ (fun x => { down := True }) = fun x_1 => { down := x_1 ≠ x }

Tactic:
refine h.hom_ext fun j ↦ ?_

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
j : J
⊢ (t.ι.app j ≫ fun x => { down := True }) = t.ι.app j ≫ fun x_1 => { down := x_1 ≠ x }

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
j : J
⊢ (t.ι.app j ≫ fun x => { down := True }) = t.ι.app j ≫ fun x_1 => { down := x_1 ≠ x }

Tactic:
ext y

Result:
case h.h.a
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x
j : J
y : F.obj j
⊢ ((t.ι.app j ≫ fun x => { down := True }) y).down ↔ ((t.ι.app j ≫ fun x_1 => { down := x_1 ≠ x }) y).down
-- Mathlib/NumberTheory/WellApproximable.lean
/-- **Dirichlet's approximation theorem**

See also `Real.exists_rat_abs_sub_le_and_den_le`. -/
lemma exists_norm_nsmul_le (ξ : 𝕊) {n : ℕ} (hn : 0 < n) :
    ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)

Proof state:
case hδ
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ volume univ ≤ (n + 1) • volume (closedBall 0 (T / ↑(n + 1) / 2))

Tactic:
rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
  mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
  mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)

Tactic:
apply NormedAddCommGroup.exists_norm_nsmul_le (μ := volume) ξ hn

Result:
case hδ
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ volume univ ≤ (n + 1) • volume (closedBall 0 (T / ↑(n + 1) / 2))
-- Mathlib/Data/Real/EReal.lean
lemma bot_lt_inv (x : EReal) : ⊥ < x⁻¹

Proof state:
case h_real
x : ℝ
⊢ ⊥ < (↑x)⁻¹

Tactic:
exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

Result:
no goals

Proof state:
x : EReal
⊢ ⊥ < x⁻¹

Tactic:
cases x with
| h_bot => exact inv_bot ▸ bot_lt_zero
| h_top => exact EReal.inv_top ▸ bot_lt_zero
| h_real x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

Result:
no goals

Proof state:
case h_bot

⊢ ⊥ < ⊥⁻¹

Tactic:
exact inv_bot ▸ bot_lt_zero

Result:
no goals

Proof state:
case h_top

⊢ ⊥ < ⊤⁻¹

Tactic:
exact EReal.inv_top ▸ bot_lt_zero

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsUpperSet.mem_interior_of_forall_lt (hs : IsUpperSet s) (hx : x ∈ closure s)
    (h : ∀ i, x i < y i) : y ∈ interior s

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ y ∈ interior s

Tactic:
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h

Result:
case intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
⊢ y ∈ interior s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s

Tactic:
refine hs (fun i => ?_) hz

Result:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
i : ι
⊢ z i ≤ w i

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : dist x z < ε
⊢ y ∈ interior s

Tactic:
rw [dist_pi_lt_iff hε] at hxz

Result:
case intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ y ∈ interior s
-- Mathlib/Tactic/Rify.lean
@[rify_simps] lemma ratCast_lt (a b : ℚ) : a < b ↔ (a : ℝ) < (b : ℝ)

Proof state:
a b : ℚ
⊢ a < b ↔ ↑a < ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_le_prod_of_ne_one' (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
    ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Tactic:
exact fun _ _ ↦ le_of_eq

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ filter (fun x => f x ≠ 1) s ⊆ t

Tactic:
simpa only [subset_iff, mem_filter, and_imp]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
calc
∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
rw [← prod_union, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
_ ≤ ∏ x ∈ t, f x :=
mul_le_of_le_one_of_le
(prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
(prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp] )

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∀ i ∈ filter (fun x => f x = 1) s, f i ≤ 1

Tactic:
simp only [mem_filter, and_imp]

Result:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
classical calc
  ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
    rw [← prod_union, filter_union_filter_neg_eq]
    exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
  _ ≤ ∏ x ∈ t, f x :=
    mul_le_of_le_one_of_le
      (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
      (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp] )

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ ∏ x ∈ s, f x = (∏ x ∈ filter (fun x => f x = 1) s, f x) * ∏ x ∈ filter (fun x => f x ≠ 1) s, f x

Tactic:
rw [← prod_union, filter_union_filter_neg_eq]

Result:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ Disjoint (filter (fun x => f x = 1) s) (filter (fun x => f x ≠ 1) s)

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ Disjoint (filter (fun x => f x = 1) s) (filter (fun x => f x ≠ 1) s)

Tactic:
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F}
    (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) :
    ∃ a b : ℝ, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0

Proof state:
case intro.intro.intro.a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0
⊢ (InnerProductSpace.toDualMap ℝ F) (a • x₀) + (InnerProductSpace.toDualMap ℝ F) (b • T x₀) = 0

Tactic:
simp only [map_smulₛₗ _, RCLike.conj_to_real]

Result:
case intro.intro.intro.a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0
⊢ a • (InnerProductSpace.toDualMap ℝ F) x₀ + b • (InnerProductSpace.toDualMap ℝ F) (T x₀) = 0

Proof state:
case intro.intro.intro.a.a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0
⊢ (fun x => 2 • x) (a • (innerSL ℝ) x₀ + b • (innerSL ℝ) (T x₀)) = (fun x => 2 • x) 0

Tactic:
simpa only [two_smul, smul_add, add_smul, add_zero] using h₂

Result:
no goals

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀

Tactic:
convert hextr

Result:
case h.e'_6
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} = sphere 0 ‖x₀‖
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma sSup_iff (S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) :
    sSup S f ↔ ∃ (W : S), W.1 f

Proof state:
case mp.intro.intro.intro.mk.intro.mk.intro.mk
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
val✝ : (i : C) → ⦃Y : C⦄ → (i ⟶ Y) → Prop
h : val✝ ∈ S
hf : ↑⟨(fun f => ↑f Y) ⟨(fun f => ↑f X) ⟨val✝, h⟩, ⋯⟩, ⋯⟩ f
⊢ ∃ W, ↑W f

Tactic:
exact ⟨⟨_, h⟩, hf⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ W, ↑W f) → ∃ a ∈ Set.range fun f_1 => ↑f_1 f, a

Tactic:
rintro ⟨⟨W, hW⟩, hf⟩

Result:
case mpr.intro.mk
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
W : MorphismProperty C
hW : W ∈ S
hf : ↑⟨W, hW⟩ f
⊢ ∃ a ∈ Set.range fun f_1 => ↑f_1 f, a

Proof state:
case mpr.intro.mk
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
W : MorphismProperty C
hW : W ∈ S
hf : ↑⟨W, hW⟩ f
⊢ ∃ a ∈ Set.range fun f_1 => ↑f_1 f, a

Tactic:
exact ⟨_, ⟨⟨_, ⟨_, ⟨⟨W, hW⟩, rfl⟩⟩, rfl⟩, rfl⟩, hf⟩

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ a ∈ Set.range fun f_1 => ↑f_1 f, a) → ∃ W, ↑W f

Tactic:
rintro ⟨_, ⟨⟨_, ⟨⟨_, ⟨_, h⟩, rfl⟩, rfl⟩⟩, rfl⟩, hf⟩

Result:
case mp.intro.intro.intro.mk.intro.mk.intro.mk
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
val✝ : (i : C) → ⦃Y : C⦄ → (i ⟶ Y) → Prop
h : val✝ ∈ S
hf : ↑⟨(fun f => ↑f Y) ⟨(fun f => ↑f X) ⟨val✝, h⟩, ⋯⟩, ⋯⟩ f
⊢ ∃ W, ↑W f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ sSup S f ↔ ∃ W, ↑W f

Tactic:
dsimp [sSup, iSup]

Result:
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ a ∈ Set.range fun f_1 => ↑f_1 f, a) ↔ ∃ W, ↑W f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ a ∈ Set.range fun f_1 => ↑f_1 f, a) ↔ ∃ W, ↑W f

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ a ∈ Set.range fun f_1 => ↑f_1 f, a) → ∃ W, ↑W f

case mpr
C : Type u
inst✝ : Category.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ (∃ W, ↑W f) → ∃ a ∈ Set.range fun f_1 => ↑f_1 f, a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_add_const (l : Array α) (a b : Nat) :
    l.foldl (fun x _ => x + a) b = b + a * l.size

Proof state:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ Array.foldl (fun x x_1 => x + a) b { toList := l } = b + a * { toList := l }.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
a b : Nat
⊢ Array.foldl (fun x x_1 => x + a) b l = b + a * l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ Array.foldl (fun x x_1 => x + a) b { toList := l } = b + a * { toList := l }.size
-- Mathlib/Order/LiminfLimsup.lean
theorem isBounded_top : IsBounded r ⊤ ↔ ∃ t, ∀ x, r x t

Proof state:
α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t

Tactic:
simp [IsBounded, eq_univ_iff_forall]

Result:
no goals