harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem map_fundamentalDomain {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) :
    f '' (fundamentalDomain b) = fundamentalDomain (b.map f)

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ ⇑f.toEquiv '' fundamentalDomain b

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ f.symm x = f.toEquiv.symm x

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
⊢ ⇑f '' fundamentalDomain b = fundamentalDomain (b.map f)

Tactic:
ext x

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ fundamentalDomain (b.map f)

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ fundamentalDomain (b.map f)

Tactic:
rw [mem_fundamentalDomain, Basis.map_repr, LinearEquiv.trans_apply, ← mem_fundamentalDomain,
  show f.symm x = f.toEquiv.symm x by rfl, ← Set.mem_image_equiv]

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ ⇑f.toEquiv '' fundamentalDomain b
-- Mathlib/Data/Set/Card.lean
theorem Nat.encard_range (k : ℕ) : {i | i < k}.encard = k

Proof state:
case h.e'_3
k : ℕ
⊢ ↑k = ↑(Finset.range k).card

Tactic:
rw [Finset.card_range]

Result:
no goals

Proof state:
case h.e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard

Tactic:
rw [Finset.coe_range, Iio_def]

Result:
no goals

Proof state:
k : ℕ
⊢ {i | i < k}.encard = ↑k

Tactic:
convert encard_coe_eq_coe_finsetCard (Finset.range k) using 1

Result:
case h.e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard

case h.e'_3
k : ℕ
⊢ ↑k = ↑(Finset.range k).card
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem hasStrictDerivAt_sinh (x : ℂ) : HasStrictDerivAt sinh (cosh x) x

Proof state:
x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
simp only [cosh, div_eq_mul_inv]

Result:
x : ℂ
⊢ HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x

Proof state:
x : ℂ
⊢ HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x

Tactic:
convert ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).neg.cexp).mul_const (2 : ℂ)⁻¹
  using 1

Result:
case h.e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹

Proof state:
case h.e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹

Tactic:
rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_sq (x : α) : |x ^ 2| = x ^ 2

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x : α
⊢ |x ^ 2| = x ^ 2

Tactic:
simpa only [sq] using abs_mul_self x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_abs_toReal_of_sign_nonneg {θ : Angle} (h : 0 ≤ θ.sign) : ↑|θ.toReal| = θ

Proof state:
θ : Angle
h : 0 ≤ θ.sign
⊢ ↑|θ.toReal| = θ

Tactic:
rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_bmod_bmod : Int.bmod (x * Int.bmod y n) n = Int.bmod (x * y) n

Proof state:
x y : Int
n : Nat
⊢ (x * y.bmod n).bmod n = (x * y).bmod n

Tactic:
rw [Int.mul_comm x, bmod_mul_bmod, Int.mul_comm x]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} :
    x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a • v i) = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, (c.sum fun i a => a • v i) = x

Tactic:
simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma mul_one_div_cancel (h : IsUnit a) : a * (1 / a) = 1

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * (1 / a) = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x)
    (hx : f x = x) (n : ℕ) : HasDerivAt f^[n] (f' ^ n) x :=
  hf.iterate _ (have := hf.tendsto_nhds le_rfl; by rwa [hx] at this) hx n

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAt f f' x
hx : f x = x
n : ℕ
this : Tendsto f (𝓝 x) (𝓝 (f x))
⊢ Tendsto f (𝓝 x) (𝓝 x)

Tactic:
rwa [hx] at this

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_le_of_le_one_left [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_edist_eq_card (f g : WithLp 0 (α × β)) :
    edist f g =
      (if edist f.fst g.fst = 0 then 0 else 1) + (if edist f.snd g.snd = 0 then 0 else 1)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : EDist α
inst✝ : EDist β
f g : WithLp 0 (α × β)
⊢ edist f g = (if edist f.1 g.1 = 0 then 0 else 1) + if edist f.2 g.2 = 0 then 0 else 1

Tactic:
convert if_pos rfl

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem le_sup_iff {u : Ultrafilter α} {f g : Filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g :=
  not_iff_not.1 <| by simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

Proof state:
α : Type u
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)

Tactic:
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
    (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Array α
⊢ (x ∈ if p then #[] else l) ↔ ¬p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENat_le_iff_of_lt_aleph0 {c c' : Cardinal} (hc' : c' < ℵ₀) :
    toENat c ≤ toENat c' ↔ c ≤ c'

Proof state:
case intro
c : Cardinal.{u_1}
c' : ℕ
⊢ toENat c ≤ toENat ↑c' ↔ c ≤ ↑c'

Tactic:
simp_rw [toENat_nat, ← toENat_le_nat]

Result:
no goals

Proof state:
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
lift c' to ℕ using hc'

Result:
case intro
c : Cardinal.{u_1}
c' : ℕ
⊢ toENat c ≤ toENat ↑c' ↔ c ≤ ↑c'
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem dvd_of_le (hv : Integers v O) {x y : O}
    (h : v (algebraMap O F x) ≤ v (algebraMap O F y)) : y ∣ x :=
  by_cases
    (fun hy : algebraMap O F y = 0 =>
      have hx : x = 0 :=
        hv.1 <|
          (algebraMap O F).map_zero.symm ▸ (v.zero_iff.1 <| le_zero_iff.1 (v.map_zero ▸ hy ▸ h))
      hx.symm ▸ dvd_zero y)
    fun hy : algebraMap O F y ≠ 0 =>
    have : v ((algebraMap O F y)⁻¹ * algebraMap O F x) ≤ 1

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ 1

Tactic:
rw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul]

Result:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) y)

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) y)

Tactic:
exact mul_le_mul_left' h _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
    (h : m.WF) : (Const.alter m k f).contains k' =
      if k == k' then (f (Const.get? m k)).isSome else m.contains k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).contains k' = if (k == k') = true then (f (get? m k)).isSome else m.contains k'

Tactic:
simp_to_raw using Raw₀.Const.contains_alter

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_bot_bot : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, ⊥)

Proof state:
r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑0 ∧ x✝.2 < ↑r
⊢ x✝.1 + x✝.2 < ↑r

Tactic:
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Result:
no goals

Proof state:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < ↑x

Tactic:
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
  (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_

Result:
r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑0 ∧ x✝.2 < ↑r
⊢ x✝.1 + x✝.2 < ↑r

Proof state:
⊢ ContinuousAt (fun p => p.1 + p.2) (⊥, ⊥)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Result:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < ↑x
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem prod_top (s : NonUnitalSubsemiring R) :
    s.prod (⊤ : NonUnitalSubsemiring S) = s.comap (NonUnitalRingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.biInter_Ici_aecover [Preorder ι] {φ : ι → Set α}
    (hφ : AECover μ atTop φ) : AECover μ atTop fun n : ι => ⋂ (k) (_h : k ∈ Ici n), φ k where
  ae_eventually_mem := hφ.ae_eventually_mem.mono fun x h ↦ by
    simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]
  measurableSet _ := .biInter (to_countable _) fun n _ => hφ.measurableSet n

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Countable ι
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
x : α
h : ∀ᶠ (i : ι) in atTop, x ∈ φ i
⊢ ∀ᶠ (i : ι) in atTop, x ∈ ⋂ k ∈ Ici i, φ k

Tactic:
simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem exists_apply_eq_finset_sup (p : ι → Seminorm 𝕜 E) {s : Finset ι} (hs : s.Nonempty) (x : E) :
    ∃ i ∈ s, s.sup p x = p i x

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
rcases Finset.exists_mem_eq_sup s hs (fun i ↦ (⟨p i x, apply_nonneg _ _⟩ : ℝ≥0)) with ⟨i, hi, hix⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
rw [finset_sup_apply]

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = (p i) x

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = (p i) x

Tactic:
exact ⟨i, hi, congr_arg _ hix⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_mem_iff {f : E → F} {t : Set E} {s : Set (E →L[𝕜] F)} {x : E} :
    fderivWithin 𝕜 f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨
        ¬DifferentiableWithinAt 𝕜 f t x ∧ (0 : E →L[𝕜] F) ∈ s

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 : E → F
t : Set E
s : Set (E →L[𝕜] F)
x : E
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableWithinAt 𝕜 f t x <;>
  simp [fderivWithin_zero_of_not_differentiableWithinAt, *]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_finset {s : Finset α} : a ∈ stabilizer G s ↔ ∀ b, a • b ∈ s ↔ b ∈ s

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
    finsuppLeft R M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ p i = 0 → (Finsupp.single i (0 ⊗ₜ[R] n)) i = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ ((finsuppLeft R M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n

Tactic:
rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
  Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma ιFunctorObj_eq (j : κ.ord.toType) :
    letI := hasColimitsOfShape_discrete I κ
    letI := hasPushouts I κ
    ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
      (relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)) ≫
        (relativeCellComplexιObjFObjSuccIso I κ f j).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
⊢ ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom

Tactic:
simpa using Arrow.leftFunc.congr_map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.w

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_swap {a b : EReal}
    (h : ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (a, b)) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (b, a)

Proof state:
case h.e'_5.h
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
x✝ : EReal × EReal
⊢ x✝.1 * x✝.2 = ((fun p => p.1 * p.2) ∘ Prod.swap) x✝

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
⊢ ContinuousAt (fun p => p.1 * p.2) (b, a)

Tactic:
convert h.comp continuous_swap.continuousAt (x := (b, a))

Result:
case h.e'_5.h
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
x✝ : EReal × EReal
⊢ x✝.1 * x✝.2 = ((fun p => p.1 * p.2) ∘ Prod.swap) x✝
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem doublingGamma_one : doublingGamma 1 = 1

Proof state:
⊢ doublingGamma 1 = 1

Tactic:
simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
  rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_non_aestronglyMeasurable_of_le (h : a ≤ b)
    (hf : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))) : ∫ x in a..b, f x ∂μ = 0 :=
  integral_non_aestronglyMeasurable <| by rwa [uIoc_of_le h]

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
hf : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))
⊢ ¬AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
rwa [uIoc_of_le h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_le_iff {x y : ℝ≥0∞} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z

Tactic:
rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (inv_pos.2 hz)]

Result:
no goals

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne.symm]

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
nth_rw 1 [← ENNReal.rpow_one y]

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem Eq.congr_left {x y z : α} (h : x = y) : x = z ↔ y = z

Proof state:
α : Sort u_1
x y z : α
h : x = y
⊢ x = z ↔ y = z

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
    xs.idxOf? a = (xs.finIdxOf? a).map (·.val)

Proof state:
α : Type u_1
inst✝ : BEq α
xs : List α
a : α
⊢ idxOf? a xs = Option.map (fun x => ↑x) (finIdxOf? a xs)

Tactic:
simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]

Result:
no goals
-- Mathlib/Topology/Instances/ENat.lean
theorem nhds_eq_pure {n : ℕ∞} (h : n ≠ ⊤) : 𝓝 n = pure n

Proof state:
case intro
n : ℕ
⊢ 𝓝 ↑n = pure ↑n

Tactic:
simp [nhds_natCast]

Result:
no goals

Proof state:
n : ℕ∞
h : n ≠ ⊤
⊢ 𝓝 n = pure n

Tactic:
lift n to ℕ using h

Result:
case intro
n : ℕ
⊢ 𝓝 ↑n = pure ↑n
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setIntegral_condKernel_univ_right (a : α) {s : Set β} (hs : MeasurableSet s)
    (hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)) :
    ∫ b in s, ∫ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)
      = ∫ x in s ×ˢ Set.univ, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

Tactic:
rw [← setIntegral_condKernel a hs MeasurableSet.univ hf]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals