harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/Predicate.lean
lemma Construction.wIso_eq_isoOfHom {X Y : C} (f : X ⟶ Y) (hf : W f) :
    Construction.wIso f hf = isoOfHom W.Q W f hf

Proof state:
case w
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ (wIso f hf).hom = (isoOfHom W.Q W f hf).hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ wIso f hf = isoOfHom W.Q W f hf

Tactic:
ext

Result:
case w
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ (wIso f hf).hom = (isoOfHom W.Q W f hf).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
    (s ++ t).set i x (by simp; omega) = s.set i x ++ t

Proof state:
α : Type ?u.250577
s t : Array α
i : Nat
x : α
h : i < s.size
⊢ i < s.size + t.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h : i < s.size
⊢ (s ++ t).set i x ⋯ = s.set i x h ++ t

Tactic:
simp [set_append, h]

Result:
no goals

Proof state:
α : Type ?u.250577
s t : Array α
i : Nat
x : α
h : i < s.size
⊢ i < (s ++ t).size

Tactic:
simp

Result:
α : Type ?u.250577
s t : Array α
i : Nat
x : α
h : i < s.size
⊢ i < s.size + t.size
-- Mathlib/Algebra/CharP/Algebra.lean
theorem RingHom.charP {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
    (H : Function.Injective f) (p : ℕ) [CharP A p] : CharP R p

Proof state:
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
⊢ CharP R p

Tactic:
obtain ⟨q, h⟩ := CharP.exists R

Result:
case intro
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
q : ℕ
h : CharP R q
⊢ CharP R p

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
q : ℕ
h : CharP R q
⊢ CharP R p

Tactic:
exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem finite_quotient_span_sub_one' [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) :
    Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ✝.toInteger - 1})

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ✝.toInteger - 1})

Tactic:
exact hζ.finite_quotient_span_sub_one

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa using hcycl

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem iterate_frobenius_mk (n : ℕ) (x : K) :
    (frobenius (PerfectClosure K p) p)^[n] (mk K p ⟨n, x⟩) = of K p x

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n + 1] (mk K p (n + 1, x)) = (of K p) x

Tactic:
rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[0] (mk K p (0, x)) = (of K p) x

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

Tactic:
induction' n with n ih

Result:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[0] (mk K p (0, x)) = (of K p) x

case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n + 1] (mk K p (n + 1, x)) = (of K p) x
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
@[simp]
lemma transfiniteCompositions_le_iff {P Q : MorphismProperty C}
    [IsStableUnderTransfiniteComposition.{w} Q] :
    transfiniteCompositions.{w} P ≤ Q ↔ P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ P ≤ Q → transfiniteCompositions.{w, v, u} P ≤ Q

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
h : P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
h : P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q

Tactic:
exact (transfiniteCompositions_monotone.{w} h).trans Q.transfiniteCompositions_le

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
exact (le_transfiniteCompositions P).trans

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ P ≤ Q → transfiniteCompositions.{w, v, u} P ≤ Q
-- Mathlib/Data/Matroid/Restrict.lean
theorem isBasis'_restrict_iff : (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Tactic:
simp_rw [IsBasis', maximal_iff, restrict_indep_iff, subset_inter_iff, and_imp]

Result:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
-- Mathlib/Tactic/Abel.lean
theorem zero_smul {α} [AddCommMonoid α] (c) : smul c (0 : α) = 0

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0

Tactic:
simp [smul, nsmul_zero]

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem det_rotation (a : Circle) : LinearMap.det ((rotation a).toLinearEquiv : ℂ →ₗ[ℝ] ℂ) = 1

Proof state:
a : Circle
⊢ LinearMap.det ↑(rotation a).toLinearEquiv = 1

Tactic:
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_rotation, Matrix.det_fin_two]

Result:
a : Circle
⊢ ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 0 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 1 -
      ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 1 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 0 =
    1

Proof state:
a : Circle
⊢ ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 0 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 1 -
      ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 1 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 0 =
    1

Tactic:
simp [← normSq_apply]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
/-- Finsets form an order-connected suborder of sets. -/
lemma ordConnected_range_coe : Set.OrdConnected (Set.range ((↑) : Finset α → Set α)) :=
  ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩⟩

Proof state:
α : Type u_1
⊢ ∀ ⦃x : Set α⦄, x ∈ Set.range toSet → ∀ ⦃y : Set α⦄, y ∈ Set.range toSet → Set.Icc x y ⊆ Set.range toSet

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht

Result:
case intro
α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range toSet
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range toSet

Proof state:
case intro
α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range toSet
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range toSet

Tactic:
exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_add_eq_of_leadingCoeff_add_ne_zero (h : leadingCoeff p + leadingCoeff q ≠ 0) :
    degree (p + q) = max p.degree q.degree :=
  le_antisymm (degree_add_le _ _) <|
    match lt_trichotomy (degree p) (degree q) with
    | Or.inl hlt => by
      rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
    | Or.inr (Or.inl HEq) =>
      le_of_not_gt fun hlt : max (degree p) (degree q) > degree (p + q) =>
        h <|
          show leadingCoeff p + leadingCoeff q = 0 by
            rw [HEq, max_self] at hlt
            rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
            exact coeff_natDegree_eq_zero_of_degree_lt hlt
    | Or.inr (Or.inr hlt) => by
      rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ p.degree ⊔ q.degree ≤ (p + q).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
⊢ p.degree ⊔ q.degree ≤ (p + q).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : p.degree ⊔ q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
rw [HEq, max_self] at hlt

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ (p + q).coeff q.natDegree = 0

Tactic:
exact coeff_natDegree_eq_zero_of_degree_lt hlt

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ (p + q).coeff q.natDegree = 0
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousAt_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {x : α × β} :
    ContinuousAt f x ↔ ContinuousAt (f ⟨x.1, ·⟩) x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x.1, x_1)) x.2

Tactic:
simp_rw [← continuousWithinAt_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) univ x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) univ x.2

Tactic:
exact continuousWithinAt_prod_of_discrete_left

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_add (v w : VectorMeasure α M) (i : Set α) :
    (v + w).restrict i = v.restrict i + w.restrict i

Proof state:
case pos
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
ext j hj

Result:
case pos.h
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((v + w).restrict i) j = ↑(v.restrict i + w.restrict i) j

Proof state:
case pos.h
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑((v + w).restrict i) j = ↑(v.restrict i + w.restrict i) j

Tactic:
simp [restrict_apply _ hi hj]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

case neg
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Proof state:
case neg
α : Type u_1
inst✝³ : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
simp [restrict_not_measurable _ hi]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp]
lemma biUnion_insert [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t :=
  ext fun x ↦ by
    simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or,
      exists_eq_left]

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
a : α
x : β
⊢ x ∈ (insert a s).biUnion t ↔ x ∈ t a ∪ s.biUnion t

Tactic:
simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or,
  exists_eq_left]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem finset_sup_apply [SemilatticeSup β] [OrderBot β] {f : γ → α →ₛ β} (s : Finset γ) (a : α) :
    s.sup f a = s.sup fun c => f c a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c => (f c) a✝¹
⊢ ((insert a s).sup f) a✝¹ = (insert a s).sup fun c => (f c) a✝¹

Tactic:
rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ (s.sup f) a = s.sup fun c => (f c) a

Tactic:
refine Finset.induction_on s rfl ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    a_1 ∉ s → ((s.sup f) a = s.sup fun c => (f c) a) → ((insert a_1 s).sup f) a = (insert a_1 s).sup fun c => (f c) a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ (s.sup f) a = s.sup fun c => (f c) a

Tactic:
classical
refine Finset.induction_on s rfl ?_
intro a s _ ih
rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    a_1 ∉ s → ((s.sup f) a = s.sup fun c => (f c) a) → ((insert a_1 s).sup f) a = (insert a_1 s).sup fun c => (f c) a

Tactic:
intro a s _ ih

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c => (f c) a✝¹
⊢ ((insert a s).sup f) a✝¹ = (insert a s).sup fun c => (f c) a✝¹
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
    m.isEmpty → ¬a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a : α
⊢ m.isEmpty = true → ¬a ∈ m

Tactic:
simpa [mem_iff_contains] using contains_of_isEmpty

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma ringHomComp_eq_one_iff {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
    χ.ringHomComp f = 1 ↔ χ = 1

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = 1 ↔ χ = 1

Tactic:
conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by ext; simp)]

Result:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1

Tactic:
exact (injective_ringHomComp hf).eq_iff

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ ringHomComp 1 f = 1

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
a✝ : Rˣ
⊢ (ringHomComp 1 f) ↑a✝ = 1 ↑a✝

Proof state:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
a✝ : Rˣ
⊢ (ringHomComp 1 f) ↑a✝ = 1 ↑a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem PreconnectedSpace.trivial_of_discrete [PreconnectedSpace X] [DiscreteTopology X] :
    Subsingleton X

Proof state:
case mk.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False

Tactic:
exact hxy (mem_univ x)

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
⊢ ¬Nontrivial X

Tactic:
rintro ⟨x, y, hxy⟩

Result:
case mk.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ False

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
⊢ Subsingleton X

Tactic:
rw [← not_nontrivial_iff_subsingleton]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
⊢ ¬Nontrivial X

Proof state:
case mk.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ False

Tactic:
rw [Ne, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy

Result:
case mk.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_rel {l : Array α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b)

Proof state:
case mk
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (Array.foldl (fun acc a => f acc a) a { toList := l }) (Array.foldl (fun acc a => g acc a) b { toList := l })

Tactic:
simpa using List.foldl_rel r h (by simpa using h')

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (Array.foldl (fun acc a => f acc a) a l) (Array.foldl (fun acc a => g acc a) b l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (Array.foldl (fun acc a => f acc a) a { toList := l }) (Array.foldl (fun acc a => g acc a) b { toList := l })