harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_comp_rev {α n} (a : α) (f : Fin n → α) :
    Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a

Proof state:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ cons a f ∘ rev = snoc (f ∘ rev) a

Tactic:
funext i

Result:
case h
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i

Proof state:
case h
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i

Tactic:
exact cons_rev ..

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ_self {n} {i : Fin (n + 2)} :
    X.δ i ≫ X.δ (Fin.castSucc i) = X.δ i ≫ X.δ i.succ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.castSucc) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.succ)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.castSucc) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.succ)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_δ_self]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/RCLike.lean
theorem norm_smul_inv_norm' {r : ℝ} (r_nonneg : 0 ≤ r) {x : E} (hx : x ≠ 0) :
    ‖((r : 𝕜) * (‖x‖ : 𝕜)⁻¹) • x‖ = r

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
field_simp [norm_smul, r_nonneg, rclike_simps]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_one (n : ℕ) : ack 1 n = n + 2

Proof state:
case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (n + 1) = n + 1 + 2

Tactic:
simp [IH]

Result:
no goals

Proof state:
n : ℕ
⊢ ack 1 n = n + 2

Tactic:
induction' n with n IH

Result:
case zero

⊢ ack 1 0 = 0 + 2

case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (n + 1) = n + 1 + 2

Proof state:
case zero

⊢ ack 1 0 = 0 + 2

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_C (n : ℕ) (a : R) : coeff R n (C R a : R⟦X⟧) = if n = 0 then a else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ (coeff R n) ((C R) a) = if n = 0 then a else 0

Tactic:
rw [← monomial_zero_eq_C_apply, coeff_monomial]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.comp_hasDerivWithinAt_of_eq (hh₂ : HasDerivAt h₂ h₂' y)
    (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
exact hh₂.comp_hasDerivWithinAt x hh

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_left_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist x y ≤ dist x z

Proof state:
x y z : ℝ
h : y ∈ uIcc x z
⊢ dist x y ≤ dist x z

Tactic:
simpa only [dist_comm x] using abs_sub_left_of_mem_uIcc h

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_eq_map_pullback' {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :
    (Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ =
      (Subobject.map f₁.arrow).obj ((Subobject.pullback f₁.arrow).obj f₂)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) = (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' f₂))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ : MonoOver A
f₂ : Subobject A
⊢ (inf.obj (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

Tactic:
induction' f₂ using Quotient.inductionOn' with f₂

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) = (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' f₂))
-- Mathlib/Topology/Ultrafilter.lean
theorem clusterPt_iff_ultrafilter {f : Filter X} : ClusterPt x f ↔
    ∃ u : Ultrafilter X, u ≤ f ∧ u ≤ 𝓝 x

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x

Tactic:
simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem xgcdAux_fst (x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
  gcd.induction x y (by simp) fun x y h IH s t s' t' => by
    simp only [h, xgcdAux_rec, IH]
    rw [← gcd_rec]

Proof state:
x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').1 = gcd 0 n

Tactic:
simp

Result:
no goals

Proof state:
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (x.xgcdAux s t y s' t').1 = x.gcd y

Tactic:
simp only [h, xgcdAux_rec, IH]

Result:
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (y % x).gcd x = x.gcd y

Proof state:
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (y % x).gcd x = x.gcd y

Tactic:
rw [← gcd_rec]

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_apply_eq' (x : E) :
    (fun n ↦ ofScalars E c n (fun _ ↦ x)) = fun n ↦ c n • x ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : E
⊢ (fun n => (ofScalars E c n) fun x_1 => x) = fun n => c n • x ^ n

Tactic:
simp [ofScalars]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem ι_mul_ι_mem_evenOdd_zero (m₁ m₂ : M) : ι Q m₁ * ι Q m₂ ∈ evenOdd Q 0 :=
  Submodule.mem_iSup_of_mem ⟨2, rfl⟩
    (by
      rw [Subtype.coe_mk, pow_two]
      exact
        Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
          (LinearMap.mem_range_self (ι Q) m₂))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)

Tactic:
exact
  Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
    (LinearMap.mem_range_self (ι Q) m₂)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ LinearMap.range (ι Q) ^ ↑⟨2, ⋯⟩

Tactic:
rw [Subtype.coe_mk, pow_two]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_nil_right : dot xs ([] : IntList) = 0

Proof state:
xs : IntList
⊢ xs.dot [] = 0

Tactic:
simp [dot]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Submodule.rank_eq_zero [Nontrivial R] [NoZeroSMulDivisors R M] {S : Submodule R M} :
    Module.rank R S = 0 ↔ S = ⊥ :=
  ⟨fun h =>
    (Submodule.eq_bot_iff _).2 fun x hx =>
      congr_arg Subtype.val <|
        ((Submodule.eq_bot_iff _).1 <| Eq.symm <| Submodule.bot_eq_top_of_rank_eq_zero h) ⟨x, hx⟩
          Submodule.mem_top,
    fun h => by rw [h, rank_bot]⟩

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
S : Submodule R M
h : S = ⊥
⊢ Module.rank R ↥S = 0

Tactic:
rw [h, rank_bot]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
protected lemma isNilpotent_mul_right_iff (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsRight R) :
    IsNilpotent (x * y) ↔ IsNilpotent y

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) → IsNilpotent y

Tactic:
rintro ⟨k, hk⟩

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent y

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) ↔ IsNilpotent y

Tactic:
refine ⟨?_, h_comm.isNilpotent_mul_right⟩

Result:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) → IsNilpotent y

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent y

Tactic:
rw [mul_pow h_comm] at hk

Result:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y

Proof state:
case intro
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y

Tactic:
exact ⟨k, (nonZeroDivisorsRight R).pow_mem hx k _ hk⟩

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Raised.add_right (k) {n m} (H : Raised n m) : Raised (n + k) (m + k)

Proof state:
k n m : ℕ
H : Raised n m
⊢ Raised (n + k) (m + k)

Tactic:
rw [add_comm, add_comm m]

Result:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Proof state:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
exact H.add_left _

Result:
no goals
-- Mathlib/Data/Prod/Lex.lean
/-- Variant of `Prod.Lex.toLex_lt_toLex` for partial orders. -/
lemma toLex_lt_toLex' : toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
rw [toLex_lt_toLex]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
simp only [lt_iff_le_not_le, le_antisymm_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
-- Mathlib/Order/Filter/Basic.lean
theorem set_eventuallyLE_iff_inf_principal_le {s t : Set α} {l : Filter α} :
    s ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t :=
  set_eventuallyLE_iff_mem_inf_principal.trans <| by
    simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

Proof state:
α : Type u
s t : Set α
l : Filter α
⊢ t ∈ l ⊓ 𝓟 s ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t

Tactic:
simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem subsingleton_of_preimage (hf : Function.Surjective f) (s : Set β)
    (hs : (f ⁻¹' s).Subsingleton) : s.Subsingleton := fun fx hx fy hy => by
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact congr_arg f (hs hx hy)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y

Tactic:
exact congr_arg f (hs hx hy)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
⊢ fx = fy

Tactic:
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_add [∀ i, AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] (f g : Π₀ i, β i) :
    (f + g).filter p = f.filter p + g.filter p

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (f + g)) i✝ = (filter p f + filter p g) i✝

Tactic:
simp [ite_add_zero]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
⊢ filter p (f + g) = filter p f + filter p g

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (f + g)) i✝ = (filter p f + filter p g) i✝
-- Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean
theorem Metric.exists_isLocalMin_mem_ball [TopologicalSpace β]
    [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a z : α} {r : ℝ}
    (hf : ContinuousOn f (closedBall a r)) (hz : z ∈ closedBall a r)
    (hf1 : ∀ z' ∈ sphere a r, f z < f z') : ∃ z ∈ ball a r, IsLocalMin f z

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ sphere a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Tactic:
simp_rw [← closedBall_diff_ball] at hf1

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Tactic:
exact (isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1
  isOpen_ball

Result:
no goals
-- Mathlib/CategoryTheory/Opposites.lean
theorem unop_op {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op = f

Tactic:
(ext; rfl)

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op = f

Tactic:
ext

Result:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom

Proof state:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_mul_le_right (f g : A) : basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 g

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 g

Tactic:
rw [basicOpen_mul 𝒜 f g]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g

Tactic:
exact inf_le_right

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Range/Lemmas.lean
theorem size_step_1 (start stop) : size ⟨start, stop, 1, by decide⟩ = stop - start

Proof state:
start stop : Nat
⊢ { start := start, stop := stop, step := 1, step_pos := ⋯ }.size = stop - start

Tactic:
simp [size]

Result:
no goals

Proof state:
start stop : Nat
⊢ 0 < 1

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ico : (some : α → WithTop α) ⁻¹' Ico a b = Ico a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem mul_add_left_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (x * z + y)

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)

Tactic:
exact h.add_mul_left_right z

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (x * z + y)

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_comp_add_right (a : E) :
    fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ fderiv 𝕜 (fun x => f (x + a)) x = fderiv 𝕜 f (x + a)

Tactic:
simp [← fderivWithin_univ, fderivWithin_comp_add_right]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem eq_reverse_iff [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b)
    (g : b ⟶ a) : f = reverse g ↔ reverse f = g

Proof state:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g

Tactic:
rw [← reverse_inj, reverse_reverse]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N]
    (g : F) (f : ι → M) (s : Finset ι) :
    g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i)

Proof state:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module ℚ≥0 M
inst✝³ : AddCommMonoid N
inst✝² : Module ℚ≥0 N
F : Type u_5
inst✝¹ : FunLike F M N
inst✝ : LinearMapClass F ℚ≥0 M N
g : F
f : ι → M
s : Finset ι
⊢ g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i)

Tactic:
simp only [expect, map_smul, map_natCast, map_sum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.getLeft? = none ↔ x.isRight = true

Tactic:
cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean
theorem convs_succ (n : ℕ) :
    (of v).convs (n + 1) = ⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n

Proof state:
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
⊢ (of v).convs (n + 1) = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n

Tactic:
rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
lemma toPartialHomeomorph_left_inv {x : X} : (h.toPartialHomeomorph f).symm (f x) = x

Proof state:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (f x) = x

Tactic:
rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.left_inv]

Result:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toPartialHomeomorph f h).source

Proof state:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toPartialHomeomorph f h).source

Tactic:
exact Set.mem_univ _

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma antitone_of_le_pred (hf : ∀ a, ¬ IsMin a → f a ≤ f (pred a)) : Antitone f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ Antitone f

Tactic:
simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a ≤ f (pred a)

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_one : toList (1 : Perm α) x = []

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ toList 1 x = []

Tactic:
simp [toList, cycleOf_one]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isCycle_of_prime_order {σ : Perm α} (h1 : (orderOf σ).Prime)
    (h2 : σ.support.card < 2 * orderOf σ) : σ.IsCycle

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
rw [← card_cycleType_eq_one, hn, card_replicate, h2]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : σ.support.card < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
  mul_lt_mul_right (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : n = 0
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : σ.support.card < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
obtain ⟨n, hn⟩ := cycleType_prime_order h1

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : σ.support.card < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle