harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_eq_of_subset_of_ae_diff_eq_zero (ht : NullMeasurableSet t μ) (hts : s ⊆ t)
    (h't : ∀ᵐ x ∂μ, x ∈ t \ s → f x = 0) : ∫ x in t, f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ f' =ᶠ[ae (μ.restrict s)] f

Tactic:
apply ae_restrict_of_ae_restrict_of_subset hts

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∀ᵐ (x : X) ∂μ.restrict t, f' x = f x

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by_cases h : IntegrableOn f t μ

Result:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t μ
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib/Data/List/Count.lean
theorem count_map_of_injective [DecidableEq β] (l : List α) (f : α → β)
    (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP (fun x_1 => (fun x_2 => x_2 == f x) (f x_1)) l = countP (fun x_1 => x_1 == x) l

Tactic:
simp only [hf.beq_eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP ((fun x_1 => x_1 == f x) ∘ f) l = countP (fun x_1 => x_1 == x) l

Tactic:
unfold Function.comp

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP (fun x_1 => (fun x_2 => x_2 == f x) (f x_1)) l = countP (fun x_1 => x_1 == x) l

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ count (f x) (map f l) = count x l

Tactic:
simp only [count, countP_map]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP ((fun x_1 => x_1 == f x) ∘ f) l = countP (fun x_1 => x_1 == x) l
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem isBigO_cocompact_zpow [ProperSpace E] (k : ℤ) :
    f =O[cocompact E] fun x => ‖x‖ ^ k

Proof state:
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
k : ℤ
⊢ ⇑f =O[cocompact E] fun x => ‖x‖ ^ k

Tactic:
simpa only [Real.rpow_intCast] using isBigO_cocompact_rpow f k

Result:
no goals
-- Mathlib/Logic/Godel/GodelBetaFunction.lean
private lemma pairwise_coprime_coprimes (a : Fin m → ℕ) : Pairwise (Coprime on coprimes a)

Proof state:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : ↑j < Nat.supOfSeq a
⊢ ↑j + 1 - (↑i + 1) ≤ Nat.supOfSeq a

Tactic:
simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)

Result:
no goals

Proof state:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : ↑j < Nat.supOfSeq a
⊢ ((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)

Tactic:
exact coprime_mul_succ
  (Nat.succ_le_succ <| le_of_lt ltij)
  (Nat.dvd_factorial (by omega)
    (by simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)))

Result:
no goals

Proof state:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : ↑j < Nat.supOfSeq a
⊢ 0 < ↑j + 1 - (↑i + 1)

Tactic:
omega

Result:
no goals

Proof state:
case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on Nat.coprimes a) i j
ltij : ¬i < j
⊢ (Coprime on Nat.coprimes a) i j

Tactic:
exact (this a hij.symm (lt_of_le_of_ne (Fin.not_lt.mp ltij) hij.symm)).symm

Result:
no goals

Proof state:
m : ℕ
a : Fin m → ℕ
⊢ Pairwise (Coprime on Nat.coprimes a)

Tactic:
intro i j hij

Result:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
⊢ (Coprime on Nat.coprimes a) i j

Proof state:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (Coprime on Nat.coprimes a) i j

Tactic:
unfold Function.onFun coprimes

Result:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ ((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)

Proof state:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
⊢ (Coprime on Nat.coprimes a) i j

Tactic:
wlog ltij : i < j

Result:
case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on Nat.coprimes a) i j
ltij : ¬i < j
⊢ (Coprime on Nat.coprimes a) i j

m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (Coprime on Nat.coprimes a) i j

Proof state:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ ((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)

Tactic:
have hja : j < supOfSeq a := lt_of_lt_of_le j.prop (le_step (le_max_left _ _))

Result:
m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : ↑j < Nat.supOfSeq a
⊢ ((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)
-- Mathlib/Algebra/CharP/Quotient.lean
theorem quotient_iff {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
    CharP (R ⧸ I) n ↔ ∀ x : ℕ, ↑x ∈ I → (x : R) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0

Tactic:
refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0

Tactic:
exact (Submodule.Quotient.mk_eq_zero I).mpr hx

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_one : iteratedDeriv 1 f = deriv f

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ iteratedDeriv 1 f = deriv f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 1 f x = deriv f x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 1 f x = deriv f x

Tactic:
simp [iteratedDeriv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isPath_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).IsPath ↔ p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsPath ↔ p.IsPath

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsPath ↔ p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsPath ↔ p.IsPath

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2

Proof state:
case e_a.e_a
x : Int
m : Nat
h : 0 < m
⊢ ↑m - -(1 - 2) = ↑m - 1

Tactic:
congr

Result:
no goals

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1 - 2) / 2 + 1 = (↑m - 1) / 2 + 1

Tactic:
congr 2

Result:
case e_a.e_a
x : Int
m : Nat
h : 0 < m
⊢ ↑m + 1 - 2 = ↑m - 1

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ 2 ∣ 2

Tactic:
trivial

Result:
no goals

Proof state:
case e_a.e_a
x : Int
m : Nat
h : 0 < m
⊢ ↑m + 1 - 2 = ↑m - 1

Tactic:
rw [Int.add_sub_assoc, ← Int.sub_neg]

Result:
case e_a.e_a
x : Int
m : Nat
h : 0 < m
⊢ ↑m - -(1 - 2) = ↑m - 1

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1 - 2 + 2) / 2 = (↑m - 1) / 2 + 1

Tactic:
rw [add_ediv_of_dvd_right]

Result:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1 - 2) / 2 + 2 / 2 = (↑m - 1) / 2 + 1

x : Int
m : Nat
h : 0 < m
⊢ 2 ∣ 2

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1) / 2 = (↑m + 1 - 2 + 2) / 2

Tactic:
simp

Result:
no goals

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1 - 2) / 2 + 2 / 2 = (↑m - 1) / 2 + 1

Tactic:
simp +decide only [Int.ediv_self]

Result:
x : Int
m : Nat
h : 0 < m
⊢ (↑m + 1 - 2) / 2 + 1 = (↑m - 1) / 2 + 1

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ x.bmod m ≤ (↑m - 1) / 2

Tactic:
refine lt_add_one_iff.mp ?_

Result:
x : Int
m : Nat
h : 0 < m
⊢ x.bmod m < (↑m - 1) / 2 + 1
-- Mathlib/Data/List/ProdSigma.lean
theorem length_sigma' (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    length (l₁.sigma l₂) = Nat.sum (l₁.map fun a ↦ length (l₂ a))

Proof state:
α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) l₁)

Tactic:
induction' l₁ with x l₁ IH

Result:
case nil
α : Type u_1
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) [])

case cons
α : Type u_1
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) l₁)
⊢ ((x :: l₁).sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) (x :: l₁))

Proof state:
case cons
α : Type u_1
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) l₁)
⊢ ((x :: l₁).sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) (x :: l₁))

Tactic:
simp only [map, sigma_cons, length_append, length_map, IH, Nat.sum_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = Nat.sum (map (fun a => (l₂ a).length) [])

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma X_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P x * Q z ^ 2 = Q x * P z ^ 2

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u x * Q z ^ 2 = Q x * (fun m => m • Q) u z ^ 2

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 2 * Q x * Q z ^ 2 = Q x * (↑u * Q z) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z ^ 2 = Q x * P z ^ 2

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u x * Q z ^ 2 = Q x * (fun m => m • Q) u z ^ 2

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 2 * Q x * Q z ^ 2 = Q x * (↑u * Q z) ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) :
    (x.sshiftRight' y)[i] =
      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

Proof state:
w : Nat
x y : BitVec w
i : Nat
h : i < w
⊢ (x.sshiftRight' y)[i] = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

Tactic:
simp only [← getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
    (modify f m l)[n]? = l[n]?

Proof state:
α : Type u_1
f : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ (modify f m l)[n]? = l[n]?

Tactic:
simp only [getElem?_modify, if_neg h, id_map']

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_of_degree_le_of_eval_finset_eq
    (h_deg_le : f.degree ≤ #s)
    (h_deg_eq : f.degree = g.degree)
    (hlc : f.leadingCoeff = g.leadingCoeff)
    (h_eval : ∀ x ∈ s, f.eval x = g.eval x) :
    f = g

Proof state:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : degree 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g

Tactic:
rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
hf : f ≠ 0
⊢ f = g

Tactic:
exact eq_of_degree_sub_lt_of_eval_finset_eq s
  (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le) h_eval

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
rcases eq_or_ne f 0 with rfl | hf

Result:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : degree 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
hf : f ≠ 0
⊢ f = g
-- Mathlib/Analysis/Convex/Gauge.lean
theorem Seminorm.gauge_ball (p : Seminorm ℝ E) : gauge (p.ball 0 1) = p

Proof state:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ (p x + ε)⁻¹ • x ∈ p.ball 0 1

Tactic:
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε),
  inv_mul_lt_iff₀ hpε, mul_one]

Result:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ p x < p x + ε

Proof state:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : p y < 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ p ((fun x => r • x) y) ≤ r

Tactic:
rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos hr]

Result:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : p y < 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ r * p y ≤ r
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem sin_eq_one_iff_angle_eq_pi_div_two : sin (angle x y) = 1 ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π / 2
⊢ sin (angle x y) = 1

Tactic:
rw [h, sin_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ √(1 - 1 ^ 2) = 0

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ angle x y = π / 2

Tactic:
rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ √(1 - 1 ^ 2) = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) = 1 ↔ angle x y = π / 2

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, sin_pi_div_two]⟩

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ angle x y = π / 2
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
lemma arctan_ne_mul_pi_div_two {x : ℝ} : ∀ (k : ℤ), arctan x ≠ (2 * k + 1) * π / 2

Proof state:
x : ℝ
⊢ ∀ (k : ℤ), arctan x ≠ (2 * ↑k + 1) * π / 2

Tactic:
by_contra!

Result:
x : ℝ
this : ∃ k, arctan x = (2 * ↑k + 1) * π / 2
⊢ False

Proof state:
x : ℝ
this : ∃ k, arctan x = (2 * ↑k + 1) * π / 2
⊢ False

Tactic:
obtain ⟨k, h⟩ := this

Result:
case intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
⊢ False

Proof state:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * (π / 2) < 1 * (π / 2)
⊢ 0 < π / 2

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * (π / 2)
ub : arctan x < π / 2
⊢ 0 < π / 2

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -(π / 2) < arctan x
ub : arctan x < π / 2
⊢ False

Tactic:
rw [h, neg_eq_neg_one_mul, mul_div_assoc, mul_lt_mul_right (by positivity)] at lb

Result:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : arctan x < π / 2
⊢ False

Proof state:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : 2 * ↑k + 1 < 1
⊢ False

Tactic:
norm_cast at lb ub

Result:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ False

Proof state:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : arctan x < π / 2
⊢ False

Tactic:
rw [h, ← one_mul (π / 2), mul_div_assoc, mul_lt_mul_right (by positivity)] at ub

Result:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : 2 * ↑k + 1 < 1
⊢ False

Proof state:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
ub : 2 * k + 1 < 1
lb : -1 < 2 * k + 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ False

Tactic:
change -1 < _ at lb

Result:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
ub : 2 * k + 1 < 1
lb : -1 < 2 * k + 1
⊢ False

Proof state:
case intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
⊢ False

Tactic:
obtain ⟨lb, ub⟩ := arctan_mem_Ioo x

Result:
case intro.intro
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -(π / 2) < arctan x
ub : arctan x < π / 2
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/BasicAux.lean
theorem List.size_toArrayAux (as : List α) (bs : Array α) : (as.toArrayAux bs).size = as.length + bs.size

Proof state:
α : Type u_1
as : List α
bs : Array α
⊢ (as.toArrayAux bs).size = as.length + bs.size

Tactic:
induction as generalizing bs with
| nil => simp [toArrayAux]
| cons a as ih => simp_arith [toArrayAux, *]

Result:
no goals

Proof state:
α : Type u_1
a : List α
b : Array α
⊢ (a.toArrayAux b).size = b.size + a.length

Tactic:
simp [size]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
as : List α
ih : ∀ (bs : Array α), (as.toArrayAux bs).size = as.length + bs.size
bs : Array α
⊢ ((a :: as).toArrayAux bs).size = (a :: as).length + bs.size

Tactic:
simp_arith [toArrayAux, *]

Result:
no goals

Proof state:
case nil
α : Type u_1
bs : Array α
⊢ ([].toArrayAux bs).size = [].length + bs.size

Tactic:
simp [toArrayAux]

Result:
no goals
-- Mathlib/LinearAlgebra/Contraction.lean
theorem rTensorHomEquivHomRTensor_apply (x : (M →ₗ[R] P) ⊗[R] Q) :
    rTensorHomEquivHomRTensor R M P Q x = rTensorHomToHomRTensor R M P Q x

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : (M →ₗ[R] P) ⊗[R] Q
⊢ (rTensorHomEquivHomRTensor R M P Q) x = (rTensorHomToHomRTensor R M P Q) x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma rightHomologyIso_hom_naturality :
    S₁.rightHomologyIso.hom ≫ homologyMap φ =
      rightHomologyMap φ ≫ S₂.rightHomologyIso.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.rightHomologyIso.hom ≫ homologyMap φ = rightHomologyMap φ ≫ S₂.rightHomologyIso.hom

Tactic:
simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using
  RightHomologyData.rightHomologyIso_inv_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
    have := mkGate_le_size aig input
    (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (aig.mkGate input).aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [mkGate, Array.getElem_push]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx]
    else Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) =
    aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
this : aig.decls.size ≤ (aig.mkGate input).aig.decls.size
⊢ idx < (aig.mkGate input).aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx]
    else Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) =
    aig.decls[idx]

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
rfl

Result:
no goals