harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_le_one_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : v x ≤ 1 ↔ 1 ≤ v x⁻¹

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ v x ≤ 1 ↔ 1 ≤ v x⁻¹

Tactic:
simp [one_le_inv₀ (v.pos_iff.2 h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ l₁.erase a <+ l₂.erase a

Tactic:
simp only [erase_eq_eraseP']

Result:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ eraseP (fun x => x == a) l₁ <+ eraseP (fun x => x == a) l₂

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ eraseP (fun x => x == a) l₁ <+ eraseP (fun x => x == a) l₂

Tactic:
exact h.eraseP

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem vanishingIdeal_union (t t' : Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal

Tactic:
exact (gc_ideal 𝒜).u_inf

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

Tactic:
ext1

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_eq_contract_of_basis' [Fintype ι] [DecidableEq ι] (b : Basis ι R M) :
    LinearMap.trace R M = contractLeft R M ∘ₗ (dualTensorHomEquivOfBasis b).symm.toLinearMap

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R M
⊢ trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm

Tactic:
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
-- Mathlib/Algebra/RingQuot.lean
theorem Rel.sub_right {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) :
    Rel r (a - b) (a - c)

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a - b) (a - c)

Tactic:
simp only [sub_eq_add_neg, h.neg.add_right]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem UnderMorphism.ext {X : T} {U V : Under X} {f g : U ⟶ V} (h : f.right = g.right) :
    f = g

Proof state:
case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : { left := left✝¹, right := b, w := w✝¹ }.right = { left := left✝, right := e, w := w✝ }.right
⊢ left✝¹ = left✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
h : f.right = g.right
⊢ f = g

Tactic:
let ⟨_,b,_⟩ := f

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : { left := left✝, right := b, w := w✝ }.right = g.right
⊢ { left := left✝, right := b, w := w✝ } = g

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : { left := left✝¹, right := b, w := w✝¹ }.right = { left := left✝, right := e, w := w✝ }.right
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }

Tactic:
congr

Result:
case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : { left := left✝¹, right := b, w := w✝¹ }.right = { left := left✝, right := e, w := w✝ }.right
⊢ left✝¹ = left✝

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : { left := left✝, right := b, w := w✝ }.right = g.right
⊢ { left := left✝, right := b, w := w✝ } = g

Tactic:
let ⟨_,e,_⟩ := g

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : { left := left✝¹, right := b, w := w✝¹ }.right = { left := left✝, right := e, w := w✝ }.right
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma colimitHomIsoLimitYoneda_inv_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
    (colimitHomIsoLimitYoneda F A).inv ≫ (coyoneda.map (colimit.ι F i).op).app A =
      limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (colimitHomIsoLimitYoneda F A).inv ≫ (coyoneda.map (colimit.ι F i).op).app A = limit.π (F.op ⋙ yoneda.obj A) (op i)

Tactic:
rw [← colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc,
  Iso.inv_hom_id, Category.id_comp]

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem eq_iff [CommRing K] [IsReduced K] (p : ℕ) [Fact p.Prime] [CharP K p] (x y : ℕ × K) :
    mk K p x = mk K p y ↔ (frobenius K p)^[y.1] x.2 = (frobenius K p)^[x.1] y.2 :=
  (mk_eq_iff K p x y).trans
    ⟨fun ⟨z, H⟩ => (frobenius_inj K p).iterate z <| by simpa only [add_comm, iterate_add] using H,
      fun H => ⟨0, H⟩⟩

Proof state:
K : Type u
inst✝³ : CommRing K
inst✝² : IsReduced K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
x✝ : ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
z : ℕ
H : (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
⊢ (⇑(frobenius K p))^[z] ((⇑(frobenius K p))^[y.1] x.2) = (⇑(frobenius K p))^[z] ((⇑(frobenius K p))^[x.1] y.2)

Tactic:
simpa only [add_comm, iterate_add] using H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat

Proof state:
n : Nat
x y : BitVec n
⊢ (x / y).toNat = x.toNat / y.toNat

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma «forall» {p : ℂ → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩

Proof state:
p : ℂ → Prop
⊢ (∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }

Tactic:
aesop

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem ι_isOpenEmbedding [HasLimits C] (i : D.J) : IsOpenEmbedding (𝖣.ι i).base

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding
    (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)))

Tactic:
exact (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).isOpenEmbedding.comp
    (D.toTopGlueData.ι_isOpenEmbedding i)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (D.ι i).base)

Tactic:
rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _, TopCat.coe_comp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding
    (⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)))
-- Mathlib/Control/Fold.lean
theorem foldrm_map (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) :
    foldrm f a (g <$> l) = foldrm (f ∘ g) a l

Proof state:
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l

Tactic:
simp only [foldrm, foldMap_map, Function.comp_def, flip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b

Proof state:
α : Type u_1
p : α → Bool
a : α
b : Bool
⊢ p ⊨ (a, b) ↔ p a = b

Tactic:
simp only [Entails.eval]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Iio : Neg.neg '' Iio a = Ioi (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a : α
⊢ Neg.neg '' Iio a = Ioi (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_neg_mul (d : ℤ) : selfZPow x B (-d) * selfZPow x B d = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZPow x B (-d) * selfZPow x B d = 1

Tactic:
rw [mul_comm, selfZPow_mul_neg x B d]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioc_left (f : ∀ i, α i) (i : ι) (a : α i) :
    update f i '' Ioc a (f i) = Ioc (update f i a) f

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioc a (f i) = Ioc (update f i a) f

Tactic:
simpa using image_update_Ioc f i a (f i)

Result:
no goals
-- Mathlib/Order/Circular.lean
theorem compl_cIcc {a b : α} : (cIcc a b)ᶜ = cIoo b a

Proof state:
α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIcc a b)ᶜ = cIoo b a

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a

Proof state:
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a

Tactic:
rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem iSup_le_succ (u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = (⨆ k ≤ n, u k) ⊔ u (n + 1)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α] (l : Array α) (a : α) (i : Nat) (w : l.idxOf a = i) (h : i < l.size) :
    l.erase a = l.eraseIdx i

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
i : Nat
l : List α
h : i < { toList := l }.size
w : List.idxOf a l = i
⊢ { toList := l }.erase a = { toList := l }.eraseIdx i h

Tactic:
simp [List.erase_eq_eraseIdx_of_idxOf, *]

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
i : Nat
l : List α
w : idxOf a { toList := l } = i
h : i < { toList := l }.size
⊢ { toList := l }.erase a = { toList := l }.eraseIdx i h

Tactic:
simp at w

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
i : Nat
l : List α
h : i < { toList := l }.size
w : List.idxOf a l = i
⊢ { toList := l }.erase a = { toList := l }.eraseIdx i h

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : Array α
a : α
i : Nat
w : idxOf a l = i
h : i < l.size
⊢ l.erase a = l.eraseIdx i h

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
i : Nat
l : List α
w : idxOf a { toList := l } = i
h : i < { toList := l }.size
⊢ { toList := l }.erase a = { toList := l }.eraseIdx i h
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_comm (x y : V) : angle x y = angle y x

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = angle y x

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner x y / (‖x‖ * ‖y‖)) = arccos (inner y x / (‖y‖ * ‖x‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner x y / (‖x‖ * ‖y‖)) = arccos (inner y x / (‖y‖ * ‖x‖))

Tactic:
rw [real_inner_comm, mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem mem_compression :
    a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).get? k = m.get? k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).get? k = m.get? k

Tactic:
simp_to_raw using Raw₀.get?_insertMany_list_of_contains_eq_false

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

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

Tactic:
by_cases b <;> cases assignment <;> simp_all [hasAssignment, removeAssignment,
  removePosAssignment, hasPosAssignment, removeNegAssignment, hasNegAssignment]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem subset_insert_iff {a : α} {s t : Finset α} : s ⊆ insert a t ↔ erase s a ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t

Tactic:
exact forall_congr' fun x => forall_swap

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ s.erase a ⊆ t

Tactic:
simp only [subset_iff, or_iff_not_imp_left, mem_erase, mem_insert, and_imp]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g • a) = (stabilizer G a).map (MulAut.conj g).toMonoidHom

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
  inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
ext h

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_le {I J K : FractionalIdeal S P} : I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J K : FractionalIdeal S P
⊢ ⟨↑I * ↑J, ⋯⟩ ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Tactic:
exact Submodule.mul_le

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J K : FractionalIdeal S P
⊢ I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J K : FractionalIdeal S P
⊢ ⟨↑I * ↑J, ⋯⟩ ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
-- Mathlib/Data/Finsupp/Weight.lean
theorem degree_zero : degree (0 : σ →₀ R) = 0

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : AddCommMonoid R
⊢ degree 0 = 0

Tactic:
simp [degree]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
    (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i)

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i)

Tactic:
rw [rotateLeftAux, getMsbD_or]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ ((x <<< r).getMsbD i || (x >>> (w - r)).getMsbD i) = x.getMsbD (r + i)

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ ((x <<< r).getMsbD i || (x >>> (w - r)).getMsbD i) = x.getMsbD (r + i)

Tactic:
simp [show i < w - r by omega, Nat.add_comm]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ i < w - r

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_cons_inl (ha) :
    (cons (inl a) u ha).toRight = u.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toRight = u.toRight

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem isOpen_iff : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Tactic:
simp [isOpen_iff_nhds, mem_nhds_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem disjoint_def {p₁ p₂ : Submonoid M} :
    Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Proof state:
M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem drop_append_stream : ∀ (l : List α) (s : Stream' α), drop l.length (l ++ₛ s) = s
  | [], s => by rfl
  | List.cons a l, s => by
    rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]

Proof state:
α : Type u
s : Stream' α
⊢ drop [].length ([] ++ₛ s) = s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
s : Stream' α
⊢ drop (a :: l).length (a :: l ++ₛ s) = s

Tactic:
rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem measure_eq_zero_or_one_of_indepSet_self [IsFiniteMeasure μ] {t : Set Ω}
    (h_indep : IndepSet t t μ) : μ t = 0 ∨ μ t = 1

Proof state:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t μ
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
  using Kernel.measure_eq_zero_or_one_of_indepSet_self h_indep

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_eq_of_equiv_equiv (i : R ≃+* R') (j : S ≃+* S')
    (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    Module.rank R S = Module.rank R' S'

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)
⊢ Module.rank R S = Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateLeft_eq_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
    x.rotateLeft r = x.rotateLeftAux r

Proof state:
w : Nat
x : BitVec w
r : Nat
hr : r < w
⊢ x.rotateLeft r = x.rotateLeftAux r

Tactic:
simp only [rotateLeft, Nat.mod_eq_of_lt hr]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem measurableSet_mulSupport {m : MeasurableSpace α} [One β] [TopologicalSpace β]
    [MetrizableSpace β] (hf : StronglyMeasurable f) : MeasurableSet (mulSupport f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
⊢ MeasurableSet (mulSupport f)

Tactic:
borelize β

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (mulSupport f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (mulSupport f)

Tactic:
exact measurableSet_mulSupport hf.measurable

Result:
no goals