harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
    {toInsert : List α} {k : α} :
    containsKey k (insertListIfNewUnit l toInsert) = (containsKey k l || toInsert.contains k)

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
l : List ((_ : α) × Unit)
⊢ containsKey k (insertListIfNewUnit l []) = (containsKey k l || [].contains k)

Tactic:
simp [insertListIfNewUnit]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
⊢ containsKey k (insertListIfNewUnit l toInsert) = (containsKey k l || toInsert.contains k)

Tactic:
induction toInsert generalizing l with
| nil => simp [insertListIfNewUnit]
| cons hd tl ih =>
  simp only [insertListIfNewUnit, List.contains_cons]
  rw [ih, containsKey_insertEntryIfNew]
  rw [Bool.or_comm (hd == k), Bool.or_assoc, BEq.comm (a:=hd)]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, containsKey k (insertListIfNewUnit l tl) = (containsKey k l || tl.contains k)
l : List ((_ : α) × Unit)
⊢ containsKey k (insertListIfNewUnit l (hd :: tl)) = (containsKey k l || (hd :: tl).contains k)

Tactic:
simp only [insertListIfNewUnit, List.contains_cons]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, containsKey k (insertListIfNewUnit l tl) = (containsKey k l || tl.contains k)
l : List ((_ : α) × Unit)
⊢ containsKey k (insertListIfNewUnit (insertEntryIfNew hd () l) tl) = (containsKey k l || (k == hd || tl.contains k))

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, containsKey k (insertListIfNewUnit l tl) = (containsKey k l || tl.contains k)
l : List ((_ : α) × Unit)
⊢ (hd == k || containsKey k l || tl.contains k) = (containsKey k l || (k == hd || tl.contains k))

Tactic:
rw [Bool.or_comm (hd == k), Bool.or_assoc, BEq.comm (a:=hd)]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, containsKey k (insertListIfNewUnit l tl) = (containsKey k l || tl.contains k)
l : List ((_ : α) × Unit)
⊢ containsKey k (insertListIfNewUnit (insertEntryIfNew hd () l) tl) = (containsKey k l || (k == hd || tl.contains k))

Tactic:
rw [ih, containsKey_insertEntryIfNew]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, containsKey k (insertListIfNewUnit l tl) = (containsKey k l || tl.contains k)
l : List ((_ : α) × Unit)
⊢ (hd == k || containsKey k l || tl.contains k) = (containsKey k l || (k == hd || tl.contains k))
-- Mathlib/Order/Bounds/Basic.lean
theorem IsGLB.insert [SemilatticeInf γ] (a) {b} {s : Set γ} (hs : IsGLB s b) :
    IsGLB (insert a s) (a ⊓ b)

Proof state:
γ : Type v
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB (insert a s) (a ⊓ b)

Tactic:
rw [insert_eq]

Result:
γ : Type v
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB ({a} ∪ s) (a ⊓ b)

Proof state:
γ : Type v
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB ({a} ∪ s) (a ⊓ b)

Tactic:
exact isGLB_singleton.union hs

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_segment (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E)
    (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (a b : R) (hab : a + b = 1) :
    a • s.centerMass w₁ z + b • s.centerMass w₂ z =
    s.centerMass (fun i => a * w₁ i + b * w₂ i) z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z

Tactic:
have hw : (∑ i ∈ s, (a * w₁ i + b * w₂ i)) = 1 := by
  simp only [← mul_sum, sum_add_distrib, mul_one, *]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
hw : ∑ i ∈ s, (a * w₁ i + b * w₂ i) = 1
⊢ a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
hw : ∑ i ∈ s, (a * w₁ i + b * w₂ i) = 1
⊢ a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z

Tactic:
simp only [Finset.centerMass_eq_of_sum_1, Finset.centerMass_eq_of_sum_1 _ _ hw,
  smul_sum, sum_add_distrib, add_smul, mul_smul, *]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ ∑ i ∈ s, (a * w₁ i + b * w₂ i) = 1

Tactic:
simp only [← mul_sum, sum_add_distrib, mul_one, *]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_equiv_zero_iff {x : PGame} : (-x ≈ 0) ↔ (x ≈ 0)

Proof state:
x : PGame
⊢ -x ≈ 0 ↔ x ≈ 0

Tactic:
rw [neg_equiv_iff, neg_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_prod_filter (f : α → M) (s : Set α) [DecidablePred (· ∈ s)]
    (hf : (mulSupport f).Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ Finset.filter (· ∈ s) hf.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by
    ext x
    simp [and_comm]

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : (mulSupport f).Finite
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ ↑(Finset.filter (fun x => x ∈ s) hf.toFinset) ∩ mulSupport f

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : (mulSupport f).Finite
⊢ s ∩ mulSupport f = ↑(Finset.filter (fun x => x ∈ s) hf.toFinset) ∩ mulSupport f

Tactic:
ext x

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hf : (mulSupport f).Finite
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ ↑(Finset.filter (fun x => x ∈ s) hf.toFinset) ∩ mulSupport f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_add_const (l : Array α) (a b : Nat) :
    l.foldl (fun x _ => x + a) b = b + a * l.size

Proof state:
α : Type u_1
l : Array α
a b : Nat
⊢ foldl (fun x x_1 => x + a) b l = b + a * l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ foldl (fun x x_1 => x + a) b { toList := l } = b + a * { toList := l }.size

Proof state:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ foldl (fun x x_1 => x + a) b { toList := l } = b + a * { toList := l }.size

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem induce_empty : G'.induce ∅ = ⊥

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce ∅ = ⊥

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem map_piMap_pi_finite {α β : ι → Type*} [Finite ι]
    (f : ∀ i, α i → β i) (l : ∀ i, Filter (α i)) :
    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
  map_piMap_pi (by simp) l

Proof state:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst✝ : Finite ι
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
⊢ ∀ᶠ (i : ι) in cofinite, Surjective (f i)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp]
lemma count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + count a s ⊓ count a t

Tactic:
rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∩ t) = count a s ⊓ count a t

Tactic:
apply @Nat.add_left_cancel (count a (s - t))

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + count a s ⊓ count a t
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma changeLevel_eq_cast_of_dvd {m : ℕ} (hm : n ∣ m) (a : Units (ZMod m)) :
    (changeLevel hm χ) a = χ (ZMod.cast (a : ZMod m))

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : (ZMod m)ˣ
⊢ ((changeLevel hm) χ) ↑a = χ (↑a).cast

Tactic:
simp [changeLevel_def, ZMod.unitsMap_val]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_app_self :
    hU.fromSpec.app U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫
      (Spec Γ(X, U)).presheaf.map (eqToHom hU.fromSpec_preimage_self).op

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
rw [← hU.ΓSpecIso_hom_fromSpec_app, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpTo.eq_iteratedFDeriv
    (h : HasFTaylorSeriesUpTo n f p) {m : ℕ} (hmn : m ≤ n) (x : E) :
    p x m = iteratedFDeriv 𝕜 m f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDeriv 𝕜 m f x

Tactic:
rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x
-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem curryFinFinset_apply_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l) (f : MultilinearMap R (fun _ : Fin n => M') M₂) (x y : M') :
    (curryFinFinset R M₂ M' hk hl f (fun _ => x) fun _ => y) =
      f (s.piecewise (fun _ => x) fun _ => y)

Proof state:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm ((curryFinFinset R M₂ M' hk hl) f)) (s.piecewise (fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)

Tactic:
rw [LinearEquiv.symm_apply_apply]

Result:
no goals

Proof state:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ ((((curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) = f (s.piecewise (fun x_1 => x) fun x => y)

Tactic:
refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_

Result:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm ((curryFinFinset R M₂ M' hk hl) f)) (s.piecewise (fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lcs_le_self : N.lcs k ≤ N

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs 0 N ≤ N

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs k N ≤ N

Tactic:
induction k with
| zero => simp
| succ k ih =>
  simp only [lcs_succ]
  exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ ⁅⊤, lcs k N⁆ ≤ N

Tactic:
exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ lcs (k + 1) N ≤ N

Tactic:
simp only [lcs_succ]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ ⁅⊤, lcs k N⁆ ≤ N
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
@[simp]
lemma log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r)

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
⊢ log ((algebraMap ℝ A) r) = (algebraMap ℝ A) (Real.log r)

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma Indep_iff (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    Indep m₁ m₂ μ
      ↔ ∀ t1 t2, MeasurableSet[m₁] t1 → MeasurableSet[m₂] t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Proof state:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
rw [Indep_iff_IndepSets, IndepSets_iff]

Result:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → μ (t1 ∩ t2) = μ t1 * μ t2) ↔
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Proof state:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → μ (t1 ∩ t2) = μ t1 * μ t2) ↔
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
theorem shiftFun_succ {n : ℕ} {X : Type*} [Zero X] (f : Fin n → X) (i : Fin n) :
    shiftFun f i.succ = f i

Proof state:
case pos
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : i.succ = 0
⊢ 0 = f i

Tactic:
exfalso

Result:
case pos
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : i.succ = 0
⊢ False

Proof state:
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ shiftFun f i.succ = f i

Tactic:
dsimp [shiftFun]

Result:
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ (if x : i.succ = 0 then 0 else f (i.succ.pred x)) = f i

Proof state:
case neg
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : ¬i.succ = 0
⊢ f (i.succ.pred h) = f i

Tactic:
simp only [Fin.pred_succ]

Result:
no goals

Proof state:
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ (if x : i.succ = 0 then 0 else f (i.succ.pred x)) = f i

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : i.succ = 0
⊢ 0 = f i

case neg
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : ¬i.succ = 0
⊢ f (i.succ.pred h) = f i

Proof state:
case pos
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : i.succ = 0
⊢ False

Tactic:
simp only [Fin.ext_iff, Fin.val_succ, Fin.val_zero, add_eq_zero, and_false, reduceCtorEq] at h

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_nil_iff : l ~r [] ↔ l = [] :=
  ⟨fun ⟨n, hn⟩ => by simpa using hn, fun h => h ▸ by rfl⟩

Proof state:
α : Type u
l : List α
h : l = []
⊢ l ~r l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l : List α
x✝ : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []

Tactic:
simpa using hn

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_of_le {a b : α} (h : a ≤ b) : a ⇔ b = b ⇨ a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : a ≤ b
⊢ a ⇔ b = b ⇨ a

Tactic:
rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem isOption_neg {x y : PGame} : IsOption x (-y) ↔ IsOption (-x) y

Proof state:
x y : PGame
⊢ ((∃ i, x = (-y).moveRight i) ∨ ∃ i, x = (-y).moveLeft i) ↔ (∃ i, -x = y.moveLeft i) ∨ ∃ i, -x = y.moveRight i

Tactic:
cases y

Result:
case mk
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((∃ i, x = (-mk α✝ β✝ a✝¹ a✝).moveRight i) ∨ ∃ i, x = (-mk α✝ β✝ a✝¹ a✝).moveLeft i) ↔
    (∃ i, -x = (mk α✝ β✝ a✝¹ a✝).moveLeft i) ∨ ∃ i, -x = (mk α✝ β✝ a✝¹ a✝).moveRight i

Proof state:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : (-mk α✝ β✝ a✝² a✝¹).LeftMoves
⊢ x = (-mk α✝ β✝ a✝² a✝¹).moveLeft a✝ ↔ -x = (mk α✝ β✝ a✝² a✝¹).moveRight a✝

Tactic:
rw [neg_eq_iff_eq_neg]

Result:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : (-mk α✝ β✝ a✝² a✝¹).LeftMoves
⊢ x = (-mk α✝ β✝ a✝² a✝¹).moveLeft a✝ ↔ x = -(mk α✝ β✝ a✝² a✝¹).moveRight a✝

Proof state:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : (-mk α✝ β✝ a✝² a✝¹).LeftMoves
⊢ x = (-mk α✝ β✝ a✝² a✝¹).moveLeft a✝ ↔ x = -(mk α✝ β✝ a✝² a✝¹).moveRight a✝

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
⊢ x.IsOption (-y) ↔ (-x).IsOption y

Tactic:
rw [isOption_iff, isOption_iff, or_comm]

Result:
x y : PGame
⊢ ((∃ i, x = (-y).moveRight i) ∨ ∃ i, x = (-y).moveLeft i) ↔ (∃ i, -x = y.moveLeft i) ∨ ∃ i, -x = y.moveRight i

Proof state:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), x = (-mk α✝ β✝ a✝¹ a✝).moveLeft a ↔ -x = (mk α✝ β✝ a✝¹ a✝).moveRight a

Tactic:
intro

Result:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : (-mk α✝ β✝ a✝² a✝¹).LeftMoves
⊢ x = (-mk α✝ β✝ a✝² a✝¹).moveLeft a✝ ↔ -x = (mk α✝ β✝ a✝² a✝¹).moveRight a✝

Proof state:
case mk.h₂
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∃ i, x = (-mk α✝ β✝ a✝¹ a✝).moveLeft i) ↔ ∃ i, -x = (mk α✝ β✝ a✝¹ a✝).moveRight i

Tactic:
apply exists_congr

Result:
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), x = (-mk α✝ β✝ a✝¹ a✝).moveLeft a ↔ -x = (mk α✝ β✝ a✝¹ a✝).moveRight a
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.succ_lt (hb : IsSuccPrelimit b) (ha : a < b) : succ a < b

Proof state:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b

Tactic:
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]

Result:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b

Proof state:
case pos
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
⊢ succ a < b

Tactic:
rwa [h.succ_eq]

Result:
no goals

Proof state:
case neg
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsMax a
hb : IsSuccPrelimit (succ a)
ha : a < succ a
⊢ False

Tactic:
exact (h hb.isMax).elim

Result:
no goals

Proof state:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b

Tactic:
refine ⟨ha, fun hab => ?_⟩

Result:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False

Proof state:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False

Tactic:
subst hab

Result:
case neg
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsMax a
hb : IsSuccPrelimit (succ a)
ha : a < succ a
⊢ False

Proof state:
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b

Tactic:
by_cases h : IsMax a

Result:
case pos
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
⊢ succ a < b

case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
-- Mathlib/Data/Set/Prod.lean
theorem image_prod_mk_subset_prod_right (ha : a ∈ s) : Prod.mk a '' t ⊆ s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a '' t ⊆ s ×ˢ t

Tactic:
rintro _ ⟨b, hb, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (a, b) ∈ s ×ˢ t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (a, b) ∈ s ×ˢ t

Tactic:
exact ⟨ha, hb⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem mk_coord_apply_eq (i : ι) : (Basis.mk hli hsp).coord i (v i) = 1 :=
  show hli.repr ⟨v i, Submodule.subset_span (mem_range_self i)⟩ i = 1 by simp [hli.repr_eq_single i]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
i : ι
⊢ (hli.repr ⟨v i, ⋯⟩) i = 1

Tactic:
simp [hli.repr_eq_single i]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem cosh_strictMonoOn : StrictMonoOn cosh (Ici 0) :=
  strictMonoOn_of_deriv_pos (convex_Ici _) continuous_cosh.continuousOn fun x hx => by
    rw [interior_Ici, mem_Ioi] at hx; rwa [deriv_cosh, sinh_pos_iff]

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x

Tactic:
rwa [deriv_cosh, sinh_pos_iff]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x

Tactic:
rw [interior_Ici, mem_Ioi] at hx

Result:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x