harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Proper.lean
lemma isProper_iff_inter_eq_indicator_mul (h𝓑𝓧 : 𝓑 ≤ 𝓧) :
    IsProper π ↔
      ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (_hB : MeasurableSet[𝓑] B) (x : X),
        π x (A ∩ B) = B.indicator 1 x * π x A

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s → ((π.restrict ⋯) x) s = B.indicator (fun x => 1) x * (π x) s) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A

Tactic:
aesop

Result:
no goals

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃A : Set X⦄,
      MeasurableSet A →
        ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
congr! 5 with A hA B hB x

Result:
case a.h.h'.h.h.h.a
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
calc
  _ ↔ ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
        π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A := by
    simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
  _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

Result:
no goals

Proof state:
case a.h.h'.h.h.h.a
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
rw [restrict_apply, Measure.restrict_apply hA]

Result:
no goals

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A

Tactic:
simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s → ((π.restrict ⋯) x) s = B.indicator (fun x => 1) x * (π x) s) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
@[aesop 30% apply]
lemma IsSymmetric.mul_of_commute {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hT : T.IsSymmetric)
    (hST : Commute S T) : (S * T).IsSymmetric :=
  fun _ _ ↦ by rw [mul_apply, hS, hT, hST, mul_apply]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x✝¹ x✝ : E
⊢ inner ((S * T) x✝¹) x✝ = inner x✝¹ ((S * T) x✝)

Tactic:
rw [mul_apply, hS, hT, hST, mul_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_id {V : Π (x : M), TangentSpace I x} (h : UniqueMDiffWithinAt I s x) :
    mpullbackWithin I I id V s x = V x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V : (x : M) → TangentSpace I x
h : UniqueMDiffWithinAt I s x
⊢ mpullbackWithin I I _root_.id V s x = V x

Tactic:
simp [mpullbackWithin_apply, mfderivWithin_id h]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem map_val_atTop_of_Ici_subset [Preorder α] [IsDirected α (· ≤ ·)] {a : α} {s : Set α}
    (h : Ici a ⊆ s) : map ((↑) : s → α) atTop = atTop

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
⊢ map Subtype.val atTop = atTop

Tactic:
choose f hl hr using exists_ge_ge (α := α)

Result:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
⊢ map Subtype.val atTop = atTop

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ IsDirected ↑s fun x1 x2 => x1 ≤ x2

Tactic:
rw [directedOn_iff_directed] at this

Result:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 => x1 ≤ x2) Subtype.val
⊢ IsDirected ↑s fun x1 x2 => x1 ≤ x2

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) s
this : IsDirected ↑s fun x1 x2 => x1 ≤ x2
⊢ map Subtype.val atTop = atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_

Result:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) s
this : IsDirected ↑s fun x1 x2 => x1 ≤ x2
c : α
hc : c ≥ a
⊢ ∃ x, ↑x = c ∧ ∀ (a : { x // x ∈ s }), ↑a ≤ c ↔ a ≤ x

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 => x1 ≤ x2) Subtype.val
⊢ IsDirected ↑s fun x1 x2 => x1 ≤ x2

Tactic:
rwa [← directed_id_iff]

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) s
this : IsDirected ↑s fun x1 x2 => x1 ≤ x2
c : α
hc : c ≥ a
⊢ ∃ x, ↑x = c ∧ ∀ (a : { x // x ∈ s }), ↑a ≤ c ↔ a ≤ x

Tactic:
exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_lt : sqrt m < n ↔ m < n * n

Proof state:
m n : ℕ
⊢ m.sqrt < n ↔ m < n * n

Tactic:
simp only [← not_le, le_sqrt]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- The non-zero values of a multiplicative character `χ` such that `χ^n = 1`
are `n`th roots of unity. -/
lemma apply_mem_rootsOfUnity_of_pow_eq_one {χ : MulChar F R} {n : ℕ} (hχ : χ ^ n = 1)
    {a : F} (ha : a ≠ 0) :
    ∃ ζ ∈ rootsOfUnity n R, ζ = χ a

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
⊢ ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

Tactic:
obtain ⟨μ, hμ₁, hμ₂⟩ := χ.apply_mem_rootsOfUnity_orderOf ha

Result:
case intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
μ : Rˣ
hμ₁ : μ ∈ rootsOfUnity (orderOf χ) R
hμ₂ : ↑μ = χ a
⊢ ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

Proof state:
case intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
μ : Rˣ
hμ₁ : μ ∈ rootsOfUnity (orderOf χ) R
hμ₂ : ↑μ = χ a
⊢ ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

Tactic:
exact ⟨μ, rootsOfUnity_le_of_dvd (orderOf_dvd_of_pow_eq_one hχ) hμ₁, hμ₂⟩

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < sInf { m | p m }) :
    sInf { m | p m } + n = sInf { m | p (m - n) }

Proof state:
case intro.refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Tactic:
exact hb

Result:
no goals

Proof state:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
suffices h₁ : n ≤ sInf {m | p (m - n)} by
  convert sInf_add h₁
  simp_rw [Nat.add_sub_cancel_right]

Result:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ n ≤ sInf {m | p (m - n)}

Proof state:
case intro.refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}

Tactic:
dsimp

Result:
case intro.refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)

Proof state:
case intro
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ n ≤ sInf {m | p (m - n)}

Tactic:
refine
  le_csInf ⟨m + n, ?_⟩ fun b hb ↦
    le_of_not_lt fun hbn ↦
      ne_of_mem_of_not_mem ?_ (not_mem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)

Result:
case intro.refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}

case intro.refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Proof state:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
convert sInf_add h₁

Result:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n

Proof state:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n

Tactic:
simp_rw [Nat.add_sub_cancel_right]

Result:
no goals

Proof state:
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ n ≤ sInf {m | p (m - n)}

Tactic:
obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h

Result:
case intro
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ n ≤ sInf {m | p (m - n)}

Proof state:
case intro.refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)

Tactic:
rwa [Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (f ^ n) x

Proof state:
case negSucc
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.negSucc m) x

Tactic:
simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
⊢ MeromorphicAt (f ^ n) x

Tactic:
cases n with
| ofNat m => simpa only [Int.ofNat_eq_coe, zpow_natCast] using hf.pow m
| negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

Result:
no goals

Proof state:
case ofNat
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.ofNat m) x

Tactic:
simpa only [Int.ofNat_eq_coe, zpow_natCast] using hf.pow m

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

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

Tactic:
simp_to_model [insert] using List.getValueCastD_insertEntry

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iAlls [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} {v' : Fin 0 → M} :
    BoundedFormula.Realize (φ.iAlls β) v v' ↔
      ∀ (i : β → M), φ.Realize (fun a => Sum.elim v i a)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v

Tactic:
congr

Result:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Proof state:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Tactic:
rw [← Formula.realize_iAlls, iff_iff_eq]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
-- Mathlib/Data/Complex/Basic.lean
lemma im_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).im = z.im *  r

Proof state:
z : ℂ
r : ℝ
⊢ (z * ↑r).im = z.im * r

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Lucas.lean
theorem choose_modEq_choose_mul_prod_range_choose (a : ℕ) :
    choose n k ≡ choose (n / p ^ a) (k / p ^ a) *
      ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p] :=
  match a with
  | Nat.zero => by simp
  | Nat.succ a => (choose_modEq_choose_mul_prod_range_choose a).trans <| by
    rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]
    gcongr
    apply choose_modEq_choose_mod_mul_choose_div.trans
    simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD
    ↑p]

Tactic:
rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) *
      ↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) [ZMOD
    ↑p]

Proof state:
case h
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / p ^ a / p).choose (k / p ^ a / p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Tactic:
simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]

Result:
no goals

Proof state:
case h
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Tactic:
apply choose_modEq_choose_mod_mul_choose_div.trans

Result:
case h
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / p ^ a / p).choose (k / p ^ a / p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) *
      ↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) [ZMOD
    ↑p]

Tactic:
gcongr

Result:
case h
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ↑(n.choose k) ≡
    ↑((n / p ^ Nat.zero).choose (k / p ^ Nat.zero)) *
      ↑(∏ i ∈ range Nat.zero, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD
    ↑p]

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/StoneSeparation.lean
theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hst : Disjoint s t) :
    ∃ C : Set E, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
⊢ False

Tactic:
obtain ⟨p, hp, u, hu, hut⟩ := h x hx

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
⊢ False
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_induction_nonempty (p : α → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅)
    (p_s : ∀ a ∈ s, p a) : p s.prod

Proof state:
case empty
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
hs : 0 ≠ ∅
p_s : ∀ a ∈ 0, p a
⊢ p (prod 0)

Tactic:
simp at hs

Result:
no goals

Proof state:
case neg
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hps : ∀ x ∈ s, p x
⊢ p (a * s.prod)

Tactic:
exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

Result:
no goals

Proof state:
case pos
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

Tactic:
simp [hs_empty, p_s a]

Result:
no goals

Proof state:
case neg
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)

Tactic:
have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)

Result:
case neg
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hps : ∀ x ∈ s, p x
⊢ p (a * s.prod)

Proof state:
case cons
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ p (a ::ₘ s).prod

Tactic:
rw [prod_cons]

Result:
case cons
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ p (a * s.prod)

Proof state:
case cons
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ p (a * s.prod)

Tactic:
by_cases hs_empty : s = ∅

Result:
case pos
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

case neg
α : Type u_3
inst✝ : CommMonoid α
s✝ : Multiset α
p : α → Prop
p_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)
-- Mathlib/RingTheory/FiniteType.lean
theorem support_gen_of_gen' {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
    Algebra.adjoin R (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support

Tactic:
simp only [Set.image_iUnion]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤

Tactic:
suffices (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of R M '' (f.support : Set M) by
  rw [this]
  exact support_gen_of_gen hS

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤

Tactic:
rw [this]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support
⊢ adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support
⊢ adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support) = ⊤

Tactic:
exact support_gen_of_gen hS

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Count.lean
theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (l.concat a) = (count a l).succ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_self (x : Nat) : x &&& x = x

Proof state:
x : Nat
⊢ x &&& x = x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x : Nat
⊢ ∀ (i : Nat), (x &&& x).testBit i = x.testBit i

Proof state:
case pred
x : Nat
⊢ ∀ (i : Nat), (x &&& x).testBit i = x.testBit i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem to_of_nat : ∀ n : ℕ, ((n : Num) : ℕ) = n
  | 0 => by rw [Nat.cast_zero, cast_zero]
  | n + 1 => by rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]

Proof state:
n : ℕ
⊢ ↑↑(n + 1) = n + 1

Tactic:
rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]

Result:
no goals

Proof state:
⊢ ↑↑0 = 0

Tactic:
rw [Nat.cast_zero, cast_zero]

Result:
no goals