harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_push {p : α → Prop} {xs : Vector α n} {a : α} :
    (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.push a → p x) ↔
    p a ∧ ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p x

Tactic:
simp [or_comm, forall_eq_or_imp]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Prop
xs : Vector α n
a : α
⊢ (∀ (x : α), x ∈ xs.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ xs → p x

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.push a → p x) ↔
    p a ∧ ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p x
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem comap_normalClosure (s : Set N) (f : G ≃* N) :
    normalClosure (f ⁻¹' s) = (normalClosure s).comap f

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
this : ⇑f.toEquiv ⁻¹' s = ⇑f.symm '' s
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

Tactic:
simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

Tactic:
have := Set.preimage_equiv_eq_image_symm s f.toEquiv

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
this : ⇑f.toEquiv ⁻¹' s = ⇑f.symm '' s
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) : χ₄ n = (-1) ^ (n / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Tactic:
simp only [hn, Nat.one_ne_zero, if_false]

Result:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)

Tactic:
nth_rewrite 3 [show 4 = 2 * 2 by omega]

Result:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 2 ∣ 4

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ 4 = 2 * 2

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Tactic:
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide

Result:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ χ₄ ↑n = (-1) ^ (n / 2)

Tactic:
rw [χ₄_nat_eq_if_mod_four]

Result:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Tactic:
nth_rewrite 3 [← Nat.div_add_mod n 4]

Result:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Tactic:
exact help _ (Nat.mod_lt n (by omega)) <| (Nat.mod_mod_of_dvd n (by omega : 2 ∣ 4)).trans hn

Result:
no goals

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)

Tactic:
rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ zero_lt_two, pow_add, pow_mul,
  neg_one_sq, one_pow, mul_one]

Result:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Proof state:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 4 > 0

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma multisetSum_mem {ι : Type*} (s : Multiset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) :
    (s.map f).sum ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).sum ∈ I

Tactic:
rw [mem_iff, ← Multiset.sum_map_zero]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum (Multiset.map (fun x => 0) ?m.1296).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.1292

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Multiset ?m.1293

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum (Multiset.map (fun x => 0) ?m.1296).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.1292

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Multiset ?m.1293

Tactic:
exact I.ringCon.multisetSum s hs

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem localTriv_symmL {b : B} (hb : b ∈ Z.baseSet i) :
    (Z.localTriv i).symmL R b = Z.coordChange i (Z.indexAt b) b

Proof state:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ cast ⋯ (↑(Z.localTriv i).symm (b, v)).snd = (Z.coordChange i (Z.indexAt b) b) v

case h.hb
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ b ∈ (Z.localTriv i).baseSet

Tactic:
exacts [rfl, hb]

Result:
no goals

Proof state:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ (Trivialization.symmL R (Z.localTriv i) b) v = (Z.coordChange i (Z.indexAt b) b) v

Tactic:
rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]

Result:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ cast ⋯ (↑(Z.localTriv i).symm (b, v)).snd = (Z.coordChange i (Z.indexAt b) b) v

case h.hb
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ b ∈ (Z.localTriv i).baseSet

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
⊢ Trivialization.symmL R (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b

Tactic:
ext1 v

Result:
case h
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ (Trivialization.symmL R (Z.localTriv i) b) v = (Z.coordChange i (Z.indexAt b) b) v
-- Mathlib/Data/Fin/Basic.lean
theorem mul_one' [NeZero n] (k : Fin n) : k * 1 = k

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k * 1 = k

Tactic:
rcases n with - | n

Result:
case zero
inst✝ : NeZero 0
k : Fin 0
⊢ k * 1 = k

case succ
n : ℕ
inst✝ : NeZero (n + 1)
k : Fin (n + 1)
⊢ k * 1 = k

Proof state:
case succ.succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1 + 1)
k : Fin (n✝ + 1 + 1)
⊢ k * 1 = k

Tactic:
simp [Fin.ext_iff, mul_def, mod_eq_of_lt (is_lt k)]

Result:
no goals

Proof state:
case succ.zero
inst✝ : NeZero (0 + 1)
k : Fin (0 + 1)
⊢ k * 1 = k

Tactic:
simp [fin_one_eq_zero]

Result:
no goals

Proof state:
case succ
n : ℕ
inst✝ : NeZero (n + 1)
k : Fin (n + 1)
⊢ k * 1 = k

Tactic:
cases n

Result:
case succ.zero
inst✝ : NeZero (0 + 1)
k : Fin (0 + 1)
⊢ k * 1 = k

case succ.succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1 + 1)
k : Fin (n✝ + 1 + 1)
⊢ k * 1 = k

Proof state:
case zero
inst✝ : NeZero 0
k : Fin 0
⊢ k * 1 = k

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/Fintype/Pigeonhole.lean
theorem Finite.exists_ne_map_eq_of_infinite {α β} [Infinite α] [Finite β] (f : α → β) :
    ∃ x y : α, x ≠ y ∧ f x = f y

Proof state:
α : Sort u_4
β : Sort u_5
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ x y, x ≠ y ∧ f x = f y

Tactic:
simpa [Injective, and_comm] using not_injective_infinite_finite f

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem Bijective.existsUnique_iff {f : α → β} (hf : Bijective f) {p : β → Prop} :
    (∃! y, p y) ↔ ∃! x, p (f x) :=
  ⟨fun ⟨y, hpy, hy⟩ ↦
    let ⟨x, hx⟩ := hf.surjective y
    ⟨x, by simpa [hx], fun z (hz : p (f z)) ↦ hf.injective <| hx.symm ▸ hy _ hz⟩,
    fun ⟨x, hpx, hx⟩ ↦
    ⟨f x, hpx, fun y hy ↦
      let ⟨z, hz⟩ := hf.surjective y
      hz ▸ congr_arg f (hx _ (by simpa [hz]))⟩⟩

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x => p (f x)) x
hx : ∀ (y : α), (fun x => p (f x)) y → y = x
y : β
hy : (fun y => p y) y
z : α
hz : f z = y
⊢ (fun x => p (f x)) z

Tactic:
simpa [hz]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! y, p y
y : β
hpy : (fun y => p y) y
hy : ∀ (y_1 : β), (fun y => p y) y_1 → y_1 = y
x : α
hx : f x = y
⊢ (fun x => p (f x)) x

Tactic:
simpa [hx]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem right_mem_Ioo : b ∈ Ioo a b ↔ False

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ b ∈ Ioo a b ↔ False

Tactic:
simp [lt_irrefl]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem support_restriction (p : R[X]) : support (restriction p) = support p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
⊢ ↑(p.restriction.coeff i) = 0

Tactic:
rw [H, ZeroMemClass.coe_zero]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0

Tactic:
conv_rhs => rw [← coeff_restriction]

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ ↑(p.restriction.coeff i) = 0

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ p.restriction.support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.support = p.support

Tactic:
ext i

Result:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ p.restriction.support ↔ i ∈ p.support

Proof state:
case h
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ ↑(p.restriction.coeff i) = 0

Tactic:
exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.coprime_div_left (cmn : Coprime m n) (dvd : a ∣ m) : Coprime (m / a) n

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
⊢ (m / a).Coprime n

Tactic:
match eq_zero_or_pos a with
| .inl h0 =>
  rw [h0] at dvd
  rw [Nat.eq_zero_of_zero_dvd dvd] at cmn ⊢
  simp; assumption
| .inr hpos =>
  let ⟨k, hk⟩ := dvd
  rw [hk, Nat.mul_div_cancel_left _ hpos]
  rw [hk] at cmn
  exact cmn.coprime_mul_left

Result:
no goals

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
hpos : a > 0
⊢ (m / a).Coprime n

Tactic:
let ⟨k, hk⟩ := dvd

Result:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ (m / a).Coprime n

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
h0 : a = 0
⊢ (m / a).Coprime n

Tactic:
rw [h0] at dvd

Result:
m n a : Nat
cmn : m.Coprime n
dvd : 0 ∣ m
h0 : a = 0
⊢ (m / a).Coprime n

Proof state:
m n a : Nat
dvd : a ∣ m
hpos : a > 0
k : Nat
cmn : (a * k).Coprime n
hk : m = a * k
⊢ k.Coprime n

Tactic:
exact cmn.coprime_mul_left

Result:
no goals

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ k.Coprime n

Tactic:
rw [hk] at cmn

Result:
m n a : Nat
dvd : a ∣ m
hpos : a > 0
k : Nat
cmn : (a * k).Coprime n
hk : m = a * k
⊢ k.Coprime n

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : 0 ∣ m
h0 : a = 0
⊢ (m / a).Coprime n

Tactic:
rw [Nat.eq_zero_of_zero_dvd dvd] at cmn ⊢

Result:
m n a : Nat
cmn : Coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ (0 / a).Coprime n

Proof state:
m n a : Nat
cmn : Coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ (0 / a).Coprime n

Tactic:
simp

Result:
m n a : Nat
cmn : Coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ Coprime 0 n

Proof state:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ (m / a).Coprime n

Tactic:
rw [hk, Nat.mul_div_cancel_left _ hpos]

Result:
m n a : Nat
cmn : m.Coprime n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ k.Coprime n

Proof state:
m n a : Nat
cmn : Coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ Coprime 0 n

Tactic:
assumption

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_eq_left_of_subset_of_measure_add_eq {s t : Set α} (h : (μ + ν) t ≠ ∞) (h' : s ⊆ t)
    (h'' : (μ + ν) s = (μ + ν) t) : μ s = μ t

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
this : μ t + ν t ≤ μ s + ν t
⊢ ν t ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top h (le_add_left le_rfl)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ t ≤ μ s

Tactic:
have : μ t + ν t ≤ μ s + ν t :=
  calc
    μ t + ν t = μ s + ν s := h''.symm
    _ ≤ μ s + ν t := by gcongr

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
this : μ t + ν t ≤ μ s + ν t
⊢ μ t ≤ μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
this : μ t + ν t ≤ μ s + ν t
⊢ μ t ≤ μ s

Tactic:
apply ENNReal.le_of_add_le_add_right _ this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
this : μ t + ν t ≤ μ s + ν t
⊢ ν t ≠ ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ s + ν s ≤ μ s + ν t

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ s = μ t

Tactic:
refine le_antisymm (measure_mono h') ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ t ≤ μ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEqv_eq [DecidableEq α] {l₁ l₂ : List α} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂)

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)
b : α
l₂ : List α
⊢ (((a :: l₁).isEqv (b :: l₂) fun x1 x2 => x1 == x2) = true) = (a :: l₁ = b :: l₂)

Tactic:
simp [isEqv, ih]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)
⊢ (((a :: l₁).isEqv [] fun x1 x2 => x1 == x2) = true) = (a :: l₁ = [])

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ (([].isEqv l₂ fun x1 x2 => x1 == x2) = true) = ([] = l₂)

Tactic:
cases l₂ <;> simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)
l₂ : List α
⊢ (((a :: l₁).isEqv l₂ fun x1 x2 => x1 == x2) = true) = (a :: l₁ = l₂)

Tactic:
cases l₂ with
| nil => simp
| cons b l₂ => simp [isEqv, ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)

Tactic:
induction l₁ generalizing l₂ with
| nil => cases l₂ <;> simp
| cons a l₁ ih =>
  cases l₂ with
  | nil => simp
  | cons b l₂ => simp [isEqv, ih]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Iic (e : α ≃o β) (a : α) : e '' Iic a = Iic (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e '' Iic a = Iic (e a)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Iic, e.symm_symm]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_fst_neBot_iff {f : Filter α} :
    (f.comap (Prod.fst : α × β → α)).NeBot ↔ f.NeBot ∧ Nonempty β

Proof state:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Result:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ ¬⊥.NeBot ↔ ¬(f.NeBot ∧ Nonempty β)

Proof state:
case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
simp [comap_neBot_iff_frequently, *]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ ¬⊥.NeBot ↔ ¬(f.NeBot ∧ Nonempty β)

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
cases isEmpty_or_nonempty β

Result:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem isClosed_setOf_lipschitzWith {α β} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) :
    IsClosed { f : α → β | LipschitzWith K f }

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
⊢ IsClosed {f | LipschitzWith K f}

Tactic:
simp only [← lipschitzOnWith_univ, isClosed_setOf_lipschitzOnWith]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Type*}
    {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ)
    [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
    (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectR η a)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s

Tactic:
simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (κ ⊗ₖ η) a = κ a ⊗ₘ η.sectR a

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x) :
    foldlM n f x = (List.finRange n).foldlM f x

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin n → m α
x : α
⊢ foldlM n f x = List.foldlM f x (List.finRange n)

Tactic:
induction n generalizing x with
| zero => simp
| succ n ih =>
  rw [foldlM_succ, List.finRange_succ, List.foldlM_cons]
  congr; funext
  rw [List.foldlM_map, ih]

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
f : α → Fin 0 → m α
x : α
⊢ foldlM 0 f x = List.foldlM f x (List.finRange 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x : α
⊢ foldlM (n + 1) f x = List.foldlM f x (List.finRange (n + 1))

Tactic:
rw [foldlM_succ, List.finRange_succ, List.foldlM_cons]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x : α
⊢ (f x 0 >>= foldlM n fun x j => f x j.succ) = do
    let init ← f x 0
    List.foldlM f init (List.map succ (List.finRange n))

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x : α
⊢ (f x 0 >>= foldlM n fun x j => f x j.succ) = do
    let init ← f x 0
    List.foldlM f init (List.map succ (List.finRange n))

Tactic:
congr

Result:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x : α
⊢ (foldlM n fun x j => f x j.succ) = fun init => List.foldlM f init (List.map succ (List.finRange n))

Proof state:
case succ.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x x✝ : α
⊢ foldlM n (fun x j => f x j.succ) x✝ = List.foldlM f x✝ (List.map succ (List.finRange n))

Tactic:
rw [List.foldlM_map, ih]

Result:
no goals

Proof state:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x : α
⊢ (foldlM n fun x j => f x j.succ) = fun init => List.foldlM f init (List.map succ (List.finRange n))

Tactic:
funext

Result:
case succ.e_a.h
m : Type u_1 → Type u_2
α : Type u_1
inst✝ : Monad m
n : Nat
ih : ∀ (f : α → Fin n → m α) (x : α), foldlM n f x = List.foldlM f x (List.finRange n)
f : α → Fin (n + 1) → m α
x x✝ : α
⊢ foldlM n (fun x j => f x j.succ) x✝ = List.foldlM f x✝ (List.map succ (List.finRange n))