harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Fold.lean
theorem fold_insert_idem [DecidableEq α] [hi : Std.IdempotentOp op] :
    (insert a s).fold op b f = f a * s.fold op b f

Proof state:
case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
apply fold_insert h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Proof state:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
rw [← insert_erase h]

Result:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))

Proof state:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a (insert a (s.erase a))) = op (f a) (fold op b f (insert a (s.erase a)))

Tactic:
simp [← ha.assoc, hi.idempotent]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Set.OrdConnected.convex_of_chain [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E]
    [OrderedSMul 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y-[𝕜]x] ⊆ s

Tactic:
exact (segment_subset_Icc hyx).trans (hs.out hy hx)

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [x-[𝕜]y] ⊆ s

Tactic:
rw [segment_symm]

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y-[𝕜]x] ⊆ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
⊢ [x-[𝕜]y] ⊆ s

Tactic:
obtain hxy | hyx := h.total hx hy

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x-[𝕜]y] ⊆ s

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [x-[𝕜]y] ⊆ s

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x-[𝕜]y] ⊆ s

Tactic:
exact (segment_subset_Icc hxy).trans (hs.out hx hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
⊢ Convex 𝕜 s

Tactic:
refine convex_iff_segment_subset.mpr fun x hx y hy => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 => x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
⊢ [x-[𝕜]y] ⊆ s
-- Mathlib/Data/Matrix/Bilinear.lean
theorem commute_mulLeftLinearMap_mulRightLinearMap (a : Matrix l m A) (b : Matrix n o A) :
    mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b =
      mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
⊢ mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b = mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a

Tactic:
ext c : 1

Result:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
c : Matrix m n A
⊢ (mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b) c = (mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a) c

Proof state:
case h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
c : Matrix m n A
⊢ (mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b) c = (mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a) c

Tactic:
exact (Matrix.mul_assoc a c b).symm

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem update_elim_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ} {i : β}
    {x : γ} : update (Sum.elim f g) (inr i) x = Sum.elim f (update g i x) :=
  update_eq_iff.2 ⟨by simp, by simp +contextual⟩

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update g i x) x_1

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update g i x) (inr i)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem tendsto_card_le_div {X : Set (ι → ℝ)} (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
    {F : (ι → ℝ) → ℝ} (h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r →  F (r • x) = r ^ card ι * (F x))
    (h₂ : IsBounded {x ∈ X | F x ≤ 1}) (h₃ : MeasurableSet {x ∈ X | F x ≤ 1})
    (h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0) [Nonempty ι] :
    Tendsto (fun c : ℝ ↦
      Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set (ι → ℝ)) / (c : ℝ))
        atTop (𝓝 ((volume {x ∈ X | F x ≤ 1}).toReal / covolume L))

Proof state:
case h.e'_5.h.e'_3
ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ (volume {x | x ∈ X ∧ F x ≤ 1}).toReal / covolume L volume =
    (volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})).toReal

Tactic:
rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
  ENNReal.toReal_ofReal (covolume_pos L volume).le]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma domDomRestrict_aux_right {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
    [DecidableEq {a // ¬ P a}]
    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // ¬ P a})
    (c : M₁ i) : (fun j ↦ if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c

Proof state:
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // ¬P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : M₁ ↑i
⊢ (fun j => if h : P j then x ⟨j, h⟩ else update z i c ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c

Tactic:
simpa only [dite_not] using domDomRestrict_aux _ z (fun j ↦ x ⟨j.1, not_not.mp j.2⟩) i c

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem summable_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) :
    (Summable fun i => f (i + k)) ↔ Summable f

Proof state:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun i => f (i + k)) ↔ Summable f

Tactic:
rw [← summable_coe, ← summable_coe]

Result:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)

Proof state:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)

Tactic:
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem toNonUnitalSubalgebra_injective :
    Function.Injective
      (toNonUnitalSubalgebra : NonUnitalStarSubalgebra R A → NonUnitalSubalgebra R A) :=
  fun S T h =>
  ext fun x => by rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem coe_prod (v : PrimeMultiset) : (v.prod : ℕ) = (v : Multiset ℕ).prod

Proof state:
v : PrimeMultiset
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
let h : (v.prod : ℕ) = ((v.map Coe.coe).map Coe.coe).prod :=
  PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset

Result:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map Coe.coe (Multiset.map Coe.coe v)).prod :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom v.toPNatMultiset
⊢ ↑v.prod = v.toNatMultiset.prod

Proof state:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
have : (Coe.coe : ℕ+ → ℕ) ∘ (Coe.coe : Nat.Primes → ℕ+) = Coe.coe := funext fun p => rfl

Result:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑v.prod = v.toNatMultiset.prod

Proof state:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
rw [this] at h

Result:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map Coe.coe v).prod
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑v.prod = v.toNatMultiset.prod

Proof state:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map Coe.coe (Multiset.map Coe.coe v)).prod :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom v.toPNatMultiset
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
rw [Multiset.map_map] at h

Result:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod
⊢ ↑v.prod = v.toNatMultiset.prod

Proof state:
v : PrimeMultiset
h : ↑v.prod = (Multiset.map Coe.coe v).prod
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
exact h

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem hasMFDerivAt_iff_hasFDerivAt {f'} :
    HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x

Tactic:
rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) :
    (a : ℚ) / b < c / d ↔ a * d < c * b

Proof state:
case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Tactic:
apply not_congr

Result:
case h₂.h
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑c / ↑d ≤ ↑a / ↑b ↔ c * b ≤ a * d

Proof state:
case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

Tactic:
simp [div_def', Rat.divInt_le_divInt b_pos d_pos]

Result:
no goals

Proof state:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b

Tactic:
simp only [lt_iff_le_not_le]

Result:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d

Proof state:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d

Tactic:
apply and_congr

Result:
case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Proof state:
case h₂.h
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑c / ↑d ≤ ↑a / ↑b ↔ c * b ≤ a * d

Tactic:
simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
lemma dist_anti_right_pi : AntitoneOn (dist x) (Iic x)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
x : ι → ℝ
⊢ AntitoneOn (dist x) (Iic x)

Tactic:
simpa only [dist_comm] using dist_anti_left_pi (y := x)

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem filterMap_some : s.filterMap some (by simp) = s :=
  ext fun _ => by simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

Proof state:
α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ filterMap some s ⋯ ↔ x✝ ∈ s

Tactic:
simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
s' s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (a a' b : α), b ∈ some a → b ∈ some a' → a = a'

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.div_mul_cancel'` for a stronger version. -/
protected lemma div_mul_cancel (ha₀ : a ≠ 0) (ha : a ≠ ∞) : b / a * a = b :=
  ENNReal.div_mul_cancel' (by simp [ha₀]) (by simp [ha])

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → b = 0

Tactic:
simp [ha₀]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → b = 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_mul_mk'_eq_one (x y : M) : mk' S (x : R) y * mk' S (y : R) x = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : ↥M
⊢ mk' S (↑x) y * mk' S (↑y) x = 1

Tactic:
rw [← mk'_mul, mul_comm]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1

Tactic:
exact mk'_self _ _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
theorem toENatAux_le_nat {x : Cardinal} {n : ℕ} : toENatAux x ≤ n ↔ x ≤ n

Proof state:
case inl
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
lift x to ℕ using hx

Result:
case inl.intro
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n

Proof state:
x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
cases lt_or_le x ℵ₀ with
| inl hx => lift x to ℕ using hx; simp
| inr hx => simp [toENatAux_eq_top hx, (nat_lt_aleph0 n).trans_le hx]

Result:
no goals

Proof state:
case inr
x : Cardinal.{u_1}
n : ℕ
hx : ℵ₀ ≤ x
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
simp [toENatAux_eq_top hx, (nat_lt_aleph0 n).trans_le hx]

Result:
no goals

Proof state:
case inl.intro
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
    (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r)))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ ((x >>> r).getLsbD i || (x <<< (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - (w - r)))

Tactic:
suffices (x >>> r).getLsbD i = false by
  simp only [this, getLsbD_shiftLeft, Bool.false_or]
  by_cases hiw : i < w
  <;> simp [hiw, hi]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ (x >>> r).getLsbD i = false

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
this : (x >>> r).getLsbD i = false
⊢ (decide (i < w) && !decide (i < w - r) && x.getLsbD (i - (w - r))) = (decide (i < w) && x.getLsbD (i - (w - r)))

Tactic:
by_cases hiw : i < w
<;> simp [hiw, hi]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ x.getLsbD (r + i) = false

Tactic:
apply getLsbD_ge

Result:
case ge
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ w ≤ r + i

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ (x >>> r).getLsbD i = false

Tactic:
simp only [getLsbD_ushiftRight]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ x.getLsbD (r + i) = false

Proof state:
case ge
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ w ≤ r + i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r)))

Tactic:
rw [rotateRightAux, getLsbD_or]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ ((x >>> r).getLsbD i || (x <<< (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - (w - r)))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
this : (x >>> r).getLsbD i = false
⊢ ((x >>> r).getLsbD i || (x <<< (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - (w - r)))

Tactic:
simp only [this, getLsbD_shiftLeft, Bool.false_or]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
this : (x >>> r).getLsbD i = false
⊢ (decide (i < w) && !decide (i < w - r) && x.getLsbD (i - (w - r))) = (decide (i < w) && x.getLsbD (i - (w - r)))
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem foldl_eq_foldl_finRange (f : α → Fin n → α) (x) :
    foldl n f x = (List.finRange n).foldl f x

Proof state:
case zero
α : Type u_1
f : α → Fin 0 → α
x : α
⊢ foldl 0 f x = List.foldl f x (List.finRange 0)

Tactic:
rw [foldl_zero, List.finRange_zero, List.foldl_nil]

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : α → Fin n → α) (x : α), foldl n f x = List.foldl f x (List.finRange n)
f : α → Fin (n + 1) → α
x : α
⊢ foldl (n + 1) f x = List.foldl f x (List.finRange (n + 1))

Tactic:
rw [foldl_succ, ih, List.finRange_succ, List.foldl_cons, List.foldl_map]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : α → Fin n → α
x : α
⊢ foldl n f x = List.foldl f x (List.finRange n)

Tactic:
induction n generalizing x with
| zero => rw [foldl_zero, List.finRange_zero, List.foldl_nil]
| succ n ih => rw [foldl_succ, ih, List.finRange_succ, List.foldl_cons, List.foldl_map]

Result:
no goals
-- Mathlib/Topology/Sheaves/Sheaf.lean
theorem isSheaf_unit (F : Presheaf (CategoryTheory.Discrete Unit) X) : F.IsSheaf :=
  fun x U S _ x _ => ⟨eqToHom (Subsingleton.elim _ _), by aesop_cat, fun _ => by aesop_cat⟩

Proof state:
X : TopCat
F : Presheaf (Discrete Unit) X
x✝² : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝¹ : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝²)) S.arrows
x✝ : x.Compatible
⊢ (fun t => x.IsAmalgamation t) (eqToHom ⋯)

Tactic:
aesop_cat

Result:
no goals

Proof state:
X : TopCat
F : Presheaf (Discrete Unit) X
x✝³ : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝² : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝³)) S.arrows
x✝¹ : x.Compatible
x✝ : (F ⋙ coyoneda.obj (op x✝³)).obj (op U)
⊢ (fun t => x.IsAmalgamation t) x✝ → x✝ = eqToHom ⋯

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Homotopy/Path.lean
theorem ContinuousMap.homotopic_const_iff [Nonempty Y] :
    (ContinuousMap.const Y x₀).Homotopic (ContinuousMap.const Y x₁) ↔ Joined x₀ x₁

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
  fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩ <;> simp

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
inhabit Y

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp] lemma enorm_mul (a b : α) : ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
⊢ ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ (a - c) ⊔ (b - d) + c ⊔ d ∧ b ≤ (a - c) ⊔ (b - d) + c ⊔ d

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ (a - c) ⊔ (b - d) + c ⊔ d

case right
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ b ≤ (a - c) ⊔ (b - d) + c ⊔ d

Proof state:
case right
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ b ≤ (a - c) ⊔ (b - d) + c ⊔ d

Tactic:
calc
b = b - d + d := (sub_add_cancel b d).symm
_ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)

Result:
no goals

Proof state:
case left
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ (a - c) ⊔ (b - d) + c ⊔ d

Tactic:
calc
a = a - c + c := (sub_add_cancel a c).symm
_ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ⊔ b - c ⊔ d ≤ (a - c) ⊔ (b - d)

Tactic:
simp only [sub_le_iff_le_add, max_le_iff]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ (a - c) ⊔ (b - d) + c ⊔ d ∧ b ≤ (a - c) ⊔ (b - d) + c ⊔ d