harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_iUnion_apply_eq_iSup [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s)
    {t : Set α} (ht : MeasurableSet t) : μ.restrict (⋃ i, s i) t = ⨆ i, μ.restrict (s i) t

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t

Tactic:
simp only [restrict_apply ht, inter_iUnion]

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ⨆ i, μ (t ∩ s i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i => t ∩ s i

Tactic:
exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ⨆ i, μ (t ∩ s i)

Tactic:
rw [Directed.measure_iUnion]

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i => t ∩ s i
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem sum_apply {ι : Type*} (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) (v : V₁) :
    (∑ i ∈ s, f i) v = ∑ i ∈ s, f i v

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
ι : Type u_5
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
v : V₁
⊢ (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

Tactic:
simp only [coe_sum, Finset.sum_apply]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.norm_map_cons_le (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0)
    (m : ∀ i : Fin n, Ei i.succ) : ‖f (cons x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖ :=
  calc
    ‖f (cons x m)‖ ≤ ‖f‖ * ∏ i, ‖cons x m i‖ := f.le_opNorm _
    _ = ‖f‖ * ‖x‖ * ∏ i, ‖m i‖

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
m : (i : Fin n) → Ei i.succ
⊢ ‖f‖ * ∏ i : Fin (n + 1), ‖Fin.cons x m i‖ = ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖

Tactic:
rw [prod_univ_succ]

Result:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
m : (i : Fin n) → Ei i.succ
⊢ ‖f‖ * (‖Fin.cons x m 0‖ * ∏ i : Fin n, ‖Fin.cons x m i.succ‖) = ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
m : (i : Fin n) → Ei i.succ
⊢ ‖f‖ * (‖Fin.cons x m 0‖ * ∏ i : Fin n, ‖Fin.cons x m i.succ‖) = ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Topology/Sheaves/Skyscraper.lean
theorem skyscraperPresheaf_eq_pushforward
    [hd : ∀ U : Opens (TopCat.of PUnit.{u + 1}), Decidable (PUnit.unit ∈ U)] :
    skyscraperPresheaf p₀ A =
      (ofHom (ContinuousMap.const (TopCat.of PUnit) p₀)) _*
        skyscraperPresheaf (X := TopCat.of PUnit) PUnit.unit A

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A =
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)

Tactic:
convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
    ContinuousMap.const _ p₀).obj U)
  C _ _ A = _ <;> congr

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.of_dvd_left (h : IsRelPrime y z) (dvd : x ∣ y) : IsRelPrime x z

Proof state:
case intro
α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z

Tactic:
exact IsRelPrime.of_mul_left_left h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
h : IsRelPrime y z
dvd : x ∣ y
⊢ IsRelPrime x z

Tactic:
obtain ⟨d, rfl⟩ := dvd

Result:
case intro
α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_range' {g : β → α} (hg : (mulSupport (f ∘ g)).InjOn g) :
    ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)

Tactic:
rw [← image_univ, finprod_mem_image', finprod_mem_univ]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport (f ∘ g))

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport (f ∘ g))

Tactic:
rwa [univ_inter]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.cos (o.oangle y (y - x)) = ‖y - x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_quotient_jacobson : jacobson R (M ⧸ jacobson R M) = ⊥

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ jacobson R (M ⧸ jacobson R M) = ⊥

Tactic:
rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma oneLePart_le_one : a⁺ᵐ ≤ 1 ↔ a ≤ 1

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁺ᵐ ≤ 1 ↔ a ≤ 1

Tactic:
simp [oneLePart]

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
@[simp] lemma single_nonneg : 0 ≤ single i a ↔ 0 ≤ a

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ 0 ≤ single i a ↔ 0 ≤ a

Tactic:
classical exact Pi.single_nonneg

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ 0 ≤ single i a ↔ 0 ≤ a

Tactic:
exact Pi.single_nonneg

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma prob_le_one {μ : Measure α} [IsZeroOrProbabilityMeasure μ] {s : Set α} : μ s ≤ 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ s ≤ 1

Tactic:
apply (measure_mono (subset_univ _)).trans

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ univ ≤ 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ univ ≤ 1

Tactic:
rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem natSize_pos (n) : 0 < natSize n

Proof state:
n : PosNum
⊢ 0 < n.natSize

Tactic:
cases n <;> apply Nat.succ_pos

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc (attr := simp)]
lemma s_r (s : S.Splitting) : s.s ≫ s.r = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : Epi S.g
⊢ s.s ≫ s.r = 0

Tactic:
simp only [← cancel_epi S.g, comp_zero, g_s_assoc, sub_comp, id_comp,
  assoc, f_r, comp_id, sub_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ s.s ≫ s.r = 0

Tactic:
have := s.epi_g

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : Epi S.g
⊢ s.s ≫ s.r = 0
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem zeta_mul_vonMangoldt : (ζ : ArithmeticFunction ℝ) * Λ = log

Proof state:
⊢ Λ * ↑ζ = log

Tactic:
simp

Result:
no goals

Proof state:
⊢ ↑ζ * Λ = log

Tactic:
rw [mul_comm]

Result:
⊢ Λ * ↑ζ = log
-- Mathlib/Order/Filter/Prod.lean
theorem map_prod_map_coprod_le.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
    map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Proof state:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)

Tactic:
simp only [mem_map, mem_coprod_iff]

Result:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Proof state:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩

Result:
case intro.intro.intro.intro.intro
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Proof state:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Tactic:
intro s

Result:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)

Proof state:
case intro.intro.intro.intro.intro
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩ <;> convert hx

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_ne_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
    ∀ᵐ x ∂(η a), rnDeriv κ η a x ≠ ∞

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂η a, κ.rnDeriv η a x ≠ ⊤

Tactic:
filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} (h : m.WF) :
    (m.modify k f).get! k' =
      if heq : k == k' then
        m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
      else
        m.get! k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
hi : Inhabited (β k')
f : β k → β k
h : m.WF
⊢ (m.modify k f).get! k' =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'

Tactic:
simp_to_raw using Raw₀.get!_modify

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_strict_mono_left (ha : a < a') (hr : r < 1) : lineMap a b r < lineMap a' b r

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b

Tactic:
exact add_lt_add_right (smul_lt_smul_of_pos_left ha (sub_pos.2 hr)) _

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (lineMap a b) r < (lineMap a' b) r

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
-- Mathlib/Order/SymmDiff.lean
theorem le_bihimp_iff {a b c : α} : a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b

Tactic:
simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma HasUnifEigenvector.hasUnifEigenvalue {f : End R M} {μ : R} {k : ℕ∞} {x : M}
    (h : f.HasUnifEigenvector μ k x) : f.HasUnifEigenvalue μ k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ f.HasUnifEigenvalue μ k

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0

Tactic:
use x

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ x ∈ (f.genEigenspace μ) k ∧ x ≠ 0

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ x ∈ (f.genEigenspace μ) k ∧ x ≠ 0

Tactic:
exact h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂

Proof state:
α : Type u_1
f : List α → List α
n : Nat
l₁ l₂ : List α
⊢ modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂

Tactic:
induction l₁ <;> simp [*, Nat.succ_add]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The **coheight** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and beginning with `a`.

This is not the definition of `coheight`. The definition of `coheight` is via the `height` in the
dual order, in order to easily transfer theorems between `height` and `coheight`.
-/
lemma coheight_eq (a : α) :
    coheight a = ⨆ (p : LTSeries α) (_ : a ≤ p.head), (p.length : ℕ∞)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries fun x1 x2 => x1 < x2),
    ⨆ (_ : a ≤ ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last ≤ a), ↑x.length

Tactic:
congr! 1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ coheight a = ⨆ p, ⨆ (_ : a ≤ RelSeries.head p), ↑p.length

Tactic:
apply Equiv.iSup_congr ⟨RelSeries.reverse, RelSeries.reverse, RelSeries.reverse_reverse,
  RelSeries.reverse_reverse⟩

Result:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries fun x1 x2 => x1 < x2),
    ⨆ (_ : a ≤ ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last ≤ a), ↑x.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast!

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ l.toArray.back! = l.getLast!

Tactic:
simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_comp_cons (f : α → β) (t) : map f ∘ cons t = cons (f t) ∘ map f

Proof state:
case h
α : Type u_1
β : Type v
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f

Tactic:
ext

Result:
case h
α : Type u_1
β : Type v
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_right_self : x \ (x \ y) = x ⊓ y

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (x \ y) = x ⊓ y

Tactic:
rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
@[ext]
lemma ext {m : R} {A B : FixedDetMatrix n R m} (h : ∀ i j , A.1 i j = B.1 i j) : A = B

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
⊢ A = B

Tactic:
apply ext'

Result:
case h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
⊢ ↑A = ↑B

Proof state:
case h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
⊢ ↑A = ↑B

Tactic:
ext i j

Result:
case h.a
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
i j : n
⊢ ↑A i j = ↑B i j

Proof state:
case h.a
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
i j : n
⊢ ↑A i j = ↑B i j

Tactic:
apply h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin'_apply (M : Matrix n n R₁) (x y : n → R₁) :
    Matrix.toBilin' M x y = ∑ i, ∑ j, x i * M i j * y j :=
  (Matrix.toLinearMap₂'_apply _ _ _).trans
    (by simp only [smul_eq_mul, mul_assoc, mul_comm, mul_left_comm])

Proof state:
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
x y : n → R₁
⊢ ∑ i : n, ∑ j : n, x i • y j • M i j = ∑ i : n, ∑ j : n, x i * M i j * y j

Tactic:
simp only [smul_eq_mul, mul_assoc, mul_comm, mul_left_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_fin_three (A : Matrix (Fin 3) (Fin 3) R) : trace A = A 0 0 + A 1 1 + A 2 2

Proof state:
R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + A 1 1 + A 2 2

Tactic:
rw [← add_zero (A 2 2), add_assoc]

Result:
R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))

Proof state:
R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_or {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i])

Proof state:
w : Nat
x y : BitVec w
i : Nat
h : i < w
⊢ (x ||| y)[i] = (x[i] || y[i])

Tactic:
simp [getElem_eq_testBit_toNat]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem ofENat_le {x y : ℕ∞} : ofENat x ≤ ofENat y ↔ x ≤ y

Proof state:
x y : ℕ∞
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
rw [← toWithTop_le, toWithTop_ofENat, toWithTop_ofENat]

Result:
no goals

Proof state:
x y : ℕ∞
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
classical
rw [← toWithTop_le, toWithTop_ofENat, toWithTop_ofENat]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem le_mul_of_le_one_left [ExistsAddOfLE α] [MulPosMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hb : b ≤ 0
h : a ≤ 1
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_isSome_iff {f : α → Option β} {l : Array α} :
    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (findSome? f { toList := toList✝ }).isSome = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ (f x).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (findSome? f l).isSome = true ↔ ∃ x, x ∈ l ∧ (f x).isSome = true

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (findSome? f { toList := toList✝ }).isSome = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ (f x).isSome = true
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_sSup (S : Set (UpperSet α)) : (sSup S).compl = ⨆ s ∈ S, UpperSet.compl s :=
  LowerSet.ext <| by simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
⊢ ↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)

Tactic:
simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]

Result:
no goals