harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isInitial_omega0 : IsInitial ω

Proof state:
⊢ ω.IsInitial

Tactic:
rw [IsInitial, card_omega0, ord_aleph0]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_right_strictAnti₀ (ha₀ : 0 < a) (ha₁ : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Tactic:
rw [zpow_add_one₀ ha₀.ne']

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a < 1
⊢ StrictAnti fun n => a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem sum_sub_index [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommGroup γ]
    {f g : Π₀ i, β i} {h : ∀ i, β i → γ} (h_sub : ∀ i b₁ b₂, h i (b₁ - b₂) = h i b₁ - h i b₂) :
    (f - g).sum h = f.sum h - g.sum h

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
have := (liftAddHom (β := β) fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (f.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) - g.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)
⊢ (f - g).sum h = f.sum h - g.sum h

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (f.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) - g.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
exact this

Result:
no goals
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_inv_neg {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} :
    IsRat a (.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (.negOfNat d) (Nat.succ n)

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ

Tactic:
generalize Nat.succ n = n at *

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n

Proof state:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat n.succ) d → IsRat a⁻¹ (Int.negOfNat d) n.succ

Tactic:
rintro ⟨_, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat n.succ) * ⅟↑d)⁻¹ (Int.negOfNat d) n.succ

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat n.succ) * ⅟↑d)⁻¹ (Int.negOfNat d) n.succ

Tactic:
simp only [Int.negOfNat_eq]

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n

Tactic:
use this

Result:
case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n

Proof state:
case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n

Tactic:
simp only [Int.ofNat_eq_coe, Int.cast_neg,
Int.cast_natCast, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, LipschitzWith Kα fun a => f a b)
    (hβ : ∀ a, LipschitzWith Kβ (f a)) : LipschitzWith (Kα + Kβ) (Function.uncurry f)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
⊢ LipschitzWith (Kα + Kβ) (uncurry f)

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩

Result:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ ↑(Kα + Kβ) * edist (a₁, b₁) (a₂, b₂)

Proof state:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)

Tactic:
exact
  add_le_add (le_trans (hα _ _ _) <| mul_left_mono <| le_max_left _ _)
    (le_trans (hβ _ _ _) <| mul_left_mono <| le_max_right _ _)

Result:
no goals

Proof state:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ ↑(Kα + Kβ) * edist (a₁, b₁) (a₂, b₂)

Tactic:
simp only [Function.uncurry, ENNReal.coe_add, add_mul]

Result:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)

Proof state:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)

Tactic:
apply le_trans (edist_triangle _ (f a₂ b₁) _)

Result:
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
-- Mathlib/Algebra/Order/Floor.lean
lemma le_ceil_iff : z ≤ ⌈a⌉ ↔ z - 1 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
rw [← sub_one_lt_iff, lt_ceil]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z - 1) < a ↔ ↑z - 1 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z - 1) < a ↔ ↑z - 1 < a

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_le_norm_add_norm' (a b : E) : dist a b ≤ ‖a‖ + ‖b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ dist a b ≤ ‖a‖ + ‖b‖

Tactic:
rw [dist_eq_norm_div]

Result:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ ≤ ‖a‖ + ‖b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ ≤ ‖a‖ + ‖b‖

Tactic:
apply norm_div_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.ne_to_beq (a b : Bool) : (a ≠ b) = ((!(a == b)) = true)

Proof state:
a b : Bool
⊢ (a ≠ b) = ((!a == b) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- Nonarchimedean norm of a product is less than or equal to the largest norm of a term in the
product. -/
@[to_additive "Nonarchimedean norm of a sum is less than or equal to the largest norm of a term in
the sum."]
lemma _root_.Finset.nnnorm_prod_le_sup_nnnorm (s : Finset ι) (f : ι → M) :
    ‖∏ i ∈ s, f i‖₊ ≤ s.sup (‖f ·‖₊)

Proof state:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏ i ∈ ∅, f i‖₊ ≤ ∅.sup fun x => ‖f x‖₊

Tactic:
simp only [Finset.prod_empty, nnnorm_one', Finset.sup_empty, bot_eq_zero', le_refl]

Result:
no goals

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
⊢ ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun x => ‖f x‖₊

Tactic:
rcases s.eq_empty_or_nonempty with rfl|hs

Result:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏ i ∈ ∅, f i‖₊ ≤ ∅.sup fun x => ‖f x‖₊

case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun x => ‖f x‖₊

Proof state:
case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun x => ‖f x‖₊

Tactic:
simpa only [← Finset.sup'_eq_sup hs, Finset.le_sup'_iff, coe_le_coe, coe_nnnorm']
  using hs.norm_prod_le_sup'_norm f

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem ae_not_liouville : ∀ᵐ x, ¬Liouville x :=
  ae_not_liouvilleWith.mono fun _ h₁ h₂ => h₁ 3 (by norm_num) (h₂.liouvilleWith 3)

Proof state:
x✝ : ℝ
h₁ : ∀ p > 2, ¬LiouvilleWith p x✝
h₂ : Liouville x✝
⊢ 3 > 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem average_eq_integral_normalize {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (nonzero : μ ≠ 0) (f : Ω → E) :
    average (μ : Measure Ω) f = ∫ ω, f ω ∂(μ.normalize : Measure Ω)

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ ∫ (x : Ω), f x ∂(↑μ univ)⁻¹ • ↑μ = ∫ (ω : Ω), f ω ∂μ.mass⁻¹ • ↑μ

Tactic:
congr

Result:
case e_μ.e_a
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ (↑μ univ)⁻¹ = ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom μ.mass⁻¹

Proof state:
case e_μ.e_a
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ (↑μ univ)⁻¹ = ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom μ.mass⁻¹

Tactic:
simp [ENNReal.coe_inv (μ.mass_nonzero_iff.mpr nonzero), ennreal_mass]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize

Tactic:
rw [μ.toMeasure_normalize_eq_of_nonzero nonzero, average]

Result:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ ∫ (x : Ω), f x ∂(↑μ univ)⁻¹ • ↑μ = ∫ (ω : Ω), f ω ∂μ.mass⁻¹ • ↑μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
| _, 0 => rfl
| _, k + 1 => by
  rw [shiftRight_succ _ (k+1)]
  rw [shiftRight_succ_inside _ k, shiftRight_succ]

Proof state:
x✝ k : Nat
⊢ x✝ >>> (k + 1) / 2 = (x✝ / 2) >>> (k + 1)

Tactic:
rw [shiftRight_succ_inside _ k, shiftRight_succ]

Result:
no goals

Proof state:
x✝ k : Nat
⊢ x✝ >>> (k + 1 + 1) = (x✝ / 2) >>> (k + 1)

Tactic:
rw [shiftRight_succ _ (k+1)]

Result:
x✝ k : Nat
⊢ x✝ >>> (k + 1) / 2 = (x✝ / 2) >>> (k + 1)
-- Mathlib/Data/Finset/Max.lean
theorem ofDual_min' {s : Finset αᵒᵈ} (hs : s.Nonempty) :
    ofDual (min' s hs) = max' (s.image ofDual) (hs.image _)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ s.sup (WithBot.some ∘ fun x => ofDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑ofDual)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.min' hs) = (image (⇑ofDual) s).max' ⋯

Tactic:
rw [← WithBot.coe_eq_coe]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ↑(ofDual (s.min' hs)) = ↑((image (⇑ofDual) s).max' ⋯)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ↑(ofDual (s.min' hs)) = ↑((image (⇑ofDual) s).max' ⋯)

Tactic:
simp only [min'_eq_inf', id_eq, ofDual_inf', Function.comp_apply, coe_sup', max'_eq_sup',
  sup_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ s.sup (WithBot.some ∘ fun x => ofDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑ofDual)
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem volume_closedBall (x : E) (r : ℝ) :
    volume (Metric.closedBall x r) = (.ofReal r) ^ finrank ℝ E *
      .ofReal (sqrt π ^ finrank ℝ E / Gamma (finrank ℝ E / 2 + 1))

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ volume (closedBall x r) =
    ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, InnerProductSpace.volume_ball _]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma Connected.exists_path_of_dist (hconn : G.Connected) (u v : V) :
    ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Tactic:
exact ⟨p, p.isPath_of_length_eq_dist h, h⟩

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Tactic:
obtain ⟨p, h⟩ := hconn.exists_walk_length_eq_dist  u v

Result:
case intro
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v
-- Mathlib/Data/PFun.lean
theorem core_restrict (f : α → β) (s : Set β) : (f : α →. β).core s = s.preimage f

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x : α
⊢ x ∈ (↑f).core s ↔ x ∈ f ⁻¹' s

Tactic:
simp [core_def]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).core s = f ⁻¹' s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x : α
⊢ x ∈ (↑f).core s ↔ x ∈ f ⁻¹' s
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.embedding (he : OrthogonalIdempotents e) {J} (i : J ↪ I) :
    OrthogonalIdempotents (e ∘ i)

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
J : Type u_4
i : J ↪ I
⊢ OrthogonalIdempotents (e ∘ ⇑i)

Tactic:
simp [iff_mul_eq, he.mul_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
J : Type u_4
i : J ↪ I
⊢ OrthogonalIdempotents (e ∘ ⇑i)

Tactic:
classical
simp [iff_mul_eq, he.mul_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem measurable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Measurable (rnDeriv s μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x =>
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable (s.rnDeriv μ)

Tactic:
rw [rnDeriv_def]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x =>
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
-- Mathlib/Data/Finsupp/Defs.lean
@[simp]
lemma mapRange_mapRange (e₁ : N → P) (e₂ : M → N) (he₁ he₂) (f : α →₀ M) :
    mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) (by simp [*]) f := ext fun _ ↦ rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
e₁ : N → P
e₂ : M → N
he₁ : e₁ 0 = 0
he₂ : e₂ 0 = 0
f : α →₀ M
⊢ (e₁ ∘ e₂) 0 = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Fintype/Quotient.lean
@[simp]
lemma finRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
    (a : ∀ i, α i) :
    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (finRecOn fun x => ⟦a x⟧) = fun f x => f a

Tactic:
unfold finRecOn

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h => finHRecOn (fun x => ⟦a x⟧) f ⋯) = fun f x => f a

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h => finHRecOn (fun x => ⟦a x⟧) f ⋯) = fun f x => f a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toNNReal_eq_toNNReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
    x.toNNReal = y.toNNReal ↔ x = y

Proof state:
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x.toNNReal = y.toNNReal ↔ x = y

Tactic:
simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
    {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) :
    k' ∈ Const.alter m k f ↔ k' ∈ m

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
he : (k == k') = false
⊢ k' ∈ alter m k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_flatten (L : List (List α)) : L.flatten.length = (L.map length).sum

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten.length = (map length L).sum

Tactic:
induction L with
| nil => rfl
| cons =>
  simp [flatten, length_append, *]

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : tail✝.flatten.length = (map length tail✝).sum
⊢ (head✝ :: tail✝).flatten.length = (map length (head✝ :: tail✝)).sum

Tactic:
simp [flatten, length_append, *]

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [].flatten.length = (map length []).sum

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Multiset/Range.lean
theorem range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ (range b).map (a + ·)

Proof state:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x => a + x) (range b))

Tactic:
apply range_disjoint_map_add

Result:
no goals

Proof state:
a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x => a + x) (range b)

Tactic:
rw [range_add, add_eq_union_iff_disjoint]

Result:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x => a + x) (range b))