harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
    Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x

Proof state:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False

Tactic:
exact h2 h1

Result:
no goals

Proof state:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
h1 : Limplies α x l
h2 : Limplies α x l.negate
p : α → Bool
px : p ⊨ x
⊢ False

Tactic:
specialize h1 p px

Result:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
h2 : Limplies α x l.negate
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False

Proof state:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negate
⊢ False

Tactic:
rw [sat_negate_iff_not_sat] at h2

Result:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False

Proof state:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
h2 : Limplies α x l.negate
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False

Tactic:
specialize h2 p px

Result:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negate
⊢ False

Proof state:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
⊢ Limplies α x l → Limplies α x l.negate → Unsatisfiable α x

Tactic:
intro h1 h2 p px

Result:
α : Type u_1
t : Type u_2
inst✝ : Entails α t
x : t
l : Literal α
h1 : Limplies α x l
h2 : Limplies α x l.negate
p : α → Bool
px : p ⊨ x
⊢ False
-- Mathlib/Analysis/Convex/Quasiconvex.lean
theorem QuasilinearOn.monotoneOn_or_antitoneOn [LinearOrder β] (hf : QuasilinearOn 𝕜 s f) :
    MonotoneOn f s ∨ AntitoneOn f s

Proof state:
𝕜 : Type u_1
β : Type u_3
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ MonotoneOn f s ∨ AntitoneOn f s

Tactic:
simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]

Result:
𝕜 : Type u_1
β : Type u_3
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)

Proof state:
𝕜 : Type u_1
β : Type u_3
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)

Tactic:
rintro a ha b hb c _ h

Result:
𝕜 : Type u_1
β : Type u_3
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)

Proof state:
𝕜 : Type u_1
β : Type u_3
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)

Tactic:
refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩ <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem sub_smul_slope (f : k → PE) (a b : k) : (b - a) • slope f a b = f b -ᵥ f a

Proof state:
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ (a - a) • slope f a a = f a -ᵥ f a

Tactic:
rw [sub_self, zero_smul, vsub_self]

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
rcases eq_or_ne a b with (rfl | hne)

Result:
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ (a - a) • slope f a a = f a -ᵥ f a

case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • slope f a b = f b -ᵥ f a

Proof state:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertListConst [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} :
    containsKey k (insertListConst l toInsert) =
    (containsKey k l || (toInsert.map Prod.fst).contains k)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
⊢ containsKey k (insertListConst l toInsert) = (containsKey k l || (List.map Prod.fst toInsert).contains k)

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
⊢ containsKey k (insertList l (List.map Prod.toSigma toInsert)) =
    (containsKey k l || (List.map Prod.fst toInsert).contains k)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
⊢ containsKey k (insertList l (List.map Prod.toSigma toInsert)) =
    (containsKey k l || (List.map Prod.fst toInsert).contains k)

Tactic:
rw [containsKey_insertList]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
⊢ (containsKey k l || (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k) =
    (containsKey k l || (List.map Prod.fst toInsert).contains k)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
⊢ (containsKey k l || (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k) =
    (containsKey k l || (List.map Prod.fst toInsert).contains k)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_def_lt' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m < p → ¬m ∣ p :=
  prime_def_lt.trans <|
    and_congr_right fun p2 =>
      forall_congr' fun m =>
        ⟨fun h m2 l d => not_lt_of_ge m2 ((h l d).symm ▸ by decide), fun h l d => by
          rcases m with (_ | _ | m)
          · rw [eq_zero_of_zero_dvd d] at p2
            revert p2
            decide
          · rfl
          · exact (h (le_add_left 2 m) l).elim d⟩

Proof state:
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

Tactic:
rw [eq_zero_of_zero_dvd d] at p2

Result:
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

Proof state:
case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
exact (h (le_add_left 2 m) l).elim d

Result:
no goals

Proof state:
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

Tactic:
revert p2

Result:
case zero
p : ℕ
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 2 ≤ 0 → 0 = 1

Proof state:
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1

Tactic:
rcases m with (_ | _ | m)

Result:
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Proof state:
case zero
p : ℕ
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 2 ≤ 0 → 0 = 1

Tactic:
decide

Result:
no goals

Proof state:
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ 1 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem bit_to_nat (b n) : (bit b n : ℕ) = Nat.bit b n

Proof state:
b : Bool
n : Num
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
cases b <;> cases n <;> simp [bit, two_mul] <;> rfl

Result:
no goals
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem natPow_zero_natMod_succ_succ :
    Nat.mod (Nat.pow a (nat_lit 0)) (Nat.succ (Nat.succ m)) = nat_lit 1

Proof state:
case h
a : ℕ
m : ℕ
⊢ 1 < m.succ.succ

Tactic:
exact Nat.one_lt_succ_succ _

Result:
no goals

Proof state:
a : ℕ
m : ℕ
⊢ (a.pow 0).mod m.succ.succ = 1

Tactic:
rw [natPow_zero]

Result:
a : ℕ
m : ℕ
⊢ Nat.mod 1 m.succ.succ = 1

Proof state:
a : ℕ
m : ℕ
⊢ Nat.mod 1 m.succ.succ = 1

Tactic:
apply Nat.mod_eq_of_lt

Result:
case h
a : ℕ
m : ℕ
⊢ 1 < m.succ.succ
-- Mathlib/Topology/Instances/AddCircle.lean
theorem addOrderOf_period_div {n : ℕ} (h : 0 < n) : addOrderOf ((p / n : 𝕜) : AddCircle p) = n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0

Tactic:
replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬↑(↑m * (p / ↑n)) = 0

Tactic:
rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]

Result:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬∃ n_1, n_1 • p = ↑m * (p / ↑n)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ addOrderOf ↑(p / ↑n) = n

Tactic:
rw [addOrderOf_eq_iff h]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0

Proof state:
case refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ ↑(↑n * (p / ↑n)) = 0

Tactic:
rw [mul_div_cancel₀ _ h.ne', coe_period]

Result:
no goals

Proof state:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False

Tactic:
exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_lt hn

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬∃ n_1, n_1 • p = ↑m * (p / ↑n)

Tactic:
rintro ⟨k, hk⟩

Result:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = ↑m * (p / ↑n)
⊢ False

Proof state:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = ↑m * (p / ↑n)
⊢ False

Tactic:
rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul,
  (mul_left_injective₀ hp.out.ne').eq_iff, Nat.cast_inj, mul_comm] at hk

Result:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0

Tactic:
refine ⟨?_, fun m hn h0 => ?_⟩ <;> simp only [Ne, ← coe_nsmul, nsmul_eq_mul]

Result:
case refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ ↑(↑n * (p / ↑n)) = 0

case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬↑(↑m * (p / ↑n)) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_push {p : α → Bool} {a : α} {l : Array α} :
    (l.push a).filter p = if p a then (l.filter p).push a else l.filter p

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
⊢ filter p (l.push a) = if p a = true then (filter p l).push a else filter p l

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem div_mul_eq_mul_div₀ (a b c : G₀) : a / c * b = a * b / c

Proof state:
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {f g : α → ℝ≥0∞} (hg : AEMeasurable g μ)
    (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ x ∂μ, f x ≠ g x) :
    ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h_le : f ≤ᶠ[ae μ] g
h : ∃ᵐ (x : α) ∂μ, f x ≠ g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
contrapose! h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ¬∃ᵐ (x : α) ∂μ, f x ≠ g x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x

Tactic:
exact ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ¬∃ᵐ (x : α) ∂μ, f x ≠ g x

Tactic:
simp only [not_frequently, Ne, Classical.not_not]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
h_le : f ≤ᶠ[ae μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x
-- Mathlib/RingTheory/PowerSeries/Binomial.lean
lemma rescale_neg_one_invOneSubPow [CommRing A] (d : ℕ) :
    rescale (-1 : A) (invOneSubPow A d) = binomialSeries A (-d : ℤ)

Proof state:
case h.zero
A : Type u_2
inst✝ : CommRing A
n : ℕ
⊢ ↑(↑n).negOnePow • (coeff A n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

Tactic:
by_cases hn : n = 0 <;> simp [invOneSubPow, Ring.choose_zero_ite, hn]

Result:
no goals

Proof state:
case h.succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose d) = ↑(Ring.choose (-1 + -↑d) n)

Tactic:
rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
  show (d : ℤ) + 1 + n - 1 = d + n by omega, ← Nat.cast_add, Ring.choose_eq_nat_choose]

Result:
case h.succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • ↑((d + n).choose n))

Proof state:
case h.succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • ↑((d + n).choose n))

Tactic:
norm_cast

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ -1 + -↑d = -(↑d + 1)

Tactic:
abel

Result:
no goals

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (coeff A n) ((rescale (-1)) ↑(invOneSubPow A d)) = (coeff A n) (binomialSeries A (-↑d))

Tactic:
rw [coeff_rescale, binomialSeries_coeff, ← Int.cast_negOnePow_natCast, ← zsmul_eq_mul]

Result:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ ↑(↑n).negOnePow • (coeff A n) ↑(invOneSubPow A d) = Ring.choose (-↑d) n • 1

Proof state:
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑d + 1 + ↑n - 1 = ↑d + ↑n

Tactic:
omega

Result:
no goals

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ ↑(↑n).negOnePow • (coeff A n) ↑(invOneSubPow A d) = Ring.choose (-↑d) n • 1

Tactic:
cases d with
| zero =>
  by_cases hn : n = 0 <;> simp [invOneSubPow, Ring.choose_zero_ite, hn]
| succ d =>
  simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
    zsmul_eq_mul, mul_one]
  rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
    show (d : ℤ) + 1 + n - 1 = d + n by omega, ← Nat.cast_add, Ring.choose_eq_nat_choose]
  norm_cast

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommRing A
d : ℕ
⊢ (rescale (-1)) ↑(invOneSubPow A d) = binomialSeries A (-↑d)

Tactic:
ext n

Result:
case h
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (coeff A n) ((rescale (-1)) ↑(invOneSubPow A d)) = (coeff A n) (binomialSeries A (-↑d))

Proof state:
case h.succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑(↑n).negOnePow • (coeff A n) ↑(invOneSubPow A (d + 1)) = Ring.choose (-↑(d + 1)) n • 1

Tactic:
simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
  zsmul_eq_mul, mul_one]

Result:
case h.succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose d) = ↑(Ring.choose (-1 + -↑d) n)
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_inter _ _

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ ↑(s ∩ t).offDiag = ↑(s.offDiag ∩ t.offDiag)

Tactic:
push_cast

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (↑s ∩ ↑t).offDiag = (↑s).offDiag ∩ (↑t).offDiag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (↑s ∩ ↑t).offDiag = (↑s).offDiag ∩ (↑t).offDiag

Tactic:
exact Set.offDiag_inter _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ}
    (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
    ∫ v : ι → ℝ, cexp (- ∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i)
      = ∏ i, (π / b i) ^ (1 / 2 : ℂ) * cexp (c i ^ 2 / (4 * b i))

Proof state:
case e_f.h
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
have : (-b i).re < 0 := by simpa using hb i

Result:
case e_f.h
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ (-b i).re < 0

Tactic:
simpa using hb i

Result:
no goals

Proof state:
case e_f.h
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
convert integral_cexp_quadratic this (c i) 0 using 1 <;> simp [div_neg]

Result:
no goals

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) =
    ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Result:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x)) =
    ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x)) =
    ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
rw [integral_fintype_prod_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]

Result:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∏ i : ι, ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Proof state:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∏ i : ι, ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
congr with i

Result:
case e_f.h
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β))
    (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
    getValue k' (alterKey k f l) hc =
      if h : k == k' then
        haveI hc' : (f (getValue? k l)).isSome

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this : some (getValue k' (alterKey k f l) hc) = if (k == k') = true then f (getValue? k l) else getValue? k' l
heq : (k == k') = true
⊢ some (getValue k' (alterKey k f l) hc) = some ((f (getValue? k l)).get ⋯)

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_atTop_prod_self' [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Proof state:
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Tactic:
simp only [eventually_atTop_prod_self, forall_cond_comm]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Transitive.lean
theorem isPretransitive_iff_orbit_eq_univ (a : X) :
    IsPretransitive G X ↔ orbit G a = .univ

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (∃ g, g • a = a_1) ↔ (a_1 ∈ orbit G a ↔ a_1 ∈ Set.univ)

Tactic:
intro x

Result:
case h
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X ↔ orbit G a = Set.univ

Tactic:
rw [isPretransitive_iff_base a, Set.ext_iff]

Result:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ x ∈ Set.univ

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)

Tactic:
simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ x ∈ Set.univ

Tactic:
apply forall_congr'

Result:
case h
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (∃ g, g • a = a_1) ↔ (a_1 ∈ orbit G a ↔ a_1 ∈ Set.univ)
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for separated morphisms. -/
lemma IsSeparated.eq_valuativeCriterion :
    @IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f

Tactic:
exact ⟨fun _ ↦ ⟨IsSeparated.valuativeCriterion f, inferInstance⟩,
  fun ⟨H, _⟩ ↦ .of_valuativeCriterion f H⟩

Result:
no goals

Proof state:
⊢ @IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f