harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/Replicate.lean
theorem lt_replicate_succ {m : Multiset α} {x : α} {n : ℕ} :
    m < replicate (n + 1) x ↔ m ≤ replicate n x

Proof state:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
rw [replicate_succ]

Result:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x

Proof state:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

Tactic:
rintro ⟨x', hx'⟩

Result:
case mp.intro
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x

Proof state:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
intro h

Result:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Proof state:
case mp.intro
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x

Tactic:
rwa [this, replicate_succ, cons_le_cons_iff] at hx'

Result:
no goals

Proof state:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x

Tactic:
rw [lt_iff_cons_le]

Result:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x

Proof state:
case mp.intro
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x

Tactic:
have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))

Result:
case mp.intro
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x

Proof state:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x

Tactic:
exact ⟨x, cons_le_cons _ h⟩

Result:
no goals

Proof state:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x

Tactic:
constructor

Result:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pow_of_pell {m n k} :
    n ^ k = m ↔ k = 0 ∧ m = 1 ∨0 < k ∧ (n = 0 ∧ m = 0 ∨
      0 < n ∧ ∃ (w a t z : ℕ) (a1 : 1 < a), xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
      2 * a * n = t + (n * n + 1) ∧ m < t ∧
      n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Proof state:
case mp
n k : ℕ
⊢ k = 0 ∧ n ^ k = 1 ∨
    0 < k ∧
      (n = 0 ∧ n ^ k = 0 ∨
        0 < n ∧
          ∃ w a t z,
            ∃ (a1 : 1 < a),
              xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
                2 * a * n = t + (n * n + 1) ∧
                  n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Tactic:
refine k.eq_zero_or_pos.imp (fun k0 : k = 0 => k0.symm ▸ ⟨rfl, rfl⟩) fun hk => ⟨hk, ?_⟩

Result:
case mp
n k : ℕ
hk : 0 < k
⊢ n = 0 ∧ n ^ k = 0 ∨
    0 < n ∧
      ∃ w a t z,
        ∃ (a1 : 1 < a),
          xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
            2 * a * n = t + (n * n + 1) ∧
              n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_lt_size {p : α → Bool} {xs : Array α} :
    xs.findIdx p < xs.size ↔ ∃ x ∈ xs, p x

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } < { toList := xs }.size ↔ ∃ x, x ∈ { toList := xs } ∧ p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
⊢ findIdx p xs < xs.size ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } < { toList := xs }.size ↔ ∃ x, x ∈ { toList := xs } ∧ p x = true
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
    (univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ =>
        Pi.mulSingle_apply_commute x i j) = x

Proof state:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝² : i ∈ ↑univ
j : ι
a✝¹ : j ∈ ↑univ
a✝ : i ≠ j
⊢ (Commute on fun i => (MonoidHom.mulSingle M i) (x i)) i j

Tactic:
exact Pi.mulSingle_apply_commute x i j

Result:
no goals

Proof state:
case h.convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j => Pi.mulSingle j (x j) i) ⋯ = x i

Tactic:
rw [noncommProd_insert_of_not_mem _ _ _ _ (not_mem_erase _ _),
  noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]

Result:
case h.convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i

case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrable_inv_one_add_sq : Integrable fun (x : ℝ) ↦ (1 + x ^ 2)⁻¹

Proof state:
⊢ Integrable (fun x => (1 + x ^ 2)⁻¹) volume

Tactic:
suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]

Result:
⊢ Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume

Proof state:
⊢ ↑(Module.finrank ℝ ℝ) < 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume

Tactic:
exact integrable_rpow_neg_one_add_norm_sq (by simp)

Result:
no goals

Proof state:
this : Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume
⊢ Integrable (fun x => (1 + x ^ 2)⁻¹) volume

Tactic:
simpa [rpow_neg_one]

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem preVal_eq_zero {x : ModP O p} : preVal K v O p x = 0 ↔ x = 0 :=
  ⟨fun hvx =>
    by_contradiction fun hx0 : x ≠ 0 => by
      rw [← v_p_lt_preVal (hv := hv), hvx] at hx0
      exact not_lt_zero' hx0,
    fun hx => hx.symm ▸ preVal_zero⟩

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hvx : preVal K v O p x = 0
hx0 : v ↑p < 0
⊢ False

Tactic:
exact not_lt_zero' hx0

Result:
no goals

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hvx : preVal K v O p x = 0
hx0 : x ≠ 0
⊢ False

Tactic:
rw [← v_p_lt_preVal (hv := hv), hvx] at hx0

Result:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hvx : preVal K v O p x = 0
hx0 : v ↑p < 0
⊢ False
-- Mathlib/Data/Finsupp/Multiset.lean
theorem mem_toMultiset (f : α →₀ ℕ) (i : α) : i ∈ toMultiset f ↔ i ∈ f.support

Proof state:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ i ∈ toMultiset f ↔ i ∈ f.support

Tactic:
rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

Result:
no goals

Proof state:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ i ∈ toMultiset f ↔ i ∈ f.support

Tactic:
classical
rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem toAdd_list_sum (s : List (Multiplicative α)) : s.prod.toAdd = (s.map toAdd).sum

Proof state:
α : Type u_3
inst✝ : AddMonoid α
s : List (Multiplicative α)
⊢ toAdd s.prod = (List.map (⇑toAdd) s).sum

Tactic:
simp [toAdd, ofAdd]

Result:
α : Type u_3
inst✝ : AddMonoid α
s : List (Multiplicative α)
⊢ s.prod = s.sum

Proof state:
α : Type u_3
inst✝ : AddMonoid α
s : List (Multiplicative α)
⊢ s.prod = s.sum

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNorm_indicator_norm_ge_le (hf : MemLp f p μ) (hmeas : StronglyMeasurable f) {ε : ℝ}
    (hε : 0 < ε) : ∃ M : ℝ, eLpNorm ({ x | M ≤ ‖f x‖₊ }.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hp_ne_zero : p = 0

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ⊤ μ
hp_ne_zero : ¬⊤ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ⊤ μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas

Result:
case pos.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ⊤ μ
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) ⊤ μ ≤ ENNReal.ofReal ε

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x => ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∉ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ 0 ^ p.toReal = 0

Tactic:
simp [ENNReal.toReal_pos hp_ne_zero hp_ne_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨1, hp_ne_zero.symm ▸ ?_⟩

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ eLpNorm ({x | 1 ≤ ↑‖f x‖₊}.indicator f) 0 μ ≤ ENNReal.ofReal ε
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_comp [IsIso f] [IsIso h] : inv (f ≫ h) = inv h ≫ inv f

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

Tactic:
apply inv_eq_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X

Proof state:
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem unique' {p : A[X]} (hm : p.Monic) (hp : Polynomial.aeval x p = 0)
    (hl : ∀ q : A[X], degree q < degree p → q = 0 ∨ Polynomial.aeval x q ≠ 0) :
    p = minpoly A x

Proof state:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x

Tactic:
obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 h

Result:
case inl.intro
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
⊢ p = minpoly A x

Tactic:
nontriviality A

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
⊢ p = minpoly A x
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem finite_of_finrank_pos (h : 0 < finrank R M) : Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ¬Module.Finite R M
⊢ ¬0 < finrank R M

Tactic:
simp [finrank_of_not_finite h]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : 0 < finrank R M
⊢ Module.Finite R M

Tactic:
contrapose h

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ¬Module.Finite R M
⊢ ¬0 < finrank R M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Pow.lean
theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n

Proof state:
b n : Nat
⊢ ↑(b ^ 0) = ↑b ^ 0

Tactic:
rfl

Result:
no goals

Proof state:
b n✝ n : Nat
⊢ ↑(b ^ (n + 1)) = ↑b ^ (n + 1)

Tactic:
simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]

Result:
no goals

Proof state:
b n : Nat
⊢ ↑(b ^ n) = ↑b ^ n

Tactic:
match n with
| 0 => rfl
| n + 1 =>
  simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
lemma diffContOnCl_interpStrip :
    DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Proof state:
case neg.intro.h.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow ↑(sSupNormIm f 1)) z

Tactic:
refine DifferentiableAt.const_cpow ?_ ?_

Result:
case neg.intro.h.refine_2.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun x => x) z

case neg.intro.h.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 0 = 0

Tactic:
rwa [eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
lemma pow_unbounded_of_one_lt [ExistsAddOfLE α] (x : α) (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n

Proof state:
case intro.intro
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x z : α
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (1 + z) ^ n

Tactic:
rw [add_comm]

Result:
case intro.intro
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x z : α
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (z + 1) ^ n

Proof state:
case intro.intro
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x z : α
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (z + 1) ^ n

Tactic:
exact add_one_pow_unbounded_of_pos _ hz

Result:
no goals

Proof state:
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
y : α
inst✝ : ExistsAddOfLE α
x : α
hy1 : 1 < y
⊢ ∃ n, x < y ^ n

Tactic:
obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1

Result:
case intro.intro
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x z : α
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (1 + z) ^ n
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem _root_.LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {T : F →L[ℝ] F}
    (hT : (T : F →ₗ[ℝ] F).IsSymmetric) (x₀ : F) :
    HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ (T x₀))) x₀

Proof state:
case h.e'_12.h.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : Real.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
y : F
⊢ (2 • (innerSL ℝ) (T x₀)) y = ((fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))) y

Tactic:
rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
  ContinuousLinearMap.prod_apply, innerSL_apply, id, ContinuousLinearMap.id_apply,
  hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]

Result:
no goals

Proof state:
case h.e'_12.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : Real.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 2 • (innerSL ℝ) (T x₀) = (fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))

Tactic:
ext y

Result:
case h.e'_12.h.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : Real.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
y : F
⊢ (2 • (innerSL ℝ) (T x₀)) y = ((fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))) y

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
⊢ HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀

Tactic:
convert T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1

Result:
case h.e'_12.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : Real.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 2 • (innerSL ℝ) (T x₀) = (fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))
-- Mathlib/NumberTheory/Divisors.lean
theorem pos_of_mem_divisors {m : ℕ} (h : m ∈ n.divisors) : 0 < m

Proof state:
case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

Tactic:
rw [mem_divisors, zero_dvd_iff (a := n)] at h

Result:
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0

Proof state:
case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1

Tactic:
apply Nat.succ_pos

Result:
no goals

Proof state:
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0

Tactic:
cases h.2 h.1

Result:
no goals

Proof state:
n m : ℕ
h : m ∈ n.divisors
⊢ 0 < m

Tactic:
cases m

Result:
case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_int_mul_pi_sub (x : ℝ) (n : ℤ) : sin (n * π - x) = -((-1) ^ n * sin x)

Proof state:
x : ℝ
n : ℤ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)

Tactic:
simpa only [sin_neg, mul_neg, Int.cast_negOnePow] using sin_antiperiodic.int_mul_sub_eq n

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g :=
  { epi

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
inst✝ : Mono z
⊢ HasLiftingProperty g z

Tactic:
apply HasLiftingProperty.of_arrow_iso_left e z

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi g

Tactic:
rw [Arrow.iso_w' e]

Result:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi (e.inv.left ≫ f ≫ e.hom.right)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Mono z], HasLiftingProperty g z

Tactic:
intro

Result:
C : Type u
inst✝¹ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
inst✝ : Mono z
⊢ HasLiftingProperty g z

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi (e.inv.left ≫ f ≫ e.hom.right)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_insert_of_mem {a : α} (h : a ∈ s) : ncard (insert a s) = s.ncard

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).ncard = s.ncard

Tactic:
rw [insert_eq_of_mem h]

Result:
no goals