harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
    dropInfix?.go i l acc = some (p, s) ↔ ∃ p',
      p = acc.reverse ++ p' ∧
      -- `i` is an infix up to `==`
      (∃ i', l = p' ++ i' ++ s ∧ i' == i) ∧
        -- and there is no shorter prefix for which that is the case
        (∀ p'' i'' s'', l = p'' ++ i'' ++ s'' → i'' == i → p''.length ≥ p'.length)

Proof state:
case h_2.h_1.mpr.intro.intro.intro.intro.intro.inr.intro.intro.inl.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
a' : List α
h : (a :: (a' ++ s)).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), a :: (a' ++ s) = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ [].length
h₂ : (a :: a' == i) = true
⊢ ∃ p',
    acc.reverse ++ [] = (a :: acc).reverse ++ p' ∧
      (∃ i', a' ++ s = p' ++ i' ++ s ∧ (i' == i) = true) ∧
        ∀ (p'' i'' s'' : List α), a' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Tactic:
rw [← cons_append] at h

Result:
case h_2.h_1.mpr.intro.intro.intro.intro.intro.inr.intro.intro.inl.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
a' : List α
h : (a :: a' ++ s).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), a :: (a' ++ s) = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ [].length
h₂ : (a :: a' == i) = true
⊢ ∃ p',
    acc.reverse ++ [] = (a :: acc).reverse ++ p' ∧
      (∃ i', a' ++ s = p' ++ i' ++ s ∧ (i' == i) = true) ∧
        ∀ (p'' i'' s'' : List α), a' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
-- Mathlib/Algebra/Star/Center.lean
theorem Set.star_mem_centralizer' (h : ∀ a : R, a ∈ s → star a ∈ s) (ha : a ∈ Set.centralizer s) :
    star a ∈ Set.centralizer s := fun y hy => by simpa using congr_arg star (ha _ (h _ hy)).symm

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y

Tactic:
simpa using congr_arg star (ha _ (h _ hy)).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insert [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] {v : β k} :
    (m.insert k v).get! a = if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a

Tactic:
simp_to_raw using Raw₀.get!_insert

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Colorable.chromaticNumber_le {n : ℕ} (hc : G.Colorable n) : G.chromaticNumber ≤ n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ sInf {n' | G.Colorable n'} ≤ n

Tactic:
apply csInf_le chromaticNumber_bddBelow

Result:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ∈ {n | G.Colorable n}

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ G.chromaticNumber ≤ ↑n

Tactic:
rw [hc.chromaticNumber_eq_sInf]

Result:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n

Tactic:
norm_cast

Result:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ sInf {n' | G.Colorable n'} ≤ n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ∈ {n | G.Colorable n}

Tactic:
exact hc

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem iter_deriv_zpow' (m : ℤ) (k : ℕ) :
    (deriv^[k] fun x : 𝕜 => x ^ m) =
      fun x => (∏ i ∈ Finset.range k, ((m : 𝕜) - i)) * x ^ (m - k)

Proof state:
case succ
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
ihk : (deriv^[k] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
⊢ (deriv^[k + 1] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range (k + 1), (↑m - ↑i)) * x ^ (m - ↑(k + 1))

Tactic:
simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
  Finset.prod_range_succ, Int.ofNat_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast, mul_assoc]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
⊢ (deriv^[k] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)

Tactic:
induction' k with k ihk

Result:
case zero
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
⊢ (deriv^[0] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range 0, (↑m - ↑i)) * x ^ (m - ↑0)

case succ
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
ihk : (deriv^[k] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
⊢ (deriv^[k + 1] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range (k + 1), (↑m - ↑i)) * x ^ (m - ↑(k + 1))

Proof state:
case zero
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
⊢ (deriv^[0] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range 0, (↑m - ↑i)) * x ^ (m - ↑0)

Tactic:
simp only [one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero,
  Function.iterate_zero]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem countable_not_continuousWithinAt_Ioi [SecondCountableTopology β] :
    Set.Countable { x | ¬ContinuousWithinAt f (Ioi x) x }

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u

Tactic:
have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsGT xv

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[>] x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem div_C_mul : p / (C a * q) = C a⁻¹ * (p / q)

Proof state:
case neg.e_a.e_a.e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹)) = q * C q.leadingCoeff⁻¹

Tactic:
rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]

Result:
no goals

Proof state:
case pos
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a = 0
⊢ p / (C a * q) = C a⁻¹ * (p / q)

Tactic:
simp [ha]

Result:
no goals

Proof state:
case neg
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ p / (C a * q) = C a⁻¹ * (p / q)

Tactic:
simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]

Result:
case neg
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹))))) =
    C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)))

Proof state:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
⊢ p / (C a * q) = C a⁻¹ * (p / q)

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a = 0
⊢ p / (C a * q) = C a⁻¹ * (p / q)

case neg
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ p / (C a * q) = C a⁻¹ * (p / q)

Proof state:
case neg
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹))))) =
    C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)))

Tactic:
congr 3

Result:
case neg.e_a.e_a.e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹)) = q * C q.leadingCoeff⁻¹
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal}
    (h : brange o f ⊆ brange o' g) : blsub.{u, max v w} o f ≤ blsub.{v, max u w} o' g :=
  bsup_le_of_brange_subset.{u, v, w} fun a ⟨b, hb, hb'⟩ => by
    obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩
    simp_rw [← hc'] at hb'
    exact ⟨c, hc, hb'⟩

Proof state:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha => succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
⊢ a ∈ o'.brange fun a ha => succ (g a ha)

Tactic:
obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩

Result:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha => succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha => succ (g a ha)

Proof state:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha => succ (f a ha)
b : Ordinal.{u}
hb : b < o
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ o'.brange fun a ha => succ (g a ha)

Tactic:
exact ⟨c, hc, hb'⟩

Result:
no goals

Proof state:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha => succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha => succ (g a ha)

Tactic:
simp_rw [← hc'] at hb'

Result:
case intro.intro
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha => succ (f a ha)
b : Ordinal.{u}
hb : b < o
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ o'.brange fun a ha => succ (g a ha)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
  extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo)

Proof state:
case pred
x n hi lo i : Nat
a✝ : i < hi - lo + 1
⊢ (extractLsb hi lo (BitVec.ofNat n x)).getLsbD i = (BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)).getLsbD i

Tactic:
simp [BitVec.ofNat]

Result:
no goals

Proof state:
x n hi lo : Nat
⊢ extractLsb hi lo (BitVec.ofNat n x) = BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)

Tactic:
ext i

Result:
case pred
x n hi lo i : Nat
a✝ : i < hi - lo + 1
⊢ (extractLsb hi lo (BitVec.ofNat n x)).getLsbD i = (BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)).getLsbD i
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem _root_.tendsto_tsum_div_pow_atTop_integral (hF : Continuous F) (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
    Tendsto (fun n : ℕ ↦ (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι)
      atTop (nhds (∫ x in s, F x))

Proof state:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
hs : x ∈ s
⊢ ‖F x‖ ≤ 0 ⊔ C₀

Tactic:
exact le_max_of_le_right (h₀ x hx)

Result:
no goals
-- Mathlib/Data/Rat/Star.lean
@[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) :
    closure (range fun x : ℚ≥0 ↦ x ^ n) = ⊤

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x ∈ closure (range fun x => x ^ n)

Tactic:
suffices x = (x.num * x.den ^ (n - 1)) • (x.den : ℚ≥0)⁻¹ ^ n by
  rw [this]
  exact nsmul_mem (subset_closure <| mem_range_self _) _

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑(x.num * x.den ^ (n - 1)) * (↑x.den)⁻¹ ^ n

Tactic:
push_cast

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * ↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n

Proof state:
n : ℕ
hn₀ : n ≠ 0
⊢ closure (range fun x => x ^ n) = ⊤

Tactic:
refine (eq_top_iff' _).2 fun x ↦ ?_

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x ∈ closure (range fun x => x ^ n)

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * ↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n

Tactic:
rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul,
  ← div_eq_mul_inv, num_div_den]

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
⊢ (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n ∈ closure (range fun x => x ^ n)

Tactic:
exact nsmul_mem (subset_closure <| mem_range_self _) _

Result:
no goals

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
all_goals simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]

Result:
no goals

Proof state:
case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]

Result:
no goals

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n

Tactic:
rw [nsmul_eq_mul]

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑(x.num * x.den ^ (n - 1)) * (↑x.den)⁻¹ ^ n

Proof state:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
⊢ x ∈ closure (range fun x => x ^ n)

Tactic:
rw [this]

Result:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
⊢ (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n ∈ closure (range fun x => x ^ n)
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_def {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1

Tactic:
apply Or.imp_right _ (h.2 a _)

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1

p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp only [Nat.isUnit_iff]

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1

Proof state:
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1

Tactic:
rw [← mul_right_inj' (not_eq_zero_of_lt h1), ← hab, mul_one]

Result:
no goals

Proof state:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

Tactic:
refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p

Tactic:
have h1 := Nat.one_lt_two.trans_le h.1

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p

Tactic:
refine ⟨mt Nat.isUnit_iff.mp h1.ne', fun a b hab => ?_⟩

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p

Tactic:
rw [hab]

Result:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b

Proof state:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1

Tactic:
rintro rfl

Result:
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The two-variable Jacobi theta function is quasi-periodic in `z` with period `τ`. -/
lemma jacobiTheta₂_add_left' (z τ : ℂ) :
    jacobiTheta₂ (z + τ) τ = cexp (-π * I * (τ + 2 * z)) * jacobiTheta₂ z τ

Proof state:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z) + (2 * ↑π * I * (↑n + ↑1) * z + ↑π * I * (↑n + ↑1) ^ 2 * τ))

Tactic:
ring_nf

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) n) z τ

Tactic:
simp_rw [jacobiTheta₂_term, ← Complex.exp_add, Equiv.coe_addRight, Int.cast_add]

Result:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z) + (2 * ↑π * I * (↑n + ↑1) * z + ↑π * I * (↑n + ↑1) ^ 2 * τ))

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂ z τ

Tactic:
conv_rhs => erw [← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]

Result:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = ∑' (c : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) c) z τ

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = ∑' (c : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) c) z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Result:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) n) z τ
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotQuotEquivQuotOfLE_comp_quotQuotMk (h : I ≤ J) :
    RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = (Ideal.Quotient.mk J)

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J) = Ideal.Quotient.mk J

Tactic:
ext

Result:
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J)) x✝ = (Ideal.Quotient.mk J) x✝

Proof state:
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J)) x✝ = (Ideal.Quotient.mk J) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem _root_.IsPrimePow.deficient (h : IsPrimePow n) : Deficient n

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient

Tactic:
exact hp.nat_prime.deficient_pow

Result:
no goals

Proof state:
n : ℕ
h : IsPrimePow n
⊢ n.Deficient

Tactic:
obtain ⟨p, k, hp, -, rfl⟩ := h

Result:
case intro.intro.intro.intro
p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_union (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f)
    (hst : Disjoint s t) : ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Tactic:
let e := MeasurableEquiv.piFinsetUnion π hst

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Proof state:
case hf.h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ Measurable fun z => f (updateFinset x (s ∪ t) ((MeasurableEquiv.piFinsetUnion π hst) z))

Tactic:
exact hf.comp <| measurable_updateFinset.comp e.measurable

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sigma_isBasis_iff {I X} :
    (Matroid.sigma M).IsBasis I X ↔ ∀ i, (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

Proof state:
case refine_4
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
⊢ ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t

Tactic:
refine fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i,x⟩ hx ↦ ?_

Result:
case refine_4
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝¹ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
J : Set ((i : ι) × α i)
hJ : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
hJX : J ⊆ X
hIJ : I ⊆ J
x✝ : (i : ι) × α i
i : ι
x : α i
hx : ⟨i, x⟩ ∈ J
⊢ ⟨i, x⟩ ∈ I

Proof state:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
⊢ (Matroid.sigma M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

Tactic:
simp only [IsBasis, sigma_indep_iff, maximal_subset_iff, and_imp, and_assoc, sigma_ground_eq,
  forall_and, and_congr_right_iff]

Result:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) →
    ((I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ univ.sigma fun i => (M i).E) ↔
      (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E)