harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Relation.lean
theorem tail'_iff : TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Proof state:
case single
α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
exact ⟨_, by rfl, hac⟩

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a c b✝ : α
hab : TransGen r a b✝
hbc : r b✝ c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
exact ⟨_, hab.to_reflTransGen, hbc⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ReflTransGen r a a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩

Result:
α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Proof state:
α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
cases h with
| single hac => exact ⟨_, by rfl, hac⟩
| tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem coeff_scaleRoots_natDegree (p : R[X]) (s : R) :
    (scaleRoots p s).coeff p.natDegree = p.leadingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff

Tactic:
rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem eventually_not_disjoint_imp_le_of_mem_splitMany (s : Finset (Box ι)) :
    ∀ᶠ t : Finset (ι × ℝ) in atTop, ∀ (I : Box ι), ∀ J ∈ s, ∀ J' ∈ splitMany I t,
      ¬Disjoint (J : WithBot (Box ι)) J' → J' ≤ J

Proof state:
case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, J.lower i), (i, J.upper i)} ⊆ t

Tactic:
exact fun p hp =>
  ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Proof state:
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Tactic:
classical
cases nonempty_fintype ι
refine eventually_atTop.2
  ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
    fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩
exact fun p hp =>
  ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)

Result:
no goals

Proof state:
case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Tactic:
refine eventually_atTop.2
  ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
    fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩

Result:
case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, J.lower i), (i, J.upper i)} ⊆ t
-- Mathlib/RingTheory/TensorProduct/Finite.lean
theorem Subalgebra.finite_sup {K L : Type*} [CommSemiring K] [CommSemiring L] [Algebra K L]
    (E1 E2 : Subalgebra K L) [Module.Finite K E1] [Module.Finite K E2] :
    Module.Finite K ↥(E1 ⊔ E2)

Proof state:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range

Tactic:
exact Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(E1 ⊔ E2)

Tactic:
rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]

Result:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ => x ^ y) atTop atTop

Proof state:
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y

Tactic:
intro b

Result:
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y

Proof state:
y : ℝ
hy : 0 < y
b x : ℝ
hx : (b ⊔ 0) ^ (1 / y) ≤ x
⊢ b ⊔ ?m.824 ≤ x ^ y

Tactic:
convert rpow_le_rpow (rpow_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy)
  using 1

Result:
case h.e'_3
y : ℝ
hy : 0 < y
b x : ℝ
hx : (b ⊔ 0) ^ (1 / y) ≤ x
⊢ b ⊔ ?m.824 = ((b ⊔ 0) ^ (1 / y)) ^ y

Proof state:
case h.e'_3
y : ℝ
hy : 0 < y
b x : ℝ
hx : (b ⊔ 0) ^ (1 / y) ≤ x
⊢ b ⊔ ?m.824 = ((b ⊔ 0) ^ (1 / y)) ^ y

Tactic:
rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one]

Result:
no goals

Proof state:
case h
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∀ (a : ℝ), (b ⊔ 0) ^ (1 / y) ≤ a → b ≤ a ^ y

Tactic:
intro x hx

Result:
case h
y : ℝ
hy : 0 < y
b x : ℝ
hx : (b ⊔ 0) ^ (1 / y) ≤ x
⊢ b ≤ x ^ y

Proof state:
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y

Tactic:
use max b 0 ^ (1 / y)

Result:
case h
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∀ (a : ℝ), (b ⊔ 0) ^ (1 / y) ≤ a → b ≤ a ^ y

Proof state:
case h
y : ℝ
hy : 0 < y
b x : ℝ
hx : (b ⊔ 0) ^ (1 / y) ≤ x
⊢ b ≤ x ^ y

Tactic:
exact
  le_of_max_le_left
    (by
      convert rpow_le_rpow (rpow_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy)
        using 1
      rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one])

Result:
no goals

Proof state:
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Result:
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → m.contains a = false

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → m.contains a = false

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → containsKey a (toListModel m.val.buckets) = false

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → containsKey a (toListModel m.val.buckets) = false

Tactic:
empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_mkArray (w : stop = n) :
    (mkArray n a).filter p 0 stop = if p a then mkArray n a else #[]

Proof state:
case h
stop n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
w : stop = n
⊢ (filter p (mkArray n a) 0 stop).toList = (if p a = true then mkArray n a else #[]).toList

Tactic:
simp only [w, toList_filter', toList_mkArray, List.filter_replicate]

Result:
case h
stop n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
w : stop = n
⊢ (filter p (mkArray n a) 0 n).toList = (if p a = true then mkArray n a else #[]).toList

Proof state:
case h
stop n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
w : stop = n
⊢ (filter p (mkArray n a) 0 n).toList = (if p a = true then mkArray n a else #[]).toList

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
stop n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
w : stop = n
⊢ filter p (mkArray n a) 0 stop = if p a = true then mkArray n a else #[]

Tactic:
apply Array.ext'

Result:
case h
stop n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
w : stop = n
⊢ (filter p (mkArray n a) 0 stop).toList = (if p a = true then mkArray n a else #[]).toList
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem sum_antidiagonal_card_esymm_psum_eq_zero :
    ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
⊢ (-1) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Tactic:
simp [k, ← sum_filter_add_sum_filter_not (antidiagonal k) (fun a ↦ a.fst < k),
  ← mul_esymm_eq_sum, mul_add, ← mul_assoc, ← pow_add, mul_comm ↑k (esymm σ R k)]

Result:
no goals

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
this : (-1) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Tactic:
simpa using this

Result:
no goals

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Tactic:
let k := Fintype.card σ

Result:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Tactic:
suffices (-1 : MvPolynomial σ R) ^ (k + 1) *
    ∑ a ∈ antidiagonal k, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0 by
  simpa using this

Result:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
⊢ (-1) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_int (a : α) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
z : ℤ
⊢ ⌈a + ↑z⌉ = ⌈a⌉ + z

Tactic:
rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_int]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
@[to_additive]
lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
    a * b = b * a

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.IsCommutative
a b : G
ha : a ∈ H
hb : b ∈ H
⊢ a * b = b * a

Tactic:
simpa only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions monovary iff the rearrangement inequality holds. -/
lemma monovaryOn_iff_smul_rearrangement :
    MonovaryOn f g s ↔
      ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j :=
  monovaryOn_iff_forall_smul_nonneg.trans <| forall₄_congr fun i _ j _ ↦ by
    simp [smul_sub, sub_smul, ← add_sub_right_comm, le_sub_iff_add_le, add_comm (f i • g i),
      add_comm (f i • g j)]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : j ∈ s
⊢ 0 ≤ (f j - f i) • (g j - g i) ↔ f i • g j + f j • g i ≤ f i • g i + f j • g j

Tactic:
simp [smul_sub, sub_smul, ← add_sub_right_comm, le_sub_iff_add_le, add_comm (f i • g i),
  add_comm (f i • g j)]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
@[simp] lemma posFittingCompOf_eq_bot_of_isNilpotent
    [IsNilpotent L M] (x : L) :
    posFittingCompOf R M x = ⊥

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNilpotent L M
x : L
⊢ posFittingCompOf R M x = ⊥

Tactic:
simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
  posFittingCompOf_le_lowerCentralSeries, forall_const]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measure_zero_of_nhdsWithin (hs : IsCompact s) :
    (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0

Tactic:
simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhdsWithin

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_pos_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : 0 < x ^ y

Proof state:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < x ^ y

Tactic:
rw [rpow_def_of_pos hx]

Result:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < rexp (log x * y)

Proof state:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < rexp (log x * y)

Tactic:
apply exp_pos

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_basisDivisor_of_ne (hxy : x ≠ y) : (basisDivisor x y).degree = 1

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (basisDivisor x y).degree = 1

Tactic:
rw [basisDivisor, degree_mul, degree_X_sub_C, degree_C, zero_add]

Result:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (sub_ne_zero_of_ne hxy)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_addX_of_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) {n d : F}
    (hd : d ≠ 0) : W.toAffine.addX (P x / P z) (Q x / Q z) (n / d) =
      (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2
        - Q x * P z * d ^ 2) * d / (P z * Q z) ^ 2 / (d ^ 3 / (P z * Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).addX (P x / P z) (Q x / Q z) (n / d) =
    (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 - Q x * P z * d ^ 2) *
          d /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
field_simp [hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * d + (toAffine W).a₁ * n * d ^ 2 - d ^ 2 * d * (toAffine W).a₂) * P z - d ^ 2 * d * P x) * Q z -
        d ^ 2 * d * P z * Q x) *
      ((P z * Q z) ^ 2 * d ^ 3) =
    (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 - Q x * P z * d ^ 2) *
          d *
        (P z * Q z) *
      (d ^ 2 * d * P z * Q z)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * d + (toAffine W).a₁ * n * d ^ 2 - d ^ 2 * d * (toAffine W).a₂) * P z - d ^ 2 * d * P x) * Q z -
        d ^ 2 * d * P z * Q x) *
      ((P z * Q z) ^ 2 * d ^ 3) =
    (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 - Q x * P z * d ^ 2) *
          d *
        (P z * Q z) *
      (d ^ 2 * d * P z * Q z)

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem mem_iff {x : R} : x ∈ skewAdjoint R ↔ star x = -x

Proof state:
R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ skewAdjoint R ↔ star x = -x

Tactic:
rw [← AddSubgroup.mem_carrier]

Result:
R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).carrier ↔ star x = -x

Proof state:
R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).carrier ↔ star x = -x

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Spanning.superset (hS : M.Spanning S) (hST : S ⊆ T) (hT : T ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.closure S ⊆ M.closure T

Tactic:
exact M.closure_subset_closure hST

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.E ⊆ M.closure T

Tactic:
rw [← hS.closure_eq]

Result:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.closure S ⊆ M.closure T
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem zeta_pmul (f : ArithmeticFunction R) : (ζ : ArithmeticFunction R).pmul f = f

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ (↑ζ).pmul f = f

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ ((↑ζ).pmul f) x = f x

Proof state:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ ((↑ζ).pmul f) x = f x

Tactic:
cases x <;> simp [Nat.succ_ne_zero]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
/-- The moment generating function is antitone in the random variable for `t ≤ 0`. -/
lemma mgf_anti_of_nonpos {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : t ≤ 0)
    (htX : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    mgf Y μ t ≤ mgf X μ t

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
refine integral_mono_ae htY htX ?_

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ (fun ω => rexp (t * Y ω)) ≤ᶠ[ae μ] fun ω => rexp (t * X ω)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : ¬Integrable (fun ω => rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : ¬Integrable (fun ω => rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t

Tactic:
exact mgf_nonneg

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ (fun ω => rexp (t * Y ω)) ≤ᶠ[ae μ] fun ω => rexp (t * X ω)

Tactic:
filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : ¬Integrable (fun ω => rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
rw [mgf_undef htY]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (fun ω => rexp (t * X ω)) μ
htY : ¬Integrable (fun ω => rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
lemma Measurable.forall [Countable ι] {p : ι → α → Prop} (hp : ∀ i, Measurable (p i)) :
    Measurable fun a ↦ ∀ i, p i a :=
  measurableSet_setOf.1 <| by rw [setOf_forall]; exact MeasurableSet.iInter fun i ↦ (hp i).setOf

Proof state:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})

Tactic:
exact MeasurableSet.iInter fun i ↦ (hp i).setOf

Result:
no goals

Proof state:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∀ (i : ι), p i a}

Tactic:
rw [setOf_forall]

Result:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋂ i, {x | p i x})
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem one_le_succ_nth_stream_b {ifp_succ_n : IntFractPair K}
    (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : 1 ≤ ifp_succ_n.b

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ 1 ≤ ifp_succ_n.b

Tactic:
obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
      ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
  succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Result:
case intro.intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ 1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b

Proof state:
case intro.intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ifp_n.fr ≤ 1

Tactic:
exact (nth_stream_fr_lt_one nth_stream_eq).le

Result:
no goals

Proof state:
case intro.intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ 1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b

Tactic:
rw [IntFractPair.of, le_floor, cast_one, one_le_inv₀
  ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)]

Result:
case intro.intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ifp_n.fr ≤ 1