harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Image.lean
theorem preimage_eq_empty {s : Set β} (h : Disjoint s (range f)) :
    f ⁻¹' s = ∅

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅

Tactic:
simpa using h.preimage f

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem coe_add : ((x + y : R) : ℍ[R,c₁,c₂,c₃]) = x + y

Proof state:
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_one_right' (r : R) : multichoose r 1 = r ^ 1

Proof state:
R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose r 1 = r ^ 1

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
  factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
  one_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem _root_.RCLike.intervalIntegral_ofReal {𝕜 : Type*} [RCLike 𝕜] {a b : ℝ}
    {μ : Measure ℝ} {f : ℝ → ℝ} : (∫ x in a..b, (f x : 𝕜) ∂μ) = ↑(∫ x in a..b, f x ∂μ)

Proof state:
𝕜 : Type u_6
inst✝ : RCLike 𝕜
a b : ℝ
μ : Measure ℝ
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, integral_ofReal, RCLike.ofReal_sub]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
@[simp]
lemma sub_filter_eq_filter_not (p : α → Prop) [DecidablePred p] (s : Multiset α) :
    s - s.filter p = s.filter fun a ↦ ¬ p a

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a => ¬p a) s)

Tactic:
by_cases h : p a <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s - filter p s = filter (fun a => ¬p a) s

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a => ¬p a) s)
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem sub (x : E) : f (c - x) = f (c + x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ ↑f (c - x) = ↑f (c + x)

Tactic:
simp [f.apply, ContDiffBumpBase.symmetric]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {f : α → β}
    (hf : MeasurePreserving f μa μb) (c : R) : MeasurePreserving f (c • μa) (c • μb) where
  measurable := hf.measurable
  map_eq

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
⊢ map f (c • μa) = c • μb

Tactic:
rw [Measure.map_smul, hf.map_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem coord_repr_symm (b : Basis ι R M) (i : ι) (f : ι →₀ R) :
    b.coord i (b.repr.symm f) = f i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
f : ι →₀ R
⊢ (b.coord i) (b.repr.symm f) = f i

Tactic:
simp only [repr_symm_apply, coord_apply, repr_linearCombination]

Result:
no goals
-- Mathlib/Probability/Distributions/Pareto.lean
lemma paretoPDF_of_lt (hx : x < t) : paretoPDF t r x = 0

Proof state:
t r x : ℝ
hx : x < t
⊢ paretoPDF t r x = 0

Tactic:
simp only [paretoPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem monomial_eq : monomial s a = C a * (s.prod fun n e => X n ^ e : MvPolynomial σ R)

Proof state:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial s) a = C a * s.prod fun n e => X n ^ e

Tactic:
simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_floor_left_pure_sub_one (n : ℤ) :
    Tendsto (floor : α → ℤ) (𝓝[<] n) (pure (n - 1))

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[<] ↑n) (pure (n - 1))

Tactic:
simpa only [ceil_intCast] using tendsto_floor_left_pure_ceil_sub_one (n : α)

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_eq_empty_iff : Ioc a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩

Proof state:
o₁ o₂ : Ordering
h : o₁.swap = o₂.swap
⊢ o₁ = o₂

Tactic:
simpa using congrArg swap h

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_invMul_mul_mul (A B C : Finset G) :
    #B * #(A⁻¹ * C) ≤ #(B * A) * #(B * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B * A) * #(B * C)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_invMul_invMul A B⁻¹ C

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
@[reassoc (attr := simp)]
lemma inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) :
    (inl S.f).v i j h ≫ (descShortComplex S).f j = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
i j : ℤ
h : i + -1 = j
⊢ (inl S.f).v i j h ≫ (descShortComplex S).f j = 0

Tactic:
simp [descShortComplex]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_le_card_of_leftTotal_unique (h₁ : LeftTotal r) (h₂ : LeftUnique r) :
    Fintype.card α ≤ Fintype.card β :=
  card_le_card_of_forall_subsingleton r (by simpa using h₁) fun _ _ _ ha₁ _ ha₂ ↦ h₂ ha₁.2 ha₂.2

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : LeftTotal r
h₂ : LeftUnique r
⊢ ∀ a ∈ univ, ∃ b ∈ univ, r a b

Tactic:
simpa using h₁

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma sub_succ_le_sub_of_le {n : ℕ} {u v : Fin (n + 2)} (h : u < v) : v - (u + 1) < v - u

Proof state:
n : ℕ
u v : Fin (n + 2)
h : u < v
⊢ v - (u + 1) < v - u

Tactic:
fin_omega

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma forall_apply_eq_zero : (∀ ψ : AddChar α ℂ, ψ a = 1) ↔ a = 0

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∀ (ψ : AddChar α ℂ), ψ a = 1) ↔ a = 0

Tactic:
simpa using exists_apply_ne_zero.not

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma wInner_cWeight_eq_one_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 1 ↔ ψ₁ = ψ₂

Tactic:
rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_re_le (a : ℝ) : frontier { z : ℂ | z.re ≤ a } = { z | z.re = a }

Proof state:
a : ℝ
⊢ frontier {z | z.re ≤ a} = {z | z.re = a}

Tactic:
simpa only [frontier_Iic] using frontier_preimage_re (Iic a)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem stirlingSeq_one : stirlingSeq 1 = exp 1 / √2

Proof state:
⊢ stirlingSeq 1 = rexp 1 / √2

Tactic:
rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cotrident.coequalizer_ext [Nonempty J] (s : Cotrident f) {W : C} {k l : s.pt ⟶ W}
    (h : s.π ≫ k = s.π ≫ l) : ∀ j : WalkingParallelFamily J, s.ι.app j ≫ k = s.ι.app j ≫ l
  | zero => by rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
  | one => h

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l

Tactic:
rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.congr_cofinite (hf : Multipliable f) (hfg : f =ᶠ[cofinite] g) :
    Multipliable g :=
  hfg.multipliable_compl_iff.mp <| (hfg.multipliable_compl_iff.mpr hf).congr (by simp)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hf : Multipliable f
hfg : f =ᶠ[cofinite] g
⊢ ∀ (b : ↑{x | (fun x => f x = g x) x}ᶜᶜ), (f ∘ Subtype.val) b = (g ∘ Subtype.val) b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem isCompact_Ioc_iff {a b : α} : IsCompact (Set.Ioc a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ioc_iff.mp h.isClosed, by simp_all⟩

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioc a b)

Tactic:
simp_all

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_union (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf s a ⊓ truncatedInf t a

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a

Tactic:
simpa only [truncatedInf_of_mem, hs, ht, upper_aux.2 (Or.inl hs), filter_union] using
  inf'_union _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
  | ⟨e, he⟩, ⟨f, hf⟩ =>
    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩

Proof state:
a b c d e : Nat
he : b = a * e
f : Nat
hf : d = c * f
⊢ b * d = a * c * (e * f)

Tactic:
simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem re_eq_self_of_le {a : K} (h : ‖a‖ ≤ re a) : (re a : K) = a

Proof state:
K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ ↑(re a) = a

Tactic:
rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atBot_iff [NeBot l] :
    Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_inter (s t : Finset α) : filter p s ∩ t = filter p (s ∩ t)

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ t = filter p (s ∩ t)

Tactic:
ext

Result:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p s ∩ t ↔ a✝ ∈ filter p (s ∩ t)

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p s ∩ t ↔ a✝ ∈ filter p (s ∩ t)

Tactic:
simp only [mem_inter, mem_filter, and_right_comm]

Result:
no goals
-- Mathlib/Data/Fintype/Sigma.lean
lemma Set.biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
    ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩

Proof state:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toStream_toList {t : RBSet α cmp} : (toStream t).toList = t.toList

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ (toStream t).toList = t.toList

Tactic:
simp [toStream_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma degree_polynomial [Nontrivial R] : W'.polynomial.degree = 2

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
          d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly.degree =
    2

Tactic:
exact Cubic.degree_of_b_ne_zero' one_ne_zero

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ W'.polynomial.degree = 2

Tactic:
rw [polynomial_eq]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
          d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly.degree =
    2
-- Mathlib/Data/Nat/Init.lean
lemma pred_eq_of_eq_succ (H : m = n.succ) : m.pred = n

Proof state:
m n : ℕ
H : m = n.succ
⊢ m.pred = n

Tactic:
simp [H]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_left (hab : a ≤ b) : Ioc a b ∪ {a} = Icc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b

Tactic:
rw [← Icc_diff_left, diff_union_self,
  union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma codisjoint_mk_iff {p q : Submodule R M}
    (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) :
    Codisjoint (α := f.invtSubmodule) ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q

Tactic:
rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
  Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive one_sub_natCast_zsmul]
lemma zpow_one_sub_natCast (a : G) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a 1 n

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vadd_vsub_vadd_cancel_right (v₁ v₂ : G) (p : P) : (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
⊢ (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂

Tactic:
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux3 (y z : E) :
    ‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)

Tactic:
convert parallelogram_identity (y + z) z using 4 <;> abel

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Computable f)
    (hg : Computable₂ g) (hh : Computable₂ h) :
    @Computable _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
  option_some_iff.1 <|
    (cond (nat_bodd.comp <| encode_iff.2 hf)
          (option_map (Computable.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hh)
          (option_map (Computable.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hg)).of_eq
      fun a => by
        rcases f a with b | c <;> simp [Nat.div2_val]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
rcases f a with b | c <;> simp [Nat.div2_val]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_eq_smul_add (x y : V) : midpoint R x y = (⅟ 2 : R) • (x + y)

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y = ⅟2 • (x + y)

Tactic:
rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
  two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma mk₀_zero (m₀ : M) (hm₀ : m₀ = 0) : mk₀ m₀ hm₀ (0 : X ⟶ Y) = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y : C
inst✝ : Preadditive C
m₀ : M
hm₀ : m₀ = 0
⊢ mk₀ m₀ hm₀ 0 = 0

Tactic:
simp [mk₀]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem eq_insertNth_iff {p : Fin (n + 1)} {a : α p} {f : ∀ i, α (p.succAbove i)} {g : ∀ j, α j} :
    g = insertNth p a f ↔ g p = a ∧ removeNth p g = f

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

Tactic:
simpa [eq_comm] using insertNth_eq_iff

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueSet_eq_empty_iff : G.cliqueSet n = ∅ ↔ G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n

Tactic:
simp_rw [CliqueFree, Set.eq_empty_iff_forall_not_mem, mem_cliqueSet_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_op [T2Space 𝔸] (x : 𝔸) : exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
⊢ exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x)

Tactic:
simp_rw [exp, expSeries_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_of_not_le (hm_not : ¬m ≤ m₀) : μ[f|m] = 0

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm_not : ¬m ≤ m₀
⊢ μ[f|m] = 0

Tactic:
rw [condExp, dif_neg hm_not]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_zero' (o : ONote) (h : fundamentalSequence o = Sum.inl none) :
    fastGrowing o = Nat.succ

Proof state:
o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ o.fastGrowing = Nat.succ

Tactic:
rw [fastGrowing_def h]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Independence.lean
theorem independent_iff_not_dependent : Independent f ↔ ¬Dependent f

Proof state:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬Dependent f

Tactic:
rw [dependent_iff_not_independent, Classical.not_not]

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.integrable_truncation [IsFiniteMeasure μ]
    (hf : AEStronglyMeasurable f μ) {A : ℝ} : Integrable (truncation f A) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ Integrable (truncation f A) μ

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Tactic:
exact hf.memLp_truncation

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
lemma not_isLeft_and_isRight {x : α ⊕ β} : ¬(x.isLeft ∧ x.isRight)

Proof state:
α : Type u
β : Type v
x : α ⊕ β
⊢ ¬(x.isLeft = true ∧ x.isRight = true)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
lemma ArithmeticFunction.const_one_eq_zeta {R : Type*} [Semiring R] {n : ℕ} (hn : n ≠ 0) :
    (1 : ℕ → R) n = (ζ ·) n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ 1 n = ↑((fun x => ζ x) n)

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem partNum_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) :
    g.partNums.get? n = some gp.a

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partNums.get? n = some gp.a

Tactic:
simp [partNums, s_nth_eq]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atBot_of_pos (hr : 0 < r) :
    Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α} {fallback : β}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    getD (insertMany m l) k fallback = getD m k fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
fallback : β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ getD (insertMany m l) k fallback = getD m k fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem not_modEq_iff_toIcoDiv_eq_toIocDiv :
    ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b

Tactic:
rw [not_modEq_iff_toIcoMod_eq_toIocMod hp, toIcoMod, toIocMod, sub_right_inj,
  zsmul_left_inj hp]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_singleton_mem (i : ι) {r : ℝ} (hr : 0 < r) : (p i).ball 0 r ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨{i}, _, hr, by rw [Finset.sup_singleton]⟩

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
i : ι
r : ℝ
hr : 0 < r
⊢ (p i).ball 0 r = ({i}.sup p).ball 0 r

Tactic:
rw [Finset.sup_singleton]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toStream_toList' {t : RBNode α} {s} : (t.toStream s).toList = t.toList ++ s.toList

Proof state:
α : Type u_1
t : RBNode α
s : RBNode.Stream α
⊢ (t.toStream s).toList = t.toList ++ s.toList

Tactic:
induction t generalizing s <;> simp [*, toStream]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem braiding_hom_fst {X Y : C} : (β_ X Y).hom ≫ fst _ _ = snd _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
⊢ (β_ X Y).hom ≫ fst Y X = snd X Y

Tactic:
simp [braiding_eq_braiding, fst, snd]

Result:
no goals
-- Mathlib/Order/Category/Lat.lean
lemma comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : Lat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals