harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} :
    map f (expand R p q) = expand S p (map f q)

Proof state:
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Tactic:
simp [hp]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Tactic:
ext

Result:
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ (map f ((expand R p) q)).coeff n✝ = ((expand S p) (map f q)).coeff n✝

Proof state:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f ((expand R p) q) = (expand S p) (map f q)

case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Proof state:
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ (map f ((expand R p) q)).coeff n✝ = ((expand S p) (map f q)).coeff n✝

Tactic:
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]

Result:
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Ici_add_bij : BijOn (· + d) (Ici a) (Ici (a + d))

Proof state:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ici a

Tactic:
exact ⟨a + c, h, by rw [add_right_comm]⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d x✝ : M
h : x✝ ∈ Ici (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ici a

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)

Result:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ici a

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ (fun x => x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ici a

Tactic:
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h

Result:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ici a

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ BijOn (fun x => x + d) (Ici a) (Ici (a + d))

Tactic:
refine
  ⟨fun x h => add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).injOn, fun _ h => ?_⟩

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d x✝ : M
h : x✝ ∈ Ici (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ici a
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem eq_zero_of_inner_right (hK : Dense (K : Set E)) (h : ∀ v : K, ⟪(v : E), x⟫ = 0) : x = 0 :=
  hK.eq_of_inner_right fun v => by rw [inner_zero_right, h v]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hK : Dense ↑K
h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = 0
v : ↥K
⊢ ⟪↑v, x⟫_𝕜 = ⟪↑v, 0⟫_𝕜

Tactic:
rw [inner_zero_right, h v]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem to_leftMoves_one_toPGame_symm (i) :
    (@toLeftMovesToPGame 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩

Proof state:
i : (toPGame 1).LeftMoves
⊢ toLeftMovesToPGame.symm i = ⟨0, ⋯⟩

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_mem_Ioc [NeZero n] (x : ZMod n) : x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n

Proof state:
case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ x.val ≤ n

Tactic:
exact x.val_lt.le

Result:
no goals

Proof state:
case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2

Tactic:
linarith only [h]

Result:
no goals

Proof state:
case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0

Tactic:
rw [sub_nonpos, Int.ofNat_le]

Result:
case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ x.val ≤ n

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]

Result:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Proof state:
case pos.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ 0 ≤ ↑x.val

case pos.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ 0 ≤ 2

Tactic:
exacts [Nat.cast_nonneg _, zero_le_two]

Result:
no goals

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩

Result:
case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2

case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
refine ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (mul_nonneg ?_ ?_), h⟩

Result:
case pos.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ 0 ≤ ↑x.val

case pos.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ 0 ≤ 2
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- The negated addition of two nonsingular affine points in `W` on a sloped line is nonsingular. -/
lemma nonsingular_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : W.Nonsingular
      (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.negAddY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂)

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
            (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
    0

Tactic:
simp only [neg_ne_zero, sub_self, mul_zero, add_zero]

Result:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
apply nonsingular_negAdd_of_eval_derivative_ne_zero <| equation_negAdd h₁.left h₂.left hxy

Result:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) ≠ 0
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem coe_eq_of_mem_split_of_lt_mem {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J)
    (h₃ : x < y i) : (J : Set (ι → ℝ)) = ↑I ∩ { y | x < y i }

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Tactic:
rw [← Box.mem_coe, H] at h₂

Result:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
⊢ ↑J = ↑I ∩ {y | x < y i}

Tactic:
refine (mem_split_iff'.1 h₁).resolve_left fun H => ?_

Result:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Tactic:
exact h₃.not_le h₂.2

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem tendsto_translationNumber (x : ℝ) :
    Tendsto (fun n : ℕ => ((f ^ n) x - x) / n) atTop (𝓝 <| τ f)

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => ((f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x)))))

Tactic:
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_

Result:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ((↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    ((f ^ n) x - x) / ↑n

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => ((f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))

Tactic:
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]

Result:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => ((f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x)))))

Proof state:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ((↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    ((f ^ n) x - x) / ↑n

Tactic:
simp [sub_eq_neg_add, Units.conj_pow']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum

Proof state:
L : List ℕ
⊢ L.headI + L.tail.sum = L.sum

Tactic:
cases L <;> simp

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem card_le_one_iff_subsingleton (α : Type*) : card α ≤ 1 ↔ Subsingleton α

Proof state:
α : Type u_1
⊢ card α ≤ 1 ↔ toPartENat #α ≤ ↑1

Tactic:
simp only [PartENat.card, Nat.cast_one]

Result:
no goals

Proof state:
α : Type u_1
⊢ card α ≤ 1 ↔ #α ≤ ↑1

Tactic:
rw [← Cardinal.toPartENat_le_natCast_iff]

Result:
α : Type u_1
⊢ card α ≤ 1 ↔ toPartENat #α ≤ ↑1

Proof state:
α : Type u_1
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
rw [← le_one_iff_subsingleton]

Result:
α : Type u_1
⊢ card α ≤ 1 ↔ #α ≤ 1

Proof state:
α : Type u_1
⊢ card α ≤ 1 ↔ #α ≤ 1

Tactic:
conv_rhs => rw [← Nat.cast_one]

Result:
α : Type u_1
⊢ card α ≤ 1 ↔ #α ≤ ↑1
-- Mathlib/Data/Nat/Choose/Bounds.lean
lemma choose_le_descFactorial (n k : ℕ) : n.choose k ≤ n.descFactorial k

Proof state:
n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k

Tactic:
exact Nat.div_le_self _ _

Result:
no goals

Proof state:
n k : ℕ
⊢ n.choose k ≤ n.descFactorial k

Tactic:
rw [choose_eq_descFactorial_div_factorial]

Result:
n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_univ_three (a b c : ℕ) :
    multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)

Proof state:
a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)

Tactic:
rfl

Result:
no goals

Proof state:
a b c : ℕ
⊢ multinomial univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)

Tactic:
rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]

Result:
a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
-- Mathlib/Order/LiminfLimsup.lean
lemma limsInf_principal_eq_sInf (s : Set α) : limsInf (𝓟 s) = sInf s

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsInf = sInf s

Tactic:
simpa only [limsInf, eventually_principal] using sSup_lowerBounds_eq_sInf s

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem set_support_apply_mem {p : Perm α} {a : α} :
    p a ∈ { x | p x ≠ x } ↔ a ∈ { x | p x ≠ x }

Proof state:
α : Type u_1
p : Perm α
a : α
⊢ p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem map_exp_atTop : map exp atTop = atTop

Proof state:
⊢ Filter.map rexp atTop = atTop

Tactic:
rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_dite {p : Prop} [Decidable p] {b : p → β} :
    (if h : p then some (b h) else none).isSome = true ↔ p

Proof state:
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
⊢ (if h : p then some (b h) else none).isSome = true ↔ p

Tactic:
split <;> simpa

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem distortion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) :
    (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = π₁.distortion ⊔ π₂.distortion

Tactic:
classical exact sup_union

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = π₁.distortion ⊔ π₂.distortion

Tactic:
exact sup_union

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) :
    derivWithin f₁ s x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
rw [fderivWithin_congr hs hx]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
theorem MemLp.meas_ge_lt_top' {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    μ { x | ε ≤ ‖f x‖₊ } < ∞

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ε⁻¹ ^ p.toReal < ⊤

Tactic:
simp [hε, lt_top_iff_ne_top]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ⊤

Tactic:
apply (meas_ge_le_mul_pow_eLpNorm μ hp_ne_zero hp_ne_top hℒp.aestronglyMeasurable hε).trans_lt
  (ENNReal.mul_lt_top ?_ ?_)

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ε⁻¹ ^ p.toReal < ⊤

α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ eLpNorm f p μ ^ p.toReal < ⊤

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ eLpNorm f p μ ^ p.toReal < ⊤

Tactic:
simp [hℒp.eLpNorm_lt_top.ne, lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma leRec_trans {n m k} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le)
    (hnm : n ≤ m) (hmk : m ≤ k) :
    leRec (motive := motive) refl le_succ_of_le (Nat.le_trans hnm hmk) =
      leRec
        (leRec refl (fun _ h => le_succ_of_le h) hnm)
        (fun _ h => le_succ_of_le <| Nat.le_trans hnm h) hmk

Proof state:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
hmk : m ≤ k
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) hmk

Tactic:
induction hmk with
| refl => rw [leRec_self]
| step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]

Result:
no goals

Proof state:
case refl
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) ⋯

Tactic:
rw [leRec_self]

Result:
no goals

Proof state:
case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) hmk
⊢ leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) ⋯

Tactic:
rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_merge (le) {s₁ s₂ : Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) :
    (merge le s₁ s₂).size = s₁.size + s₂.size

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ (if le a✝¹ a✝ = true then node a✝¹ (node a✝ c✝ c✝¹) nil else node a✝ (node a✝¹ c✝¹ c✝) nil).size =
    (node a✝¹ c✝¹ nil).size + (node a✝ c✝ nil).size

Tactic:
split <;> simp_arith [size]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ (merge le (node a✝¹ c✝¹ nil) (node a✝ c✝ nil)).size = (node a✝¹ c✝¹ nil).size + (node a✝ c✝ nil).size

Tactic:
unfold merge

Result:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ (match node a✝¹ c✝¹ nil, node a✝ c✝ nil with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size =
    (node a✝¹ c✝¹ nil).size + (node a✝ c✝ nil).size

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ (match node a✝¹ c✝¹ nil, node a✝ c✝ nil with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size =
    (node a✝¹ c✝¹ nil).size + (node a✝ c✝ nil).size

Tactic:
dsimp

Result:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ (if le a✝¹ a✝ = true then node a✝¹ (node a✝ c✝ c✝¹) nil else node a✝ (node a✝¹ c✝¹ c✝) nil).size =
    (node a✝¹ c✝¹ nil).size + (node a✝ c✝ nil).size

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
⊢ (merge le s₁ s₂).size = s₁.size + s₂.size

Tactic:
match h₁, h₂ with
| .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [merge, size]
| .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp_arith [size]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : s₁.NoSibling
h₂ : s₂.NoSibling
a✝ : α
c✝ : Heap α
⊢ (merge le (node a✝ c✝ nil) nil).size = (node a✝ c✝ nil).size + nil.size

Tactic:
simp [merge, size]

Result:
no goals
-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem isLocalization_isLocalization_atPrime_isLocalization (p : Ideal S) [Hp : p.IsPrime]
    [IsLocalization.AtPrime T p] : IsLocalization.AtPrime T (p.comap (algebraMap R S))

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False

Tactic:
exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)

Tactic:
apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ p.primeCompl

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ p.primeCompl

Tactic:
intro x hx hx'

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False