harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem dite_none_right_eq_some {p : Prop} [Decidable p] {b : p → Option α} :
    (if h : p then b h else none) = some a ↔ ∃ h, b h = some a

Proof state:
α : Type u_1
a : α
p : Prop
inst✝ : Decidable p
b : p → Option α
⊢ (if h : p then b h else none) = some a ↔ ∃ h, b h = some a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem keys_union {s₁ s₂ : Finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=
  induction_on₂ s₁ s₂ fun s₁ s₂ => Finset.ext <| by simp [keys]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α), a ∈ (⟦s₁⟧ ∪ ⟦s₂⟧).keys ↔ a ∈ ⟦s₁⟧.keys ∪ ⟦s₂⟧.keys

Tactic:
simp [keys]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem fintype_card_le_finrank [Module.Finite R M]
    {ι : Type*} [Fintype ι] {b : ι → M} (h : LinearIndependent R b) :
    Fintype.card ι ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
ι : Type u_1
inst✝ : Fintype ι
b : ι → M
h : LinearIndependent R b
⊢ Fintype.card ι ≤ finrank R M

Tactic:
simpa using h.cardinalMk_le_finrank

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma balance_zero : balance (0 : ι → G) = 0

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
⊢ balance 0 = 0

Tactic:
simp [balance]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem le_of_comm {B : C} {X Y : Subobject B} (f : (X : C) ⟶ (Y : C)) (w : f ≫ Y.arrow = X.arrow) :
    X ≤ Y

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ Y.arrow = X.arrow
⊢ X ≤ Y

Tactic:
convert mk_le_mk_of_comm _ w <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_sub (x y : R) (p q : R[X][Y]) :
    (p - q).evalEval x y = p.evalEval x y - q.evalEval x y

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p - q) = evalEval x y p - evalEval x y q

Tactic:
simp only [evalEval, eval_sub]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closure_range_iff {e : β → α} {a : α} :
    a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k : β, dist a (e k) < ε

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
e : β → α
a : α
⊢ a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε

Tactic:
simp only [mem_closure_iff, exists_range_iff]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem comp_tail {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) :
    g ∘ tail q = tail (g ∘ q)

Proof state:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
⊢ g ∘ tail q = tail (g ∘ q)

Tactic:
ext j

Result:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ tail q) j = tail (g ∘ q) j

Proof state:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ tail q) j = tail (g ∘ q) j

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem toGL_one : toGL (1 : unitaryGroup n α) = 1 := Units.ext <| by
  simp only [coe_toGL, toLin'_one]
  rfl

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
⊢ ↑(toGL 1) = ↑1

Tactic:
simp only [coe_toGL, toLin'_one]

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
⊢ LinearMap.id = ↑1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
⊢ LinearMap.id = ↑1

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.isoProd_hom {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoProd X Y).hom = prod.lift biprod.fst biprod.snd

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).hom = prod.lift fst snd

Tactic:
ext <;> simp [biprod.isoProd]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_sub_pi_div_two (x : ℝ) : sin (x - π / 2) = -cos x

Proof state:
x : ℝ
⊢ sin (x - π / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_coe : Disjoint (a : α) b ↔ Disjoint a b

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint ↑a ↑b ↔ Disjoint a b

Tactic:
rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {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) :
    (m.insertMany l).1.getKey? k' = some k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
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
⊢ (m.insertMany l).val.getKey? k' = some k

Tactic:
simp_to_model [insertMany] using List.getKey?_insertList_of_mem

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mk_neg {f : CauSeq ℚ abs} : mk (-f) = -mk f

Proof state:
f : CauSeq ℚ abs
⊢ mk (-f) = -mk f

Tactic:
simp [mk, ← ofCauchy_neg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval₂_at_zero : p.eval₂ f 0 = f (coeff p 0)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ eval₂ f 0 p = f (p.coeff 0)

Tactic:
simp +contextual only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero,
  mul_one, sum, Classical.not_not, mem_support_iff, sum_ite_eq', ite_eq_left_iff,
  RingHom.map_zero, imp_true_iff, eq_self_iff_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
    o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : (a : α) → a ∈ o → Option β
⊢ o.pbind f =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ => f x h

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Ring/NonZeroDivisors.lean
@[simp]
lemma mul_cancel_left_mem_nonZeroDivisors (hr : r ∈ R⁰) : r * x = r * y ↔ x = y

Proof state:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
⊢ r * x = r * y ↔ x = y

Tactic:
simp_rw [mul_comm r, mul_cancel_right_mem_nonZeroDivisors hr]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(μ + ν).toSignedMeasure i = ↑(μ.toSignedMeasure + ν.toSignedMeasure) i

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(μ + ν).toSignedMeasure i = ↑(μ.toSignedMeasure + ν.toSignedMeasure) i

Tactic:
rw [toSignedMeasure_apply_measurable hi, add_apply,
  ENNReal.toReal_add (ne_of_lt (measure_lt_top _ _)) (ne_of_lt (measure_lt_top _ _)),
  VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
  toSignedMeasure_apply_measurable hi]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_hasStrictFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
⊢ HasStrictFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasStrictFDerivAt f f' x

Tactic:
refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x H⟩

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x
⊢ HasStrictFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x
⊢ HasStrictFDerivAt f f' x

Tactic:
convert iso.symm.hasStrictFDerivAt.comp x H using 1 <;>
  ext z <;> apply (iso.symm_apply_apply _).symm

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
lemma _root_.rootsOfUnityEquivOfPrimitiveRoots_symm_apply
    {S F} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ} [NeZero n]
    {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots n R).Nonempty) (η) :
    f ((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η : Rˣ) = (η : Sˣ)

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
n : ℕ
inst✝ : NeZero n
f : F
hf : Function.Injective ⇑f
hζ : (primitiveRoots n R).Nonempty
η : ↥(rootsOfUnity n S)
⊢ f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η

Tactic:
obtain ⟨ε, rfl⟩ := (rootsOfUnityEquivOfPrimitiveRoots hf hζ).surjective η

Result:
case intro
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
n : ℕ
inst✝ : NeZero n
f : F
hf : Function.Injective ⇑f
hζ : (primitiveRoots n R).Nonempty
ε : ↥(rootsOfUnity n R)
⊢ f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm ((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)) =
    ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)

Proof state:
case intro
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
n : ℕ
inst✝ : NeZero n
f : F
hf : Function.Injective ⇑f
hζ : (primitiveRoots n R).Nonempty
ε : ↥(rootsOfUnity n R)
⊢ f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm ((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)) =
    ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)

Tactic:
rw [MulEquiv.symm_apply_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe]

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem le_zero_iff {G : PGame} [G.Impartial] : G ≤ 0 ↔ 0 ≤ G

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G ≤ 0 ↔ 0 ≤ G

Tactic:
rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_bUnion [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} :
    (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using s.wellFoundedOn_sup

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem eq_pow_of_mul_eq_pow_odd_right {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k)
    (h : a * b = c ^ k) : ∃ d, b = d ^ k :=
  eq_pow_of_mul_eq_pow_odd_left (c := c) hab.symm hk (by rwa [mul_comm] at h)

Proof state:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ b * a = c ^ k

Tactic:
rwa [mul_comm] at h

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem mem_closure_iff_nhds_basis {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
  (mem_closure_iff_nhds_basis' h).trans <| by
    simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]

Proof state:
X : Type u
ι : Sort w
x : X
t : Set X
inst✝ : TopologicalSpace X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ (i : ι), p i → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i

Tactic:
simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.int_mul [Ring α] (h : Periodic f c) (n : ℤ) : Periodic f (n * c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : Ring α
h : Periodic f c
n : ℤ
⊢ Periodic f (↑n * c)

Tactic:
simpa only [zsmul_eq_mul] using h.zsmul n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    a ∈ m.insert k v ↔ k == a ∨ a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

Tactic:
simp [mem_iff_contains, contains_insert h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
    {v' : β k'} (h : k' == k) : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = true
⊢ replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l

Tactic:
simp [replaceEntry, h]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem injective_left [Mul α] [i : @Std.Commutative α (· * ·)] [PartialOrder α] {a : α}
    (ha : MulLECancellable a) :
    Injective (· * a) := fun b c h => ha.Injective <| by dsimp; rwa [i.comm a, i.comm a]

Proof state:
α : Type u_1
inst✝¹ : Mul α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ (fun x => a * x) b = (fun x => a * x) c

Tactic:
dsimp

Result:
α : Type u_1
inst✝¹ : Mul α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c

Proof state:
α : Type u_1
inst✝¹ : Mul α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c

Tactic:
rwa [i.comm a, i.comm a]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_range_le (f : M →ₗ[R] M₁) : Module.rank R (LinearMap.range f) ≤ Module.rank R M

Proof state:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
⊢ Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M

Tactic:
simpa using lift_rank_range_le f

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_inf (x y : α) : x \ y ⊓ (x ⊓ y) = ⊥

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊓ (x ⊓ y) = ⊥

Tactic:
rw [inf_comm, inf_inf_sdiff]

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
theorem eq_re_of_ofReal_le {r : ℝ} {z : ℂ} (hz : (r : ℂ) ≤ z) : z = z.re

Proof state:
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re

Tactic:
rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_apply_eq_zero' {μ : ι → Measure α} {s : Set α} (hs : MeasurableSet s) :
    sum μ s = 0 ↔ ∀ i, μ i s = 0

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp] lemma toReal_nonneg {f : C_c(α, ℝ≥0)} : 0 ≤ f.toReal := fun _ ↦ by simp

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
x✝ : α
⊢ 0 x✝ ≤ f.toReal x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists'_cons (a : α) (l : List α) :
    sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)

Proof state:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'

Tactic:
simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem linear_eq_linearIsometry : f.linear = f.linearIsometry.toLinearMap

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x✝ : V
⊢ f.linear x✝ = f.linearIsometry.toLinearMap x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
⊢ f.linear = f.linearIsometry.toLinearMap

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x✝ : V
⊢ f.linear x✝ = f.linearIsometry.toLinearMap x✝
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem isOrtho_iSup_right {ι : Sort*} {U : Submodule 𝕜 E} {V : ι → Submodule 𝕜 E} :
    U ⟂ iSup V ↔ ∀ i, U ⟂ V i :=
  isOrtho_comm.trans <| isOrtho_iSup_left.trans <| by simp_rw [isOrtho_comm]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Sort u_4
U : Submodule 𝕜 E
V : ι → Submodule 𝕜 E
⊢ (∀ (i : ι), V i ⟂ U) ↔ ∀ (i : ι), U ⟂ V i

Tactic:
simp_rw [isOrtho_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWithAll_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : Option α' → Option β → γ) :
    zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
α' : Type u_1
γ : Type u_3
l₁ : List α
l₂ : List β
f : α → α'
g : Option α' → Option β → γ
⊢ zipWithAll g (map f l₁) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_apply_zero (p₀ p₁ : P1) : lineMap p₀ p₁ (0 : k) = p₀

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ (lineMap p₀ p₁) 0 = p₀

Tactic:
simp [lineMap_apply]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem tendsto_lift_nhdsWithin_mk {f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y}
    {s : Set (SeparationQuotient X)} {l : Filter α} :
    Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l

Proof state:
X : Type u_1
α : Type u_4
inst✝ : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
l : Filter α
⊢ Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l

Tactic:
simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem vsub_midpoint (p₁ p₂ p : P) :
    p -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p -ᵥ p₁) + (⅟ 2 : R) • (p -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
  neg_vsub_eq_vsub_rev]

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)
    {h'} :
    (m.insertMany l).get k h' =
      m.get k (mem_of_mem_insertMany_list h h' contains_eq_false)

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
h' : k ∈ m.insertMany l
⊢ (m.insertMany l).get k h' = m.get k ⋯

Tactic:
simp_to_raw using Raw₀.get_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem lt_compl_self [Nontrivial α] : a < aᶜ ↔ a = ⊥

Proof state:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a < aᶜ ↔ a = ⊥

Tactic:
rw [lt_iff_le_and_ne]

Result:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.singleton : (Heap.singleton a).WF le 0 := ⟨by decide, rfl, ⟨⟩⟩

Proof state:
α✝ : Type u_1
a : α✝
le : α✝ → α✝ → Bool
⊢ 0 ≤ 0

Tactic:
decide

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
@[reassoc (attr := simp)]
lemma ι_sigmaIsoGlued_hom (i) :
    Sigma.ι f i ≫ (sigmaIsoGlued f).hom = (disjointGlueData f).ι i

Proof state:
ι : Type u
f : ι → Scheme
i : ι
⊢ Sigma.ι f i ≫ (sigmaIsoGlued f).hom = (disjointGlueData f).ι i

Tactic:
rw [← ι_sigmaIsoGlued_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.map_toArray (f : α → β) (l : List α) :
    l.toArray.map f = (l.map f).toArray

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ (map f l.toArray).toList = (List.map f l).toArray.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l.toArray = (List.map f l).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ (map f l.toArray).toList = (List.map f l).toArray.toList
-- Mathlib/Topology/Instances/Rat.lean
theorem uniformContinuous_neg : UniformContinuous (@Neg.neg ℚ _) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩

Proof state:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ dist (-x✝¹) (-x✝) < ε

Tactic:
simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h

Result:
no goals