harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
@[simp, reassoc]
lemma Spec.preimage_comp {R S T : CommRingCat} (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec T) :
    Spec.preimage (f ≫ g) = Spec.preimage g ≫ Spec.preimage f :=
  Spec.map_injective (by simp)

Proof state:
R S T : CommRingCat
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec T
⊢ map (preimage (f ≫ g)) = map (preimage g ≫ preimage f)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_lt_iff_lt_one_left [MulPosStrictMono α] [MulPosReflectLT α] (b0 : 0 < b) :
    a * b < b ↔ a < 1 :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_right b0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
b0 : 0 < b
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem lin_1 (l k r) : a k l * (newBasis K) r =
    ∑ u, (a' K a k l r u) * (newBasis K) u

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
l : β
k : α
r : K →+* ℂ
⊢ a k l * (NumberField.house.newBasis K) r =
    ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u

Tactic:
simp only [Basis.sum_repr (newBasis K) (a k l * (newBasis K) r), a', ← zsmul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_natTrailingDegree (hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) :
    n ≤ p.natTrailingDegree

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' hp]

Result:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯

Tactic:
exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.any p = l.any p

Tactic:
rw [any_toList]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_C_mul_X (a : R) (ha : a ≠ 0) : natDegree (C a * X) = 1

Proof state:
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X).natDegree = 1

Tactic:
simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_mkVector_of_pos (h : 0 < n) : findSome? f (mkVector n a) = f a

Proof state:
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
h : 0 < n
⊢ findSome? f (mkVector n a) = f a

Tactic:
simp [findSome?_mkVector, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_one_const_right (f : ι → 𝕜) (a : 𝕜) :
    ⟪f, const _ a⟫_[𝕜] = (∑ i, conj (f i)) * a

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : ι → 𝕜
a : 𝕜
⊢ wInner 1 f (const ι a) = (∑ i : ι, (starRingEnd 𝕜) (f i)) * a

Tactic:
simp [wInner_one_eq_sum, sum_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.stronglyMeasurable_const_smul_iff {m : MeasurableSpace α} (c : G) :
    (StronglyMeasurable fun x => c • f x) ↔ StronglyMeasurable f :=
  ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, fun h => h.const_smul c⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
G : Type u_6
inst✝³ : TopologicalSpace β
inst✝² : Group G
inst✝¹ : MulAction G β
inst✝ : ContinuousConstSMul G β
m : MeasurableSpace α
c : G
h : StronglyMeasurable fun x => c • f x
⊢ StronglyMeasurable f

Tactic:
simpa only [inv_smul_smul] using h.const_smul' c⁻¹

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem braid_natural [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
    prod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ prod.map f g ≫ (prod.braiding Y W).hom = (prod.braiding X Z).hom ≫ prod.map g f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem limZero_sub_rev {f g : CauSeq β abv} (hfg : LimZero (f - g)) : LimZero (g - f)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hfg : (f - g).LimZero
⊢ (g - f).LimZero

Tactic:
simpa using neg_limZero hfg

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq_add_sin_sq : cos x ^ 2 + sin x ^ 2 = 1

Proof state:
x : ℂ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
rw [add_comm, sin_sq_add_cos_sq]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x

Tactic:
simp [one_eq_range]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_snd_fst_fst (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.fst (𝒰.map j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
  pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
  pullbackRightPullbackFstIso_hom_fst_assoc]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_nonempty : s.offDiag.Nonempty ↔ s.Nontrivial

Proof state:
α : Type u_1
s : Set α
⊢ s.offDiag.Nonempty ↔ s.Nontrivial

Tactic:
simp [offDiag, Set.Nonempty, Set.Nontrivial]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frequently_nhds_iff {p : X → Prop} :
    (∃ᶠ y in 𝓝 x, p y) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ y ∈ U, p y :=
  (nhds_basis_opens x).frequently_iff.trans <| by simp

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
p : X → Prop
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen i → ∃ x ∈ i, p x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Constructions.lean
theorem continuous_iff {f : X → Mˣ} :
    Continuous f ↔ Continuous (val ∘ f) ∧ Continuous (fun x => ↑(f x)⁻¹ : X → M)

Proof state:
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
f : X → Mˣ
⊢ Continuous f ↔ Continuous (val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹

Tactic:
simp only [isInducing_embedProduct.continuous_iff, embedProduct_apply, Function.comp_def,
  continuous_prod_mk, opHomeomorph.symm.isInducing.continuous_iff, opHomeomorph_symm_apply,
  unop_op]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_sin_ofReal_re (x : ℝ) : ((sin x).re : ℂ) = sin x :=
  conj_eq_iff_re.1 <| by rw [← sin_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (sin ↑x) = sin ↑x

Tactic:
rw [← sin_conj, conj_ofReal]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem factorization_mul {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
    factorization (a * b) = factorization a + factorization b

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (a * b) = factorization a + factorization b

Tactic:
simp [factorization, normalizedFactors_mul ha hb]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem ite_and : ite (P ∧ Q) a b = ite P (ite Q a b) b

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem coe_linear_mk (f : M →ₗ[R] N) (h) : ((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M →ₗ[R] N) = f

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M →ₗ[R] N
h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆
⊢ ↑{ toLinearMap := f, map_lie' := h } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supportedEquivFinsupp_symm_apply_coe (s : Set α) [DecidablePred (· ∈ s)]
    (f : s →₀ M) : (supportedEquivFinsupp (R := R) s).symm f = f.extendDomain

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f : ↑s →₀ M
⊢ ↑((supportedEquivFinsupp s).symm f) = f.extendDomain

Tactic:
convert restrictSupportEquiv_symm_apply_coe ..

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_dvd_of_dvd_div (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b :=
  have ⟨d, hd⟩ := h
  ⟨d, by simpa [Nat.mul_comm, Nat.mul_left_comm] using Nat.eq_mul_of_div_eq_left hcb hd⟩

Proof state:
a b c : ℕ
hcb : c ∣ b
h : a ∣ b / c
d : ℕ
hd : b / c = a * d
⊢ b = c * a * d

Tactic:
simpa [Nat.mul_comm, Nat.mul_left_comm] using Nat.eq_mul_of_div_eq_left hcb hd

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem nextn_stop : ∀ {s}, Valid s → ∀ n, s.nextn n ⟨s.bsize⟩ = ⟨s.bsize⟩
  | _, h, n => let ⟨l, m, r, h⟩ := h.validFor; by simp [h.bsize, h.nextn_stop]

Proof state:
x✝ : Substring
h✝ : x✝.Valid
n : Nat
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.nextn n { byteIdx := x✝.bsize } = { byteIdx := x✝.bsize }

Tactic:
simp [h.bsize, h.nextn_stop]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem factorization_eq_count {n p : α} :
    factorization n p = Multiset.count p (normalizedFactors n)

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n p : α
⊢ (factorization n) p = Multiset.count p (normalizedFactors n)

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_ite {p : Prop} [Decidable p] :
    (if p then some b else none).isSome = true ↔ p

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
⊢ (if p then some b else none).isSome = true ↔ p

Tactic:
split <;> simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesCoimage.hom_coimageImageComparison :
    (PreservesCoimage.iso F f).hom ≫ coimageImageComparison (F.map f) =
      F.map (coimageImageComparison f) ≫ (PreservesImage.iso F f).hom

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (iso F f).hom ≫ coimageImageComparison (F.map f) = F.map (coimageImageComparison f) ≫ (PreservesImage.iso F f).hom

Tactic:
simp [← Functor.map_comp, ← Iso.eq_inv_comp, ← cancel_epi (Abelian.coimage.π (F.map f)),
  ← cancel_mono (Abelian.image.ι (F.map f))]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mulEquivOfQuotient_monoidOf (x) :
    mulEquivOfQuotient f ((monoidOf S).toMap x) = f.toMap x

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ (mulEquivOfQuotient f) ((monoidOf S).toMap x) = f.toMap x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem StrictMono.div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α}
    (hc : 0 < c) : StrictMono fun x => f x / c

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono fun x => f x / c

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem neg_dotProduct : -v ⬝ᵥ w = -(v ⬝ᵥ w)

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ w = -(v ⬝ᵥ w)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
    (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G

Proof state:
α : Type u_1
β : Type u_2
l : List α
acc : Array β
G : α → β
⊢ (List.foldl (fun acc a => acc.push (G a)) acc l).toList = acc.toList ++ List.map G l

Tactic:
induction l generalizing acc <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasBasis_nhds_of_ne_top (xt : x ≠ ∞) :
    (𝓝 x).HasBasis (0 < ·) (fun ε => Icc (x - ε) (x + ε))

Proof state:
x : ℝ≥0∞
xt : x ≠ ⊤
⊢ (𝓝 x).HasBasis (fun x => 0 < x) fun ε => Icc (x - ε) (x + ε)

Tactic:
simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_himp_self_right (a b : α) : a ⊔ b ⇨ b = a ⇨ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ b = a ⇨ b

Tactic:
rw [sup_himp_distrib, himp_self, inf_top_eq]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.move_right_mk' {Γ} [Inhabited Γ] (L R : ListBlank Γ) :
    (Tape.mk' L R).move Dir.right = Tape.mk' (L.cons R.head) R.tail

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.right (mk' L R) = mk' (ListBlank.cons R.head L) R.tail

Tactic:
simp only [Tape.move, Tape.mk', ListBlank.head_cons, eq_self_iff_true, ListBlank.cons_head_tail,
  and_self_iff, ListBlank.tail_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsertIfNew_fst_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α}
    {b : β a} : (m.containsThenInsertIfNew a b).1 =
      (Raw₀.containsThenInsertIfNew ⟨m, h.size_buckets_pos⟩ a b).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.containsThenInsertIfNew a b).fst = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).fst

Tactic:
simp [Raw.containsThenInsertIfNew, h.size_buckets_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_umod {x : BitVec w} : (0#w) % x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ 0#w % x = 0#w

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem card_le_mul_card_image_of_maps_to {f : α → β} {s : Finset α} {t : Finset β}
    (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, #{a ∈ s | f a = b} ≤ n) : #s ≤ n * #t :=
  calc
    #s = ∑ b ∈ t, #{a ∈ s | f a = b} := card_eq_sum_card_fiberwise Hf
    _ ≤ ∑ _b ∈ t, n := sum_le_sum hn
    _ = _

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, #(filter (fun a => f a = b) s) ≤ n
⊢ ∑ _b ∈ t, n = n * #t

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
@[simp]
lemma volume_closedBall_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ 3 * .ofReal (π * 4 / 3)

Proof state:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (π * 4 / 3)

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_three x]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem smulTower_leftMulMatrix_algebraMap_ne (x : S) (i j) {k k'} (h : k ≠ k') :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k') = 0

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k k' : n
h : k ≠ k'
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0

Tactic:
rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem self_le_sinh_iff : x ≤ sinh x ↔ 0 ≤ x :=
  calc
    x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Proof state:
x : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma setLIntegral_smul_measure (c : ℝ≥0∞) (f : α → ℝ≥0∞) (s : Set α) :
    ∫⁻ a in s, f a ∂(c • μ) = c * ∫⁻ a in s, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂c • μ = c * ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [Measure.restrict_smul, lintegral_smul_measure]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_eq_betaIntegral_of_re_pos {s : ℂ} (hs : 0 < re s) (n : ℕ) :
    GammaSeq s n = (n : ℂ) ^ s * betaIntegral s (n + 1)

Proof state:
s : ℂ
hs : 0 < s.re
n : ℕ
⊢ s.GammaSeq n = ↑n ^ s * s.betaIntegral (↑n + 1)

Tactic:
rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem OuterMeasure.coe_mkMetric [MeasurableSpace X] [BorelSpace X] (m : ℝ≥0∞ → ℝ≥0∞) :
    ⇑(OuterMeasure.mkMetric m : OuterMeasure X) = Measure.mkMetric m

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ ⇑(mkMetric m) = ⇑(Measure.mkMetric m)

Tactic:
rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_dblZ (P : Fin 3 → A) : (W'.baseChange B).toJacobian.dblZ (f ∘ P) =
    f ((W'.baseChange A).toJacobian.dblZ P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.dblZ (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblZ P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblZ, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem one_mem_div_iff : (1 : α) ∈ s / t ↔ ¬Disjoint s t

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem Iio_mem_nhdsSet_Ico (h : b ≤ c) : Iio c ∈ 𝓝ˢ (Ico a b) :=
  nhdsSet_mono Ico_subset_Iio_self <| by simpa

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c : α
h : b ≤ c
⊢ Iio c ∈ 𝓝ˢ (Iio b)

Tactic:
simpa

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsMatching.toEdge_eq_toEdge_of_adj (h : M.IsMatching)
    (hv : v ∈ M.verts) (hw : w ∈ M.verts) (ha : M.Adj v w) :
    h.toEdge ⟨v, hv⟩ = h.toEdge ⟨w, hw⟩

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hw : w ∈ M.verts
ha : M.Adj v w
⊢ h.toEdge ⟨v, hv⟩ = h.toEdge ⟨w, hw⟩

Tactic:
rw [h.toEdge_eq_of_adj hv ha, h.toEdge_eq_of_adj hw (M.symm ha), Subtype.mk_eq_mk, Sym2.eq_swap]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
theorem _root_.SemiconjBy.tprod {a₁ a₂ a₃ : Π i, A i}
    (ha : SemiconjBy a₁ a₂ a₃) :
    SemiconjBy (tprod R a₁) (tprod R a₂) (tprod R a₃)

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
a₁ a₂ a₃ : (i : ι) → A i
ha : SemiconjBy a₁ a₂ a₃
⊢ SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)

Tactic:
rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_append (a : Vector α m) (b : Vector α n) :
    (a ++ b).toList = a.toList ++ b.toList

Proof state:
α : Type u_1
m n : Nat
a : Vector α m
b : Vector α n
⊢ (a ++ b).toList = a.toList ++ b.toList

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma image_comp (g : F' ⟶ F'') :
    G.image (f ≫ g) = (G.image f).image g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : F ⟶ F'
g : F' ⟶ F''
⊢ G.image (f ≫ g) = (G.image f).image g

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/ModN.lean
@[simp] lemma natCard_eq : Nat.card (ModN G n) = n ^ Module.finrank ℤ G

Proof state:
G : Type u_1
inst✝³ : AddCommGroup G
n : ℕ
inst✝² : NeZero n
inst✝¹ : Module.Free ℤ G
inst✝ : Module.Finite ℤ G
⊢ Nat.card (ModN G n) = n ^ Module.finrank ℤ G

Tactic:
simp [Nat.card_congr (basis <| Module.Free.chooseBasis ℤ G).repr.toEquiv,
  Nat.card_eq_fintype_card, Module.finrank_eq_card_chooseBasisIndex]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardDistinctFactors_apply_prime {p : ℕ} (hp : p.Prime) : ω p = 1

Proof state:
p : ℕ
hp : Nat.Prime p
⊢ ω p = 1

Tactic:
rw [← pow_one p, cardDistinctFactors_apply_prime_pow hp one_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_mkArray_of_neg (w : stop = n) (h : ¬ p a) :
    (mkArray n a).filter p 0 stop = #[]

Proof state:
stop n : Nat
α✝ : Type u_1
p : α✝ → Bool
a : α✝
w : stop = n
h : ¬p a = true
⊢ filter p (mkArray n a) 0 stop = #[]

Tactic:
simp [filter_mkArray, h, w]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Filter.EventuallyEq.fderiv_eq (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ x = fderiv 𝕜 f 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
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
⊢ fderiv 𝕜 f₁ x = fderiv 𝕜 f x

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_nhds]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_preΨ (n : ℤ) : (W.baseChange B).preΨ n = ((W.baseChange A).preΨ n).map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).preΨ n = Polynomial.map (↑f) ((W.baseChange A).preΨ n)

Tactic:
rw [← map_preΨ, map_baseChange]

Result:
no goals