harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem addHaar_image_eq_zero_of_det_fderivWithin_eq_zero
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (h'f' : ∀ x ∈ s, (f' x).det = 0) :
    μ (f '' s) = 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)
this : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝 0) (𝓝 (↑0 * μ (closedBall 0 R)))
⊢ Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)

Tactic:
simp only [zero_mul, ENNReal.coe_zero] at this

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ↑ε * μ (closedBall 0 R)
this : Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝 0) (𝓝 0)
⊢ Tendsto (fun ε => ↑ε * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0)
-- Mathlib/Order/GameAdd.lean
theorem Acc.sym2_gameAdd {a b} (ha : Acc rα a) (hb : Acc rα b) :
    Acc (Sym2.GameAdd rα) s(a, b)

Proof state:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
refine Acc.intro _ fun s => ?_

Result:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
s : Sym2 α
⊢ Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s

Proof state:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
s : Sym2 α
⊢ Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s

Tactic:
induction' s with c d

Result:
case intro.intro.h
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ Sym2.GameAdd rα s(c, d) s(a, b) → Acc (Sym2.GameAdd rα) s(c, d)

Proof state:
case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(d, b)

Tactic:
exact iha d rd ⟨b, hb⟩

Result:
no goals

Proof state:
case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(b, d)

Tactic:
rw [Sym2.eq_swap]

Result:
case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(d, b)
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_eq_zero_of_pos_iff (hp : 0 < p) {x : 𝕜} (hx : 0 < x) :
    (x : AddCircle p) = 0 ↔ ∃ n : ℕ, n • p = x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ n.toNat • p = n • p

Tactic:
rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x

Tactic:
constructor <;> rintro ⟨n, rfl⟩

Result:
case mp.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p

case mpr.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n

Tactic:
contrapose! hx

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0

Proof state:
case mp.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p

Tactic:
replace hx : 0 < n := by
  contrapose! hx
  simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)

Result:
case mp.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ n_1, n_1 • p = n • p

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ↑n • p = n • p

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ ↑x = 0 ↔ ∃ n, n • p = x

Tactic:
rw [coe_eq_zero_iff]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x

Proof state:
case mpr.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p

Tactic:
exact ⟨(n : ℤ), by simp⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0

Tactic:
simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)

Result:
no goals

Proof state:
case mp.intro
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ n_1, n_1 • p = n • p

Tactic:
exact ⟨n.toNat, by rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l)[0]? = some a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
    [NormedSpace ℝ E] [OpensMeasurableSpace X] [T2Space X]
    (hf : LocallyIntegrable f μ) {g : X → ℝ} (hg : Continuous g) (h'g : HasCompactSupport g) :
    Integrable (fun x ↦ g x • f x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
hf : LocallyIntegrable f μ
g : X → ℝ
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ ∀ x ∉ K, g x • f x = 0

Tactic:
intros x hx

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
hf : LocallyIntegrable f μ
g : X → ℝ
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ g x • f x = 0

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
hf : LocallyIntegrable f μ
g : X → ℝ
hg : Continuous g
h'g : HasCompactSupport g
⊢ Integrable (fun x => g x • f x) μ

Tactic:
let K := tsupport g

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
hf : LocallyIntegrable f μ
g : X → ℝ
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ Integrable (fun x => g x • f x) μ

Proof state:
case hφ
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
hf : LocallyIntegrable f μ
g : X → ℝ
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => g x • f x) = fun x => g x • f x
⊢ MemLp g ⊤ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_neg (M : Matrix m n α) (N : Matrix n o α) : M * (-N) = -(M * N)

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (M * -N) i✝ j✝ = (-(M * N)) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (M * -N) i✝ j✝ = (-(M * N)) i✝ j✝

Tactic:
apply dotProduct_neg

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (hy : y ≠ 1) :
    x * y = p ^ 2 ↔ x = p ∧ y = p

Proof state:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
  [skip; rw [And.comm]] <;>
  [skip; rw [mul_comm] at h pdvdxy] <;>
  apply this <;>
  assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_three : cos (π / 3) = 1 / 2

Proof state:
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)

Tactic:
refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]

Result:
no goals

Proof state:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
have : cos π < cos (π / 3) := by
  refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]

Result:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2

Proof state:
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0

Tactic:
have : cos (3 * (π / 3)) = cos π := by
  congr 1
  ring

Result:
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0

Proof state:
case inl
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
linarith [pow_eq_zero h]

Result:
no goals

Proof state:
case e_x

⊢ 3 * (π / 3) = π

Tactic:
ring

Result:
no goals

Proof state:
⊢ cos (3 * (π / 3)) = cos π

Tactic:
congr 1

Result:
case e_x

⊢ 3 * (π / 3) = π

Proof state:
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
rcases mul_eq_zero.mp h₁ with h | h

Result:
case inl
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2

case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Proof state:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2

Tactic:
linarith [cos_pi]

Result:
no goals

Proof state:
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0

Tactic:
linarith [cos_pi, cos_three_mul (π / 3)]

Result:
no goals

Proof state:
⊢ cos (π / 3) = 1 / 2

Tactic:
have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 := by
  have : cos (3 * (π / 3)) = cos π := by
    congr 1
    ring
  linarith [cos_pi, cos_three_mul (π / 3)]

Result:
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomorph M H}
    (he : e ∈ G.maximalAtlas M) (he' : e' ∈ G.maximalAtlas M) : e.symm ≫ₕ e' ∈ G

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : PartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : PartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ e.symm.restr (e.symm.source ∩ ↑e.symm ⁻¹' f.source) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'

Tactic:
apply refl

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem tail_think (s : Computation α) : tail (think s) = s

Proof state:
case mk.a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(think ⟨f, al⟩).tail = ↑⟨f, al⟩

Tactic:
dsimp [tail, think]

Result:
no goals

Proof state:
α : Type u
s : Computation α
⊢ s.think.tail = s

Tactic:
obtain ⟨f, al⟩ := s

Result:
case mk
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (think ⟨f, al⟩).tail = ⟨f, al⟩

Proof state:
case mk
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (think ⟨f, al⟩).tail = ⟨f, al⟩

Tactic:
apply Subtype.eq

Result:
case mk.a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(think ⟨f, al⟩).tail = ↑⟨f, al⟩
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map
    (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x) (Measure.map X μ)

Tactic:
rw [← Measure.fst_map_prod_mk₀ hY, condDistrib]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a => (X a, Y a)) μ).fst

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a => (X a, Y a)) μ).fst

Tactic:
exact hf.integral_condKernel

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_min (a b : Nat) : ((min a b : Nat) : Int) = min (a : Int) (b : Int)

Proof state:
a b : Nat
⊢ ↑(min a b) = min ↑a ↑b

Tactic:
simp only [Nat.min_def, Int.min_def, Int.ofNat_le]

Result:
a b : Nat
⊢ ↑(if a ≤ b then a else b) = if a ≤ b then ↑a else ↑b

Proof state:
a b : Nat
⊢ ↑(if a ≤ b then a else b) = if a ≤ b then ↑a else ↑b

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverseAux_eq_reverse_append {u v w : V} (p : G.Walk u v) (q : G.Walk u w) :
    p.reverseAux q = p.reverse.append q

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk u w
⊢ p.reverseAux q = p.reverse.append q

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem dvd_ofDigits_sub_ofDigits {α : Type*} [CommRing α] {a b k : α} (h : k ∣ a - b)
    (L : List ℕ) : k ∣ ofDigits a L - ofDigits b L

Proof state:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []

Tactic:
change k ∣ 0 - 0

Result:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0

Proof state:
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
⊢ k ∣ ofDigits a L - ofDigits b L

Tactic:
induction' L with d L ih

Result:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []

case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)

Proof state:
case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ a * ofDigits a L - b * ofDigits b L

Tactic:
exact dvd_mul_sub_mul h ih

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)

Tactic:
simp only [ofDigits, add_sub_add_left_eq_sub]

Result:
case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ a * ofDigits a L - b * ofDigits b L

Proof state:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_eval_one : p.mirror.eval 1 = p.eval 1

Proof state:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ a,
    ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
      (revAt (p.natDegree + p.natTrailingDegree)) a = n

Tactic:
use revAt (p.natDegree + p.natTrailingDegree) n

Result:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ (_ : (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)) (_ :
    p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree)) ((revAt (p.natDegree + p.natTrailingDegree)) n) = n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n₁ : ℕ
x✝⁴ : n₁ ∈ Finset.range (p.natDegree + 1)
x✝³ : p.mirror.coeff n₁ ≠ 0
x✝² : ℕ
x✝¹ : x✝² ∈ Finset.range (p.natDegree + 1)
x✝ : p.mirror.coeff x✝² ≠ 0
h : (revAt (p.natDegree + p.natTrailingDegree)) n₁ = (revAt (p.natDegree + p.natTrailingDegree)) x✝²
⊢ n₁ = x✝²

Tactic:
rw [← @revAt_invol _ n₁, h, revAt_invol]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma IsUniformInducing.uniformGroup {γ : Type*} [Group γ] [UniformSpace γ] [UniformGroup γ]
    [UniformSpace β] {F : Type*} [FunLike F β γ] [MonoidHomClass F β γ]
    (f : F) (hf : IsUniformInducing f) :
    UniformGroup β where
  uniformContinuous_div

Proof state:
β : Type u_2
inst✝⁶ : Group β
γ : Type u_3
inst✝⁵ : Group γ
inst✝⁴ : UniformSpace γ
inst✝³ : UniformGroup γ
inst✝² : UniformSpace β
F : Type u_4
inst✝¹ : FunLike F β γ
inst✝ : MonoidHomClass F β γ
f : F
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun p => p.1 / p.2

Tactic:
simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]

Result:
β : Type u_2
inst✝⁶ : Group β
γ : Type u_3
inst✝⁵ : Group γ
inst✝⁴ : UniformSpace γ
inst✝³ : UniformGroup γ
inst✝² : UniformSpace β
F : Type u_4
inst✝¹ : FunLike F β γ
inst✝ : MonoidHomClass F β γ
f : F
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun x => f x.1 / f x.2

Proof state:
β : Type u_2
inst✝⁶ : Group β
γ : Type u_3
inst✝⁵ : Group γ
inst✝⁴ : UniformSpace γ
inst✝³ : UniformGroup γ
inst✝² : UniformSpace β
F : Type u_4
inst✝¹ : FunLike F β γ
inst✝ : MonoidHomClass F β γ
f : F
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun x => f x.1 / f x.2

Tactic:
exact uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem coeff_mul_one_sub_of_lt_order {R : Type*} [CommRing R] {φ ψ : R⟦X⟧} (n : ℕ)
    (h : ↑n < ψ.order) : coeff R n (φ * (1 - ψ)) = coeff R n φ

Proof state:
R : Type u_2
inst✝ : CommRing R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff R n) (φ * (1 - ψ)) = (coeff R n) φ

Tactic:
simp [coeff_mul_of_lt_order h, mul_sub]

Result:
no goals
-- Mathlib/Data/List/InsertIdx.lean
theorem insertIdx_injective (n : ℕ) (x : α) : Function.Injective (insertIdx n x)

Proof state:
case zero
α : Type u
x : α
⊢ Injective (insertIdx 0 x)

Tactic:
have : insertIdx 0 x = cons x := funext fun _ => rfl

Result:
case zero
α : Type u
x : α
this : insertIdx 0 x = cons x
⊢ Injective (insertIdx 0 x)

Proof state:
α : Type u
n : ℕ
x : α
⊢ Injective (insertIdx n x)

Tactic:
induction' n with n IH

Result:
case zero
α : Type u
x : α
⊢ Injective (insertIdx 0 x)

case succ
α : Type u
x : α
n : ℕ
IH : Injective (insertIdx n x)
⊢ Injective (insertIdx (n + 1) x)

Proof state:
case zero
α : Type u
x : α
this : insertIdx 0 x = cons x
⊢ Injective (insertIdx 0 x)

Tactic:
simp [this]

Result:
no goals

Proof state:
case succ
α : Type u
x : α
n : ℕ
IH : Injective (insertIdx n x)
⊢ Injective (insertIdx (n + 1) x)

Tactic:
rintro (_ | ⟨a, as⟩) (_ | ⟨b, bs⟩) h <;> simpa [IH.eq_iff] using h

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem bottom_row_coprime {R : Type*} [CommRing R] (g : SL(2, R)) :
    IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ (↑g).det = 1

Tactic:
exact g.det_coe

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ IsCoprime (↑g 1 0) (↑g 1 1)

Tactic:
use -(↑g : Matrix (Fin 2) (Fin 2) R) 0 1, (↑g : Matrix (Fin 2) (Fin 2) R) 0 0

Result:
case h
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ -↑g 0 1 * ↑g 1 0 + ↑g 0 0 * ↑g 1 1 = 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ -↑g 0 1 * ↑g 1 0 + ↑g 0 0 * ↑g 1 1 = 1

Tactic:
rw [add_comm, neg_mul, ← sub_eq_add_neg, ← det_fin_two]

Result:
case h
R : Type u_1
inst✝ : CommRing R
g : SL(2, R)
⊢ (↑g).det = 1