harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_comm (x y : BitVec w) :
    x &&& y = y &&& x

Proof state:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& y).getLsbD i = (y &&& x).getLsbD i

Tactic:
simp [Bool.and_comm]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x &&& y = y &&& x

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& y).getLsbD i = (y &&& x).getLsbD i
-- Mathlib/Algebra/Ring/Identities.lean
theorem pow_four_add_four_mul_pow_four' :
    a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem fin_comap_jointlySurjective
    (hC : IsClosed C)
    (f : LocallyConstant C ℤ) : ∃ (s : Finset I)
    (g : LocallyConstant (π C (· ∈ s)) ℤ), f = g.comap ⟨(ProjRestrict C (· ∈ s)),
      continuous_projRestrict _ _⟩

Proof state:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
J : (Finset I)ᵒᵖ
g : LocallyConstant ↑((spanFunctor ⋯).obj J).toTop ℤ
h : f = LocallyConstant.comap (TopCat.Hom.hom ((spanCone ⋯).π.app J)) g
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g

Tactic:
exact ⟨(Opposite.unop J), g, h⟩

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g

Tactic:
obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
  (spanCone hC.isCompact) ℤ
  (spanCone_isLimit hC.isCompact) f

Result:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
J : (Finset I)ᵒᵖ
g : LocallyConstant ↑((spanFunctor ⋯).obj J).toTop ℤ
h : f = LocallyConstant.comap (TopCat.Hom.hom ((spanCone ⋯).π.app J)) g
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} {h} :
    get m a h = get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h✝ : m.val.WF
a : α
h : m.contains a = true
⊢ get m a h = get! m a

Tactic:
simp_to_model using List.getValue_eq_getValue!

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean
theorem prod_finset_product (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :
    ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.fst, x.snd)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.fst, x.snd)

Tactic:
apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_inf_principal_univ_pi_neBot :
    NeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ i, NeBot (f i ⊓ 𝓟 (s i))

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (pi f ⊓ 𝓟 (univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
    (mkArray n v)[i]? = if i < n then some v else none

Proof state:
α : Type u_1
n : Nat
v : α
i : Nat
⊢ (mkArray n v)[i]? = if i < n then some v else none

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem one_dotProduct_one : (1 : n → α) ⬝ᵥ 1 = Fintype.card n

Proof state:
n : Type u_3
α : Type v
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
⊢ 1 ⬝ᵥ 1 = ↑(Fintype.card n)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_smul_right_self (x : V) {r : ℝ} : (2 : ℤ) • o.oangle x (r • x) = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ 2 • o.oangle x (r • x) = 0

Tactic:
rcases lt_or_le r 0 with (h | h) <;> simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.subset_closure (h : M.IsBasis I X) : X ⊆ M.closure I

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ X ⊆ M.closure I

Tactic:
rw [← closure_subset_closure_iff_subset_closure, h.closure_eq_closure]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_right_iff {a b : Cardinal} : a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0

Proof state:
a b : Cardinal.{u_1}
⊢ a + b = b ↔ ℵ₀ ⊔ a ≤ b ∨ a = 0

Tactic:
rw [add_comm, add_eq_left_iff]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_zero_right (i : ℤ) : gcd i 0 = natAbs i

Proof state:
i : ℤ
⊢ i.gcd 0 = i.natAbs

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem hasDerivAt_circleMap (c : ℂ) (R : ℝ) (θ : ℝ) :
    HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ

Proof state:
c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ

Tactic:
simpa only [mul_assoc, one_mul, ofRealCLM_apply, circleMap, ofReal_one, zero_add]
  using (((ofRealCLM.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem prod_top (s : Subsemigroup M) : s.prod (⊤ : Subsemigroup N) = s.comap (MulHom.fst M N) :=
  ext fun x => by simp [mem_prod, MulHom.coe_fst]

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MulHom.fst M N) s

Tactic:
simp [mem_prod, MulHom.coe_fst]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma eLpNorm_density_le (hκν : fst κ ≤ ν) (a : α) (s : Set β) :
    eLpNorm (fun x ↦ density κ ν a x s) 1 (ν a) ≤ ν a univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
⊢ eLpNorm (fun x => κ.density ν a x s) 1 (ν a) ≤ (ν a) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
t : γ
⊢ ‖κ.density ν a t s‖ ≤ 1

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
t : γ
⊢ ‖κ.density ν a t s‖ ≤ 1

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg (density_nonneg hκν a t s),
  density_le_one hκν a t s]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem norm_inner_le_norm (x y : F) : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ :=
  nonneg_le_nonneg_of_sq_le_sq (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) <|
    calc
      ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ = ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ = ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖

Tactic:
rw [norm_inner_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
simp only [inner_self_eq_norm_mul_norm]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem infEdist_inv (x : E) (s : Set E) : infEdist x⁻¹ s = infEdist x s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEdist x⁻¹ s = infEdist x s⁻¹

Tactic:
rw [← infEdist_inv_inv, inv_inv]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem toAffineMap_injective : Injective (toAffineMap : (P →ᵃⁱ[𝕜] P₂) → P →ᵃ[𝕜] P₂)

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₂
⊢ Injective toAffineMap

Tactic:
rintro ⟨f, _⟩ ⟨g, _⟩ rfl

Result:
case mk.mk
𝕜 : 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₂
norm_map✝¹ : ∀ (x : V), ‖f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖{ toAffineMap := f, norm_map := norm_map✝¹ }.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }

Proof state:
case mk.mk
𝕜 : 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₂
norm_map✝¹ : ∀ (x : V), ‖f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖{ toAffineMap := f, norm_map := norm_map✝¹ }.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem mul_num (q₁ q₂ : ℚ) :
    (q₁ * q₂).num = q₁.num * q₂.num / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den)

Proof state:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
rw [mul_def, normalize_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_toArray (l : List α) (f : (i : Nat) → α → (h : i < l.length) → β) :
    l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem one_ne_of (a : α) : 1 ≠ of a :=
  letI := Classical.decEq α; ne_of_apply_ne toWord <| by simp

Proof state:
α : Type u_1
a : α
this : DecidableEq α := Classical.decEq α
⊢ toWord 1 ≠ (of a).toWord

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLastD_eq_getLast? (a l) : @getLastD α l a = (getLast? l).getD a

Proof state:
α : Type u_1
a : α
l : List α
⊢ l.getLastD a = l.getLast?.getD a

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem Subset.dedup_append_right {xs ys : List α} (h : xs ⊆ ys) :
    dedup (xs ++ ys) = dedup ys

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
rw [List.dedup_append, Subset.union_eq_right (h.trans <| subset_dedup _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0

Proof state:
case h
α : Type u_1
l : Array α
⊢ countP (fun x => false) l = Function.const (Array α) 0 l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ (countP fun x => false) = Function.const (Array α) 0

Tactic:
funext l

Result:
case h
α : Type u_1
l : Array α
⊢ countP (fun x => false) l = Function.const (Array α) 0 l
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setIntegral_eq_tsum (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α}
    (hf : IntegrableOn f t μ) : ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ :=
  calc
    ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ.restrict t :=
      h.integral_eq_tsum_of_ac restrict_le_self.absolutelyContinuous f hf
    _ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ

Tactic:
simp only [h.restrict_restrict, measure_smul, inter_comm]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem TFAE_mem_nhdsLT {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[<] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b)`
        s ∈ 𝓝[Ico a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b)`
        s ∈ 𝓝[Ioo a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b)`
        ∃ l ∈ Ico a b, Ioo l b ⊆ s,-- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`
        ∃ l ∈ Iio b, Ioo l b ⊆ s]

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[<] b, s ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE

Tactic:
simpa only [exists_prop, OrderDual.exists, dual_Ioi, dual_Ioc, dual_Ioo] using
  TFAE_mem_nhdsGT h.dual (ofDual ⁻¹' s)

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_filter {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
    Disjoint (s.filter p) (s.filter q) ↔ ∀ x ∈ s, p x → ¬q x

Proof state:
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
constructor <;> simp +contextual [disjoint_left]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem fst_eq_or_snd_eq_of_wcovBy : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y → x.1 = y.1 ∨ x.2 = y.2

Tactic:
refine fun h => of_not_not fun hab => ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
hab : ¬(x.1 = y.1 ∨ x.2 = y.2)
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
hab : ¬(x.1 = y.1 ∨ x.2 = y.2)
⊢ False

Tactic:
push_neg at hab

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
hab : x.1 ≠ y.1 ∧ x.2 ≠ y.2
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
hab : x.1 ≠ y.1 ∧ x.2 ≠ y.2
⊢ False

Tactic:
exact
  h.2 (mk_lt_mk.2 <| Or.inl ⟨hab.1.lt_of_le h.1.1, le_rfl⟩)
    (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hab.2.lt_of_le h.1.2⟩)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem type_fintype (r : α → α → Prop) [IsWellOrder α r] [Fintype α] :
    type r = Fintype.card α

Proof state:
α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)

Tactic:
rw [← card_eq_nat, card_type, mk_fintype]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem inv : t⁻¹ = t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ t⁻¹ = t

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ (w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ (w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem comp_add (X Y Z : C) (f : X ⟶ Y) (g h : Y ⟶ Z) : f ≫ (g + h) = f ≫ g + f ≫ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_def]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma four_nsmul_coPolarization_compl_polarization_apply_root (i : ι) :
    (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    (P.RootForm (P.root i) (P.root i) * P.CorootForm (P.coroot i) (P.coroot i)) • P.root i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i

Tactic:
rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
  ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem toMeasurable_ae_eq (h : NullMeasurableSet s μ) : toMeasurable μ s =ᵐ[μ] s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ toMeasurable μ s =ᶠ[ae μ] s

Tactic:
rw [toMeasurable_def, dif_pos]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᶠ[ae μ] s

case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᶠ[ae μ] s

case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
exact (exists_measurable_superset_ae_eq h).choose_spec.2.2

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
/-- For any `w`-small type `X`, there exists a regular cardinal `κ : Cardinal.{w}`
such that `HasCardinalLT X κ`. -/
lemma exists_regular_cardinal (X : Type u) [Small.{w} X] :
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ HasCardinalLT X κ :=
  ⟨Order.succ (max (Cardinal.mk (Shrink.{w} X)) .aleph0),
    Cardinal.isRegular_succ (le_max_right _ _), by
      simp [hasCardinalLT_iff_of_equiv (equivShrink.{w} X),
        hasCardinalLT_iff_cardinal_mk_lt]⟩

Proof state:
X : Type u
inst✝ : Small.{w, u} X
⊢ HasCardinalLT X (Order.succ (Cardinal.mk (Shrink.{w, u} X) ⊔ Cardinal.aleph0))

Tactic:
simp [hasCardinalLT_iff_of_equiv (equivShrink.{w} X),
  hasCardinalLT_iff_cardinal_mk_lt]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
@[to_additive]
lemma not_isCyclic : ¬IsCyclic G :=
  fun h ↦ by simpa using h.exponent_eq_card

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
h : IsCyclic G
⊢ False

Tactic:
simpa using h.exponent_eq_card

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem exists_memBaseSet_le_iUnion_eq (l : IntegrationParams) (π₀ : Prepartition I)
    (hc₁ : π₀.distortion ≤ c) (hc₂ : π₀.compl.distortion ≤ c) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : π.IsHenstock
hr : π.IsSubordinate r
hd : π.distortion = π₀.distortion
hU : π.iUnion = π₀.iUnion
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion

Tactic:
refine ⟨π, ⟨hr, fun _ => hH, fun _ => hd.trans_le hc₁, fun _ => ⟨π₀.compl, ?_, hc₂⟩⟩, ⟨hle, hU⟩⟩

Result:
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : π.IsHenstock
hr : π.IsSubordinate r
hd : π.distortion = π₀.distortion
hU : π.iUnion = π₀.iUnion
x✝ : l.bDistortion = true
⊢ π₀.compl.iUnion = ↑I \ π.iUnion

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : π.IsHenstock
hr : π.IsSubordinate r
hd : π.distortion = π₀.distortion
hU : π.iUnion = π₀.iUnion
x✝ : l.bDistortion = true
⊢ π₀.compl.iUnion = ↑I \ π.iUnion

Tactic:
exact Prepartition.compl_congr hU ▸ π.toPrepartition.iUnion_compl

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion

Tactic:
rcases π₀.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq r with ⟨π, hle, hH, hr, hd, hU⟩

Result:
case intro.intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π₀ : Prepartition I
hc₁ : π₀.distortion ≤ c
hc₂ : π₀.compl.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : TaggedPrepartition I
hle : π.toPrepartition ≤ π₀
hH : π.IsHenstock
hr : π.IsSubordinate r
hd : π.distortion = π₀.distortion
hU : π.iUnion = π₀.iUnion
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion