harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ofNat {n : Nat} (x : Nat) :
  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n)

Proof state:
n x : Nat
⊢ (BitVec.ofNat n x).toInt = (↑x).bmod (2 ^ n)

Tactic:
simp [toInt_eq_toNat_bmod]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.closedBall_one_div (hs : IsCompact s) (hδ : 0 ≤ δ) :
    closedBall 1 δ / s = cthickening δ s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearDepOn_iff'ₛ : ¬LinearIndepOn R v s ↔
      ∃ f g : ι →₀ R, f ∈ Finsupp.supported R R s ∧ g ∈ Finsupp.supported R R s ∧
        Finsupp.linearCombination R v f = Finsupp.linearCombination R v g ∧ f ≠ g

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

Tactic:
simp [linearIndepOn_iffₛ, and_left_comm]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem Codisjoint.himp_inf_cancel_right (h : Codisjoint a b) : a ⇨ a ⊓ b = b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇨ a ⊓ b = b

Tactic:
rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
lemma subset_preimage_val_image_val_iff : D ⊆ A ↓∩ ↑E ↔ D ⊆ E

Proof state:
α : Type u_2
A : Set α
D E : Set ↑A
⊢ D ⊆ A ↓∩ Subtype.val '' E ↔ D ⊆ E

Tactic:
rw [preimage_image_eq _ Subtype.val_injective]

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem sum_apply' [Countable ι] (κ : ι → Kernel α β) (a : α) {s : Set β} (hs : MeasurableSet s) :
    Kernel.sum κ a s = ∑' n, κ n a s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum κ) a) s = ∑' (n : ι), ((κ n) a) s

Tactic:
rw [sum_apply κ a, Measure.sum_apply _ hs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_ψ₂ : (W.map f).ψ₂ = W.ψ₂.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).ψ₂ = Polynomial.map (mapRingHom f) W.ψ₂

Tactic:
simp only [ψ₂, Affine.map_polynomialY]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_add_mod (m n k : Nat) : (m % n + k) % n = (m + k) % n

Proof state:
m n k : Nat
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n

Tactic:
rwa [Nat.add_right_comm, mod_add_div] at this

Result:
no goals

Proof state:
m n k : Nat
⊢ (m % n + k) % n = (m + k) % n

Tactic:
have := (add_mul_mod_self_left (m % n + k) n (m / n)).symm

Result:
m n k : Nat
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n
-- Mathlib/Order/LiminfLimsup.lean
lemma limsSup_principal_eq_sSup (s : Set α) : limsSup (𝓟 s) = sSup s

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsSup = sSup s

Tactic:
simpa only [limsSup, eventually_principal] using sInf_upperBounds_eq_csSup s

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem Integrable.withDensityᵥ_trim_eq_integral {m m0 : MeasurableSpace α} {μ : Measure α}
    (hm : m ≤ m0) {f : α → ℝ} (hf : Integrable f μ) {i : Set α} (hi : MeasurableSet[m] i) :
    (μ.withDensityᵥ f).trim hm i = ∫ x in i, f x ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ↑((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ

Tactic:
rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_opow_mul {b v : Ordinal} (hb : 1 < b) (u : Ordinal) (hv : v ≠ 0) :
    log b (b ^ u * v) = u + log b v

Proof state:
b v : Ordinal.{u_1}
hb : 1 < b
u : Ordinal.{u_1}
hv : v ≠ 0
⊢ log b (b ^ u * v) = u + log b v

Tactic:
simpa using log_opow_mul_add hb hv (opow_pos u (bot_lt_of_lt hb))

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_ite_irrel (p : Prop) [Decidable p] (s : Finset α) (f g : α → β) :
    ∏ x ∈ s, (if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
p : Prop
inst✝ : Decidable p
s : Finset α
f g : α → β
⊢ (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

Tactic:
split_ifs with h <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ #v[s + n]

Proof state:
s n : Nat
⊢ range' s (n + 1) = range' s n ++ { toArray := #[s + n], size_toArray := ⋯ }

Tactic:
simp [range'_concat]

Result:
no goals
-- Mathlib/RingTheory/AlgebraTower.lean
theorem Basis.smulTower'_apply (ij) : b.smulTower' c ij = b ij.2 • c ij.1

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower' c) ij = b ij.2 • c ij.1

Tactic:
rw [smulTower', reindex_apply, smulTower_apply]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_drop (a : Vector α n) (m) :
    (a.drop m).toList = a.toList.drop m

Proof state:
α : Type u_1
n : Nat
a : Vector α n
m : Nat
⊢ (a.drop m).toList = List.drop m a.toList

Tactic:
simp [List.take_of_length_le]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_nhdsWithin_nhdsWithin [PseudoMetricSpace β] {t : Set β} {f : α → β} {a b} :
    Tendsto f (𝓝[s] a) (𝓝[t] b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε :=
  (nhdsWithin_basis_ball.tendsto_iff nhdsWithin_basis_ball).trans <| by
    simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
t : Set β
f : α → β
a : α
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, 0 < ia ∧ ∀ x ∈ ball a ia ∩ s, f x ∈ ball b ib ∩ t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

Tactic:
simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem toProd_surjective : Surjective (toProd : M ∗ N →* M × N) := fun x =>
  ⟨inl x.1 * inr x.2, by rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]⟩

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ toProd (inl x.1 * inr x.2) = x

Tactic:
rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem isStarNormal {x : R} (hx : IsSelfAdjoint x) : IsStarNormal x :=
  ⟨by simp only [Commute, SemiconjBy, hx.star_eq]⟩

Proof state:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x

Tactic:
simp only [Commute, SemiconjBy, hx.star_eq]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem principal_coprod_principal (s : Set α) (t : Set β) :
    (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
  preimage_compl, preimage_compl, compl_compl, compl_compl]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_div_right_comm : a * b / c = a / c * b

Proof state:
a b c : ℝ≥0∞
⊢ a * b / c = a / c * b

Tactic:
simp only [div_eq_mul_inv, mul_right_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasStrictDerivAt.sub (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) :
    HasStrictDerivAt (fun x => f x - g x) (f' - g') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
⊢ HasStrictDerivAt (fun x => f x - g x) (f' - g') x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem size_attach {L : Array α} : L.attach.size = L.size

Proof state:
α : Type u_1
L : Array α
⊢ L.attach.size = L.size

Tactic:
cases L

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.size = { toList := toList✝ }.size

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.size = { toList := toList✝ }.size

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0 :=
  have : -0 < -a

Proof state:
a : Int
h : 0 < -a
⊢ -0 < -a

Tactic:
rwa [Int.neg_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma zero_lt_posForm_apply_root (i : ι)
    (hi : P.root i ∈ span S (range P.root) := subset_span (mem_range_self i)) :
    0 < B.posForm ⟨P.root i, hi⟩ ⟨P.root i, hi⟩

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ι
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root i, hi⟩

Tactic:
simpa only [zero_lt_posForm_iff] using B.exists_pos_eq i

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ιMapObj_D₂ (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) :
    K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' =
      K.d₂ c₁₂ i.1 i.2 i₁₂'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
i : I₁ × I₂
h : c₁.π c₂ c₁₂ i = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i.1 i.2 i₁₂'

Tactic:
simp [D₂]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_unitBall {c : 𝕜} (hc : c ≠ 0) : c • ball (0 : E) (1 : ℝ) = ball (0 : E) ‖c‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ c • ball 0 1 = ball 0 ‖c‖

Tactic:
rw [_root_.smul_ball hc, smul_zero, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_mul_uIcc (a b c : α) : (a * ·) '' [[b, c]] = [[a * b, a * c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
⊢ (fun x => a * x) '' [[b, c]] = [[a * b, a * c]]

Tactic:
simpa only [mul_comm] using image_mul_const_uIcc a b c

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Cast.lean
theorem cast_ascFactorial : (a.ascFactorial b : S) = (ascPochhammer S b).eval (a : S)

Proof state:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.ascFactorial b) = Polynomial.eval (↑a) (ascPochhammer S b)

Tactic:
rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_ne_zero_iff {θ : ℂ} : tan θ ≠ 0 ↔ ∀ k : ℤ, (k * π / 2 : ℂ) ≠ θ

Proof state:
θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑π / 2 ≠ θ

Tactic:
rw [← not_exists, not_iff_not, tan_eq_zero_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem beq_self_left  : ∀(a b : Bool), (a == (a == b)) = b

Proof state:
⊢ ∀ (a b : Bool), (a == (a == b)) = b

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <:+ l₂
t : List α✝
h : t ++ l₁ = l₂
⊢ t ++ l₁ ++ [] = l₂

Tactic:
rw [h, append_nil]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).flatten⟩ := go ss [] where
  go : ∀ (ss : List String) cs, ss.foldl (· ++ ·) (mk cs) = ⟨cs ++ (ss.map data).flatten⟩
    | [], _ => by simp
    | ⟨s⟩::ss, _ => (go ss _).trans (by simp)

Proof state:
ss✝ : List String
s : List Char
ss : List String
x✝ : List Char
⊢ { data := x✝ ++ s ++ (List.map data ss).flatten } = { data := x✝ ++ (List.map data ({ data := s } :: ss)).flatten }

Tactic:
simp

Result:
no goals

Proof state:
ss : List String
x✝ : List Char
⊢ List.foldl (fun x1 x2 => x1 ++ x2) { data := x✝ } [] = { data := x✝ ++ (List.map data []).flatten }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem NormOneClass.nontrivial : Nontrivial G :=
  nontrivial_of_ne 0 1 <| ne_of_apply_ne norm <| by simp

Proof state:
G : Type u_1
inst✝² : SeminormedAddCommGroup G
inst✝¹ : One G
inst✝ : NormOneClass G
⊢ ‖0‖ ≠ ‖1‖

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem self_comp_symm_toHom (f : M ≃[L] N) :
    f.toHom.comp f.symm.toHom = Hom.id L N

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toHom.comp f.symm.toHom = Hom.id L N

Tactic:
rw [← comp_toHom, self_comp_symm, refl_toHom]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_bot : ramificationIdx f ⊥ P = 0 :=
  dif_neg <| not_exists.mpr fun n hn => n.lt_succ_self.not_le (hn _ (by simp))

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Ideal S
n : ℕ
hn : ∀ a ∈ {n | map f ⊥ ≤ P ^ n}, a ≤ n
⊢ n.succ ∈ {n | map f ⊥ ≤ P ^ n}

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ioc_map_sectR : (Ioc a b).map (.sectR c _) = Ioc (c, a) (c, b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioc a b) = Ioc (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem isUnit_iff_abs_eq {x : ℤ} : IsUnit x ↔ abs x = 1

Proof state:
x : ℤ
⊢ IsUnit x ↔ |x| = 1

Tactic:
rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsUpperSet.sdiff_of_isLowerSet (hs : IsUpperSet s) (ht : IsLowerSet t) : IsUpperSet (s \ t) :=
  hs.sdiff <| by aesop

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
ht : IsLowerSet t
⊢ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem has_add (assignment : Assignment) (b : Bool) :
    hasAssignment b (addAssignment b assignment)

Proof state:
assignment : Assignment
b : Bool
⊢ hasAssignment b (addAssignment b assignment) = true

Tactic:
by_cases b <;> cases assignment <;> simp_all [hasAssignment, hasPosAssignment, addAssignment,
  addPosAssignment, addNegAssignment, hasNegAssignment]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesOnBall.sub (hf : HasFPowerSeriesOnBall f pf x r)
    (hg : HasFPowerSeriesOnBall g pg x r) : HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
hg : HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc]
lemma w' {X Y Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z)
    [Full F] [Faithful F] : hf.fst' (F.map g) ≫ f = hf.snd (F.map g) ≫ g :=
  F.map_injective <| by simp [(hf.w (F.map g))]

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
hf : F.relativelyRepresentable (F.map f)
g : Y ⟶ Z
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.fst' (F.map g) ≫ f) = F.map (hf.snd (F.map g) ≫ g)

Tactic:
simp [(hf.w (F.map g))]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_top_of_localization₀_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized₀ P.primeCompl (f P) = ⊤) :
    N = ⊤ :=
  Submodule.eq_of_localization₀_maximal Mₚ f fun P hP ↦ by simpa using h P

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N = ⊤
P : Ideal R
hP : P.IsMaximal
⊢ localized₀ P.primeCompl (f P) N = localized₀ P.primeCompl (f P) ⊤

Tactic:
simpa using h P

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem bot_coprod_bot : (⊥ : Filter α).coprod (⊥ : Filter β) = ⊥

Proof state:
α : Type u_1
β : Type u_2
⊢ ⊥.coprod ⊥ = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem trace_adjoinSimpleGen {x : L} (hx : IsIntegral K x) :
    trace K K⟮x⟯ (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff

Tactic:
simpa [minpoly_gen K x] using PowerBasis.trace_gen_eq_nextCoeff_minpoly <| adjoin.powerBasis hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) : W.addX P Q =
      ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
        + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q
        - W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2
        - Q x * P z ^ 2 * addZ P Q ^ 2) / (P z * Q z) ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q =
    ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q -
            W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 -
          P x * Q z ^ 2 * addZ P Q ^ 2 -
        Q x * P z ^ 2 * addZ P Q ^ 2) /
      (P z * Q z) ^ 2

Tactic:
rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_bne : ∀(b : Bool), (false != b) =  b

Proof state:
⊢ ∀ (b : Bool), (false != b) = b

Tactic:
decide

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_refl_restr (s : Set β) :
    e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source])

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
simp [trans_source]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem restr_source' (s : Set X) (hs : IsOpen s) : (e.restr s).source = e.source ∩ s

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
⊢ (e.restr s).source = e.source ∩ s

Tactic:
rw [e.restr_source, hs.interior_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_two_pi : sin (2 * π) = 0

Proof state:
⊢ sin (2 * ↑π) = 0

Tactic:
simp [two_mul, sin_add]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_cons (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) :
    (cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha) :=
  eq_of_veq <| Multiset.map_cons f a s.val

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ f a ∉ map f s

Tactic:
simpa using ha

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem restrict_image_emb {f : α → β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f)
    (s : Set α) : MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set α
⊢ MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))

Tactic:
simpa only [Set.preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    m.keys.contains k = m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ m.keys.contains k = m.contains k

Tactic:
simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_quot_out [Monoid M] (a : M) : Quot.out (Associates.mk a) ~ᵤ a

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
⊢ Quot.out (Associates.mk a) ~ᵤ a

Tactic:
rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem beq_true  (b : Bool) : (b == true)  =  b

Proof state:
b : Bool
⊢ (b == true) = b

Tactic:
cases b <;> rfl

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

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a : α
⊢ ¬a ∈ m → m.getKey? a = none

Tactic:
simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false

Result:
no goals