harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Divisors.lean
theorem divisor_le {m : ℕ} : n ∈ divisors m → n ≤ m

Proof state:
case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n m : ℕ
⊢ n ∣ m + 1 → n ≤ m + 1

Tactic:
exact Nat.le_of_dvd (Nat.succ_pos m)

Result:
no goals

Proof state:
n m : ℕ
⊢ n ∈ m.divisors → n ≤ m

Tactic:
rcases m with - | m

Result:
case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Proof state:
case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]

Result:
case succ
n m : ℕ
⊢ n ∣ m + 1 → n ≤ m + 1
-- Mathlib/NumberTheory/Ostrowski.lean
/-- The standard absolute value on `ℚ` is not equivalent to any `p`-adic absolute value. -/
lemma not_real_equiv_padic (p : ℕ) [Fact p.Prime] : ¬ real ≈ (padic p)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬real ≈ padic p

Tactic:
rintro ⟨c, hc₀, hc⟩

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : (fun x => real x ^ c) = ⇑(padic p)
⊢ False

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : (fun x => real x ^ c) 2 = (padic p) 2
⊢ False

Tactic:
simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : 2 ^ c = (padic p) 2
⊢ False

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : 2 ^ c = (padic p) 2
⊢ False

Tactic:
exact ((padic_le_one p 2).trans_lt <| one_lt_rpow one_lt_two hc₀).ne' hc

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
/-- If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball
`Metric.closedBall x r` is contained in `u`. -/
lemma eventually_closedBall_subset {x : α} {u : Set α} (hu : u ∈ 𝓝 x) :
    ∀ᶠ r in 𝓝 (0 : ℝ), closedBall x r ⊆ u

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu

Result:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Proof state:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos

Result:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Iic ε ∈ 𝓝 0
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Proof state:
case intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Iic ε ∈ 𝓝 0
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε

Result:
no goals
-- Mathlib/Data/Set/Opposite.lean
theorem singleton_op (x : α) : ({x} : Set α).op = {op x}

Proof state:
case h.mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op

Tactic:
apply op_injective

Result:
no goals

Proof state:
case h.mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op → x✝ ∈ {op x}

Tactic:
apply unop_injective

Result:
no goals

Proof state:
α : Type u_1
x : α
⊢ {x}.op = {op x}

Tactic:
ext

Result:
case h
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op ↔ x✝ ∈ {op x}

Proof state:
case h
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op ↔ x✝ ∈ {op x}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op → x✝ ∈ {op x}

case h.mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem lebesgue_number_lemma_of_metric {s : Set α} {ι : Sort*} {c : ι → Set α} (hs : IsCompact s)
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ι : Sort u_3
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ i, c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i

Tactic:
simpa only [ball, UniformSpace.ball, preimage_setOf_eq, dist_comm]
  using uniformity_basis_dist.lebesgue_number_lemma hs hc₁ hc₂

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem isUnit_iff_bijective {f : CircleDeg1Lift} : IsUnit f ↔ Bijective f :=
  ⟨fun ⟨u, h⟩ => h ▸ (toOrderIso u).bijective, fun h =>
    Units.isUnit
      { val := f
        inv :=
          { toFun := (Equiv.ofBijective f h).symm
            monotone' := fun x y hxy =>
              (f.strictMono_iff_injective.2 h.1).le_iff_le.1
                (by simp only [Equiv.ofBijective_apply_symm_apply f h, hxy])
            map_add_one' := fun x =>
              h.1 <| by simp only [Equiv.ofBijective_apply_symm_apply f, f.map_add_one] }
        val_inv := ext <| Equiv.ofBijective_apply_symm_apply f h
        inv_val := ext <| Equiv.ofBijective_symm_apply_apply f h }⟩

Proof state:
f : CircleDeg1Lift
h : Bijective ⇑f
x : ℝ
⊢ f ({ toFun := ⇑(Equiv.ofBijective (⇑f) h).symm, monotone' := ⋯ }.toFun (x + 1)) =
    f ({ toFun := ⇑(Equiv.ofBijective (⇑f) h).symm, monotone' := ⋯ }.toFun x + 1)

Tactic:
simp only [Equiv.ofBijective_apply_symm_apply f, f.map_add_one]

Result:
no goals

Proof state:
f : CircleDeg1Lift
h : Bijective ⇑f
x y : ℝ
hxy : x ≤ y
⊢ f ((Equiv.ofBijective (⇑f) h).symm x) ≤ f ((Equiv.ofBijective (⇑f) h).symm y)

Tactic:
simp only [Equiv.ofBijective_apply_symm_apply f h, hxy]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_C (a : R) : ((C a : R[X]) : PowerSeries R) = PowerSeries.C R a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
this : ↑((monomial 0) a) = (PowerSeries.monomial R 0) a
⊢ ↑(C a) = (PowerSeries.C R) a

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ ↑(C a) = (PowerSeries.C R) a

Tactic:
have := coe_monomial 0 a

Result:
R : Type u_1
inst✝ : CommSemiring R
a : R
this : ↑((monomial 0) a) = (PowerSeries.monomial R 0) a
⊢ ↑(C a) = (PowerSeries.C R) a
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma radical_inf {I J : IdealSheafData X} :
    radical (I ⊓ J) = (radical I ⊓ radical J)

Proof state:
case ideal.h
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U

Tactic:
simp only [radical_ideal, ideal_inf, Pi.inf_apply, Ideal.radical_inf]

Result:
no goals

Proof state:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical

Tactic:
ext U : 2

Result:
case ideal.h
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_balance' {P l x r} : @All α P (balance' l x r) ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balance']

Result:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P
      (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔
    All P l ∧ P x ∧ All P r

Tactic:
split_ifs <;> simp [all_node', all_rotateL, all_rotateR]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem infEdist_le_infEdist_cthickening_add :
    infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r

Tactic:
obtain ⟨y, hy, hxy⟩ := h

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEdist x s < r

Tactic:
simp_rw [← lt_tsub_iff_right, infEdist_lt_iff, mem_cthickening_iff] at h

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ

Tactic:
refine le_of_forall_lt' fun r h => ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEdist x s < r

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r

Tactic:
exact infEdist_le_edist_add_infEdist.trans_lt
  ((ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy).trans_eq
    (tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_comm_div : a / b * c = a * (c / b)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a * (c / b)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
lemma isPreimmersion_eq_inf :
    @IsPreimmersion = (@SurjectiveOnStalks ⊓ topologically IsEmbedding : MorphismProperty _)

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsPreimmersion x✝ ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding) x✝

Tactic:
rw [isPreimmersion_iff]

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ∧ IsEmbedding ⇑(ConcreteCategory.hom x✝.base) ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ∧ IsEmbedding ⇑(ConcreteCategory.hom x✝.base) ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding) x✝

Tactic:
rfl

Result:
no goals

Proof state:
⊢ @IsPreimmersion =
    @SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsPreimmersion x✝ ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding) x✝
-- Mathlib/Data/PNat/Interval.lean
theorem card_Ico : #(Ico a b) = b - a

Proof state:
a b : ℕ+
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_single {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
    (h₁ : a ∉ s → f a = 1) : ∏ x ∈ s, f x = f a :=
  haveI := Classical.decEq α
  by_cases (prod_eq_single_of_mem a · h₀) fun this =>
    (prod_congr rfl fun b hb => h₀ b hb <| by rintro rfl; exact this hb).trans <|
      prod_const_one.trans (h₁ this).symm

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h₁ : a ∉ s → f a = 1
this✝ : DecidableEq α
this : a ∉ s
b : α
hb : b ∈ s
⊢ b ≠ a

Tactic:
rintro rfl

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
this✝ : DecidableEq α
b : α
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
this✝ : DecidableEq α
b : α
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Tactic:
exact this hb

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_zero_cochain_v (z : Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q) :
    (δ 0 1 z).v p q hpq = z.v p p (add_zero p) ≫ G.d p q - F.d p q ≫ z.v q q (add_zero q)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G 0
p q : ℤ
hpq : p + 1 = q
⊢ p = q - 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G 0
p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 z).v p q hpq = z.v p p ⋯ ≫ G.d p q - F.d p q ≫ z.v q q ⋯

Tactic:
simp only [δ_v 0 1 (zero_add 1) z p q hpq p q (by omega) hpq, zero_add,
  Int.negOnePow_one, Units.neg_smul, one_smul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem sqrt_eq_rpow (x : ℝ≥0) : sqrt x = x ^ (1 / (2 : ℝ))

Proof state:
x : ℝ≥0
⊢ √↑x = ↑x ^ (1 / 2)

Tactic:
exact Real.sqrt_eq_rpow x.1

Result:
no goals

Proof state:
x : ℝ≥0
⊢ sqrt x = x ^ (1 / 2)

Tactic:
refine NNReal.eq ?_

Result:
x : ℝ≥0
⊢ ↑(sqrt x) = ↑(x ^ (1 / 2))

Proof state:
x : ℝ≥0
⊢ ↑(sqrt x) = ↑(x ^ (1 / 2))

Tactic:
push_cast

Result:
x : ℝ≥0
⊢ √↑x = ↑x ^ (1 / 2)
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem span_of_finite_le_degreeLT {s : Set R[X]} (s_fin : s.Finite) :
    ∃ n : ℕ, Submodule.span R s ≤ degreeLT R n

Proof state:
case intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ ∃ n, Submodule.span R s ≤ degreeLT R n

Tactic:
exact ⟨n + 1, by rwa [degreeLT_succ_eq_degreeLE]⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ Submodule.span R s ≤ degreeLT R (n + 1)

Tactic:
rwa [degreeLT_succ_eq_degreeLE]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
⊢ ∃ n, Submodule.span R s ≤ degreeLT R n

Tactic:
rcases span_le_degreeLE_of_finite s_fin with ⟨n, _⟩

Result:
case intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ ∃ n, Submodule.span R s ≤ degreeLT R n
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem ones_blocksFun (n : ℕ) (i : Fin (ones n).length) : (ones n).blocksFun i = 1

Proof state:
n : ℕ
i : Fin (ones n).length
⊢ (ones n).blocksFun i = 1

Tactic:
simp only [blocksFun, ones, get_eq_getElem, getElem_replicate]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)

Tactic:
exact one_ne_zero ∘ And.right

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem le_dimH_of_hausdorffMeasure_eq_top {s : Set X} {d : ℝ≥0} (h : μH[d] s = ∞) :
    ↑d ≤ dimH s

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ⊤
⊢ ↑d ≤ dimH s

Tactic:
rw [dimH_def]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ⊤
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ⊤
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) d h

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_mulSingle_one : mulSupport (mulSingle a (1 : B)) = ∅

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
⊢ mulSupport (mulSingle a 1) = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) :
    cos x < 0 :=
  neg_pos.1 <| cos_pi_sub x ▸ cos_pos_of_mem_Ioo ⟨by linarith, by linarith⟩

Proof state:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ π - x < π / 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ -(π / 2) < π - x

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
    l.toArray.any p 0 stop = l.any p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.any p = l.any p

Tactic:
rw [any_toList]

Result:
no goals

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
l : List α
h : stop = l.toArray.size
⊢ l.toArray.any p 0 stop = l.any p

Tactic:
subst h

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.any p = l.any p
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem one_smul (x : X') : (1 : B) • x = x :=
  match x with
  | fromCoset y => by
    change fromCoset _ = fromCoset _
    simp only [one_leftCoset, Subtype.ext_iff_val]
  | ∞ => rfl

Proof state:
A B : Grp
f : A ⟶ B
x : X'
y : ↑X
⊢ 1 • fromCoset y = fromCoset y

Tactic:
change fromCoset _ = fromCoset _

Result:
A B : Grp
f : A ⟶ B
x : X'
y : ↑X
⊢ fromCoset ⟨1 • ↑y, ⋯⟩ = fromCoset y

Proof state:
A B : Grp
f : A ⟶ B
x : X'
y : ↑X
⊢ fromCoset ⟨1 • ↑y, ⋯⟩ = fromCoset y

Tactic:
simp only [one_leftCoset, Subtype.ext_iff_val]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_refl : map (OrderIso.refl α) = OrderIso.refl _

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

Tactic:
ext

Result:
case h.h.a.h
α : Type u_1
inst✝ : Preorder α
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (UpperSet α)) x✝¹)

Proof state:
case h.h.a.h
α : Type u_1
inst✝ : Preorder α
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (UpperSet α)) x✝¹)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Subobject.lean
theorem cokernel_π_imageSubobject_ext {L M N : ModuleCat.{v} R} (f : L ⟶ M) [HasImage f]
    (g : (imageSubobject f : ModuleCat.{v} R) ⟶ N) [HasCokernel g] {x y : N} (l : L)
    (w : x = y + g (factorThruImageSubobject f l)) : cokernel.π g x = cokernel.π g y

Proof state:
R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (ConcreteCategory.hom (cokernel.π g))
      (y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)) =
    (ConcreteCategory.hom (cokernel.π g)) y

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
x y : ↑N
l : ↑L
w : x = y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)
⊢ (ConcreteCategory.hom (cokernel.π g)) x = (ConcreteCategory.hom (cokernel.π g)) y

Tactic:
subst w

Result:
R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (ConcreteCategory.hom (cokernel.π g))
      (y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)) =
    (ConcreteCategory.hom (cokernel.π g)) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_erase [LawfulBEq α] (a : α) (l : Array α) :
    (l.erase a).size = if a ∈ l then l.size - 1 else l.size

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (l.erase a).size = if a ∈ l then l.size - 1 else l.size

Tactic:
rw [erase_eq_eraseP, size_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (if (l.any fun x => a == x) = true then l.size - 1 else l.size) = if a ∈ l then l.size - 1 else l.size

Proof state:
case e_c
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ ((l.any fun x => a == x) = true) = (a ∈ l)

Tactic:
simp [mem_iff_getElem, eq_comm (a := a)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (if (l.any fun x => a == x) = true then l.size - 1 else l.size) = if a ∈ l then l.size - 1 else l.size

Tactic:
congr

Result:
case e_c
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ ((l.any fun x => a == x) = true) = (a ∈ l)
-- Mathlib/Data/Set/Image.lean
lemma preimage_val_subset_preimage_val_iff (s t u : Set α) :
    (Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Proof state:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → s ∩ t ⊆ s ∩ u

Tactic:
rw [← image_preimage_coe, ← image_preimage_coe]

Result:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' (val ⁻¹' t) ⊆ val '' (val ⁻¹' u)

Proof state:
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Tactic:
constructor

Result:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → s ∩ t ⊆ s ∩ u

case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Proof state:
case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
intro h x a

Result:
case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : ↑s
a : x ∈ val ⁻¹' t
⊢ x ∈ val ⁻¹' u

Proof state:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' (val ⁻¹' t) ⊆ val '' (val ⁻¹' u)

Tactic:
exact image_subset _

Result:
no goals

Proof state:
case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : ↑s
a : x ∈ val ⁻¹' t
⊢ x ∈ val ⁻¹' u

Tactic:
exact (h ⟨x.2, a⟩).2

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Completion.lean
lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
    ‖(x : v.Completion)‖ = |x|

Proof state:
v : InfinitePlace ℚ
x : ℚ
⊢ ‖↑x‖ = ↑|x|

Tactic:
rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
  norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
  Rat.infinitePlace_apply]

Result:
no goals