harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_hasFDerivWithinAt_iff' {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivWithinAt (f ∘ iso) f' (iso ⁻¹' s) x ↔
      HasFDerivWithinAt f (f'.comp (iso.symm : F →L[𝕜] E)) s (iso x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp ↑iso.symm) s (iso x)

Tactic:
rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
  iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1

Proof state:
n : Nat
⊢ (iota n).reverse.head? = if n = 0 then none else some 1

Tactic:
simp [head?_range']

Result:
no goals

Proof state:
n : Nat
⊢ (iota n).getLast? = if n = 0 then none else some 1

Tactic:
rw [getLast?_eq_head?_reverse]

Result:
n : Nat
⊢ (iota n).reverse.head? = if n = 0 then none else some 1
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_min_iff (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) :
    MeasurableSet[(hτ.min hπ).measurableSpace] s ↔
      MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    a ∈ m → get? m a = some (get! m a)

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ a ∈ m → get? m a = some (get! m a)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma card_insertNthEquiv_filter_piFinset (P : (∀ i, α (p.succAbove i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (p.removeNth r)}.card =
      (S p).card * {r ∈ piFinset (p.removeNth  S) | P r}.card

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ #(filter (fun r => P (p.removeNth r)) (piFinset S)) = #(S p) * #(filter (fun r => P r) (piFinset (p.removeNth S)))

Tactic:
rw [← card_product, ← map_insertNthEquiv_filter_piFinset, card_map]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion₂_subset_iff {s : ∀ i, κ i → Set α} {t : Set α} :
    ⋃ (i) (j), s i j ⊆ t ↔ ∀ i j, s i j ⊆ t

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
simp_rw [iUnion_subset_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
@[simp]
lemma Spec.map_eq_id {R : CommRingCat} {ϕ : R ⟶ R} : Spec.map ϕ = 𝟙 (Spec R) ↔ ϕ = 𝟙 R

Proof state:
R : CommRingCat
ϕ : R ⟶ R
⊢ map ϕ = 𝟙 (Spec R) ↔ ϕ = 𝟙 R

Tactic:
simp [← map_inj]

Result:
no goals
-- Mathlib/Order/Category/Lat.lean
lemma inv_hom_apply {X Y : Lat} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : Lat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_lt_of_lt_mul (h : a < b * c) : a / c < b :=
  mul_lt_of_lt_div <| by rwa [div_eq_mul_inv, inv_inv]

Proof state:
a b c : ℝ≥0∞
h : a < b * c
⊢ a < b / c⁻¹

Tactic:
rwa [div_eq_mul_inv, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ico_add_one_right_eq_Icc (a b : α) : Ico a (b + 1) = Icc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using  Ico_succ_right_eq_Icc a b

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem oangle_center_eq_two_zsmul_oangle {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) :
    ∡ p₁ s.center p₃ = (2 : ℤ) • ∡ p₁ p₂ p₃

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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃

Tactic:
rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃] <;>
  simp [hp₂p₁, hp₂p₃]

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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

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)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_nodal [Nontrivial R] : (nodal s v).degree = #s

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ (nodal s v).degree = ↑(#s)

Tactic:
simp_rw [degree_eq_natDegree nodal_ne_zero, natDegree_nodal]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem isManifold_of_contDiffOn {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*)
    [TopologicalSpace M] [ChartedSpace H M]
    (h : ∀ e e' : PartialHomeomorph M H, e ∈ atlas H M → e' ∈ atlas H M →
      ContDiffOn 𝕜 n (I ∘ e.symm ≫ₕ e' ∘ I.symm) (I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I)) :
    IsManifold I n M where
  compatible

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : PartialHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
⊢ ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
haveI : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (h _ _)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : PartialHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
this : HasGroupoid M (contDiffGroupoid n I)
⊢ ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : PartialHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
this : HasGroupoid M (contDiffGroupoid n I)
⊢ ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
apply StructureGroupoid.compatible

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gauge_gaugeRescale' (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) :
    gauge t (gaugeRescale s t x) = gauge s x

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
  smul_eq_mul, div_mul_cancel₀ _ hx]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_ssubset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Set.Subsingleton.closure [T1Space X] {s : Set X} (hs : s.Subsingleton) :
    (closure s).Subsingleton

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Subsingleton
⊢ (_root_.closure s).Subsingleton

Tactic:
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩) <;> simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_pow_left {n : ℕ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y

Tactic:
rw [← zpow_natCast, sameCycle_zpow_left]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem prod_divisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
    (∏ x ∈ (p ^ k).divisors, f x) = ∏ x ∈ range (k + 1), f (p ^ x)

Proof state:
α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ range (k + 1), f (p ^ x)

Tactic:
simp [h, divisors_prime_pow]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem isNilpotent_mulRight_iff (a : A) : IsNilpotent (mulRight R a) ↔ IsNilpotent a

Proof state:
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a

Tactic:
constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
    simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢ <;>
  exact hn

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem strongRec_eq {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n → motive m) → motive n)
    (t : Nat) : Nat.strongRec ind t = ind t fun m _ => Nat.strongRec ind m

Proof state:
motive : Nat → Sort u_1
ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n
t : Nat
⊢ Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m

Tactic:
conv => lhs; unfold Nat.strongRec

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem rhs_get_cast {aig1 aig2 : AIG α} (s : BinaryRefVec aig1 len) (idx : Nat)
    (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).rhs.get idx hidx
      =
    (s.rhs.get idx hidx).cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig1 aig2 : AIG α
s : aig1.BinaryRefVec len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).rhs.get idx hidx = (s.rhs.get idx hidx).cast hcast

Tactic:
simp [cast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_sub_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)}
    (h₁ : m.contains k) (h₂ : (f (m.get? k)).isNone) :
    (m.alter k f).1.size = m.1.size - 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h₁ : m.contains k = true
h₂ : (f (m.get? k)).isNone = true
⊢ (m.alter k f).val.size = m.val.size - 1

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1

Proof state:
⊢ ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1

Tactic:
simp [le_succ_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_C_mul_T_n (n : ℤ) (r : R) : (C r * T n).smeval x = r • (x ^ n).val

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ (C r * T n).smeval x = r • ↑(x ^ n)

Tactic:
rw [← single_eq_C_mul_T, smeval_single]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_id' (l : Array (Array α)) : l.flatMap (fun a => a) = l.flatten

Proof state:
α : Type u_1
l : Array (Array α)
⊢ flatMap (fun a => a) l = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/Order/Category/BddLat.lean
lemma comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : Lat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
lemma prop_isoClosure_iff (X : C) :
    isoClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X ↔ ∃ Y x, Nonempty (X ≅ Y)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Baire/Lemmas.lean
theorem nonempty_interior_of_iUnion_of_closed [Nonempty X] [Countable ι] {f : ι → Set X}
    (hc : ∀ i, IsClosed (f i)) (hU : ⋃ i, f i = univ) : ∃ i, (interior <| f i).Nonempty

Proof state:
X : Type u_1
ι : Sort u_3
inst✝³ : TopologicalSpace X
inst✝² : BaireSpace X
inst✝¹ : Nonempty X
inst✝ : Countable ι
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : ⋃ i, f i = univ
⊢ ∃ i, (interior (f i)).Nonempty

Tactic:
simpa using (dense_iUnion_interior_of_closed hc hU).nonempty

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_affineSegment (x y : P) : μH[1] (affineSegment ℝ x y) = edist x y

Proof state:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ μH[1] (affineSegment ℝ x y) = edist x y

Tactic:
rw [affineSegment, hausdorffMeasure_lineMap_image, hausdorffMeasure_real, Real.volume_Icc,
  sub_zero, ENNReal.ofReal_one, ← Algebra.algebraMap_eq_smul_one]

Result:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ (algebraMap ℝ≥0 ℝ≥0∞) (nndist x y) = edist x y

Proof state:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ (algebraMap ℝ≥0 ℝ≥0∞) (nndist x y) = edist x y

Tactic:
exact (edist_nndist _ _).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
    tailD (map f l) (map f l') = map f (tailD l l')

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l l' : List α
⊢ (map f l).tailD (map f l') = map f (l.tailD l')

Tactic:
simp [← map_tail?]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem sInf_empty : sInf (∅ : Set ℝ≥0) = 0

Proof state:
⊢ sInf ∅ = 0

Tactic:
rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat)

Proof state:
x y : Nat
⊢ ↑(x >>> y) = ↑x / ↑(2 ^ y)

Tactic:
simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_insert' (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f) {i : δ}
    (hi : i ∉ s) :
    ∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i) ∂μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
⊢ ∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i ∂μ

Tactic:
rw [Finset.insert_eq, Finset.union_comm,
  lmarginal_union (s := s) μ f hf (Finset.disjoint_singleton_right.mpr hi), lmarginal_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/NatTrans.lean
theorem congr_app {F G : C ⥤ D} {α β : NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : NatTrans F G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem separatingRight_iff_linear_flip_nontrivial {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.SeparatingRight ↔ ∀ y : M₂, B.flip y = 0 → y = 0

Proof state:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingRight ↔ ∀ (y : M₂), B.flip y = 0 → y = 0

Tactic:
rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem mem_annihilator_span_singleton (g : M) (r : R) :
    r ∈ (Submodule.span R ({g} : Set M)).annihilator ↔ r • g = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
r : R
⊢ r ∈ (span R {g}).annihilator ↔ r • g = 0

Tactic:
simp [mem_annihilator_span]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2

Proof state:
x : ℂ
⊢ cos (2 * x) = cos x ^ 2 - sin x ^ 2

Tactic:
rw [two_mul, cos_add, ← sq, ← sq]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem _root_.PrimrecPred.not {p : α → Prop} [DecidablePred p] (hp : PrimrecPred p) :
    PrimrecPred fun a => ¬p a :=
  (Primrec.not.comp hp).of_eq fun n => by simp

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
n : α
⊢ (!decide (p n)) = decide ((fun a => ¬p a) n)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Category/BoolAlg.lean
lemma inv_hom_apply {X Y : BoolAlg} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : BoolAlg
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ1728_j [Fact (IsUnit (2 : R))] : (ofJ1728 R).j = 1728

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (ofJ1728 R).j = 1728

Tactic:
rw [j, Units.inv_mul_eq_iff_eq_mul, ofJ1728_c₄, coe_Δ', ofJ1728_Δ]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = -64 * 1728

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = -64 * 1728

Tactic:
norm_num1

Result:
no goals
-- Mathlib/Topology/Algebra/MulAction.lean
/-- The stabilizer of a continuous group action on a discrete space is an open subgroup. -/
lemma stabilizer_isOpen [DiscreteTopology X] (x : X) : IsOpen (MulAction.stabilizer M x : Set M) :=
  IsOpen.preimage (f := fun g ↦ g • x) (by fun_prop) (isOpen_discrete {x})

Proof state:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : MulAction M X
inst✝¹ : ContinuousSMul M X
inst✝ : DiscreteTopology X
x : X
⊢ Continuous fun g => g • x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
theorem m_le_card_of_mem_chunk_parts (hs : s ∈ (chunk hP G ε hU).parts) : m ≤ #s :=
  (card_eq_of_mem_parts_chunk hs).elim ge_of_eq fun i => by simp [i]

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
i : #s = m + 1
⊢ m ≤ #s

Tactic:
simp [i]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem natSize_to_nat (n) : natSize n = Nat.size n

Proof state:
n : Num
⊢ n.natSize = (↑n).size

Tactic:
rw [← size_eq_natSize, size_to_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_self {n : Nat} : testBit (2 ^ n) n = true

Proof state:
n : Nat
⊢ (2 ^ n).testBit n = true

Tactic:
simp [testBit_two_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem one_div_two : 1/2 = 0

Proof state:
⊢ 1 / 2 = 0

Tactic:
trivial

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_right_eq_self₀ : a * b = a ↔ b = 1 ∨ a = 0 :=
  calc
    a * b = a ↔ a * b = a * 1

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
⊢ a * b = a ↔ a * b = a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_norm_iff {f : α → β} (hf : AEStronglyMeasurable f μ) :
    Integrable (fun a => ‖f a‖) μ ↔ Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Integrable (fun a => ‖f a‖) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
    ∫ v : ι → ℝ, cexp (- b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i)
      = (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp ((∑ i, c i ^ 2) / (4 * b))

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i : ι, c i ^ 2) / (4 * b))

Tactic:
simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
  Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
  Finset.sum_div, div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem eq_some_iff_get_eq : o = some a ↔ ∃ h : o.isSome, o.get h = a

Proof state:
α✝ : Type u_1
o : Option α✝
a : α✝
⊢ o = some a ↔ ∃ h, o.get h = a

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} :
    m.contains a = false → m.get? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
⊢ m.contains a = false → m.get? a = none

Tactic:
simp_to_raw using Raw₀.get?_eq_none

Result:
no goals