harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_at_natCast (q : ℕ[X]) : ∀(n : ℕ), q.smeval (n : S) = q.smeval n

Proof state:
case h_add
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : ℕ[X]
ph : ∀ (n : ℕ), p.smeval ↑n = ↑(p.smeval n)
qh : ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
n : ℕ
⊢ (p + q).smeval ↑n = ↑((p + q).smeval n)

Tactic:
simp only [add_mul, smeval_add, ph, qh, Nat.cast_add]

Result:
no goals

Proof state:
case h_monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n a : ℕ
⊢ ∀ (n_1 : ℕ), ((monomial n) a).smeval ↑n_1 = ↑(((monomial n) a).smeval n_1)

Tactic:
intro n

Result:
case h_monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ((monomial n✝) a).smeval ↑n = ↑(((monomial n✝) a).smeval n)

Proof state:
case h_add
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : ℕ[X]
ph : ∀ (n : ℕ), p.smeval ↑n = ↑(p.smeval n)
qh : ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
⊢ ∀ (n : ℕ), (p + q).smeval ↑n = ↑((p + q).smeval n)

Tactic:
intro n

Result:
case h_add
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : ℕ[X]
ph : ∀ (n : ℕ), p.smeval ↑n = ↑(p.smeval n)
qh : ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
n : ℕ
⊢ (p + q).smeval ↑n = ↑((p + q).smeval n)

Proof state:
case h_monomial
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
n✝ a n : ℕ
⊢ ((monomial n✝) a).smeval ↑n = ↑(((monomial n✝) a).smeval n)

Tactic:
rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]

Result:
no goals

Proof state:
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
⊢ ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)

Tactic:
induction q using Polynomial.induction_on' with
| h_add p q ph qh =>
  intro n
  simp only [add_mul, smeval_add, ph, qh, Nat.cast_add]
| h_monomial n a =>
  intro n
  rw [smeval_monomial, smeval_monomial, nsmul_eq_mul, smul_eq_mul, Nat.cast_mul, Nat.cast_npow]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem eventually_swap_iff {p : α × β → Prop} :
    (∀ᶠ x : α × β in f ×ˢ g, p x) ↔ ∀ᶠ y : β × α in g ×ˢ f, p y.swap

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map (fun p => (p.2, p.1)) (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rw [prod_comm]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map (fun p => (p.2, p.1)) (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_findGreatest {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N}
    (hN : ∀ k ≤ N, MeasurableSet { x | p x k }) : Measurable fun x => Nat.findGreatest (p x) N

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
⊢ Measurable fun x => Nat.findGreatest (p x) N

Tactic:
refine measurable_findGreatest' fun k hk => ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet {x | Nat.findGreatest (p x) N = k}

Proof state:
case h₂.h₂
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝² : ℕ
b✝¹ : k < b✝²
b✝ : b✝² ≤ N
⊢ MeasurableSet {a | p a b✝²}ᶜ

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
MeasurableSet.compl, hN] <;> try intros

Result:
no goals

Proof state:
case h₂.h₂
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ

Tactic:
intros

Result:
case h₂.h₂
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝² : ℕ
b✝¹ : k < b✝²
b✝ : b✝² ≤ N
⊢ MeasurableSet {a | p a b✝²}ᶜ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet {x | Nat.findGreatest (p x) N = k}

Tactic:
simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ i, ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a | p a i}ᶜ))

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ i, ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a | p a i}ᶜ))

Tactic:
repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
  MeasurableSet.compl, hN] <;> try intros

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_eq_zero_iff {ι} {f : ι → Ordinal.{u}} [Small.{u} ι] :
    iSup f = 0 ↔ ∀ i, f i = 0

Proof state:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
h : iSup f = 0
i : ι
⊢ f i = 0

Tactic:
rw [← Ordinal.le_zero, ← h]

Result:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f

Proof state:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f

Tactic:
exact Ordinal.le_iSup f i

Result:
no goals

Proof state:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
refine
  ⟨fun h i => ?_, fun h =>
    le_antisymm (Ordinal.iSup_le fun i => Ordinal.le_zero.2 (h i)) (Ordinal.zero_le _)⟩

Result:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
h : iSup f = 0
i : ι
⊢ f i = 0
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_isWeightedHomogeneous :
    (weightedHomogeneousComponent w n φ).IsWeightedHomogeneous w n

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w n) φ) n

Tactic:
classical
intro d hd
contrapose! hd
rw [coeff_weightedHomogeneousComponent, if_neg hd]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ coeff d ((weightedHomogeneousComponent w n) φ) = 0

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg hd]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d ((weightedHomogeneousComponent w n) φ) ≠ 0
⊢ (weight w) d = n

Tactic:
contrapose! hd

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ coeff d ((weightedHomogeneousComponent w n) φ) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w n) φ) n

Tactic:
intro d hd

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d ((weightedHomogeneousComponent w n) φ) ≠ 0
⊢ (weight w) d = n
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Iio_top : Real.toEReal ⁻¹' Iio ⊤ = univ

Proof state:
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑⊤) = univ

Tactic:
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio_top]

Result:
no goals

Proof state:
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑⊤ = univ

Tactic:
refine preimage_comp.trans ?_

Result:
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑⊤) = univ

Proof state:
⊢ Real.toEReal ⁻¹' Iio ⊤ = univ

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some ⊤)) = _

Result:
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑⊤ = univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_rev (f : α → Fin n → α) (x) :
     foldr n (fun i x => f x i.rev) x = foldl n f x

Proof state:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : α → Fin n → α) (x : α), foldr n (fun i x => f x i.rev) x = foldl n f x
f : α → Fin (n + 1) → α
x : α
⊢ f (foldr n (fun i x => f x i.succ.rev) x) (rev 0) = f (foldr n (fun i x => f x i.rev.castSucc) x) (last n)

Tactic:
simp [rev_succ]

Result:
no goals

Proof state:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : α → Fin n → α) (x : α), foldr n (fun i x => f x i.rev) x = foldl n f x
f : α → Fin (n + 1) → α
x : α
⊢ foldr (n + 1) (fun i x => f x i.rev) x = foldl (n + 1) f x

Tactic:
rw [foldl_succ_last, foldr_succ, ← ih]

Result:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : α → Fin n → α) (x : α), foldr n (fun i x => f x i.rev) x = foldl n f x
f : α → Fin (n + 1) → α
x : α
⊢ f (foldr n (fun i x => f x i.succ.rev) x) (rev 0) = f (foldr n (fun i x => f x i.rev.castSucc) x) (last n)

Proof state:
case zero
α : Sort u_1
f : α → Fin 0 → α
x : α
⊢ foldr 0 (fun i x => f x i.rev) x = foldl 0 f x

Tactic:
simp

Result:
no goals

Proof state:
α : Sort u_1
n : Nat
f : α → Fin n → α
x : α
⊢ foldr n (fun i x => f x i.rev) x = foldl n f x

Tactic:
induction n generalizing x with
| zero => simp
| succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem rcomap'_rcomap' (r : Rel α β) (s : Rel β γ) (l : Filter γ) :
    rcomap' r (rcomap' s l) = rcomap' (r.comp s) l :=
  Filter.ext fun t => by
    simp only [mem_rcomap', Rel.preimage_comp]
    constructor
    · rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
      exact ⟨v, vsets, (Rel.preimage_mono _ hv).trans h⟩
    rintro ⟨t, tsets, ht⟩
    exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Proof state:
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (r.comp s) l

Tactic:
simp only [mem_rcomap', Rel.preimage_comp]

Result:
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Proof state:
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩

Result:
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : r.preimage u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.preimage v ⊆ u
⊢ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Proof state:
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t

Tactic:
rintro ⟨t, tsets, ht⟩

Result:
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : r.preimage (s.preimage t) ⊆ t✝
⊢ ∃ t, (∃ t_1 ∈ l, s.preimage t_1 ⊆ t) ∧ r.preimage t ⊆ t✝

Proof state:
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : r.preimage (s.preimage t) ⊆ t✝
⊢ ∃ t, (∃ t_1 ∈ l, s.preimage t_1 ⊆ t) ∧ r.preimage t ⊆ t✝

Tactic:
exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : r.preimage u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.preimage v ⊆ u
⊢ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
exact ⟨v, vsets, (Rel.preimage_mono _ hv).trans h⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
constructor

Result:
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t
-- Mathlib/RingTheory/DedekindDomain/Different.lean
@[simp]
lemma traceDual_bot :
    (⊥ : Submodule B L)ᵛ = ⊤

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
⊢ ⊥ᵛ = ⊤

Tactic:
ext

Result:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
x✝ : L
⊢ x✝ ∈ ⊥ᵛ ↔ x✝ ∈ ⊤

Proof state:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
x✝ : L
⊢ x✝ ∈ ⊥ᵛ ↔ x✝ ∈ ⊤

Tactic:
simpa [mem_traceDual, -RingHom.mem_range] using zero_mem _

Result:
no goals
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem dirac_one_mconv [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] :
    (Measure.dirac 1) ∗ μ = μ

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map ((fun x => x.1 * x.2) ∘ Prod.mk 1) μ = μ

Tactic:
simp only [Function.comp_def, one_mul, map_id']

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable fun x => x.1 * x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable (Prod.mk 1)

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x => x.1 * x.2) ((dirac 1).prod μ) = μ

Tactic:
rw [MeasureTheory.Measure.dirac_prod, map_map (by fun_prop)]

Result:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map ((fun x => x.1 * x.2) ∘ Prod.mk 1) μ = μ

M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable (Prod.mk 1)

Proof state:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ dirac 1 ∗ μ = μ

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x => x.1 * x.2) ((dirac 1).prod μ) = μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array β} {b : β} :
    filterMap f l = l'.push b ↔ ∃ l₁ a l₂,
      l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ (∀ x, x ∈ l₂ → f x = none)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse) ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse) →
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none) →
    ∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
l' : Array β
b : β
l : List α
⊢ filterMap f { toList := l } = l'.push b ↔
    ∃ l₁ a l₂, { toList := l } = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ filterMap f { toList := l } = { toList := l' }.push b ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l.reverse = b :: l'.reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
rw [List.filterMap_eq_cons_iff]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse) ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none
-- Mathlib/Algebra/Regular/Basic.lean
/-- An element `a` is left-regular if and only if a positive power of `a` is left-regular. -/
lemma IsLeftRegular.pow_iff (n0 : 0 < n) : IsLeftRegular (a ^ n) ↔ IsLeftRegular a where
  mp

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a

Tactic:
exact .of_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]

Result:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
-- Mathlib/Topology/Order/Bornology.lean
lemma isOrderBornology_iff_eq_orderBornology [Lattice α] [Nonempty α] :
    IsOrderBornology α ↔ ‹Bornology α› = orderBornology

Proof state:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
⊢ inst✝² = orderBornology

Tactic:
ext s

Result:
case h_cobounded.h
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Proof state:
case h_cobounded.h
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
exact isBounded_compl_iff.symm.trans (h.1 _)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ IsOrderBornology α ↔ inst✝² = orderBornology

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩

Result:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
⊢ inst✝² = orderBornology

Proof state:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : inst✝² = orderBornology
s : Set α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
rw [h, orderBornology_isBounded]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem wOppSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
    s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Proof state:
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [vsub_eq_zero_iff_eq] at h0

Result:
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (p₂' -ᵥ y)
⊢ -(r₁ * r₂) + r₂ * r₁ = 0

Tactic:
ring

Result:
no goals

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) → s.WOppSide x y

Tactic:
rintro (h' | ⟨h₁, h₂, h₃⟩)

Result:
case mpr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ s.WOppSide x y

case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (h₁ -ᵥ y)
⊢ s.WOppSide x y

Proof state:
case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (p₂' -ᵥ y)
⊢ r₁ • (x -ᵥ p₁) = r₂ • (((-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂') -ᵥ y)

Tactic:
rw [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁']

Result:
case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (p₂' -ᵥ y)
⊢ r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁')) = r₂ • ((-r₁ / r₂) • (p₁ -ᵥ p₁') + (p₂' -ᵥ y))