harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_prod_piFinset {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ → α) :
    ∑ f ∈ piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : CommSemiring α
inst✝¹ : DecidableEq ι
κ : Type u_7
inst✝ : Fintype ι
s : Finset κ
g : ι → κ → α
⊢ ∑ f ∈ piFinset fun x => s, ∏ i : ι, g i (f i) = ∏ i : ι, ∑ j ∈ s, g i j

Tactic:
rw [← prod_univ_sum]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_le_one : sqrt x ≤ 1 ↔ x ≤ 1

Proof state:
x : ℝ≥0
⊢ sqrt x ≤ 1 ↔ x ≤ 1

Tactic:
rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem singleton_repr (ι R : Type*) [Unique ι] [Semiring R] (x i) :
    (Basis.singleton ι R).repr x i = x

Proof state:
ι : Type u_10
R : Type u_11
inst✝¹ : Unique ι
inst✝ : Semiring R
x : R
i : ι
⊢ ((Basis.singleton ι R).repr x) i = x

Tactic:
simp [Basis.singleton, Unique.eq_default i]

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
theorem LeftCancelMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@LeftCancelMonoid.toMonoid M)

Proof state:
case mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h : toMonoid = toMonoid
⊢ mk mul_left_cancel✝¹ = mk mul_left_cancel✝

Tactic:
congr <;> injection h

Result:
no goals

Proof state:
M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h

Result:
case mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h : toMonoid = toMonoid
⊢ mk mul_left_cancel✝¹ = mk mul_left_cancel✝
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum₂_with_one (x : α) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i :=
  sum_congr rfl fun i _ => by rw [one_pow, mul_one]

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 ^ (n - 1 - i) = x ^ i

Tactic:
rw [one_pow, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_inf_div_inf_le_mabs (a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)

Tactic:
apply le_of_mul_le_of_one_le_right _ (one_le_mabs _)

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ?m.25299 * mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ?m.25299 * mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)

Tactic:
rw [mabs_div_sup_mul_mabs_div_inf]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem le_iff_atom_le_imp {a b : α} : a ≤ b ↔ ∀ c : α, IsAtom c → c ≤ a → c ≤ b :=
  ⟨fun ab _ _ ca => le_trans ca ab, fun h => by
    rw [← sSup_atoms_le_eq a, ← sSup_atoms_le_eq b]
    exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩⟩

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ a ≤ b

Tactic:
rw [← sSup_atoms_le_eq a, ← sSup_atoms_le_eq b]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}

Tactic:
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem lt_succ_castPred {a : Fin (n + 1)} (ha : a ≠ last n) :
    a < succ (a.castPred ha)

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ a < (a.castPred ha).succ

Tactic:
rw [lt_succ_castPred_iff, le_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false

Proof state:
⊢ ∀ (x : Bool), ((!x) == x) = false

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma integrable_pow_mul (f : 𝓢(D, V))
    (k : ℕ) : Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ

Proof state:
case h.e'_6.h.h.e'_6
D : Type u_3
V : Type u_7
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
x : D
⊢ ‖f x‖ = ‖iteratedFDeriv ℝ 0 (⇑f) x‖

Tactic:
simp

Result:
no goals

Proof state:
D : Type u_3
V : Type u_7
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
⊢ Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ

Tactic:
convert integrable_pow_mul_iteratedFDeriv μ f k 0 with x

Result:
case h.e'_6.h.h.e'_6
D : Type u_3
V : Type u_7
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
x : D
⊢ ‖f x‖ = ‖iteratedFDeriv ℝ 0 (⇑f) x‖
-- Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
lemma Over.pullbackComp_left_fst_fst [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z)
    (A : P.Over Q Z) :
    ((Over.pullbackComp f g).hom.app A).left ≫
      pullback.fst (pullback.snd A.hom g) f ≫ pullback.fst A.hom g =
        pullback.fst A.hom (f ≫ g)

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝⁴ : Q.IsMultiplicative
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.RespectsIso
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
A : P.Over Q Z
⊢ ((pullbackComp f g).hom.app A).left ≫ pullback.fst (pullback.snd A.hom g) f ≫ pullback.fst A.hom g =
    pullback.fst A.hom (f ≫ g)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem eq_zero_iff_not_coprime {a : ℤ} {b : ℕ} [NeZero b] : J(a | b) = 0 ↔ a.gcd b ≠ 1 :=
  List.prod_eq_zero_iff.trans
    (by
      rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]
      simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm])

Proof state:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ 0 ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯ ↔ a.gcd ↑b ≠ 1

Tactic:
rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]

Result:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs

Proof state:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs

Tactic:
simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
  mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
  and_assoc, _root_.and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_le_div_of_neg (hb : b < 0) : 1 ≤ a / b ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ a ≤ b

Tactic:
rw [le_div_iff_of_neg hb, one_mul]

Result:
no goals
-- Mathlib/Tactic/NormNum/NatFib.lean
theorem isFibAux_two_mul_add_one {n a b n' a' b' : ℕ} (H : IsFibAux n a b)
    (hn : 2 * n + 1 = n') (h1 : a * a + b * b = a') (h2 : b * (2 * a + b) = b') :
    IsFibAux n' a' b' :=
  ⟨by rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1],
   by rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]⟩

Proof state:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'

Tactic:
rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]

Result:
no goals

Proof state:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib n' = a'

Tactic:
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
@[simp]
lemma nonempty_Ioi : (Ioi a).Nonempty ↔ ¬ IsMax a

Proof state:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul
    {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s)
    {g : ℝ → ℝ} (hg : ∀ᵐ x, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s))
    {f' : ℝ → ℝ} (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).comap f s
      = ENNReal.ofReal (∫ x in s, |f' x| * g (f x))

Proof state:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ (Measure.comap f (volume.withDensity fun x => ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
rw [hf.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul volume hs
  hg hg_int hf']

Result:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Proof state:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
simp only [det_one_smulRight]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_Ico_atTop [Preorder α] [NoMaxOrder α]
    [(atTop : Filter α).IsCountablyGenerated] (μ : Measure α) (a : α) :
    Tendsto (fun x => μ (Ico a x)) atTop (𝓝 (μ (Ici a)))

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ico a x)) atTop (𝓝 (μ (⋃ b, Ico a b)))

Tactic:
exact tendsto_measure_iUnion_atTop (antitone_const.Ico monotone_id)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ico a x)) atTop (𝓝 (μ (Ici a)))

Tactic:
rw [← iUnion_Ico_right]

Result:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ico a x)) atTop (𝓝 (μ (⋃ b, Ico a b)))
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveRight_neg_toRightMovesNeg {x : PGame} (i) :
    (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i

Proof state:
x : PGame
i : x.LeftMoves
⊢ (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_nil (R : α → β → Prop) : LiftRel R nil nil

Proof state:
α : Type u
β : Type v
R : α → β → Prop
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) nil.destruct nil.destruct

Tactic:
simp [-liftRel_pure_left, -liftRel_pure_right]

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
⊢ LiftRel R nil nil

Tactic:
rw [liftRel_destruct_iff]

Result:
α : Type u
β : Type v
R : α → β → Prop
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) nil.destruct nil.destruct
-- Mathlib/Order/LiminfLimsup.lean
theorem isCobounded_principal (s : Set α) :
    (𝓟 s).IsCobounded r ↔ ∃ b, ∀ a, (∀ x ∈ s, r x a) → r b a

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a

Tactic:
simp [IsCobounded, subset_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Dart.lean
theorem dart_edge_eq_iff : ∀ d₁ d₂ : G.Dart, d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm

Proof state:
V : Type u_1
G : SimpleGraph V
⊢ ∀ (d₁ d₂ : G.Dart), d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm

Tactic:
rintro ⟨p, hp⟩ ⟨q, hq⟩

Result:
case mk.mk
V : Type u_1
G : SimpleGraph V
p : V × V
hp : G.Adj p.1 p.2
q : V × V
hq : G.Adj q.1 q.2
⊢ { toProd := p, adj := hp }.edge = { toProd := q, adj := hq }.edge ↔
    { toProd := p, adj := hp } = { toProd := q, adj := hq } ∨
      { toProd := p, adj := hp } = { toProd := q, adj := hq }.symm

Proof state:
case mk.mk
V : Type u_1
G : SimpleGraph V
p : V × V
hp : G.Adj p.1 p.2
q : V × V
hq : G.Adj q.1 q.2
⊢ { toProd := p, adj := hp }.edge = { toProd := q, adj := hq }.edge ↔
    { toProd := p, adj := hp } = { toProd := q, adj := hq } ∨
      { toProd := p, adj := hp } = { toProd := q, adj := hq }.symm

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Iio {a : α} : (Nat.cast : ℕ → α) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ Nat.cast ⁻¹' Iio a = Iio ⌈a⌉₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉₊

Tactic:
simp [lt_ceil]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[fun_prop]
lemma continuous_realContinuousMapOfNNReal (φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A)
    (hφ : Continuous φ) : Continuous φ.realContinuousMapOfNNReal

Proof state:
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous fun f => φ f.toNNReal - φ (-f).toNNReal

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous ⇑φ.realContinuousMapOfNNReal

Tactic:
simp [realContinuousMapOfNNReal]

Result:
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous fun f => φ f.toNNReal - φ (-f).toNNReal
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_le_card_width [StrongRankCondition R] (A : Matrix m n R) :
    A.rank ≤ Fintype.card n

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (n → R)
⊢ A.rank ≤ Fintype.card n

Tactic:
haveI : Module.Free R (n → R) := Module.Free.pi _ _

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (n → R)
this : Free R (n → R)
⊢ A.rank ≤ Fintype.card n

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card n

Tactic:
haveI : Module.Finite R (n → R) := Module.Finite.pi

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (n → R)
⊢ A.rank ≤ Fintype.card n

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (n → R)
this : Free R (n → R)
⊢ A.rank ≤ Fintype.card n

Tactic:
exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_Ioc_same (h : a ≤ b) : Icc a b \ Ioc a b = {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}

Tactic:
rw [← Icc_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Icc.2 h)]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasFDerivWithinAt (g i ·) (g' i) s x) :
    HasFDerivWithinAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x
⊢ HasFDerivWithinAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
    (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum s x

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x
⊢ HasFDerivWithinAt (fun x => (Multiset.map ((fun x_1 => g x_1 x) ∘ Subtype.val) u.attach).prod)
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum
    s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x
⊢ (Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
      (pi fun i => g' ↑i) =
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x
x✝ : E
⊢ ((Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
        (pi fun i => g' ↑i))
      x✝ =
    (Multiset.map
          ((fun x_1 =>
              (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
            Subtype.val)
          u.attach).sum
      x✝
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_pow_sub_pow_sub (x₀ : E') {n m : ℕ} (h : n < m) :
    (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => ‖x - x₀‖ ^ n :=
  haveI : Tendsto (fun x => ‖x - x₀‖) (𝓝 x₀) (𝓝 0)

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ Tendsto (fun x => ‖x - x₀‖) (𝓝 x₀) (𝓝 0)

Tactic:
apply tendsto_norm_zero.comp

Result:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 0)

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 (x₀ - x₀))

Tactic:
exact tendsto_id.sub tendsto_const_nhds

Result:
no goals

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 0)

Tactic:
rw [← sub_self x₀]

Result:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 (x₀ - x₀))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} :
    (m.insertMany l).1.1.isEmpty = (m.1.isEmpty && l.isEmpty)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
⊢ (m.insertMany l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

Tactic:
simp_to_model [insertMany] using List.isEmpty_insertList

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.div [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Antiperiodic f c)
    (hg : Antiperiodic g c) : Periodic (f / g) c

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝² : Add α
inst✝¹ : DivisionMonoid β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f / g) c

Tactic:
simp_all [neg_div_neg_eq]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_cons_succ (l : List α) (a : α) (n : ℕ) :
    (a :: l : List α).rotate (n + 1) = (l ++ [a]).rotate n

Proof state:
α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.cond {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁)
    (h₂ : MeasurableSet s₂) {i : Bool} : MeasurableSet (cond i s₁ s₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)

Tactic:
cases i

Result:
case false
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

case true
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)

Proof state:
case false
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

case true
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)

Tactic:
exacts [h₂, h₁]

Result:
no goals