harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} :
    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 :=
  ⟨fun h => by simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h, tendsto_pow_atTop_nhds_zero_of_lt_one⟩

Proof state:
r : ℝ≥0
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ pre F E ≫ π (E ⋙ F) k = π F (E.obj k)

Tactic:
erw [IsLimit.fac]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ (Cone.whisker E (cone F)).π.app k = π F (E.obj k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ (Cone.whisker E (cone F)).π.app k = π F (E.obj k)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitIsoLimitCurryCompLim_hom_π_π {j} {k} :
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k = limit.π G (j, k)

Tactic:
simp [limitIsoLimitCurryCompLim, Trans.simple]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_X_of_ne_one {n : ℕ} (hn : n ≠ 1) : coeff (X : R[X]) n = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
rw [coeff_X, if_neg hn.symm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem nextCoeff_X_sub_C [Ring S] (c : S) : nextCoeff (X - C c) = -c

Proof state:
S : Type v
inst✝ : Ring S
c : S
⊢ (X - C c).nextCoeff = -c

Tactic:
rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_X (x y : R) : X.evalEval x y = y

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y Y = y

Tactic:
rw [evalEval, eval_X, eval_C]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem one_lt_ack_succ_left : ∀ m n, 1 < ack (m + 1) n
  | 0, n => by simp
  | m + 1, 0 => by
    rw [ack_succ_zero]
    apply one_lt_ack_succ_left
  | m + 1, n + 1 => by
    rw [ack_succ_succ]
    apply one_lt_ack_succ_left

Proof state:
m : ℕ
⊢ 1 < ack (m + 1 + 1) 0

Tactic:
rw [ack_succ_zero]

Result:
m : ℕ
⊢ 1 < ack (m + 1) 1

Proof state:
n : ℕ
⊢ 1 < ack (0 + 1) n

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ 1 < ack (m + 1) (ack (m + 1 + 1) n)

Tactic:
apply one_lt_ack_succ_left

Result:
no goals

Proof state:
m n : ℕ
⊢ 1 < ack (m + 1 + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Result:
m n : ℕ
⊢ 1 < ack (m + 1) (ack (m + 1 + 1) n)

Proof state:
m : ℕ
⊢ 1 < ack (m + 1) 1

Tactic:
apply one_lt_ack_succ_left

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_map : δ n m (z.map Φ) = (δ n m z).map Φ

Proof state:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : ¬n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
simp only [δ_shape _ _ hnm, Cochain.map_zero]

Result:
no goals

Proof state:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
ext p q hpq

Result:
case pos.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (z.map Φ)).v p q hpq = ((δ n m z).map Φ).v p q hpq

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
by_cases hnm : n + 1 = m

Result:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : ¬n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Proof state:
case pos.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (z.map Φ)).v p q hpq = ((δ n m z).map Φ).v p q hpq

Tactic:
dsimp

Result:
case pos.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (z.map Φ)).v p q hpq = Φ.map ((δ n m z).v p q hpq)

Proof state:
case pos.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (z.map Φ)).v p q hpq = Φ.map ((δ n m z).v p q hpq)

Tactic:
simp only [δ_v n m hnm _ p q hpq (q-1) (p+1) rfl rfl,
  Functor.map_add, Functor.map_comp, Functor.map_units_smul,
  Cochain.map_v, Functor.mapHomologicalComplex_obj_d]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem mono_to_simple_zero_of_not_iso {X Y : C} [Simple Y] {f : X ⟶ Y} [Mono f]
    (w : IsIso f → False) : f = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False

Tactic:
exact w (isIso_of_mono_of_nonzero h)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0

Tactic:
by_contra h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0

Tactic:
classical
  by_contra h
  exact w (isIso_of_mono_of_nonzero h)

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem hasSum_of_monomials_self (f : MvPowerSeries σ R) :
    HasSum (fun d : σ →₀ ℕ => monomial R d (coeff R d f)) f

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial R i) ((coeff R i) f) d) (f d)

Tactic:
convert hasSum_single d ?_ using 1

Result:
case h.e'_6
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ f d = (monomial R d) ((coeff R d) f) d

case convert_5
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ∀ (b' : σ →₀ ℕ), b' ≠ d → (monomial R b') ((coeff R b') f) d = 0

Proof state:
case convert_5
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ∀ (b' : σ →₀ ℕ), b' ≠ d → (monomial R b') ((coeff R b') f) d = 0

Tactic:
exact fun d' h ↦ coeff_monomial_ne (Ne.symm h) _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial R i) ((coeff R i) f) x) (f x)

Tactic:
intro d

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial R i) ((coeff R i) f) d) (f d)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ HasSum (fun d => (monomial R d) ((coeff R d) f)) f

Tactic:
rw [Pi.hasSum]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial R i) ((coeff R i) f) x) (f x)

Proof state:
case h.e'_6
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ f d = (monomial R d) ((coeff R d) f) d

Tactic:
exact (coeff_monomial_same d _).symm

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_add : ((φ + ψ : R[X]) : PowerSeries R) = φ + ψ

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑(φ + ψ) = (PowerSeries.coeff R n✝) (↑φ + ↑ψ)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
⊢ ↑(φ + ψ) = ↑φ + ↑ψ

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑(φ + ψ) = (PowerSeries.coeff R n✝) (↑φ + ↑ψ)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) {hc : k ∈ m.modify k f} :
    haveI h' : k ∈ m := mem_modify h |>.mp hc
    (m.modify k f).get k hc = f (m.get k h')

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).contains k = true → (m.modify k f).get k hc = f (m.get k ⋯)

Tactic:
simp_to_raw using Raw₀.get_modify_self

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).get k hc = f (m.get k ⋯)

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
hc✝ : k ∈ m.modify k f
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).get k hc✝ = f (m.get k ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
hc✝ : k ∈ m.modify k f
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).get k hc✝ = f (m.get k ⋯)

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).contains k = true → (m.modify k f).get k hc = f (m.get k ⋯)
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_smul_measure {m : MeasurableSpace α} (μ : Measure α) (c : ℝ≥0∞) {s : Set α} :
    (weightedSMul (c • μ) s : F →L[ℝ] F) = c.toReal • weightedSMul μ s

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ((c • ⇑μ) s).toReal • x = c.toReal • (μ s).toReal • x

Tactic:
simp_rw [Pi.smul_apply, smul_eq_mul, toReal_mul, smul_smul]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ (weightedSMul (c • μ) s) x = (c.toReal • ⇑(weightedSMul μ s)) x

Tactic:
simp_rw [Pi.smul_apply, weightedSMul_apply]

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ((c • μ) s).toReal • x = c.toReal • (μ s).toReal • x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ((c • μ) s).toReal • x = c.toReal • (μ s).toReal • x

Tactic:
push_cast

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ ((c • ⇑μ) s).toReal • x = c.toReal • (μ s).toReal • x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ (weightedSMul (c • μ) s) x = (c.toReal • weightedSMul μ s) x

Tactic:
push_cast

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ (weightedSMul (c • μ) s) x = (c.toReal • ⇑(weightedSMul μ s)) x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ weightedSMul (c • μ) s = c.toReal • weightedSMul μ s

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ (weightedSMul (c • μ) s) x = (c.toReal • weightedSMul μ s) x
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem power_mul {a b c : Cardinal} : a ^ (b * c) = (a ^ b) ^ c

Proof state:
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c

Tactic:
exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α

Result:
no goals

Proof state:
a b c : Cardinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
rw [mul_comm b c]

Result:
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem mem_of_find?_eq_some {xs : Vector α n} (h : find? p xs = some a) : a ∈ xs

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp at h

Result:
case mk
α : Type
n : Nat
p : α → Bool
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : Array.find? p toArray✝ = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
α : Type
n : Nat
p : α → Bool
a : α
xs : Vector α n
h : find? p xs = some a
⊢ a ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type
n : Nat
p : α → Bool
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : Array.find? p toArray✝ = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simpa using Array.mem_of_find?_eq_some h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C_le : degree (C a) ≤ 0

Proof state:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C a).degree ≤ 0

Tactic:
rw [h, C_0]

Result:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ degree 0 ≤ 0

Proof state:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ degree 0 ≤ 0

Tactic:
exact bot_le

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
⊢ (C a).degree ≤ 0

Tactic:
by_cases h : a = 0

Result:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C a).degree ≤ 0

case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Proof state:
case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Tactic:
rw [degree_C h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
lemma measurableSet_le (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    MeasurableSet[m] {a | f a ≤ g a}

Proof state:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a ≤ g a}

Tactic:
borelize (E × E)

Result:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a ≤ g a}

Proof state:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a ≤ g a}

Tactic:
exact (hf.prod_mk hg).measurable isClosed_le_prod.measurableSet

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y]
    {φ : H → G} (j : Y →ₑ[φ] X) (hB : IsBlock G B) :
    IsBlock H (j ⁻¹' B)

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
⊢ IsBlock H (⇑j ⁻¹' B)

Tactic:
rintro g₁ g₂ hg

Result:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : g₁ • ⇑j ⁻¹' B ≠ g₂ • ⇑j ⁻¹' B
⊢ Disjoint (g₁ • ⇑j ⁻¹' B) (g₂ • ⇑j ⁻¹' B)

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : g₁ • ⇑j ⁻¹' B ≠ g₂ • ⇑j ⁻¹' B
⊢ Disjoint (g₁ • ⇑j ⁻¹' B) (g₂ • ⇑j ⁻¹' B)

Tactic:
rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢

Result:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ ⇑j ⁻¹' (φ g₂ • B)
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (⇑j ⁻¹' (φ g₂ • B))

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ ⇑j ⁻¹' (φ g₂ • B)
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (⇑j ⁻¹' (φ g₂ • B))

Tactic:
exact (hB <| ne_of_apply_ne _ hg).preimage _

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
theorem IsSelfAdjoint.im_eq_zero_of_mem_spectrum {a : A} (ha : IsSelfAdjoint a)
    {z : ℂ} (hz : z ∈ spectrum ℂ a) : z.im = 0

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ z.im = 0

Tactic:
rw [ha.mem_spectrum_eq_re hz, ofReal_im]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_swap_iff (x y : α) : support (swap x y) = {x, y} ↔ x ≠ y

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
h : (swap x x).support = {x, x}
⊢ False

Tactic:
simp [Finset.ext_iff] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : (swap x y).support = {x, y}
⊢ x ≠ y

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
h : (swap x x).support = {x, x}
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
⊢ (swap x y).support = {x, y} ↔ x ≠ y

Tactic:
refine ⟨fun h => ?_, fun h => support_swap h⟩

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : (swap x y).support = {x, y}
⊢ x ≠ y
-- Mathlib/Algebra/Ring/Basic.lean
lemma isDomain_iff_noZeroDivisors_and_nontrivial [Ring α] :
    IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Proof state:
α : Type u_2
inst✝ : Ring α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charmatrix_apply_natDegree [Nontrivial R] (i j : n) :
    (charmatrix M i j).natDegree = ite (i = j) 1 0

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
i j : n
⊢ (M.charmatrix i j).natDegree = if i = j then 1 else 0

Tactic:
by_cases h : i = j <;> simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
lemma exists_of_res_zero_of_qcqs {X : Scheme.{u}} {U : TopologicalSpace.Opens X}
    (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier)
    {f s : Γ(X, U)} (hf : f |_ X.basicOpen s = 0) :
    ∃ n, s ^ n * f = 0

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ (f |_ X.basicOpen s) ⋯ = (0 |_ X.basicOpen s) ⋯

Tactic:
simpa

Result:
no goals

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ ∃ n, s ^ n * f = 0

Tactic:
suffices h : ∃ n, s ^ n * f = s ^ n * 0 by
  simpa using h

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ ∃ n, s ^ n * f = s ^ n * 0

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ ∃ n, s ^ n * f = s ^ n * 0

Tactic:
apply exists_of_res_eq_of_qcqs hU hU'

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ (f |_ X.basicOpen s) ⋯ = (0 |_ X.basicOpen s) ⋯

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
h : ∃ n, s ^ n * f = s ^ n * 0
⊢ ∃ n, s ^ n * f = 0

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_nonpos_iff (hx : 0 ≤ x) : log x ≤ 0 ↔ x ≤ 1

Proof state:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
rw [← not_lt, log_pos_iff hx.le, not_lt]

Result:
no goals

Proof state:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

Tactic:
simp [le_refl, zero_le_one]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Result:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1