harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
/-- If `z` is a non-real complex root of a real polynomial,
then `p` is divisible by a quadratic polynomial. -/
lemma Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero (p : ℝ[X]) {z : ℂ} (h0 : aeval z p = 0)
    (hz : z.im ≠ 0) : X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2) ∣ p

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2) ∣ p

Tactic:
rw [← map_dvd_map' (algebraMap ℝ ℂ)]

Result:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) ∣ map (algebraMap ℝ ℂ) p

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - C ↑(2 * z.re) * X + C (↑‖z‖ ^ 2) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
rw [← add_conj, map_add, ← mul_conj', map_mul]

Result:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - (C z + C ((starRingEnd ℂ) z)) * X + C z * C ((starRingEnd ℂ) z) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = X ^ 2 - C ↑(2 * z.re) * X + C (↑‖z‖ ^ 2)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
calc
  map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2))
  _ = X ^ 2 - C (↑(2 * z.re) : ℂ) * X + C (‖z‖ ^ 2 : ℂ) := by simp
  _ = (X - C (conj z)) * (X - C z) := by
    rw [← add_conj, map_add, ← mul_conj', map_mul]
    ring

Result:
no goals

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) ∣ map (algebraMap ℝ ℂ) p

Tactic:
convert p.mul_star_dvd_of_aeval_eq_zero_im_ne_zero h0 hz

Result:
case h.e'_3
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - (C z + C ((starRingEnd ℂ) z)) * X + C z * C ((starRingEnd ℂ) z) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ MonovaryOn (f ∘ σ) g s

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ ∑ i ∈ s, f i • g (σ⁻¹ i) = ∑ i ∈ s, f i • g i

Tactic:
apply eq_iff_eq_cancel_right.2

Result:
case refine_1.a
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ MonovaryOn (f ∘ ⇑σ) g ↑s

Tactic:
convert h.comp_right σ

Result:
case h.e'_7
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ g = (g ∘ ⇑σ⁻¹) ∘ ⇑σ

case h.e'_8
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ ↑s = ⇑σ ⁻¹' ↑s
-- Mathlib/Data/Finset/Basic.lean
theorem filter_eq' [DecidableEq β] (s : Finset β) (b : β) :
    (s.filter fun a => a = b) = ite (b ∈ s) {b} ∅ :=
  _root_.trans (filter_congr fun _ _ => by simp_rw [@eq_comm _ b]) (filter_eq s b)

Proof state:
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ = b ↔ b = x✝¹

Tactic:
simp_rw [@eq_comm _ b]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sq : cosh x ^ 2 = sinh x ^ 2 + 1

Proof state:
x : ℝ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)

Proof state:
x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)

Tactic:
simp [cosh_sq]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem tendsto_pure_self (l : Filter X) :
    Tendsto (pure : X → Filter X) l (𝓝 l)

Proof state:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a

Tactic:
exact fun s hs ↦ Eventually.mono hs fun x ↦ id

Result:
no goals

Proof state:
X : Type u_4
l : Filter X
⊢ Tendsto pure l (𝓝 l)

Tactic:
rw [Filter.tendsto_nhds]

Result:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- Reformulation of `ZetaAsymptotics.term_tsum_of_lt` which is useful for some computations
below. -/
lemma zeta_limit_aux1 {s : ℝ} (hs : 1 < s) :
    (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1) = 1 - s * term_tsum s

Proof state:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * term_tsum s

Tactic:
rw [term_tsum_of_lt hs]

Result:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Proof state:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Tactic:
generalize (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) = Z

Result:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ Z - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * Z)

Proof state:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ Z - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * Z)

Tactic:
field_simp [(show s - 1 ≠ 0 by linarith)]

Result:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ (Z * (s - 1) - 1) * ((s - 1) * s) = ((s - 1) * s - s * (s - (s - 1) * Z)) * (s - 1)

Proof state:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ (Z * (s - 1) - 1) * ((s - 1) * s) = ((s - 1) * s - s * (s - (s - 1) * Z)) * (s - 1)

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ s - 1 ≠ 0

Tactic:
linarith

Result:
no goals
-- Mathlib/NumberTheory/Wilson.lean
theorem prime_of_fac_equiv_neg_one (h : ((n - 1)! : ZMod n) = -1) (h1 : n ≠ 1) : Prime n

Proof state:
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
⊢ Prime n

Tactic:
rcases eq_or_ne n 0 with (rfl | h0)

Result:
case inl
h : ↑(0 - 1)! = -1
h1 : 0 ≠ 1
⊢ Prime 0

case inr
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
h0 : n ≠ 0
⊢ Prime n

Proof state:
case inl
h : ↑(0 - 1)! = -1
h1 : 0 ≠ 1
⊢ Prime 0

Tactic:
norm_num at h

Result:
no goals

Proof state:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ n ∣ (n - 1)! + 1

Tactic:
rw [← ZMod.natCast_zmod_eq_zero_iff_dvd, cast_add, cast_one, h, neg_add_cancel]

Result:
no goals

Proof state:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n

Tactic:
by_contra h2

Result:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False

Proof state:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False

Tactic:
refine hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans ?_)))

Result:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ n ∣ (n - 1)! + 1

Proof state:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False

Tactic:
obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2

Result:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False

Proof state:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
h0 : n ≠ 0
⊢ Prime n

Tactic:
replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩

Result:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n

Proof state:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False

Tactic:
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)

Result:
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem le_iff' : v ≤ w ↔ ∀ i, v i ≤ w i

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), ↑v i ≤ ↑w i

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

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ ↑v i ≤ ↑w i

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ ↑v i ≤ ↑w i

Tactic:
exact h i hi

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ ↑v i ≤ ↑w i

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ ↑v i ≤ ↑w i

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i ≤ ↑w i

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i ≤ ↑w i

Tactic:
rw [v.not_measurable hi, w.not_measurable hi]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem isSymmetric_iff_inner_map_self_real (T : V →ₗ[ℂ] V) :
    IsSymmetric T ↔ ∀ v : V, conj ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ

Tactic:
rw [← inner_conj_symm x (T y)]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = (starRingEnd ℂ) ⟪T y, x⟫_ℂ

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ) → T.IsSymmetric

Tactic:
intro h x y

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ (⟪T x + T y, x + y⟫_ℂ - ⟪T x - T y, x - y⟫_ℂ - Complex.I * ⟪T x + Complex.I • T y, x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T x - Complex.I • T y, x - Complex.I • y⟫_ℂ) /
      4 =
    (⟪T x + T y, x + y⟫_ℂ - ⟪T x - T y, x - y⟫_ℂ + -(⟪T x + Complex.I • T y, x + Complex.I • y⟫_ℂ * Complex.I) +
        ⟪T x - Complex.I • T y, x - Complex.I • y⟫_ℂ * Complex.I) /
      4

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem dvd_ordCompl_of_dvd_not_dvd {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) :
    d ∣ ordCompl[p] n

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d.factorization ≤ Finsupp.erase p n.factorization

Tactic:
intro q

Result:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]

Result:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d.factorization ≤ Finsupp.erase p n.factorization

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : ¬q = p
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Tactic:
simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
simp [hn0]

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
simp [hd0] at hpd

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / p ^ n.factorization p

Tactic:
if hn0 : n = 0 then simp [hn0] else
if hd0 : d = 0 then simp [hd0] at hpd else
rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
intro q
if hqp : q = p then
  simp [factorization_eq_zero_iff, hqp, hpd]
else
  simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : q = p
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Tactic:
simp [factorization_eq_zero_iff, hqp, hpd]

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
if hd0 : d = 0 then simp [hd0] at hpd else
rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
intro q
if hqp : q = p then
  simp [factorization_eq_zero_iff, hqp, hpd]
else
  simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Result:
no goals

Proof state:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Tactic:
if hqp : q = p then
  simp [factorization_eq_zero_iff, hqp, hpd]
else
  simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem dist_algebraMap (x y : 𝕜) :
    (dist (algebraMap 𝕜 𝕜' x) (algebraMap 𝕜 𝕜' y)) = dist x y * ‖(1 : 𝕜')‖

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y * ‖1‖

Tactic:
simp only [dist_eq_norm, ← map_sub, norm_algebraMap]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean
lemma epi_of_surjective (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective (f.app X)) : Epi f where
  left_cancellation g₁ g₂ hg

Proof state:
case h.hf.h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) ((ConcreteCategory.hom (f.app X)) m₁) =
    (ModuleCat.Hom.hom (g₂.app X)) ((ConcreteCategory.hom (f.app X)) m₁)

Tactic:
exact congr_fun ((evaluation R X ⋙ forget _).congr_map hg) m₁

Result:
no goals

Proof state:
case h.hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₂ : ↑(M₂.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m₂ = (ModuleCat.Hom.hom (g₂.app X)) m₂

Tactic:
obtain ⟨m₁, rfl⟩ := hf m₂

Result:
case h.hf.h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) ((ConcreteCategory.hom (f.app X)) m₁) =
    (ModuleCat.Hom.hom (g₂.app X)) ((ConcreteCategory.hom (f.app X)) m₁)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ = g₂

Tactic:
ext X m₂

Result:
case h.hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₂ : ↑(M₂.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m₂ = (ModuleCat.Hom.hom (g₂.app X)) m₂
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem riemannZeta_neg_nat_eq_bernoulli' (k : ℕ) :
    riemannZeta (-k) = -bernoulli' (k + 1) / (k + 1)

Proof state:
case inl

⊢ riemannZeta (-↑0) = -↑(bernoulli' (0 + 1)) / (↑0 + 1)

Tactic:
rw [Nat.cast_zero, neg_zero, riemannZeta_zero, zero_add, zero_add, div_one,
  bernoulli'_one, Rat.cast_div, Rat.cast_one, Rat.cast_ofNat, neg_div]

Result:
no goals

Proof state:
case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
  (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
  Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
  div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]

Result:
no goals

Proof state:
k : ℕ
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
rcases eq_or_ne k 0 with rfl | hk

Result:
case inl

⊢ riemannZeta (-↑0) = -↑(bernoulli' (0 + 1)) / (↑0 + 1)

case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Proof state:
k : ℕ
hk : k ≠ 0
⊢ k + 1 ≠ 1

Tactic:
simp [hk]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ite_inter_closure_eq_of_inter_frontier_eq
    (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure t = s ∩ closure t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure t = s ∩ closure t

Tactic:
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
  ite_inter_self, ite_inter_of_inter_eq _ ht]

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem insertNone_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    insertNone (eraseNone s) = insert none s

Proof state:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ insertNone (eraseNone s) = insert none s

Tactic:
ext (_ | x) <;> simp

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_bisim {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ}
    {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂}
    (R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂)
    (hR :  ∀ {s q} a b, R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) :
    R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1
    ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).1 (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).1 ∧
    (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).2 = (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2

Tactic:
rcases (hR x y h₀) with ⟨hR, _⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).1 (f₂ x y s₂).1
right✝ : (f₁ x y s₁).2 = (f₂ x y s₂).2
⊢ R (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).1 (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).1 ∧
    (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).2 = (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2
-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem basicOpen_mul {U : Opens X} (f g : X.presheaf.obj (op U)) :
    X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Proof state:
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

Tactic:
by_cases hx : x ∈ U

Result:
case pos
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

case neg
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∉ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

Proof state:
case pos
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

Tactic:
simp [mem_basicOpen (hx := hx)]

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Tactic:
ext x

Result:
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)
-- Mathlib/Data/List/Defs.lean
theorem iterateTR_loop_eq (f : α → α) (a : α) (n : ℕ) (l : List α) :
    iterateTR.loop f a n l = reverse l ++ iterate f a n

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
induction n generalizing a l <;> simp [*]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Dep.dep_isRestriction (hX : M.Dep X) (hNM : N ≤r M) (hXE : X ⊆ N.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : M.Dep X
hNM : N ≤r M
hXE : autoParam (X ⊆ N.E) _auto✝
⊢ N.Dep X

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : autoParam (X ⊆ (M ↾ R).E) _auto✝
⊢ (M ↾ R).Dep X

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : autoParam (X ⊆ (M ↾ R).E) _auto✝
⊢ (M ↾ R).Dep X

Tactic:
simpa [hX.not_indep]

Result:
no goals