harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem zmodChar_primitive_of_primitive_root (n : ℕ) [NeZero n] {ζ : C} (h : IsPrimitiveRoot ζ n) :
    IsPrimitive (zmodChar n ((IsPrimitiveRoot.iff_def ζ n).mp h).left)

Proof state:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ ∀ (a : ZMod n), (zmodChar n ⋯) a = 1 → a = 0

Tactic:
intro a ha

Result:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : (zmodChar n ⋯) a = 1
⊢ a = 0

Proof state:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : (zmodChar n ⋯) a = 1
⊢ a = 0

Tactic:
rw [zmodChar_apply, ← pow_zero ζ] at ha

Result:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = ζ ^ 0
⊢ a = 0

Proof state:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = ζ ^ 0
⊢ a = 0

Tactic:
exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

Result:
no goals

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ (zmodChar n ⋯).IsPrimitive

Tactic:
apply zmod_char_primitive_of_eq_one_only_at_zero

Result:
case hψ
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ ∀ (a : ZMod n), (zmodChar n ⋯) a = 1 → a = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <+: l₁.filter p ↔ ∃ l, l <+: l₁ ∧ l₂ = l.filter p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ l₂ <+: filter p l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filter p l

Tactic:
rw [← filterMap_eq_filter, isPrefix_filterMap_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem comapRight_apply' (κ : Kernel α β) (hf : MeasurableEmbedding f) (a : α) {t : Set γ}
    (ht : MeasurableSet t) : comapRight κ hf a t = κ a (f '' t)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((κ.comapRight hf) a) t = (κ a) (f '' t)

Tactic:
rw [comapRight_apply,
  Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]

Result:
no goals
-- Mathlib/Tactic/Push.lean
theorem not_iff : (¬ (p ↔ q)) = ((p ∧ ¬ q) ∨ (¬ p ∧ q)) := propext <|
  _root_.not_iff.trans <| iff_iff_and_or_not_and_not.trans <| by rw [not_not, or_comm]

Proof state:
p q : Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
rw [not_not, or_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.nndist_eq (a b : ℝ≥0) : nndist a b = max (a - b) (b - a) :=
  eq_of_forall_ge_iff fun _ => by
    simp only [max_le_iff, tsub_le_iff_right (α := ℝ≥0)]
    simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, abs_sub_le_iff,
      tsub_le_iff_right, NNReal.coe_add]

Proof state:
a b x✝ : ℝ≥0
⊢ nndist a b ≤ x✝ ↔ (a - b) ⊔ (b - a) ≤ x✝

Tactic:
simp only [max_le_iff, tsub_le_iff_right (α := ℝ≥0)]

Result:
a b x✝ : ℝ≥0
⊢ nndist a b ≤ x✝ ↔ a ≤ x✝ + b ∧ b ≤ x✝ + a

Proof state:
a b x✝ : ℝ≥0
⊢ nndist a b ≤ x✝ ↔ a ≤ x✝ + b ∧ b ≤ x✝ + a

Tactic:
simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, abs_sub_le_iff,
  tsub_le_iff_right, NNReal.coe_add]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
@[simp]
lemma Topology.isInducing_prod_const {y : Y} {f : X → Z} :
    IsInducing (fun x => (f x, y)) ↔ IsInducing f

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing fun x => (f x, y)) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
  Function.comp_def, induced_const, inf_top_eq]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsRelPrime.prod_right_iff : IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)

Proof state:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)

Tactic:
simpa only [isRelPrime_comm] using IsRelPrime.prod_left_iff (α := α)

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_basis_Ioo' [OrderTopology α] {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  ⟨fun s => (mem_nhds_iff_exists_Ioo_subset' hl hu).trans <| by simp⟩

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
hl : ∃ l, l < a
hu : ∃ u, a < u
s : Set α
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) ↔ ∃ i, (i.1 < a ∧ a < i.2) ∧ Ioo i.1 i.2 ⊆ s

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setLaverage_congr_fun (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
    ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in s, g x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ

Tactic:
simp only [laverage_eq, setLIntegral_congr_fun hs h]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem isQuadratic_χ₈ : χ₈.IsQuadratic

Proof state:
⊢ χ₈.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Result:
⊢ ∀ (a : ZMod 8), χ₈ a = 0 ∨ χ₈ a = 1 ∨ χ₈ a = -1

Proof state:
⊢ ∀ (a : ZMod 8), χ₈ a = 0 ∨ χ₈ a = 1 ∨ χ₈ a = -1

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
lemma half_sub (a : K) : a / 2 - a = -(a / 2)

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a / 2 - a = -(a / 2)

Tactic:
rw [← neg_sub, sub_half]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem coe_injective : Injective ((↑) : Ultrafilter α → Filter α)
  | ⟨f, h₁, h₂⟩, ⟨g, _, _⟩, _ => by congr

Proof state:
α : Type u
f : Filter α
h₁ : f.NeBot
h₂ : ∀ (g : Filter α), g.NeBot → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : g.NeBot
le_of_le✝ : ∀ (g_1 : Filter α), g_1.NeBot → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem mul_sub_mul_div_mul_neg_iff (hc : c ≠ 0) (hd : d ≠ 0) :
    (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d

Tactic:
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b

Proof state:
case intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
h₁ : ra a₁✝ a₂✝
h₂ : rb b₁✝ b₂✝
⊢ Prod.Lex ra rb { fst := a₁✝, snd := b₁✝ } { fst := a₂✝, snd := b₂✝ }

Tactic:
exact Prod.Lex.left _ _ h₁

Result:
no goals

Proof state:
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a b : α × β
h : RProd ra rb a b
⊢ Prod.Lex ra rb a b

Tactic:
cases h with
| intro h₁ h₂ => exact Prod.Lex.left _ _ h₁

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem mapAccumr₂_snoc (f : α → β → σ → σ × φ) (x : α) (y : β) :
    mapAccumr₂ f (xs.snoc x) (ys.snoc y) s
    = let q := f x y s
      let r := mapAccumr₂ f xs ys q.1
      (r.1, r.2.snoc q.2)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs, ys using Vector.inductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem find_of_valid (p s) : find s p = ⟨utf8Len (s.1.takeWhile (!p ·))⟩

Proof state:
p : Char → Bool
s : String
⊢ s.find p = { byteIdx := utf8Len (List.takeWhile (fun x => !p x) s.data) }

Tactic:
simpa using findAux_of_valid p [] s.1 []

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₂_yonedaEquivFst {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst

Tactic:
simp only [YonedaCollection.yonedaEquivFst_eq, map₂_fst, yonedaEquiv_naturality]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive nsmul_zero, simp] lemma one_pow : ∀ n, (1 : M) ^ n = 1
  | 0 => pow_zero _
  | n + 1 => by rw [pow_succ, one_pow, one_mul]

Proof state:
M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 ^ (n + 1) = 1

Tactic:
rw [pow_succ, one_pow, one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Slice.lean
@[simp] lemma sized_empty : (∅ : Set (Finset α)).Sized r

Proof state:
α : Type u_1
r : ℕ
⊢ Sized r ∅

Tactic:
simp [Sized]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_incl_self : comap I.incl I = ⊤

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ comap I.incl I = ⊤

Tactic:
ext

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ comap I.incl I ↔ m✝ ∈ ⊤

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ comap I.incl I ↔ m✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GradedMonoid.lean
theorem GradedMonoid.list_prod_ofFn_eq_dProd {n : ℕ} (f : Fin n → GradedMonoid A) :
    (List.ofFn f).prod =
      GradedMonoid.mk _ ((List.finRange n).dProd (fun i => (f i).1) fun i => (f i).2)

Proof state:
ι : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ (List.ofFn f).prod =
    mk ((List.finRange n).dProdIndex fun i => (f i).fst)
      ((List.finRange n).dProd (fun i => (f i).fst) fun i => (f i).snd)

Tactic:
rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma eq_zero_of_smul_eq_zero
    (r : R) (hr : r ∈ S) (x : LocalizedModule S M) (hx : r • x = 0) : x = 0

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : x = Localization.mk 1 ⟨r, hr⟩ • 0
⊢ x = 0

Tactic:
rw [hx, smul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : r • x = 0
⊢ x = 0

Tactic:
rw [smul_eq_iff_of_mem (hr := hr)] at hx

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : x = Localization.mk 1 ⟨r, hr⟩ • 0
⊢ x = 0
-- Mathlib/Data/Complex/Trigonometric.lean
theorem norm_exp (z : ℂ) : ‖exp z‖ = Real.exp z.re

Proof state:
z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
  mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_apply_eq_self : s.mulIndicator f a = f a ↔ a ∉ s → f a = 1 :=
  letI := Classical.dec (a ∈ s)
  ite_eq_left_iff.trans (by rw [@eq_comm _ (f a)])

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ a ∉ s → 1 = f a ↔ a ∉ s → f a = 1

Tactic:
rw [@eq_comm _ (f a)]

Result:
no goals
-- Mathlib/Data/ENNReal/Operations.lean
theorem toReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
    ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toReal (f a)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ i ∈ s, ↑(f i).toNNReal = ∑ a ∈ s, (f a).toReal

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

Tactic:
rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]

Result:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ i ∈ s, ↑(f i).toNNReal = ∑ a ∈ s, (f a).toReal
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.mul_eq_one_iff {σ τ : Perm α} (hστ : Disjoint σ τ) :
    σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Proof state:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Tactic:
simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_pair_of_symmetric (hr : Symmetric r) : Set.Pairwise {a, b} r ↔ a ≠ b → r a b

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
hr : Symmetric r
⊢ {a, b}.Pairwise r ↔ a ≠ b → r a b

Tactic:
simp [pairwise_insert_of_symmetric hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ l.zipIdx k) : x.2 < l.length + k

Proof state:
α : Type u_1
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < l.length + k

Tactic:
simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx h

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_sub_Icc : (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)

Tactic:
simp [← Ici_inter_Iic, inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
    {f : Option β → Option β} {h : k ∈ Const.alter m k f} :
    (Const.alter m k f).getKey k h = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : Option β → Option β
h : k ∈ alter m k f
⊢ (alter m k f).getKey k h = k

Tactic:
simp [getKey_alter]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem sum_nat_mod (s : Finset α) (n : ℕ) (f : α → ℕ) :
    (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_nat_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl

Proof state:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Result:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n
-- Mathlib/Data/Nat/BinaryRec.lean
theorem testBit_bit_zero (b n) : (bit b n).testBit 0 = b

Proof state:
b : Bool
n : Nat
⊢ (bit b n).testBit 0 = b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_eq_self_iff {p} {l : Array α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ { toList := l }.eraseP p = { toList := l } ↔ ∀ (a : α), a ∈ { toList := l } → ¬p a = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ l.eraseP p = l ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ { toList := l }.eraseP p = { toList := l } ↔ ∀ (a : α), a ∈ { toList := l } → ¬p a = true
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_span_singleton_mul {x y : A} : x ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ map ((LinearMap.mul R A) y) P ↔ ∃ z ∈ P, Mul.mul y z = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_two_mul (hf : Involutive f) (n : ℕ) : f^[2 * n] = id

Proof state:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id

Tactic:
rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive add_sub_one_nsmul]
lemma pow_sub_one_mul (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_tensor_comp (f : W ⟶ X) (g : X ⟶ Y) : 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem comap_top (f : α → β) : comap f ⊤ = ⊤ :=
  ext_nonempty fun s hs => by rw [comap_apply, top_apply hs, top_apply (hs.image _)]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ ((comap f) ⊤) s = ⊤ s

Tactic:
rw [comap_apply, top_apply hs, top_apply (hs.image _)]

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem two_nsmul (x : R) : 2 • x = 0

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
rw [two_smul, add_self_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma π_comp_colimitRightOpIsoUnopLimit_inv (F : Jᵒᵖ ⥤ C) [HasLimit F] (j : Jᵒᵖ) :
    (limit.π F j).op ≫ (colimitRightOpIsoUnopLimit F).inv = colimit.ι F.rightOp j.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ (limit.π F j).op ≫ (colimitRightOpIsoUnopLimit F).inv = colimit.ι F.rightOp (unop j)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem diff_eq_compl_inter {s t : Set α} : s \ t = tᶜ ∩ s

Proof state:
α : Type u
s t : Set α
⊢ s \ t = tᶜ ∩ s

Tactic:
rw [diff_eq, inter_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ConvexOn.map_integral_le [IsProbabilityMeasure μ] (hg : ConvexOn ℝ s g)
    (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ)
    (hgi : Integrable (g ∘ f) μ) : g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ

Tactic:
simpa only [average_eq_integral] using hg.map_average_le hgc hsc hfs hfi hgi

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem apply (n : ℕ) (f : C(I, ℝ)) (x : I) :
    bernsteinApproximation n f x = ∑ k : Fin (n + 1), f k/ₙ * bernstein n k x

Proof state:
n : ℕ
f : C(↑I, ℝ)
x : ↑I
⊢ (bernsteinApproximation n f) x = ∑ k : Fin (n + 1), f k/ₙ * (bernstein n ↑k) x

Tactic:
simp [bernsteinApproximation]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem centerAndRescale_radius {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) :
    a.centerAndRescale.r (last N) = 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
⊢ a.centerAndRescale.r (last N) = 1

Tactic:
simp [SatelliteConfig.centerAndRescale, inv_mul_cancel₀ (a.rpos _).ne']

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem affineHomeomorph_image_Ioo {𝕜 : Type*} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)

Proof state:
𝕜 : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_mul_sqrt_self (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a * sqrt a = a

Tactic:
rw [← nnrpow_two _, nnrpow_sqrt_two _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mem_toNat' : ∀ {a : Int} {n : Nat}, toNat' a = some n ↔ a = n
  | (m : Nat), n => by simp [toNat', Int.ofNat_inj]
  | -[m+1], n => by constructor <;> nofun

Proof state:
m n : Nat
⊢ (↑m).toNat' = some n ↔ ↑m = ↑n

Tactic:
simp [toNat', Int.ofNat_inj]

Result:
no goals

Proof state:
m n : Nat
⊢ -[m+1].toNat' = some n ↔ -[m+1] = ↑n

Tactic:
constructor <;> nofun

Result:
no goals
-- Mathlib/Topology/Algebra/NonUnitalAlgebra.lean
theorem isClosedEmbedding_coe (x : A) : Topology.IsClosedEmbedding ((↑) : elemental R x → A) where
  eq_induced := rfl
  injective := Subtype.coe_injective
  isClosed_range

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousConstSMul R A
x : A
⊢ IsClosed (Set.range Subtype.val)

Tactic:
simpa using isClosed R x

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem smul_iSup {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    {ι : Sort*} (f : ι → OuterMeasure α) (c : R) :
    (c • ⨆ i, f i) = ⨆ i, c • f i :=
  ext fun s => by simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]

Proof state:
α : Type u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
ι : Sort u_4
f : ι → OuterMeasure α
c : R
s : Set α
⊢ (c • ⨆ i, f i) s = (⨆ i, c • f i) s

Tactic:
simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_insert (a : α) (s : Set α) (t : α → Set β) :
    ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Proof state:
α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
lemma biprod.decomp_hom_from (f : X ⊞ Y ⟶ Z) :
    ∃ f₁ f₂, f = biprod.fst ≫ f₁ + biprod.snd ≫ f₂ :=
  ⟨biprod.inl ≫ f, biprod.inr ≫ f, by aesop⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
Z : C
f : X ⊞ Y ⟶ Z
⊢ f = fst ≫ inl ≫ f + snd ≫ inr ≫ f

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma coheight_top (α : Type*) [Preorder α] [OrderTop α] : coheight (⊤ : α) = 0

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ coheight ⊤ = 0

Tactic:
simp

Result:
no goals