harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LaurentSeries.lean
theorem hasseDeriv_zero : hasseDeriv R 0 = LinearMap.id (M := LaurentSeries V)

Proof state:
case h.coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R 0) f).coeff n = (LinearMap.id f).coeff n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
⊢ hasseDeriv R 0 = LinearMap.id

Tactic:
ext f n

Result:
case h.coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R 0) f).coeff n = (LinearMap.id f).coeff n
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem of_normalize_eq {f g f' : a ⟶ b} {η θ : f ≅ g} (η_f : 𝟙 a ≫ f ≅ f') (η_g : 𝟙 a ≫ g ≅ f')
    (h_η : 𝟙 a ◁ η ≪≫ η_g = η_f)
    (h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f) : η = θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_η)]

Result:
no goals

Proof state:
case w
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom

Tactic:
calc
  η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
    simp [← reassoc_of% (congrArg Iso.hom h_η)]
  _ = θ.hom := by
    simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
apply Iso.ext

Result:
case w
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive (attr := simp)]
lemma locallyLipschitz_inv_iff : LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f : α → E
⊢ LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

Tactic:
simp [LocallyLipschitz]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma inf_imp_left (φ ψ : L.BoundedFormula α n) : φ ⊓ ψ ⟹[T] φ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact And.left

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ψ ⟹ φ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs

Tactic:
exact And.left

Result:
no goals
-- Mathlib/SetTheory/Cardinal/UnivLE.lean
theorem univLE_iff_exists_embedding : UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Proof state:
⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
rw [univLE_iff_cardinal_le]

Result:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Proof state:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
exact lift_mk_le'

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}}
    (h : IsLimit o) : (Ordinal.bsup.{_, v} o fun x _ => f x) = f o

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : o.IsLimit
⊢ (o.bsup fun x x_1 => f x) = f o

Tactic:
rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma dual_inv :
    dual A K I⁻¹ = dual A K 1 * I

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K I⁻¹ = dual A K 1 * I

Tactic:
rw [dual_eq_mul_inv, inv_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_empty : nodal ∅ v = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
v : ι → R
⊢ nodal ∅ v = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_polynomialY : (W'.map f).toJacobian.polynomialY = MvPolynomial.map f W'.polynomialY

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem sub_mem_Ioo_zero_iff_right : b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

Tactic:
simp only [sub_mem_Ioo_iff_right, sub_self, sub_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_xor_distrib_right {a b c : Nat} : (a ^^^ b) &&& c = (a &&& c) ^^^ (b &&& c)

Proof state:
a b c : Nat
⊢ (a ^^^ b) &&& c = a &&& c ^^^ b &&& c

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
a b c : Nat
⊢ ∀ (i : Nat), ((a ^^^ b) &&& c).testBit i = (a &&& c ^^^ b &&& c).testBit i

Proof state:
case pred
a b c : Nat
⊢ ∀ (i : Nat), ((a ^^^ b) &&& c).testBit i = (a &&& c ^^^ b &&& c).testBit i

Tactic:
simp [Bool.and_xor_distrib_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma pow_rootMultiplicity_not_dvd (p0 : p ≠ 0) (a : R) :
    ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
rw [← rootMultiplicity_le_iff p0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.get!_eq [BEq α] [Hashable α] [Inhabited β] {m : Raw α (fun _ => β)} (h : m.WF)
    {a : α} : Raw.Const.get! m a = Raw₀.Const.get! ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited β
m : Raw α fun x => β
h : m.WF
a : α
⊢ Raw.Const.get! m a = Raw₀.Const.get! ⟨m, ⋯⟩ a

Tactic:
simp [Raw.Const.get!, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem MapsTo.coe_iterate_restrict {f : α → α} (h : MapsTo f s s) (x : s) (k : ℕ) :
    h.restrict^[k] x = f^[k] x

Proof state:
case succ
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
ih : ↑((restrict f s s h)^[k] x) = f^[k] ↑x
⊢ ↑((restrict f s s h)^[k + 1] x) = f^[k + 1] ↑x

Tactic:
simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
⊢ ↑((restrict f s s h)^[0] x) = f^[0] ↑x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
⊢ ↑((restrict f s s h)^[k] x) = f^[k] ↑x

Tactic:
induction k with
| zero => simp
| succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma bi_min_div_two_pos : 0 < b (min_bi b) / 2 := div_pos (R.b_pos _) (by norm_num)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Set/Enumerate.lean
theorem enumerate_eq_none_of_sel {s : Set α} (h : sel s = none) : ∀ {n}, enumerate sel s n = none
  | 0 => by simp [h, enumerate]
  | n + 1 => by simp [h, enumerate]

Proof state:
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none

Tactic:
simp [h, enumerate]

Result:
no goals

Proof state:
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none

Tactic:
simp [h, enumerate]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_isBasis'_iff : (freeOn E).IsBasis' I X ↔ I = X ∩ E

Proof state:
α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
  and_iff_left inter_subset_right]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
hι : Nonempty ι
a : α
⊢ ⨆ x, a = a

Tactic:
rw [iSup, range_const, csSup_singleton]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁

Proof state:
d₁ d₂ n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
simp_all [divInt_neg', Int.ofNat_eq_zero, Int.neg_eq_zero,
  mkRat_eq_iff, Int.neg_mul, Int.mul_neg, Int.eq_neg_comm, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
protected lemma isCompl_iff {p q : f.invtSubmodule} :
    IsCompl p q ↔ IsCompl (p : Submodule R M) (q : Submodule R M)

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ q ↔ IsCompl ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Result:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl ↑⟨p, hp⟩ ↑⟨q, hq⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ IsCompl p q ↔ IsCompl ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ q ↔ IsCompl ↑⟨p, hp⟩ ↑q

Proof state:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquiv_symm_mk' (x : R) (y : M) : (algEquiv M S Q).symm (mk' Q x y) = mk' S x y

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
x : R
y : ↥M
⊢ (algEquiv M S Q).symm (mk' Q x y) = mk' S x y

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
    (init : β) (f : Nat → β → m (ForInStep β)) :
    forIn r init f = forIn (List.range' r.start r.size r.step) init f

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : Nat → β → m (ForInStep β)
⊢ forIn r init f = forIn (List.range' r.start r.size r.step) init f

Tactic:
simp only [forIn, forIn'_eq_forIn'_range']

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piScalarRightHom_tmul (x : N) (f : ι → R) :
    piScalarRightHom R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x)

Proof state:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
j : ι
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) j = f j • x

Tactic:
simp [piScalarRightHom, piScalarRightHomBil]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun j => f j • x

Tactic:
ext j

Result:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
j : ι
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) j = f j • x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsertIfNew_fst_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    (m.val.containsThenInsertIfNew a b).1 = (m.containsThenInsertIfNew a b).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.containsThenInsertIfNew a b).fst = (m.containsThenInsertIfNew a b).fst

Tactic:
simp [Raw.containsThenInsertIfNew, m.2]

Result:
no goals
-- Mathlib/Topology/MetricSpace/DilationEquiv.lean
@[simp]
lemma map_cobounded (e : F) : map e (cobounded X) = cobounded Y

Proof state:
X : Type u_1
Y : Type u_2
F : Type u_3
inst✝³ : PseudoMetricSpace X
inst✝² : PseudoMetricSpace Y
inst✝¹ : EquivLike F X Y
inst✝ : DilationEquivClass F X Y
e : F
⊢ map (⇑e) (cobounded X) = cobounded Y

Tactic:
rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem volume_closedBall (x : EuclideanSpace ℝ ι) (r : ℝ) :
    volume (Metric.closedBall x r) = (.ofReal r) ^ card ι *
      .ofReal (sqrt π ^ card ι / Gamma (card ι / 2 + 1))

Proof state:
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
⊢ volume (Metric.closedBall x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, EuclideanSpace.volume_ball]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sq_sqrt (h : 0 ≤ x) : √x ^ 2 = x

Proof state:
x : ℝ
h : 0 ≤ x
⊢ √x ^ 2 = x

Tactic:
rw [sq, mul_self_sqrt h]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} : IsSt x r ↔ ∀ δ : ℝ, 0 < δ → |x - ↑r| < δ

Proof state:
x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ

Tactic:
simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, IsSt, and_comm, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.of_mapCocone (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F}
    [PreservesLimitsOfShape WalkingCospan G] [ReflectsColimitsOfShape J G]
    (hc : IsUniversalColimit (G.mapCocone c)) : IsUniversalColimit c :=
  fun F' c' α f h hα H ↦
    ⟨isColimitOfReflects _ (hc (G.mapCocone c') (whiskerRight α G) (G.map f)
    (by ext j; simpa using G.congr_map (NatTrans.congr_app h j))
    (hα.whiskerRight G) (fun j ↦ (H j).map G)).some⟩

Proof state:
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝¹ : PreservesLimitsOfShape WalkingCospan G
inst✝ : ReflectsColimitsOfShape J G
hc : IsUniversalColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ whiskerRight α G ≫ (G.mapCocone c).ι = (G.mapCocone c').ι ≫ (Functor.const J).map (G.map f)

Tactic:
ext j

Result:
case w.h
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝¹ : PreservesLimitsOfShape WalkingCospan G
inst✝ : ReflectsColimitsOfShape J G
hc : IsUniversalColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (Functor.const J).map (G.map f)).app j

Proof state:
case w.h
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝¹ : PreservesLimitsOfShape WalkingCospan G
inst✝ : ReflectsColimitsOfShape J G
hc : IsUniversalColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (Functor.const J).map (G.map f)).app j

Tactic:
simpa using G.congr_map (NatTrans.congr_app h j)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem _root_.MeasurableSpace.ae_induction_on_inter
    {α β : Type*} [MeasurableSpace β] {μ : Measure β}
    {C : β → Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α]
    (h_eq : m = MeasurableSpace.generateFrom s)
    (h_inter : IsPiSystem s) (h_empty : ∀ᵐ x ∂μ, C x ∅) (h_basic : ∀ᵐ x ∂μ, ∀ t ∈ s, C x t)
    (h_compl : ∀ᵐ x ∂μ, ∀ t, MeasurableSet t → C x t → C x tᶜ)
    (h_union : ∀ᵐ x ∂μ, ∀ f : ℕ → Set α,
        Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C x (f i)) → C x (⋃ i, f i)) :
    ∀ᵐ x ∂μ, ∀ ⦃t⦄, MeasurableSet t → C x t

Proof state:
α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
⊢ ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
  using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
    h_eq h_inter hx_empty hx_basic hx_compl hx_union

Result:
no goals
-- Mathlib/Data/Sign.lean
private lemma mul_assoc : ∀ (a b c : SignType), (a * b) * c = a * (b * c)

Proof state:
⊢ ∀ (a b c : SignType), a * b * c = a * (b * c)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem Emetric.exists_smooth_forall_closedBall_subset {M} [EMetricSpace M] [ChartedSpace H M]
    [IsManifold I ∞ M] [SigmaCompactSpace M] {K : ι → Set M} {U : ι → Set M}
    (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i)
    (hfin : LocallyFinite K) :
    ∃ δ : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯,
      (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i

Proof state:
ι : Type uι
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : FiniteDimensional ℝ E
M : Type u_1
inst✝³ : EMetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I ∞ M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i

Tactic:
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι M]
  using exists_smooth_forall_mem_convex_of_local_const I
    EMetric.exists_forall_closedBall_subset_aux₂
    (EMetric.exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem not_mem_neighborFinset_self : v ∉ G.neighborFinset v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ v ∉ G.neighborFinset v

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_neg [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) : (-M)ᴴ = -Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (-M)ᴴ i j = (-Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_lt_succ (hab : a < b) : succ a < succ b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
hab : a < b
⊢ succ a < succ b

Tactic:
simp [hab]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E)

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ comap norm (𝓝 0) = 𝓝 1

Tactic:
simpa only [dist_one_right] using nhds_comap_dist (1 : E)

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem sub {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x - y)

Proof state:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)

Tactic:
simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swapIfInBounds_mk (a : Array α) (h : a.size = n) (i j) :
    (Vector.mk a h).swapIfInBounds i j = Vector.mk (a.swapIfInBounds i j) (by simp [h]) := rfl

Proof state:
α : Type ?u.15855
n : Nat
a : Array α
h : a.size = n
i j : Nat
⊢ (a.swapIfInBounds i j).size = n

Tactic:
simp [h]

Result:
no goals