harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {m : AddContent C}
    (hC : IsSetSemiring C)
    -- TODO: `m_subadd` is in fact equivalent to `m.IsSigmaSubadditive`.
    (m_subadd : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : ⋃ i, f i ∈ C)
      (_hf_disj : Pairwise (Disjoint on f)), m (⋃ i, f i) ≤ ∑' i, m (f i))
    (f : ℕ → Set α) (hf : ∀ i, f i ∈ C) (hf_Union : (⋃ i, f i) ∈ C)
    (hf_disj : Pairwise (Disjoint on f)) :
    m (⋃ i, f i) = ∑' i, m (f i)

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ f '' ↑I ⊆ C

Tactic:
rintro i ⟨j, _, rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
j : ℕ
left✝ : j ∈ ↑I
⊢ f j ∈ C

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ∀ a ∈ I, f a ⊆ ⋃ i, f i

Tactic:
exact fun i _ ↦ subset_iUnion _ i

Result:
no goals

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ↑(Finset.image f I) ⊆ C

Tactic:
simp only [coe_image, Set.image_subset_iff]

Result:
case refine_1
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ ↑I ⊆ f ⁻¹' C
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem differentiable_set_subset_D :
    { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K } ⊆ D f K

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
⊢ ∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)

Tactic:
intro e

Result:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
⊢ x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
⊢ 1 / 2 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_single_pos {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : p i) :
    (single i x).filter p = single i x

Proof state:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ filter p (single i x) = single i x

Tactic:
rw [filter_single, if_pos h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
theorem PreservesKernel.iso_hom : (PreservesKernel.iso G f).hom = kernelComparison f G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom = kernelComparison f G

Tactic:
rw [← cancel_mono (kernel.ι _)]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)

Tactic:
simp [PreservesKernel.iso]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_toMeasurable_add_inter_right {s t : Set α} (hs : MeasurableSet s)
    (ht : (μ + ν) t ≠ ∞) : ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (ν + μ) t ≠ ⊤
⊢ ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)

Tactic:
exact measure_toMeasurable_add_inter_left hs ht

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)

Tactic:
rw [add_comm] at ht ⊢

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (ν + μ) t ≠ ⊤
⊢ ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_measure_inter_spanningSets_pos [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ]
    (s : Set α) : (∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ 0 < μ s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (¬∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ ¬0 < μ s

Tactic:
simp only [not_exists, not_lt, nonpos_iff_eq_zero]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (x : ℕ), μ (s ∩ spanningSets μ x) = 0) ↔ μ s = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (x : ℕ), μ (s ∩ spanningSets μ x) = 0) ↔ μ s = 0

Tactic:
exact forall_measure_inter_spanningSets_eq_zero s

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ 0 < μ s

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (¬∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ ¬0 < μ s
-- Mathlib/Tactic/NormNum/GCD.lean
theorem int_gcd_helper {x y : ℤ} {x' y' d : ℕ}
    (hx : x.natAbs = x') (hy : y.natAbs = y') (h : Nat.gcd x' y' = d) :
    Int.gcd x y = d

Proof state:
x y : ℤ
⊢ x.gcd y = x.natAbs.gcd y.natAbs

Tactic:
rw [Int.gcd_def]

Result:
no goals

Proof state:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.gcd y' = d
⊢ x.gcd y = d

Tactic:
subst_vars

Result:
x y : ℤ
⊢ x.gcd y = x.natAbs.gcd y.natAbs
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsUpperSet.card_inter_le_finset (h𝒜 : IsUpperSet (𝒜 : Set (Finset α)))
    (hℬ : IsLowerSet (ℬ : Set (Finset α))) :
    2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
have := h𝒜.le_card_inter_finset hℬ

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : #𝒜ᶜ * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : #𝒜ᶜ * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
  card_sdiff inter_subset_right, sdiff_inter_self_right, sdiff_compl,
  _root_.inf_comm] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem derivative_succ (n ν : ℕ) : Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
    n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    ↑(n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))

Tactic:
rw [Nat.cast_succ]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))

Tactic:
apply derivative_succ_aux

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R 0 (ν + 1)) =
    ↑0 * (bernsteinPolynomial R (0 - 1) ν - bernsteinPolynomial R (0 - 1) (ν + 1))

Tactic:
simp [bernsteinPolynomial]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
    ↑n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R 0 (ν + 1)) =
    ↑0 * (bernsteinPolynomial R (0 - 1) ν - bernsteinPolynomial R (0 - 1) (ν + 1))

case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n✝ + 1) (ν + 1)) =
    ↑(n✝ + 1) * (bernsteinPolynomial R (n✝ + 1 - 1) ν - bernsteinPolynomial R (n✝ + 1 - 1) (ν + 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_replicate (n : Nat) (a : α) (p : α → Bool) :
    (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ eraseP p (replicate n a) = if p a = true then replicate (n - 1) a else replicate n a

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, eraseP_cons]
  split <;> simp [*]

Result:
no goals

Proof state:
case zero
α : Type u_1
a : α
p : α → Bool
⊢ eraseP p (replicate 0 a) = if p a = true then replicate (0 - 1) a else replicate 0 a

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : eraseP p (replicate n a) = if p a = true then replicate (n - 1) a else replicate n a
⊢ eraseP p (replicate (n + 1) a) = if p a = true then replicate (n + 1 - 1) a else replicate (n + 1) a

Tactic:
simp only [replicate_succ, eraseP_cons]

Result:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : eraseP p (replicate n a) = if p a = true then replicate (n - 1) a else replicate n a
⊢ (bif p a then replicate n a else a :: eraseP p (replicate n a)) =
    if p a = true then replicate (n + 1 - 1) a else a :: replicate n a

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : eraseP p (replicate n a) = if p a = true then replicate (n - 1) a else replicate n a
⊢ (bif p a then replicate n a else a :: eraseP p (replicate n a)) =
    if p a = true then replicate (n + 1 - 1) a else a :: replicate n a

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
h₄ : x - n * k ≥ n
⊢ (x - n * k.succ) % n = x % n

Tactic:
rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]

Result:
no goals

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x - n * k + n * k

Tactic:
rw [Nat.sub_add_cancel h₂]

Result:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ x - n * k ≥ n

Tactic:
apply Nat.le_of_add_le_add_right (b := n * k)

Result:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x - n * k + n * k

Proof state:
x k n : Nat
h₁ : n * k ≤ x
⊢ (x - n * k) % n = x % n

Tactic:
match k with
| 0 => rw [Nat.mul_zero, Nat.sub_zero]
| succ k =>
  have h₂ : n * k ≤ x := Nat.le_trans (le_add_right _ n) h₁
  have h₄ : x - n * k ≥ n := by
    apply Nat.le_of_add_le_add_right (b := n * k)
    rw [Nat.sub_add_cancel h₂]
    simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
  rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]

Result:
no goals

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ (x - n * k.succ) % n = x % n

Tactic:
have h₄ : x - n * k ≥ n := by
  apply Nat.le_of_add_le_add_right (b := n * k)
  rw [Nat.sub_add_cancel h₂]
  simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]

Result:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
h₄ : x - n * k ≥ n
⊢ (x - n * k.succ) % n = x % n

Proof state:
x k✝ n k : Nat
h₂ : n * k ≤ x
h₁ : n + n * k ≤ x
⊢ n + n * k ≤ x

Tactic:
simp [h₁]

Result:
no goals

Proof state:
x k n : Nat
h₁ : n * 0 ≤ x
⊢ (x - n * 0) % n = x % n

Tactic:
rw [Nat.mul_zero, Nat.sub_zero]

Result:
no goals

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x

Tactic:
simp [mul_succ, Nat.add_comm] at h₁

Result:
x k✝ n k : Nat
h₂ : n * k ≤ x
h₁ : n + n * k ≤ x
⊢ n + n * k ≤ x

Proof state:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
⊢ (x - n * k.succ) % n = x % n

Tactic:
have h₂ : n * k ≤ x := Nat.le_trans (le_add_right _ n) h₁

Result:
x k✝ n k : Nat
h₁ : n * k.succ ≤ x
h₂ : n * k ≤ x
⊢ (x - n * k.succ) % n = x % n
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₂_comp_bind₂ (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) :
    (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
⊢ (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)

Tactic:
ext : 2 <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem strictMonoOn_tan : StrictMonoOn tan (Ioo (-(π / 2)) (π / 2))

Proof state:
⊢ StrictMonoOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
rintro x hx y hy hlt

Result:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ tan x < tan y

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ 0 < sin (y - x)

Tactic:
exact sin_pos_of_pos_of_lt_pi (sub_pos.2 hlt) <| by linarith [hx.1, hy.2]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ y - x < π

Tactic:
linarith [hx.1, hy.2]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ tan x < tan y

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos,
  div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm, ← sub_pos, ← sin_sub]

Result:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ 0 < sin (y - x)
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_eq_one_iff (v : Valuation K Γ₀) {x : K} : v x = 1 ↔ v x⁻¹ = 1

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x = 1 ↔ v x⁻¹ = 1

Tactic:
by_cases h : x = 0

Result:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x = 1 ↔ v x⁻¹ = 1

case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x = 1 ↔ v x⁻¹ = 1

Proof state:
case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x = 1 ↔ v x⁻¹ = 1

Tactic:
simpa only [le_antisymm_iff, And.comm] using and_congr (one_le_val_iff v h) (val_le_one_iff v h)

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x = 1 ↔ v x⁻¹ = 1

Tactic:
simp only [map_inv₀, inv_eq_one]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma density_le_one (hκν : fst κ ≤ ν) (a : α) (x : γ) (s : Set β) :
    density κ ν a x s ≤ 1

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

Tactic:
exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ κ.density ν a x s ≤ 1

Tactic:
refine limsup_le_of_le ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1

Tactic:
exact Eventually.of_forall (fun n ↦ densityProcess_le_one hκν _ _ _ _)

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma rel_iff (x y : R) : I.ringCon x y ↔ x - y ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ x - y ∈ I

Tactic:
rw [mem_iff]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ I.ringCon (x - y) 0

Proof state:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y → I.ringCon (x - y) 0

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ I.ringCon (x - y) 0

Proof state:
case h.e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ 0 = y - y

Tactic:
abel

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ I.ringCon x y

Tactic:
convert I.ringCon.add h (I.ringCon.refl y) <;> abel

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ I.ringCon x y

Proof state:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ I.ringCon (x - y) 0

Tactic:
convert I.ringCon.sub h (I.ringCon.refl y)

Result:
case h.e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ 0 = y - y

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ I.ringCon (x - y) 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y → I.ringCon (x - y) 0

case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y
-- Mathlib/Data/List/Sublists.lean
theorem sublists_map (f : α → β) : ∀ (l : List α),
    sublists (map f l) = map (map f) (sublists l)
  | [] => by simp
  | a::l => by
    rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]
    induction sublists l <;> simp [*]

Proof state:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists = map (map f) (a :: l).sublists

Tactic:
rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
  bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]

Result:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x => [x, f a :: x]) (flatMap (fun x => [map f x]) l.sublists) =
    flatMap (fun x => [map f x]) (flatMap (fun x => [x, a :: x]) l.sublists)

Proof state:
α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists = map (map f) [].sublists

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x => [x, f a :: x]) (flatMap (fun x => [map f x]) l.sublists) =
    flatMap (fun x => [map f x]) (flatMap (fun x => [x, a :: x]) l.sublists)

Tactic:
induction sublists l <;> simp [*]

Result:
no goals