harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma Multiset.iInf_mem_map_of_exists_le_sInf_empty {s : Multiset ι} (f : ι → α)
    (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ x ∈ s, f x ∈ s.map f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
classical
simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain'_add [∀ i, AddZeroClass (β i)] (h : κ → ι) {h' : ι → κ}
    (hh' : Function.LeftInverse h' h) (f g : Π₀ i, β i) :
    comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f + comapDomain' h hh' g) i✝

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f + comapDomain' h hh' g) i✝

Tactic:
rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
lemma prod_indicator_const_apply (s : Finset ι) (f : ι → Set κ) (g : κ → α) (j : κ) :
    ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ #s) j

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : κ → α
j : κ
⊢ ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ #s) j

Tactic:
simp [prod_indicator_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma polynomialY_eq : W'.polynomialY = C 2 * X 1 + C W'.a₁ * X 0 * X 2 + C W'.a₃ * X 2 ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 1 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 1) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 1) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 0 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) =
    2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv y)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 1 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 1) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 1) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 0 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) =
    2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialY = C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3

Tactic:
rw [polynomialY, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv y)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3
-- Mathlib/NumberTheory/Modular.lean
theorem one_lt_normSq_T_zpow_smul (hz : z ∈ 𝒟ᵒ) (n : ℤ) : 1 < normSq (T ^ n • z : ℍ)

Proof state:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
this : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
simpa [coe_T_zpow, normSq, num, denom, -map_zpow]

Result:
no goals

Proof state:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1

Result:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
⊢ 1 < normSq ↑(T ^ n • z)

Proof state:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
have : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im := by linarith

Result:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
this : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im
⊢ 1 < normSq ↑(T ^ n • z)

Proof state:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
have hzn := Int.nneg_mul_add_sq_of_abs_le_one n (abs_two_mul_re_lt_one_of_mem_fdo hz).le

Result:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
⊢ 1 < normSq ↑(T ^ n • z)

Proof state:
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hz₁ : 1 < z.re * z.re + z.im * z.im
hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n
⊢ 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im

Tactic:
linarith

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.dist_left_right (h : s.IsDiameter p₁ p₂) : dist p₁ p₂ = 2 * s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
rw [← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * (‖2‖⁻¹ * dist p₁ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * (‖2‖⁻¹ * dist p₁ p₂)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory.lean
theorem quotient_map_out_comp_out {C D E : HomotopyCategory V c} (f : C ⟶ D) (g : D ⟶ E) :
    (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g

Proof state:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomotopyCategory V c
f : C ⟶ D
g : D ⟶ E
⊢ (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_add {n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.val) % n

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ (a + b).val = (a.val + b.val) % (n✝ + 1)

Tactic:
apply Fin.val_add

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a + b).val = (a.val + b.val) % n

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ (a + b).val = (a.val + b.val) % (n✝ + 1)

Proof state:
case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_take {l : List α} {n : Nat} :
    (l.take n).replace a b = (l.replace a b).take n

Proof state:
case cons.succ
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
ih : ∀ {n : Nat}, (take n xs).replace a b = take n (xs.replace a b)
n : Nat
⊢ (match a == x with
    | true => b :: take n xs
    | false => x :: (take n xs).replace a b) =
    take (n + 1)
      (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (take n []).replace a b = take n ([].replace a b)

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
ih : ∀ {n : Nat}, (take n xs).replace a b = take n (xs.replace a b)
n : Nat
⊢ (take (n + 1) (x :: xs)).replace a b = take (n + 1) ((x :: xs).replace a b)

Tactic:
simp only [replace_cons, take_succ_cons]

Result:
case cons.succ
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
ih : ∀ {n : Nat}, (take n xs).replace a b = take n (xs.replace a b)
n : Nat
⊢ (match a == x with
    | true => b :: take n xs
    | false => x :: (take n xs).replace a b) =
    take (n + 1)
      (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)

Proof state:
case cons.zero
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
ih : ∀ {n : Nat}, (take n xs).replace a b = take n (xs.replace a b)
⊢ (take 0 (x :: xs)).replace a b = take 0 ((x :: xs).replace a b)

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
n : Nat
⊢ (take n l).replace a b = take n (l.replace a b)

Tactic:
induction l generalizing n with
| nil => simp
| cons x xs ih =>
  cases n with
  | zero => simp [ih]
  | succ n =>
    simp only [replace_cons, take_succ_cons]
    split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
xs : List α
ih : ∀ {n : Nat}, (take n xs).replace a b = take n (xs.replace a b)
n : Nat
⊢ (take n (x :: xs)).replace a b = take n ((x :: xs).replace a b)

Tactic:
cases n with
| zero => simp [ih]
| succ n =>
  simp only [replace_cons, take_succ_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Polynomial/SeparableDegree.lean
theorem IsSeparableContraction.dvd_degree' {g} (hf : IsSeparableContraction q f g) :
    ∃ m : ℕ, g.natDegree * q ^ m = f.natDegree

Proof state:
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree

Tactic:
rw [natDegree_expand]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, g.natDegree * q ^ m = f.natDegree

Tactic:
obtain ⟨m, rfl⟩ := hf.2

Result:
case intro
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ ∃ m_1, g.natDegree * q ^ m_1 = ((expand F (q ^ m)) g).natDegree

Proof state:
case intro
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ ∃ m_1, g.natDegree * q ^ m_1 = ((expand F (q ^ m)) g).natDegree

Tactic:
use m

Result:
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_modify (h : m.1.WF) {k k' : α} {f : β k → β k} :
    (m.modify k f).get? k' =
      if h : k == k' then
        (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f))
      else
        m.get? k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : β k → β k
⊢ (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'

Tactic:
simp_to_model [modify] using List.getValueCast?_modifyKey

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma le_llp_rlp : T ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T ≤ T.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp]

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem single_subsingleton_eq_refl [Subsingleton α] (a b : α) : single a b = PEquiv.refl α

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b : α
⊢ single a b = PEquiv.refl α

Tactic:
ext i j

Result:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ j ∈ (single a b) i ↔ j ∈ (PEquiv.refl α) i

Proof state:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ j ∈ (single a b) i ↔ j ∈ (PEquiv.refl α) i

Tactic:
dsimp [single]

Result:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ (j ∈ if i = a then some b else none) ↔ j ∈ some i

Proof state:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ (j ∈ if i = a then some b else none) ↔ j ∈ some i

Tactic:
rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_iUnion_congr [Countable ι] {s : ι → Set α} :
    μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
⊢ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
⊢ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)

Proof state:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x1 x2 => x1 ⊆ x2) fun t => ⋃ i ∈ t, s i
⊢ (μ.restrict (⋃ i, s i)) t = (ν.restrict (⋃ i, s i)) t

Tactic:
rw [iUnion_eq_iUnion_finset]

Result:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x1 x2 => x1 ⊆ x2) fun t => ⋃ i ∈ t, s i
⊢ (μ.restrict (⋃ t, ⋃ i ∈ t, s i)) t = (ν.restrict (⋃ t, ⋃ i ∈ t, s i)) t

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
⊢ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)

Tactic:
ext1 t ht

Result:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = (ν.restrict (⋃ i, s i)) t

Proof state:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x1 x2 => x1 ⊆ x2) fun t => ⋃ i ∈ t, s i
⊢ (μ.restrict (⋃ t, ⋃ i ∈ t, s i)) t = (ν.restrict (⋃ t, ⋃ i ∈ t, s i)) t

Tactic:
simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_finset_biUnion_congr.2 fun i _ => h i]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_singleton (a : α) : mulRothNumber ({a} : Finset α) = 1

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ mulRothNumber {a} = 1

Tactic:
refine ThreeGPFree.mulRothNumber_eq ?_

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree ↑{a}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree {a}

Tactic:
exact threeGPFree_singleton a

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree ↑{a}

Tactic:
rw [coe_singleton]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ ThreeGPFree {a}
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
@[simp] lemma degreesLE_zero : degreesLE R σ 0 = 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x ∈ 1

Tactic:
have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
  (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ x ∈ 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ (LinearMap.toSpanSingleton R (MvPolynomial σ R) 1) (coeff 0 x) = x

Tactic:
simp [Algebra.smul_def, ← this]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degreesLE R σ 0 = 1

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (by simp)

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ 0
⊢ x ∈ 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ x ∈ 1

Tactic:
exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ 0
⊢ x ∈ 1

Tactic:
simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x ∈ 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ 1 ≤ degreesLE R σ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x.degrees.card ≤ 0

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_add_le_tsub_left : a + b - (a + c) ≤ b - c

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))

Tactic:
exact add_le_add_left le_add_tsub _

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - (a + c) ≤ b - c

Tactic:
rw [tsub_le_iff_left, add_assoc]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))
-- Mathlib/Data/Real/Sqrt.lean
theorem div_sqrt : x / √x = √x

Proof state:
case inl
x : ℝ
h : x ≤ 0
⊢ x / √x = √x

Tactic:
rw [sqrt_eq_zero'.mpr h, div_zero]

Result:
no goals

Proof state:
case inr
x : ℝ
h : 0 < x
⊢ x / √x = √x

Tactic:
rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le]

Result:
no goals

Proof state:
x : ℝ
⊢ x / √x = √x

Tactic:
rcases le_or_lt x 0 with h | h

Result:
case inl
x : ℝ
h : x ≤ 0
⊢ x / √x = √x

case inr
x : ℝ
h : 0 < x
⊢ x / √x = √x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_Δ' : (W.map φ).Δ' = Units.map φ W.Δ'

Proof state:
case a
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑(W.map φ).Δ' = ↑((Units.map ↑φ) W.Δ')

Tactic:
exact W.coe_map_Δ' φ

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).Δ' = (Units.map ↑φ) W.Δ'

Tactic:
ext

Result:
case a
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑(W.map φ).Δ' = ↑((Units.map ↑φ) W.Δ')
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem le_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) (μ : Measure X) (ε : ℝ≥0∞) (h₀ : 0 < ε)
    (h : ∀ s : Set X, diam s ≤ ε → μ s ≤ m (diam s)) : μ ≤ mkMetric m

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), diam s ≤ ε → μ s ≤ m (diam s)
⊢ μ ≤ mkMetric m

Tactic:
rw [← toOuterMeasure_le, mkMetric_toOuterMeasure]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), diam s ≤ ε → μ s ≤ m (diam s)
⊢ μ.toOuterMeasure ≤ OuterMeasure.mkMetric m

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), diam s ≤ ε → μ s ≤ m (diam s)
⊢ μ.toOuterMeasure ≤ OuterMeasure.mkMetric m

Tactic:
exact OuterMeasure.le_mkMetric m μ.toOuterMeasure ε h₀ h

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem subset (s : Set α) {t : Set α} [Finite s] (h : t ⊆ s) : Finite t

Proof state:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t

Tactic:
rw [← sep_eq_of_subset h]

Result:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
-- Mathlib/Data/PEquiv.lean
theorem bot_trans (f : β ≃. γ) : (⊥ : α ≃. β).trans f = ⊥

Proof state:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
⊢ ⊥.trans f = ⊥

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ (⊥.trans f) x✝ ↔ a✝ ∈ ⊥ x✝

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ none ↔ a✝ ∈ none

Tactic:
simp

Result:
no goals

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ (⊥.trans f) x✝ ↔ a✝ ∈ ⊥ x✝

Tactic:
dsimp [PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ a✝ ∈ none ↔ a✝ ∈ none
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma comap_prod (κ : Kernel β γ) [IsSFiniteKernel κ] (η : Kernel β δ) [IsSFiniteKernel η]
    {f : α → β} (hf : Measurable f) :
    (κ ×ₖ η).comap f hf = (κ.comap f hf) ×ₖ (η.comap f hf)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
⊢ (κ ×ₖ η).comap f hf = κ.comap f hf ×ₖ η.comap f hf

Tactic:
ext1 x

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ ((κ ×ₖ η).comap f hf) x = (κ.comap f hf ×ₖ η.comap f hf) x

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β δ
inst✝ : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
⊢ ((κ ×ₖ η).comap f hf) x = (κ.comap f hf ×ₖ η.comap f hf) x

Tactic:
rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]

Result:
no goals