harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Nth.lean
theorem count_nth {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset) :
    count p (nth p n) = n

Proof state:
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
hn : ∀ (hf : (setOf p).Finite), 0 < #hf.toFinset
⊢ count p (nth p 0) = 0

Tactic:
exact count_nth_zero _

Result:
no goals

Proof state:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (setOf p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
⊢ count p (nth p (k + 1)) = k + 1

Tactic:
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_not_mem, ←
  count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]

Result:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (setOf p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
⊢ nth p k ∉ filter (fun n => p n) (range (nth p k))

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #hf.toFinset
⊢ count p (nth p n) = n

Tactic:
induction' n with k ihk

Result:
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
hn : ∀ (hf : (setOf p).Finite), 0 < #hf.toFinset
⊢ count p (nth p 0) = 0

case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (setOf p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
⊢ count p (nth p (k + 1)) = k + 1

Proof state:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (setOf p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
⊢ nth p k ∉ filter (fun n => p n) (range (nth p k))

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem mk_smul_indicatorConstLp (c : M)
    {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (b : E) :
    mk c • indicatorConstLp p hs hμs b =
      indicatorConstLp p (hs.preimage <| measurable_const_smul c)
        (by rwa [SMulInvariantMeasure.measure_preimage_smul c hs]) b :=
  rfl

Proof state:
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁶ : MeasurableSpace M
inst✝⁵ : MeasurableSpace N
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
b : E
⊢ μ ((fun x => c • x) ⁻¹' s) ≠ ⊤

Tactic:
rwa [SMulInvariantMeasure.measure_preimage_smul c hs]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
lemma finsuppScalarLeft_apply_tmul (p : ι →₀ R) (n : N) :
    finsuppScalarLeft R N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m • n)

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = (p.sum fun i m => Finsupp.single i (m • n)) i

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

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ p i = 0 → (Finsupp.single i (0 • n)) i = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
⊢ (finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m • n)

Tactic:
ext i

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = (p.sum fun i m => Finsupp.single i (m • n)) i
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_inl :
    comul ∘ₗ inl R A B = TensorProduct.map (.inl R A B) (.inl R A B) ∘ₗ comul

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ inl R A B = TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (comul ∘ₗ inl R A B) x✝ = (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) x✝

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (comul ∘ₗ inl R A B) x✝ = (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_circumradius_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P}
    (h : ps ⊆ s) [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction]
    (hd : finrank ℝ s.direction = n) (hc : Cospherical ps) :
    ∃ r : ℝ, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumradius = r

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ Fintype.card (Fin (n + 1)) = finrank ℝ ↥s.direction + 1

Tactic:
simp [hd]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem iterate {f : α → α} (hf : LipschitzWith K f) : ∀ n, LipschitzWith (K ^ n) f^[n]
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by rw [pow_succ]; exact (LipschitzWith.iterate hf n).comp hf

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]

Tactic:
exact (LipschitzWith.iterate hf n).comp hf

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]

Tactic:
rw [pow_succ]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) f^[0]

Tactic:
simpa only [pow_zero] using LipschitzWith.id

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem lindelofSpace_of_countable_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ →
      ∃ u : Set ι, u.Countable ∧ ⋂ i ∈ u, t i = ∅) :
    LindelofSpace X where
  isLindelof_univ := isLindelof_of_countable_subfamily_closed fun t => by simpa using h t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
t : ι✝ → Set X
⊢ (∀ (i : ι✝), IsClosed (t i)) → univ ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ univ ∩ ⋂ i ∈ u, t i = ∅

Tactic:
simpa using h t

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem mem_support_map_iff : b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_right (a b : α) : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_add_zsmul hp a b 1

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem max_sq_add_min_le_pair (m n : ℕ) : max m n ^ 2 + min m n ≤ pair m n

Proof state:
case inl
m n : ℕ
h : m < n
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]

Result:
no goals

Proof state:
m n : ℕ
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rcases lt_or_le m n with h | h

Result:
case inl
m n : ℕ
h : m < n
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

case inr
m n : ℕ
h : n ≤ m
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

Proof state:
m n : ℕ
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ pair m n

Tactic:
rw [pair]

Result:
m n : ℕ
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

Proof state:
case inr
m n : ℕ
h : n ≤ m
⊢ (m ⊔ n) ^ 2 + m ⊓ n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rw [if_neg h.not_lt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc,
  Nat.add_le_add_iff_left]

Result:
case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n

Proof state:
case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n

Tactic:
exact Nat.le_add_left _ _

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma mul_mem_nonZeroDivisors : a * b ∈ M₀⁰ ↔ a ∈ M₀⁰ ∧ b ∈ M₀⁰ where
  mp h

Proof state:
case intro.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x * a = 0

Tactic:
apply hb

Result:
case intro.a.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x * a * b = 0

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰

Tactic:
constructor <;> intro x h' <;> apply h

Result:
case left.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0

case right.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0

Proof state:
case left.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0

Tactic:
rw [← mul_assoc, h', zero_mul]

Result:
no goals

Proof state:
case intro.a.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x * a * b = 0

Tactic:
rw [mul_assoc, hx]

Result:
no goals

Proof state:
case right.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0

Tactic:
rw [mul_comm a b, ← mul_assoc, h', zero_mul]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰ → a * b ∈ M₀⁰

Tactic:
rintro ⟨ha, hb⟩ x hx

Result:
case intro
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x = 0

Proof state:
case intro
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x = 0

Tactic:
apply ha

Result:
case intro.a
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
ha : a ∈ M₀⁰
hb : b ∈ M₀⁰
x : M₀
hx : x * (a * b) = 0
⊢ x * a = 0
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
/-- Let `{a | p a}` be an additive subsemigroup of an additive commutative monoid `M`. If `m` is a
subadditive function (`m (a + b) ≤ m a + m b`) preserved under division by a natural, `f` is a
function valued in that subsemigroup and `s` is a nonempty set, then
`m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
lemma le_expect_nonempty_of_subadditive_on_pred (h_add : ∀ a b, p a → p b → m (a + b) ≤ m a + m b)
    (hp_add : ∀ a b, p a → p b → p (a + b)) (h_div : ∀ (n : ℕ) a, p a → m (a /ℚ n) = m a /ℚ n)
    (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (f i)) :
    m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ (↑(#s))⁻¹ • m (∑ x ∈ s, f x) ≤ (↑(#s))⁻¹ • ∑ x ∈ s, m (f x)

Tactic:
exact smul_le_smul_of_nonneg_left
  (le_sum_nonempty_of_subadditive_on_pred _ _ h_add hp_add _ _ hs_nonempty hs) <| by positivity

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
simp only [expect, h_div _ _ (sum_induction_nonempty _ _ hp_add hs_nonempty hs)]

Result:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (f i)
⊢ (↑(#s))⁻¹ • m (∑ x ∈ s, f x) ≤ (↑(#s))⁻¹ • ∑ x ∈ s, m (f x)
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma le_iff_oneLePart_leOnePart (a b : α) : a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b

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

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ

Tactic:
exact div_le_div'' h.1 h.2

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhds {x : M} (hy : x ∈ f.source) :
    map (f.extend I) (𝓝 x) = 𝓝[range I] f.extend I x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑(f.extend I)) (𝓝 x) = 𝓝[range ↑I] ↑(f.extend I) x

Tactic:
rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_map]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_coinduced_dom {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
    Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Proof state:
α : Type u
β : Type v
γ : Type u_1
f : α → β
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous g ↔ Continuous (g ∘ f)

Tactic:
simp only [continuous_iff_coinduced_le, coinduced_compose]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_const_fun (x : β) : map (n := n) (Function.const α x) = fun _ => mkVector n x

Proof state:
β : Type u_1
n : Nat
α : Type u_2
x : β
⊢ map (Function.const α x) = fun x_1 => mkVector n x

Tactic:
funext l

Result:
case h
β : Type u_1
n : Nat
α : Type u_2
x : β
l : Vector α n
⊢ map (Function.const α x) l = mkVector n x

Proof state:
case h
β : Type u_1
n : Nat
α : Type u_2
x : β
l : Vector α n
⊢ map (Function.const α x) l = mkVector n x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
      ys.attachWith P (fun a h => H a (mem_append_right xs h))

Proof state:
α : Type u_1
n m : Nat
P : α → Prop
xs : Vector α n
ys : Vector α m
H : ∀ (a : α), a ∈ xs ++ ys → P a
⊢ (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯

Tactic:
simp [attachWith, attach_append, map_pmap, pmap_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getKey_eq [BEq α] {l : AssocList α β} {a : α} {h} :
    l.getKey a h = List.getKey a l.toList (contains_eq.symm.trans h)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
h : contains a nil = true
⊢ getKey a nil h = List.getKey a nil.toList ⋯

Tactic:
simp [contains] at h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
t : AssocList α β
ih : ∀ {h : contains a t = true}, getKey a t h = List.getKey a t.toList ⋯
h : contains a (cons k v t) = true
⊢ getKey a (cons k v t) h = List.getKey a (cons k v t).toList ⋯

Tactic:
simp only [getKey, toList_cons, List.getKey_cons, ih]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, getKey a tail✝ h = List.getKey a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ getKey a (cons key✝ value✝ tail✝) h = List.getKey a (cons key✝ value✝ tail✝).toList ⋯

Tactic:
next k v t ih => simp only [getKey, toList_cons, List.getKey_cons, ih]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a : α
h : contains a l = true
⊢ getKey a l h = List.getKey a l.toList ⋯

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
h : contains a nil = true
⊢ getKey a nil h = List.getKey a nil.toList ⋯

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, getKey a tail✝ h = List.getKey a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ getKey a (cons key✝ value✝ tail✝) h = List.getKey a (cons key✝ value✝ tail✝).toList ⋯
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma max_ne (ha : a ≠ c) (hb : b ≠ c) : max a b ≠ c

Proof state:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then b else a) ≠ c

Tactic:
split_ifs <;> assumption

Result:
no goals

Proof state:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ a ⊔ b ≠ c

Tactic:
rw [max_def]

Result:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then b else a) ≠ c
-- Mathlib/Data/List/Permutation.lean
theorem mem_permutations_of_perm_lemma {is l : List α}
    (H : l ~ [] ++ is → (∃ (ts' : _) (_ : ts' ~ []), l = ts' ++ is) ∨ l ∈ permutationsAux is []) :
    l ~ is → l ∈ permutations is

Proof state:
α : Type u_1
is l : List α
H : l ~ [] ++ is → (∃ ts', ∃ (_ : ts' ~ []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []
⊢ l ~ is → l ∈ is.permutations

Tactic:
simpa [permutations, perm_nil] using H

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.add_measure {f : α → β} (hμ : Integrable f μ) (hν : Integrable f ν) :
    Integrable f (μ + ν)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : Integrable f μ
hν : Integrable f ν
⊢ Integrable f (μ + ν)

Tactic:
simp_rw [← memLp_one_iff_integrable] at hμ hν ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ MemLp f 1 (μ + ν)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ MemLp f 1 (μ + ν)

Tactic:
refine ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 (μ + ν) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 μ < ⊤ ∧ eLpNorm f 1 ν < ⊤

Tactic:
exact ⟨hμ.eLpNorm_lt_top, hν.eLpNorm_lt_top⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 (μ + ν) < ⊤

Tactic:
rw [eLpNorm_one_add_measure, ENNReal.add_lt_top]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 μ < ⊤ ∧ eLpNorm f 1 ν < ⊤
-- Mathlib/Algebra/Star/Module.lean
theorem StarModule.selfAdjointPart_add_skewAdjointPart (x : A) :
    (selfAdjointPart R x : A) + skewAdjointPart R x = x

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x

Tactic:
simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe,
  add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem norm_sq_re_add_conj (x : K) : ‖x + conj x‖ ^ 2 = re (x + conj x) ^ 2

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖x + (starRingEnd K) x‖ ^ 2 = re (x + (starRingEnd K) x) ^ 2

Tactic:
rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_shiftConcat {x : BitVec w} {b : Bool} :
    (x.shiftConcat b).toNat
    = (x.toNat <<< 1 + b.toNat) % 2 ^ w

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ (x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w

Tactic:
simp [shiftConcat, Nat.shiftLeft_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a (a :: l) = count a l + 1

Tactic:
simp [count_cons]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝ : TransGen r b b✝
hcd : r b✝ c✝
hac : TransGen r a b✝
⊢ TransGen r a c✝

Tactic:
exact hac.tail hcd

Result:
no goals

Proof state:
case single
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ : α
hbc : r b b✝
⊢ TransGen r a b✝

Tactic:
exact tail' hab hbc

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c

Tactic:
induction hbc with
| single hbc => exact tail' hab hbc
| tail _ hcd hac => exact hac.tail hcd

Result:
no goals