harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem someExistsOneDivLT_spec (hi : ¬s ≤[i] 0) :
    someExistsOneDivLT s i ⊆ i ∧
      MeasurableSet (someExistsOneDivLT s i) ∧
        (1 / (findExistsOneDivLT s i + 1) : ℝ) < s (someExistsOneDivLT s i)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i ∧
    MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) <
        ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

Tactic:
rw [someExistsOneDivLT, dif_pos hi]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ Classical.choose ⋯ ⊆ i ∧
    MeasurableSet (Classical.choose ⋯) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (Classical.choose ⋯)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ Classical.choose ⋯ ⊆ i ∧
    MeasurableSet (Classical.choose ⋯) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (Classical.choose ⋯)

Tactic:
exact Classical.choose_spec (findExistsOneDivLT_spec hi)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp m) :
    m.isEmpty = (toListModel m.buckets).isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : WFImp m
⊢ m.isEmpty = (toListModel m.buckets).isEmpty

Tactic:
rw [Raw.isEmpty, Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, size_eq_length h,
  Nat.beq_eq_true_eq]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem Disjoint.symmDiff_left (ha : Disjoint a c) (hb : Disjoint b c) :
    Disjoint (a ∆ b) c

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c

Tactic:
exact (ha.sup_left hb).disjoint_sdiff_left

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem sepDegree_mul_sepDegree_of_isAlgebraic (K : Type v) [Field K] [Algebra F K]
    [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] :
    sepDegree F E * sepDegree E K = sepDegree F K

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
⊢ sepDegree F E * sepDegree E K = sepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E K

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem smul_ball_one : x • ball (1 : E) δ = ball x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • ball 1 δ = ball x δ

Tactic:
rw [smul_ball, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.rel_get_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : Fin l.length}
    (hab : a ≤ b) : r (l.get a) (l.get b)

Proof state:
case inl
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a : Fin l.length
hab : a ≤ a
⊢ r (l.get a) (l.get a)

case inr
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ r (l.get a) (l.get b)

Tactic:
exacts [refl _, h.rel_get_of_lt hlt]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin l.length
hab : a ≤ b
⊢ r (l.get a) (l.get b)

Tactic:
obtain rfl | hlt := Fin.eq_or_lt_of_le hab

Result:
case inl
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a : Fin l.length
hab : a ≤ a
⊢ r (l.get a) (l.get a)

case inr
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ r (l.get a) (l.get b)
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp)]
lemma finEquivPowers_symm_apply (x : G) (hx) (n : ℕ) {hn : ∃ m : ℕ, x ^ m = x ^ n} :
    (finEquivPowers x hx).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
hx : IsOfFinOrder x
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ (finEquivPowers x hx).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, ⋯⟩

Tactic:
rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/-- The elements of height zero are the minimal elements. -/
@[simp] lemma height_eq_zero {x : α} : height x = 0 ↔ IsMin x

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = 0 ↔ IsMin x

Tactic:
simpa [isMin_iff_forall_not_lt] using height_le_coe_iff (x := x) (n := 0)

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.univ : MeasurableSet (univ : Set α) :=
  .of_compl <| by simp

Proof state:
α : Type u_1
m : MeasurableSpace α
⊢ MeasurableSet univᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tsum_measure_le_measure_univ {s : ι → Set α} (hs : ∀ i, NullMeasurableSet (s i) μ)
    (H : Pairwise (AEDisjoint μ on s)) : ∑' i, μ (s i) ≤ μ (univ : Set α)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ ⨆ s_1, ∑ a ∈ s_1, μ (s a) ≤ μ univ

Tactic:
exact iSup_le fun s =>
  sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ ∑' (i : ι), μ (s i) ≤ μ univ

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ ⨆ s_1, ∑ a ∈ s_1, μ (s a) ≤ μ univ
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_rpow (x : ℝ) : (1 : ℝ) ^ x = 1

Proof state:
x : ℝ
⊢ 1 ^ x = 1

Tactic:
simp [rpow_def]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem dist_center_eq_dist_center_of_mem_sphere {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) : dist p₁ s.center = dist p₂ s.center

Proof state:
P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ s.center = dist p₂ s.center

Tactic:
rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem _root_.Algebra.TensorProduct.isField_of_isAlgebraic
    (K : Type*) [Field K] [Algebra F K] [IsDomain (E ⊗[F] K)]
    (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K) : IsField (E ⊗[F] K) :=
  have ⟨L, _, _, fa, fb, hfa, hfb, H⟩ :=
    Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective F E K
      (RingHom.injective _) (RingHom.injective _)
  let f : E ⊗[F] K ≃ₐ[F] ↥(fa.fieldRange ⊔ fb.fieldRange) :=
    Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa) (AlgEquiv.ofInjective fb hfb)
    |>.trans (Subalgebra.LinearDisjoint.mulMap H)
    |>.trans (Subalgebra.equivOfEq _ _
      (sup_toSubalgebra_of_isAlgebraic fa.fieldRange fb.fieldRange <| by
        rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
          (AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg).symm)
  f.toMulEquiv.isField _ (Field.toIsField _)

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsDomain (E ⊗[F] K)
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K
L : Type (max v u_1)
w✝¹ : Field L
w✝ : Algebra F L
fa : E →ₐ[F] L
fb : K →ₐ[F] L
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
H : fa.range.LinearDisjoint fb.range
⊢ Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange

Tactic:
rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
  (AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_le_re_and_im_le (a b : ℝ) :
    frontier { z | a ≤ re z ∧ im z ≤ b } = { z | a ≤ re z ∧ im z = b ∨ re z = a ∧ im z ≤ b }

Proof state:
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}

Tactic:
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using
  frontier_reProdIm (Ici a) (Iic b)

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_rat (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ℚ) :
    IsAlgebraic R (n : A)

Proof state:
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_ratCast (algebraMap R A)]

Result:
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)

Proof state:
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)

Tactic:
exact isAlgebraic_algebraMap (Rat.cast n)

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem map_apply {R F : Type*} [CommRing R] [IsDomain R]
    [FunLike F K[X] R[X]] [MonoidHomClass F K[X] R[X]] (φ : F)
    (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (f : RatFunc K) :
    map φ hφ f = algebraMap _ _ (φ f.num) / algebraMap _ _ (φ f.denom)

Proof state:
K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ (map φ hφ) f = (algebraMap R[X] (RatFunc R)) (φ f.num) / (algebraMap R[X] (RatFunc R)) (φ f.denom)

Tactic:
rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]

Result:
case hq
K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ f.denom ≠ 0

Proof state:
case hq
K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ f.denom ≠ 0

Tactic:
exact denom_ne_zero _

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_mul {b c : ℤ√d} (hb : IsPell b) (hc : IsPell c) : IsPell (b * c) :=
  isPell_norm.2 (by simp [mul_comm, mul_left_comm c, mul_assoc,
    star_mul, isPell_norm.1 hb, isPell_norm.1 hc])

Proof state:
d : ℤ
b c : ℤ√d
hb : IsPell b
hc : IsPell c
⊢ b * c * star (b * c) = 1

Tactic:
simp [mul_comm, mul_left_comm c, mul_assoc,
star_mul, isPell_norm.1 hb, isPell_norm.1 hc]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_mul : ((φ * ψ : R[X]) : PowerSeries R) = φ * ψ :=
  PowerSeries.ext fun n => by simp only [coeff_coe, PowerSeries.coeff_mul, coeff_mul]

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n : ℕ
⊢ (PowerSeries.coeff R n) ↑(φ * ψ) = (PowerSeries.coeff R n) (↑φ * ↑ψ)

Tactic:
simp only [coeff_coe, PowerSeries.coeff_mul, coeff_mul]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma map_finite_biSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [SupBotHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
    f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨆ a ∈ s, g a) = ⨆ a ∈ s, f (g a)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
have := map_finset_sup f hs.toFinset g

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.sup g) = hs.toFinset.sup (⇑f ∘ g)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.sup g) = hs.toFinset.sup (⇑f ∘ g)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
simp only [Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply] at this

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨆ a ∈ s, g a) = ⨆ a ∈ s, f (g a)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem left_vsub_pointReflection (x y : P) : x -ᵥ pointReflection x y = y -ᵥ x :=
  neg_injective <| by simp

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(x -ᵥ (pointReflection x) y) = -(y -ᵥ x)

Tactic:
simp

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

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

Tactic:
rw [← negAddY_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/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertList_of_mem [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Sigma.fst) :
    getKey? k' (insertList l toInsert) = some k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Sigma.fst toInsert
⊢ getKey? k' (insertList l toInsert) = some k

Tactic:
rcases List.mem_map.1 mem with ⟨⟨k, v⟩, pair_mem, rfl⟩

Result:
case intro.mk.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k' : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
k : α
v : β k
pair_mem : ⟨k, v⟩ ∈ toInsert
k_beq : (⟨k, v⟩.fst == k') = true
mem : ⟨k, v⟩.fst ∈ List.map Sigma.fst toInsert
⊢ getKey? k' (insertList l toInsert) = some ⟨k, v⟩.fst

Proof state:
case intro.mk.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k' : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
k : α
v : β k
pair_mem : ⟨k, v⟩ ∈ toInsert
k_beq : (⟨k, v⟩.fst == k') = true
mem : ⟨k, v⟩.fst ∈ List.map Sigma.fst toInsert
⊢ getKey? k' (insertList l toInsert) = some ⟨k, v⟩.fst

Tactic:
rw [getKey?_eq_getEntry?, getEntry?_insertList distinct_l distinct_toInsert,
  getEntry?_of_mem (DistinctKeys.def.2 distinct_toInsert) k_beq pair_mem, Option.some_or,
  Option.map_some']

Result:
no goals
-- Mathlib/FieldTheory/Galois/GaloisClosure.lean
nonrec lemma mem_fixingSubgroup_iff (α : K ≃ₐ[k] K) (L : FiniteGaloisIntermediateField k K) :
    α ∈ L.fixingSubgroup ↔ α.restrictNormalHom L = 1

Proof state:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
α : K ≃ₐ[k] K
L : FiniteGaloisIntermediateField k K
⊢ α ∈ L.fixingSubgroup ↔ (AlgEquiv.restrictNormalHom ↥L.toIntermediateField) α = 1

Tactic:
simp [IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
  AlgEquiv.restrictNormalHom_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k') :
    contains m k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey! (insertManyIfNewUnit m l).1 k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw₀ α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey! k' = k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
/-- If `f` and `g` are odd, then `f ∘ g` is odd. -/
lemma Odd.comp_odd [Neg β] [Neg γ] {f : β → γ} (hf : f.Odd) {g : α → β} (hg : g.Odd) :
    (f ∘ g).Odd

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
⊢ Function.Odd (f ∘ g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = -(f ∘ g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
a : α
⊢ (f ∘ g) (-a) = -(f ∘ g) a

Tactic:
simp only [comp_apply, hg a, hf _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h)

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
t : c → α
e : ¬c → α
h : c = False
⊢ dite c t e = e ⋯

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma negPart_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) {a : A} : (r • a)⁻ = r • a⁻

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
⊢ -r ≤ 0

Tactic:
simpa

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
⊢ (r • a)⁻ = r • a⁻

Tactic:
conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem ne_zero_of_natDegree_gt {n : ℕ} (h : n < natDegree p) : p ≠ 0 := fun H => by
  simp [H, Nat.not_lt_zero] at h

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natDegree
H : p = 0
⊢ False

Tactic:
simp [H, Nat.not_lt_zero] at h

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem le_add_tsub (hb : AddLECancellable b) : a ≤ a + b - b

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ b + a - b

Tactic:
exact hb.le_add_tsub_swap

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ a + b - b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ b + a - b
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Ioo (a b : ℕ) : (↑) '' Ioo a b = Ioo (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Ioo (by simp [ordConnected_Ici]) a b

Proof state:
a b : ℕ
⊢ (range ⇑castOrderEmbedding).OrdConnected

Tactic:
simp [ordConnected_Ici]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharTwoJEqZeroNF_of_char_two : W.Δ = W.a₃ ^ 4

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ W.Δ = W.a₃ ^ 4

Tactic:
rw [Δ_of_isCharTwoJEqZeroNF, b₆_of_char_two]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -(64 * W.a₄ ^ 3 + 27 * (W.a₃ ^ 2) ^ 2) = W.a₃ ^ 4

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -(64 * W.a₄ ^ 3 + 27 * (W.a₃ ^ 2) ^ 2) = W.a₃ ^ 4

Tactic:
linear_combination (-32 * W.a₄ ^ 3 - 14 * W.a₃ ^ 4) * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_left_comm {m : α → δ → ε} {n : β → γ → δ} {m' : α → γ → δ'} {n' : β → δ' → ε}
    (h_left_comm : ∀ a b c, m a (n b c) = n' b (m' a c)) :
    map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ (fun a b => m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun a b => m' b a) h f)

Tactic:
exact map₂_assoc fun _ _ _ => h_left_comm _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Tactic:
rw [map₂_swap m', map₂_swap m]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ (fun a b => m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun a b => m' b a) h f)
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem smul_eq_C_mul (a : R) : a • p = C a * p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
⊢ a • p = C a * p

Tactic:
simp [ext_iff]

Result:
no goals