harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem hasSum_coe_mul_geometric_of_norm_lt_one {r : 𝕜} (hr : ‖r‖ < 1) :
    HasSum (fun n ↦ n * r ^ n : ℕ → 𝕜) (r / (1 - r) ^ 2)

Proof state:
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)

Tactic:
convert hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1

Result:
case h.e'_6
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ r / (1 - r) ^ 2 = r * Ring.inverse (1 - r) ^ 2

Proof state:
case h.e'_6
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ r / (1 - r) ^ 2 = r * Ring.inverse (1 - r) ^ 2

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/EqLocus.lean
theorem eqLocus_eq_top {f g : F} : eqLocus f g = ⊤ ↔ f = g

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
⊢ eqLocus f g = ⊤ ↔ f = g

Tactic:
simp [SetLike.ext_iff, DFunLike.ext_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos_sq : ∫ x in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2

Tactic:
field_simp [integral_cos_pow, add_sub_assoc]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_div (a b c : EReal) : a / b / c = a / (b * c)

Proof state:
a b c : EReal
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹

Tactic:
rw [mul_assoc a b⁻¹, mul_inv]

Result:
no goals

Proof state:
a b c : EReal
⊢ a / b / c = a / (b * c)

Tactic:
change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹

Result:
a b c : EReal
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_max {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : ℵ₀ ≤ b) : a * b = max a b :=
  le_antisymm
      (mul_eq_self (ha.trans (le_max_left a b)) ▸
        mul_le_mul' (le_max_left _ _) (le_max_right _ _)) <|
    max_le (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a)
      (by simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b)

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.WF) {l : List α} {k fallback : α} :
    k ∈ m → getKeyD (insertManyIfNewUnit m l) k fallback = getKeyD m k fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ k ∈ m → (insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib/Tactic/Abel.lean
theorem zero_term {α} [AddCommMonoid α] (x a) : @term α _ 0 x a = a

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a

Tactic:
simp [term, zero_nsmul, one_nsmul]

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel_prod_right' {f : α × β → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun a => ∫⁻ b, f (a, b) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b c : A
⊢ (mulLeft R a * mulRight R b) c = (mulRight R b * mulLeft R a) c

Tactic:
exact (mul_assoc a c b).symm

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ Commute (mulLeft R a) (mulRight R b)

Tactic:
ext c

Result:
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b c : A
⊢ (mulLeft R a * mulRight R b) c = (mulRight R b * mulLeft R a) c
-- Mathlib/Order/WellFoundedSet.lean
lemma WellFoundedOn.mapsTo {α β : Type*} {r : α → α → Prop} (f : β → α)
    {s : Set α} {t : Set β} (h : MapsTo f t s) (hw : s.WellFoundedOn r) :
    t.WellFoundedOn (r on f)

Proof state:
α : Type u_6
β : Type u_7
r : α → α → Prop
f : β → α
s : Set α
t : Set β
h : MapsTo f t s
hw : s.WellFoundedOn r
⊢ t.WellFoundedOn (r on f)

Tactic:
exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw

Result:
no goals
-- Mathlib/Tactic/Push.lean
theorem empty_ne_eq_nonempty (s : Set β) : (∅ ≠ s) = s.Nonempty

Proof state:
β : Type u_2
s : Set β
⊢ (∅ ≠ s) = s.Nonempty

Tactic:
rw [ne_comm, ne_empty_eq_nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) :=
  Raw₀.get?_insertMany_empty_list_of_mem k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_if {x : β} {t : Set β} {s : Set α} [Decidable (x ∈ t)] :
    μ (if x ∈ t then s else ∅) = indicator t (fun _ => μ s) x

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst✝ : Decidable (x ∈ t)
⊢ μ (if x ∈ t then s else ∅) = t.indicator (fun x => μ s) x

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
@[simp]
lemma isNone_eq_false_iff (a : Option α) : Option.isNone a = false ↔ Option.isSome a

Proof state:
α : Type u_1
a : Option α
⊢ a.isNone = false ↔ a.isSome = true

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
lemma integral_integral_indicator {mY : MeasurableSpace Y} {ν : Measure Y} (f : X → Y → E)
    {s : Set X} (hs : MeasurableSet s) :
    ∫ x, ∫ y, s.indicator (f · y) x ∂ν ∂μ = ∫ x in s, ∫ y, f x y ∂ν ∂μ

Proof state:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x => f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ

Tactic:
simp_rw [← integral_indicator hs, integral_indicator₂]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma balance_add (f g : ι → G) : balance (f + g) = balance f + balance g

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f g : ι → G
⊢ balance (f + g) = balance f + balance g

Tactic:
simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
@[simp] lemma finite_iUnion_of_subsingleton {ι : Sort*} [Subsingleton ι] {s : ι → Set α} :
    (⋃ i, s i).Finite ↔ ∀ i, (s i).Finite

Proof state:
α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (⋃ i, s i).Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]

Result:
α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (∀ (i : PLift ι), (s i.down).Finite) ∧ {i | (s i.down).Nonempty}.Finite ↔ ∀ (i : ι), (s i).Finite

Proof state:
α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (∀ (i : PLift ι), (s i.down).Finite) ∧ {i | (s i.down).Nonempty}.Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
simp [PLift.forall, Finite.of_subsingleton]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem erase_mk [DecidableEq α] (m : Multiset α)
    (hc : Multiset.card m = n + 1) (a : α) (h : a ∈ m) :
    (mk m hc).erase a h =mk (m.erase a)
        (by rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]) :=
  rfl

Proof state:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (m.erase a).card = n

Tactic:
rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem matPolyEquiv_eval (M : Matrix n n R[X]) (r : R) (i j : n) :
    (matPolyEquiv M).eval (scalar n r) i j = (M i j).eval r

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i j : n
⊢ eval ((scalar n) r) (matPolyEquiv M) i j = eval r (M i j)

Tactic:
rw [matPolyEquiv_eval_eq_map, map_apply]

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
lemma swap_eq_iff_eq_swap {x : α × β} {y : β × α} : x.swap = y ↔ x = y.swap

Proof state:
α : Type u_1
β : Type u_2
x : α × β
y : β × α
⊢ x.swap = y ↔ x = y.swap

Tactic:
aesop

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem eq_aleph'_of_eq_card_ord {o : Ordinal} (ho : o.card.ord = o) : ∃ a, (aleph' a).ord = o :=
  ⟨aleph'.symm o.card, by simpa using ho⟩

Proof state:
o : Ordinal.{u_1}
ho : o.card.ord = o
⊢ (aleph' (aleph'.symm o.card)).ord = o

Tactic:
simpa using ho

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem Nonempty.zero_smul (ht : t.Nonempty) : (0 : Set α) • t = 0 :=
  t.zero_smul_subset.antisymm <| by simpa [mem_smul] using ht

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Set β
ht : t.Nonempty
⊢ 0 ⊆ 0 • t

Tactic:
simpa [mem_smul] using ht

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem eq_of_subset_of_ncard_le (h : s ⊆ t) (h' : t.ncard ≤ s.ncard)
    (ht : t.Finite

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.ncard ≤ s.ncard
ht : autoParam t.Finite _auto✝
⊢ t.encard ≤ s.encard

Tactic:
rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r)

Proof state:
α : Type u_1
r : α → α → Bool
inst✝ : BEq α
a b : Array α
⊢ a.toList.isEqv b.toList r = a.isEqv b r

Tactic:
simp [isEqv_eq_decide, List.isEqv_eq_decide]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem empty_vecAlt1 (α) {h} : vecAlt1 h (![] : Fin 0 → α) = ![]

Proof state:
α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

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

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

Tactic:
rw [add_comm, toIocDiv_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_of_containsKey [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
    (h : containsKey k l) : insertEntry k v l = replaceEntry k v l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ insertEntry k v l = replaceEntry k v l

Tactic:
simp [insertEntry, h]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_mem_unitary_of_mem_skewAdjoint [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸}
    (h : x ∈ skewAdjoint 𝔸) : exp 𝕂 x ∈ unitary 𝔸

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : RCLike 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp 𝕂 x ∈ unitary 𝔸

Tactic:
rw [unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
  exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
  neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[fun_prop] lemma differentiableAt_binEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) :
    DifferentiableAt ℝ binEntropy p

Proof state:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) p

Tactic:
simp only [log_inv, mul_neg]

Result:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => -(p * log p) + -((1 - p) * log (1 - p))) p

Proof state:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
unfold binEntropy

Result:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) p

Proof state:
case funProp.discharger
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ 1 - p ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => -(p * log p) + -((1 - p) * log (1 - p))) p

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
rw [ne_comm, ← sub_ne_zero] at hp₁

Result:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ binEntropy p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_eq_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} {h} :
    m.get a h = m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h✝ : m.val.WF
a : α
fallback : β a
h : m.contains a = true
⊢ m.get a h = m.getD a fallback

Tactic:
simp_to_model using List.getValueCast_eq_getValueCastD

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_map (μ : Measure α) (s : Set β) :
    (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
  Measure.ext fun t ht => by simp [hf.map_apply, ht, hf.measurable ht]

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s t : Set β
ht : MeasurableSet t
⊢ ((Measure.map f μ).restrict s) t = (Measure.map f (μ.restrict (f ⁻¹' s))) t

Tactic:
simp [hf.map_apply, ht, hf.measurable ht]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem zero_ne_one : 0 ≠ (1 : ℚ)

Proof state:
⊢ 0 ≠ 1

Tactic:
rw [ne_comm, ← divInt_one_one, divInt_ne_zero] <;> omega

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_associator {p f g h pf pfg pfgh : C}
    (η_f : p ⊗ f ≅ pf) (η_g : pf ⊗ g ≅ pfg) (η_h : pfg ⊗ h ≅ pfgh) :
    p ◁ (α_ f g h) ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h) =
    normalizeIsoComp (normalizeIsoComp η_f η_g) η_h :=
  Iso.ext (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg pfgh : C
η_f : p ⊗ f ≅ pf
η_g : pf ⊗ g ≅ pfg
η_h : pfg ⊗ h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ico_iff_Ici (h : a < b) :
    ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIciTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsGE h]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem hereditarily_iff : Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Proof state:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Tactic:
rw [← Hereditarily]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem mem_closure_iff_frequently : x ∈ closure s ↔ ∃ᶠ x in 𝓝 x, x ∈ s

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s

Tactic:
rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
  closure_eq_compl_interior_compl, mem_compl_iff, compl_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c)

Proof state:
a b c : Int
⊢ a * (b * c) = b * (a * c)

Tactic:
rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem union_empty {s : AList β} : s ∪ (∅ : AList β) = s :=
  ext <| by simp

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) : bmod x m = x - m * bdiv x m

Proof state:
x : Int
m : Nat
⊢ x.bmod m = x - ↑m * x.bdiv m

Tactic:
rw [← Int.add_sub_cancel (bmod x m), bmod_add_bdiv]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_monomial : coeff (monomial n a) m = if n = m then a else 0

Proof state:
R : Type u
a : R
m n : ℕ
inst✝ : Semiring R
⊢ ((monomial n) a).coeff m = if n = m then a else 0

Tactic:
simp [coeff, Finsupp.single_apply]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_le_div_iff (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

Proof state:
a b : ℕ
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff_mul_le hb, Nat.one_mul]

Result:
no goals
-- Mathlib/FieldTheory/ChevalleyWarning.lean
theorem char_dvd_card_solutions_of_fintype_sum_lt [Fintype ι] {f : ι → MvPolynomial σ K}
    (h : (∑ i, (f i).totalDegree) < Fintype.card σ) :
    p ∣ Fintype.card { x : σ → K // ∀ i, eval x (f i) = 0 }

Proof state:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : Fintype K
inst✝⁵ : Field K
inst✝⁴ : Fintype σ
inst✝³ : DecidableEq σ
inst✝² : DecidableEq K
p : ℕ
inst✝¹ : CharP K p
inst✝ : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i : ι, (f i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), (eval x) (f i) = 0 }

Tactic:
simpa using char_dvd_card_solutions_of_sum_lt p h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_X (H : ¬(1 : R) = 0) : (X : R[X]).support = singleton 1

Proof state:
R : Type u
inst✝ : Semiring R
H : ¬1 = 0
⊢ X.support = {1}

Tactic:
rw [← pow_one X, support_X_pow H 1]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Tower.lean
theorem aeval_algebraMap_eq_zero_iff_of_injective {x : A} {p : R[X]}
    (h : Function.Injective (algebraMap A B)) : aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0

Tactic:
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} :
    InfiniteNeg x ↔ Infinitesimal x⁻¹ ∧ x⁻¹ < 0

Proof state:
x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]

Result:
no goals
-- Mathlib/Data/Multiset/Replicate.lean
theorem count_replicate_self (a : α) (n : ℕ) : count a (replicate n a) = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n

Tactic:
convert List.count_replicate_self a n

Result:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)

Proof state:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)

Tactic:
rw [← coe_count, coe_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_singleton' (l : Array α) : (l.flatMap fun x => #[x]) = l

Proof state:
α : Type u_1
l : Array α
⊢ flatMap (fun x => #[x]) l = l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
l : List α
⊢ flatMap (fun x => #[x]) { toList := l } = { toList := l }

Proof state:
case mk
α : Type u_1
l : List α
⊢ flatMap (fun x => #[x]) { toList := l } = { toList := l }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_sshiftRight' {x y: BitVec w} :
    (x.sshiftRight' y).msb = x.msb

Proof state:
w : Nat
x y : BitVec w
⊢ (x.sshiftRight' y).msb = x.msb

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_atTop [Preorder α] : 𝓝 atTop = ⨅ x : α, 𝓟 (Iic (𝓟 (Ici x)))

Proof state:
α : Type u_2
inst✝ : Preorder α
⊢ 𝓝 atTop = ⨅ x, 𝓟 (Iic (𝓟 (Ici x)))

Tactic:
simp only [atTop, Filter.nhds_iInf, nhds_principal]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_finsupp_self' {ι : Type u} : Module.rank R (ι →₀ R) = #ι

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
ι : Type u
⊢ Module.rank R (ι →₀ R) = #ι

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_le_infEdist_add_edist : infEdist x s ≤ infEdist y s + edist x y :=
  calc
    ⨅ z ∈ s, edist x z ≤ ⨅ z ∈ s, edist y z + edist x y :=
      iInf₂_mono fun _ _ => (edist_triangle _ _ _).trans_eq (add_comm _ _)
    _ = (⨅ z ∈ s, edist y z) + edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ ⨅ z ∈ s, edist y z + edist x y = (⨅ z ∈ s, edist y z) + edist x y

Tactic:
simp only [ENNReal.iInf_add]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_sup_ker_eq_map' :
    LieIdeal.map f I ⊔ LieIdeal.map f (LieHom.ker f) = LieIdeal.map f I

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f I ⊔ map f f.ker = map f I

Tactic:
simpa using map_sup_ker_eq_map (f := f)

Result:
no goals