harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma hom_inv_apply {M N : MagmaCat} (e : M ≅ N) (s : N) : e.hom (e.inv s) = s

Proof state:
M N : MagmaCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem closure_union : closure (s ∪ t) = closure s ∪ closure t

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
⊢ closure (s ∪ t) = closure s ∪ closure t

Tactic:
simp [closure_eq_compl_interior_compl, compl_inter]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_pi_eq_bot (h : ∀ i, jacobson R (M i) = ⊥) : jacobson R (Π i, M i) = ⊥ :=
  le_bot_iff.mp <| (jacobson_pi_le R M).trans <| by simp_rw [h, pi_univ_bot, le_rfl]

Proof state:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), jacobson R (M i) = ⊥
⊢ (pi Set.univ fun x => jacobson R (M x)) ≤ ⊥

Tactic:
simp_rw [h, pi_univ_bot, le_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a fallback : α} {v : β k} : getKeyD a (insertEntryIfNew k v l) fallback =
      if k == a ∧ containsKey k l = false then k else getKeyD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a fallback : α
v : β k
⊢ getKeyD a (insertEntryIfNew k v l) fallback =
    if (k == a) = true ∧ containsKey k l = false then k else getKeyD a l fallback

Tactic:
simp [getKeyD_eq_getKey?, getKey?_insertEntryIfNew, apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Topology/Algebra/Indicator.lean
@[to_additive]
lemma continuous_mulIndicator (hs : ∀ a ∈ frontier s, f a = 1) (hf : ContinuousOn f (closure s)) :
    Continuous (mulIndicator s f)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : ContinuousOn f (closure s)
⊢ Continuous (s.mulIndicator f)

Tactic:
exact continuous_piecewise hs hf continuousOn_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : ContinuousOn f (closure s)
⊢ Continuous (s.mulIndicator f)

Tactic:
classical exact continuous_piecewise hs hf continuousOn_const

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp :
    (coproducts.{w} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
simpa using transfiniteCompositionsOfShape_le_llp_rlp (coproducts.{w} W).pushouts J

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.const_sub [AddCommGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (a - x)) c := fun x => by
  simp only [← sub_sub, h.sub_eq]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (a - x)) (x + c) = -(fun x => f (a - x)) x

Tactic:
simp only [← sub_sub, h.sub_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List (List α)
⊢ count a l.flatten = (map (count a) l).sum

Tactic:
simp only [count_eq_countP, countP_flatten, count_eq_countP']

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Int.comap_cast_atBot [StrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℤ → R) atBot = atBot :=
  comap_embedding_atBot (fun _ _ => Int.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge (-r)
    ⟨-n, by simpa [neg_le] using hn⟩

Proof state:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r

Tactic:
simpa [neg_le] using hn

Result:
no goals
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem restr_of_source_subset {f : Equidecomp X G} {A : Set X} (hA : f.source ⊆ A) :
    f.restr A = f

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f

Tactic:
apply toPartialEquiv_injective

Result:
case a
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv

Proof state:
case a
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv

Tactic:
rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    ¬a ∈ m → m.getKey? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ ¬a ∈ m → m.getKey? a = none

Tactic:
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem dotProduct_mulVec_adjMatrix [NonAssocSemiring α] (x y : V → α) :
    x ⬝ᵥ (G.adjMatrix α).mulVec y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
x y : V → α
⊢ x ⬝ᵥ adjMatrix α G *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0

Tactic:
simp only [dotProduct, mulVec, adjMatrix_apply, ite_mul, one_mul, zero_mul, mul_sum, mul_ite,
  mul_zero]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem singleton_product {a : α} :
    ({a} : Finset α) ×ˢ t = t.map ⟨Prod.mk a, Prod.mk.inj_left _⟩

Proof state:
case h.mk
α : Type u_1
β : Type u_2
t : Finset β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
simp [and_left_comm, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : Finset β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
t : Finset β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ } t
-- Mathlib/Algebra/Order/SuccPred.lean
theorem lt_one_iff_nonpos [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)]
    [SuccAddOrder α] : x < 1 ↔ x ≤ 0

Proof state:
α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ x < 1 ↔ x ≤ 0

Tactic:
rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem le_toNNReal_iff_coe_le' {r : ℝ≥0} {p : ℝ} (hr : 0 < r) : r ≤ Real.toNNReal p ↔ ↑r ≤ p :=
  (le_or_lt 0 p).elim le_toNNReal_iff_coe_le fun hp => by
    simp only [(hp.trans_le r.coe_nonneg).not_le, toNNReal_eq_zero.2 hp.le, hr.not_le]

Proof state:
r : ℝ≥0
p : ℝ
hr : 0 < r
hp : p < 0
⊢ r ≤ p.toNNReal ↔ ↑r ≤ p

Tactic:
simp only [(hp.trans_le r.coe_nonneg).not_le, toNNReal_eq_zero.2 hp.le, hr.not_le]

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
    f (x - n * c) = (-1) ^ n * f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Ring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x - ↑n * c) = (-1) ^ n * f x

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
  Int.cast_one] using h.sub_nsmul_eq n

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem closedBall_prod_same [PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) :
    closedBall x r ×ˢ closedBall y r = closedBall (x, y) r :=
  ext fun z => by simp [Prod.edist_eq]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r

Tactic:
simp [Prod.edist_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma fromOpcycles_eq_zero (hij : ¬ c.Rel i j) :
    K.fromOpcycles i j = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ K.fromOpcycles i j = 0

Tactic:
rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val

Proof state:
n : ℕ
a b : ZMod n
⊢ a.val * b.val % n ≤ a.val * b.val

Tactic:
apply Nat.mod_le

Result:
no goals

Proof state:
n : ℕ
a b : ZMod n
⊢ (a * b).val ≤ a.val * b.val

Tactic:
rw [val_mul]

Result:
n : ℕ
a b : ZMod n
⊢ a.val * b.val % n ≤ a.val * b.val
-- Mathlib/LinearAlgebra/Projection.lean
theorem ofIsCompl_right_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) :
    ofIsCompl h φ ψ (v : E) = ψ v

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
v : ↥q
⊢ (ofIsCompl h φ ψ) ↑v = ψ v

Tactic:
simp [ofIsCompl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} (h : m.1.WF)
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKeyD k' fallback =
      if k == k' then
        if (f (m.get? k)).isSome then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
k k' fallback : α
h : m.val.WF
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_model [alter] using List.getKeyD_alterKey

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem univ_pi_eq_iInter (t : ∀ i, Set (π i)) : pi univ t = ⋂ i, eval i ⁻¹' t i

Proof state:
α : Type u_1
π : α → Type u_12
t : (i : α) → Set (π i)
⊢ univ.pi t = ⋂ i, eval i ⁻¹' t i

Tactic:
simp only [pi_def, iInter_true, mem_univ]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_singleton_segment (a b c : E) :
    convexJoin 𝕜 {a} (segment 𝕜 b c) = convexHull 𝕜 {a, b, c}

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c : E
⊢ convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜) {a, b, c}

Tactic:
rw [← segment_same 𝕜, convexJoin_segments, insert_idem]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_intCast (n : ℤ) : (n : HomogeneousLocalization 𝒜 x).val = n :=
  show val (Int.castDef n) = _ by cases n <;> simp [Int.castDef, *]

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
n : ℤ
⊢ n.castDef.val = ↑n

Tactic:
cases n <;> simp [Int.castDef, *]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_lintegral_le (hint : ∫⁻ a, f a ∂μ ≠ ∞) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ ∫⁻ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
⊢ ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [laverage_eq_lintegral] using
  exists_not_mem_null_laverage_le (IsProbabilityMeasure.ne_zero μ) hint hN

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivWithinAt.cpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x)
    (h0 : f x ∈ slitPlane) : HasDerivWithinAt (fun x => f x ^ g x)
      (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x

Proof state:
f g : ℂ → ℂ
s : Set ℂ
f' g' x : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x

Tactic:
simpa only [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem coeff_add_ne_zero {f : Ring.Perfection R p} {n : ℕ} (hfn : coeff R p n f ≠ 0) (k : ℕ) :
    coeff R p (n + k) f ≠ 0 :=
  Nat.recOn k hfn fun k ih h => ih <| by
    erw [← coeff_pow_p, RingHom.map_pow, h, zero_pow hp.1.ne_zero]

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k.succ)) f = 0
⊢ (coeff R p (n + k)) f = 0

Tactic:
erw [← coeff_pow_p, RingHom.map_pow, h, zero_pow hp.1.ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (insertMany empty l).1.getKey? k' = some k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (empty.insertMany l).val.getKey? k' = some k

Tactic:
rw [getKey?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem CovBy.Iio_eq (h : a ⋖ b) : Iio b = Iic a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iio b = Iic a

Tactic:
rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
@[simp] lemma range_domRestrict [Module R M₂] (K : Submodule R M) (f : M →ₗ[R] M₂) :
    range (domRestrict f K) = K.map f

Proof state:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
K : Submodule R M
f : M →ₗ[R] M₂
x✝ : M₂
⊢ x✝ ∈ range (f.domRestrict K) ↔ x✝ ∈ map f K

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
K : Submodule R M
f : M →ₗ[R] M₂
⊢ range (f.domRestrict K) = map f K

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
K : Submodule R M
f : M →ₗ[R] M₂
x✝ : M₂
⊢ x✝ ∈ range (f.domRestrict K) ↔ x✝ ∈ map f K
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.sum_tmul_basis_left_eq_zero
    (b : ι →₀ N) (h : (b.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = 0) : b = 0 :=
  have := Classical.decEq ι
  (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective (a₂ := 0) <| by simpa

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
b : ι →₀ N
h : (b.sum fun i n => ℬ i ⊗ₜ[R] n) = 0
this : DecidableEq ι
⊢ (equivFinsuppOfBasisLeft ℬ).symm b = (equivFinsuppOfBasisLeft ℬ).symm 0

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_eq_emod_iff_emod_sub_eq_zero {m n k : Int} : m % n = k % n ↔ (m - k) % n = 0 :=
  (emod_sub_cancel_right k).symm.trans <| by simp [Int.sub_self]

Proof state:
m n k : Int
⊢ (m - k) % n = (k - k) % n ↔ (m - k) % n = 0

Tactic:
simp [Int.sub_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_singletons (x : E) : convexJoin 𝕜 {x} {y} = segment 𝕜 x y

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
y x : E
⊢ convexJoin 𝕜 {x} {y} = segment 𝕜 x y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s

Proof state:
α : Type u_1
s : Set α
⊢ (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s

Tactic:
rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_pow' (h : n ≠ 0) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n

Tactic:
rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
unfold orderOf

Result:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n
-- Mathlib/Topology/Maps/Basic.lean
theorem preimage_frontier_eq_frontier_preimage (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
    f ⁻¹' frontier s = frontier (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hfc : Continuous f
s : Set Y
⊢ f ⁻¹' frontier s = frontier (f ⁻¹' s)

Tactic:
simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
  hf.preimage_closure_eq_closure_preimage hfc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_inj {s t : Set α} (hs : MeasurableSet s) (hsμ : μ s ≠ ∞)
    (ht : MeasurableSet t) (htμ : μ t ≠ ∞) {c : E} (hc : c ≠ 0) :
    indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
hsμ : μ s ≠ ⊤
ht : MeasurableSet t
htμ : μ t ≠ ⊤
c : E
hc : c ≠ 0
⊢ indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᶠ[ae μ] t

Tactic:
simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem affineIndependent_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
    (h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
    AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]

Tactic:
simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem not_nontrivial_empty : ¬ (∅ : Finset α).Nontrivial

Proof state:
α : Type u_1
⊢ ¬∅.Nontrivial

Tactic:
simp [Finset.Nontrivial]

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem setLIntegral_condDistrib_of_measurableSet (hX : Measurable X) (hY : AEMeasurable Y μ)
    (hs : MeasurableSet s) {t : Set α} (ht : MeasurableSet[mβ.comap X] t) :
    ∫⁻ a in t, condDistrib Y X μ (X a) s ∂μ = μ (t ∩ Y ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (t ∩ Y ⁻¹' s)

Tactic:
obtain ⟨t', ht', rfl⟩ := ht

Result:
case intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
⊢ ∫⁻ (a : α) in X ⁻¹' t', ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t' ∩ Y ⁻¹' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
⊢ ∫⁻ (a : α) in X ⁻¹' t', ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t' ∩ Y ⁻¹' s)

Tactic:
rw [setLIntegral_preimage_condDistrib hX hY hs ht']

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[simp]
lemma neg_iff {f : 𝕜 → E} {x : 𝕜} :
    MeromorphicAt (-f) x ↔ MeromorphicAt f x :=
  ⟨fun h ↦ by simpa only [neg_neg] using h.neg, MeromorphicAt.neg⟩

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt (-f) x
⊢ MeromorphicAt f x

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_toPMF : p.toMeasure.toPMF = p :=
  PMF.ext fun x => by
    rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]

Proof state:
α : Type u_1
inst✝² : Countable α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
x : α
⊢ p.toMeasure.toPMF x = p x

Tactic:
rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem algebraMap_injective : (algebraMap R ℍ[R,c₁,c₂,c₃] : _ → _).Injective :=
  fun _ _ ↦ by simp [algebraMap_eq]

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
x✝¹ x✝ : R
⊢ (algebraMap R ℍ[R,c₁,c₂,c₃]) x✝¹ = (algebraMap R ℍ[R,c₁,c₂,c₃]) x✝ → x✝¹ = x✝

Tactic:
simp [algebraMap_eq]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem Function.LeftInverse.cast_eq {γ : β → Sort v} {f : α → β} {g : β → α}
    (h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :
    cast (congr_arg (fun a ↦ γ (f a)) (h a)) (C (g (f a))) = C a

Proof state:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast ⋯ (C (g (f a))) = C a

Tactic:
rw [cast_eq_iff_heq, h]

Result:
no goals
-- Mathlib/NumberTheory/Rayleigh.lean
theorem Irrational.beattySeq_symmDiff_beattySeq_pos {r s : ℝ}
    (hrs : r.IsConjExponent s) (hr : Irrational r) :
    {beattySeq r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

Tactic:
rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]

Result:
no goals