harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
lemma isVonNBounded_iff_tendsto_smallSets_nhds {𝕜 E : Type*} [NormedDivisionRing 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
    IsVonNBounded 𝕜 S ↔ Tendsto (· • S : 𝕜 → Set E) (𝓝 0) (𝓝 0).smallSets

Proof state:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ ∀ t ∈ 𝓝 0, ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t

Tactic:
refine forall₂_congr fun V hV ↦ ?_

Result:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V

Proof state:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V

Tactic:
simp only [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV), mapsTo', image_smul]

Result:
no goals

Proof state:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ Tendsto (fun x => x • S) (𝓝 0) (𝓝 0).smallSets

Tactic:
rw [tendsto_smallSets_iff]

Result:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ ∀ t ∈ 𝓝 0, ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateCol_subsingleton [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :
    A.updateCol i b = (col (Fin 1) b).submatrix id (Function.const n 0)

Proof state:
case a
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ A.updateCol i b x y = (col (Fin 1) b).submatrix id (Function.const n 0) x y

Tactic:
simp [updateCol_apply, Subsingleton.elim i y]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
⊢ A.updateCol i b = (col (Fin 1) b).submatrix id (Function.const n 0)

Tactic:
ext x y

Result:
case a
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ A.updateCol i b x y = (col (Fin 1) b).submatrix id (Function.const n 0) x y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_sin_eq_of_two_nsmul_eq {θ ψ : Angle} (h : (2 : ℕ) • θ = (2 : ℕ) • ψ) :
    |sin θ| = |sin ψ|

Proof state:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.sin| = |ψ.sin|

Tactic:
rcases h with (rfl | rfl)

Result:
case inl
θ : Angle
⊢ |θ.sin| = |θ.sin|

case inr
ψ : Angle
⊢ |(ψ + ↑π).sin| = |ψ.sin|

Proof state:
case inl
θ : Angle
⊢ |θ.sin| = |θ.sin|

Tactic:
rfl

Result:
no goals

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
rw [two_nsmul_eq_iff] at h

Result:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.sin| = |ψ.sin|

Proof state:
case inr
ψ : Angle
⊢ |(ψ + ↑π).sin| = |ψ.sin|

Tactic:
rw [sin_add_pi, abs_neg]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem single_blocksFun {n : ℕ} (h : 0 < n) (i : Fin (single n h).length) :
    (single n h).blocksFun i = n

Proof state:
n : ℕ
h : 0 < n
i : Fin (single n h).length
⊢ (single n h).blocksFun i = n

Tactic:
simp [blocksFun, single, blocks, i.2]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem rel_nodup {r : α → β → Prop} (hr : Relator.BiUnique r) : (Forall₂ r ⇒ (· ↔ ·)) Nodup Nodup
  | _, _, Forall₂.nil => by simp only [nodup_nil]
  | _, _, Forall₂.cons hab h => by
    simpa only [nodup_cons] using
      Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)

Proof state:
α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun x1 x2 => x1 ↔ x2) [].Nodup [].Nodup

Tactic:
simp only [nodup_nil]

Result:
no goals

Proof state:
α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x1 x2 => x1 ↔ x2) (a✝ :: l₁✝).Nodup (b✝ :: l₂✝).Nodup

Tactic:
simpa only [nodup_cons] using
  Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem star_mul_star (x y : R) : star (x * star y) = y * star x

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (x * star y) = y * star x

Tactic:
rw [star_mul, star_star]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem topologicalGroup_is_uniform_of_compactSpace [CompactSpace G] : UniformGroup G :=
  ⟨by
    apply CompactSpace.uniformContinuous_of_continuous
    exact continuous_div'⟩

Proof state:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
⊢ Continuous fun p => p.1 / p.2

Tactic:
exact continuous_div'

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
⊢ UniformContinuous fun p => p.1 / p.2

Tactic:
apply CompactSpace.uniformContinuous_of_continuous

Result:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
⊢ Continuous fun p => p.1 / p.2
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
@[simp]
lemma codRestrictOfInjective_comp_apply (x : M₁) :
    i (LinearMap.codRestrictOfInjective f i hi hf x) = f x

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ range i
x : M₁
⊢ i ((f.codRestrictOfInjective i hi hf) x) = f x

Tactic:
simp [LinearMap.codRestrictOfInjective]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
lemma interedges_eq_biUnion :
    interedges r s t = s.biUnion fun x ↦ {y ∈ t | r x y}.map ⟨(x, ·), Prod.mk.inj_left x⟩

Proof state:
case h.mk
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ interedges r s t ↔
    (x, y) ∈ s.biUnion fun x => map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } (filter (fun y => r x y) t)

Tactic:
simp [mem_interedges_iff]

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ interedges r s t = s.biUnion fun x => map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } (filter (fun y => r x y) t)

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ interedges r s t ↔
    (x, y) ∈ s.biUnion fun x => map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } (filter (fun y => r x y) t)
-- Mathlib/Data/Multiset/AddSub.lean
theorem count_erase_of_ne {a b : α} (ab : a ≠ b) (s : Multiset α) :
    count a (erase s b) = count a s :=
  Quotient.inductionOn s fun l => by
    convert List.count_erase_of_ne ab l <;> rw [← coe_count] <;> simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
convert List.count_erase_of_ne ab l <;> rw [← coe_count] <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_eq_lintegral [IsProbabilityMeasure μ] (f : α → ℝ≥0∞) :
    ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [laverage, measure_univ, inv_one, one_smul]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_flip (f : α → β → σ → σ × γ) :
    mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s

Tactic:
induction xs, ys using Vector.inductionOn₂ <;> simp_all[flip]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[norm_cast] lemma ofReal_nsmul (n : ℕ) (r : ℝ) : ↑(n • r) = n • (r : ℂ)

Proof state:
n : ℕ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csInf_eq_least_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z)
    (Hinh : ∃ z : ℤ, z ∈ s) : sInf s = leastOfBdd b Hb Hinh

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) = ↑(b.leastOfBdd Hb Hinh)

Tactic:
convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

Result:
no goals

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)

Tactic:
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩

Result:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)

Tactic:
simp only [sInf, this, and_self, dite_true]

Result:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) = ↑(b.leastOfBdd Hb Hinh)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_singleton_self (a : α) : count a #[a] = 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ count a #[a] = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
  | (m:Nat), (n:Nat), _ => aux1 ..
  | Nat.cast m, b, Nat.cast k => by
    rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]
  | a, (n:Nat), (k:Nat) => by
    rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]
  | -[_+1], -[_+1], (k:Nat) => aux2 ..
  | -[m+1], (n:Nat), -[k+1] => by
    rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]
  | (m:Nat), -[n+1], -[k+1] => by
    rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
  | -[m+1], -[n+1], -[k+1] => by
    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
where
  aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
    | (k:Nat) => by simp [Nat.add_assoc]
    | -[k+1]  => by simp [subNatNat_add]
  aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k)

Proof state:
m n k : Nat
⊢ -[m+1] + -[n+1] + -[k+1] = -[m+1] + (-[n+1] + -[k+1])

Tactic:
simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ ↑m + ↑n + -[k+1] = ↑m + (↑n + -[k+1])

Tactic:
simp [subNatNat_add]

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ ↑m + ↑n + ↑k = ↑m + (↑n + ↑k)

Tactic:
simp [Nat.add_assoc]

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ -[m+1] + -[n+1] + ↑k = -[m+1] + (-[n+1] + ↑k)

Tactic:
simp

Result:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (m + n + 1 + 1) = -[m+1] + subNatNat k (n + 1)

Proof state:
a : Int
n k : Nat
⊢ a + ↑n + ↑k = a + (↑n + ↑k)

Tactic:
rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]

Result:
no goals

Proof state:
m n k : Nat
⊢ -[m+1] + ↑n + -[k+1] = -[m+1] + (↑n + -[k+1])

Tactic:
rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]

Result:
no goals

Proof state:
m n k : Nat
⊢ ↑m + -[n+1] + -[k+1] = ↑m + (-[n+1] + -[k+1])

Tactic:
rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (m + n + 1 + 1) = -[m+1] + subNatNat k (n + 1)

Tactic:
rw [Int.add_comm, subNatNat_add_negSucc]

Result:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (m + n + 1 + 1) = subNatNat k (n + 1 + m.succ)

Proof state:
x✝² x✝¹ x✝ : Int
m n k : Nat
⊢ subNatNat k (m + n + 1 + 1) = subNatNat k (n + 1 + m.succ)

Tactic:
simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]

Result:
no goals

Proof state:
m : Nat
b : Int
k : Nat
⊢ ↑m + b + ↑k = ↑m + (b + ↑k)

Tactic:
rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
    coprodComparison F A B ≫ F.map (coprod.map f g) =
      coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'

Tactic:
rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
  coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.linearCombination R b v :=
  calc
    b.repr.symm v = b.repr.symm (v.sum Finsupp.single)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr.symm v = b.repr.symm (v.sum single)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ (v.sum fun i vi => b.repr.symm (single i vi)) = (linearCombination R ⇑b) v

Tactic:
simp only [repr_symm_single,
           Finsupp.linearCombination_apply]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_mul_oreDiv_comm {r₁ r₂ : R} {s₁ s₂ : S} :
    r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ ↑s₂ * r₁ = r₁ * ↑s₂

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

Tactic:
rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_self : or o o = o

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ o.or o = o

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_concat (a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ (l ++ [a]).maximum = l.maximum ⊔ ↑a

Tactic:
simp only [maximum, argmax_concat, id]

Result:
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (argmax id l) = argmax id l ⊔ ↑a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (argmax id l) = argmax id l ⊔ ↑a

Tactic:
cases argmax id l

Result:
case none
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) none = none ⊔ ↑a

case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (some val✝) = some val✝ ⊔ ↑a

Proof state:
case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (some val✝) = some val✝ ⊔ ↑a

Tactic:
simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

Result:
no goals

Proof state:
case none
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) none = none ⊔ ↑a

Tactic:
exact (max_eq_right bot_le).symm

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
@[simp]
lemma toFinite_zero : Measure.toFinite (0 : Measure α) = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
⊢ Measure.toFinite 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem mutuallySingular_singularPart (s : SignedMeasure α) (μ : Measure α) :
    singularPart s μ ⟂ᵥ μ.toENNRealVectorMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.singularPart μ ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [mutuallySingular_ennreal_iff, singularPart_totalVariation,
  VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ

Tactic:
exact (mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_pair : diam ({x, y} : Set α) = edist x y

Proof state:
α : Type u_1
x y : α
inst✝ : PseudoEMetricSpace α
⊢ diam {x, y} = edist x y

Tactic:
simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem one_eq [Nontrivial A] : σ (1 : A) = {1} :=
  calc
    σ (1 : A) = σ (↑ₐ 1)

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (↑ₐ 1)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, one_smul]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma eq_one_or_neg_one_of_mul_eq_neg_one' (h : u * v = -1) : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Proof state:
case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Tactic:
simpa [Int.neg_mul] using h

Result:
no goals

Proof state:
u v : ℤ
h : u * v = -1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1

Result:
case inl
v : ℤ
h : 1 * v = -1
⊢ 1 = 1 ∧ v = -1 ∨ 1 = -1 ∧ v = 1

case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Proof state:
case inl
v : ℤ
h : 1 * v = -1
⊢ 1 = 1 ∧ v = -1 ∨ 1 = -1 ∧ v = 1

Tactic:
exact Or.inl ⟨rfl, one_mul v ▸ h⟩

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_sup [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p q : Seminorm 𝕜 E) :
    r • (p ⊔ q) = r • p ⊔ r • q :=
  have real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => real.smul_max _ _

Proof state:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : SeminormedRing 𝕜
inst✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x y : ℝ
⊢ r • (x ⊔ y) = r • x ⊔ r • y

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_isSome {xs : Array α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (find? p { toList := toList✝ }).isSome = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (find? p { toList := toList✝ }).isSome = true ↔ ∃ x, x ∈ { toList := toList✝ } ∧ p x = true
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprodXIso_hom_snd (i : ι) :
    (biprodXIso K L i).hom ≫ biprod.snd = (biprod.snd : K ⊞ L ⟶ L).f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.snd = biprod.snd.f i

Tactic:
simp [biprodXIso]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(-π / 2)) : ∠ p₃ p₂ p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
exact angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₃ p₂ p₁ = π / 2

Tactic:
rw [angle_comm]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem incl_range (s : AddSubgroup V₁) : (incl s).range = s

Proof state:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ (incl s).toAddMonoidHom y ∈ s

Tactic:
simp

Result:
no goals

Proof state:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
hx : x ∈ s
⊢ (incl s).toAddMonoidHom ⟨x, hx⟩ = x

Tactic:
simp

Result:
no goals

Proof state:
case h
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
⊢ x ∈ (incl s).range ↔ x ∈ s

Tactic:
exact ⟨fun ⟨y, hy⟩ => by rw [← hy]; simp, fun hx => ⟨⟨x, hx⟩, by simp⟩⟩

Result:
no goals

Proof state:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ x ∈ s

Tactic:
rw [← hy]

Result:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ (incl s).toAddMonoidHom y ∈ s

Proof state:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
⊢ (incl s).range = s

Tactic:
ext x

Result:
case h
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
⊢ x ∈ (incl s).range ↔ x ∈ s
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) :
    (𝓕 fun (x : ℝ) ↦ cexp (-π * b * x ^ 2)) =
    fun t : ℝ ↦ 1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * t ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * ↑t ^ 2)

Tactic:
simpa only [mul_zero, zero_mul, add_zero] using fourierIntegral_gaussian_pi' hb 0

Result:
no goals