harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.iUnion_of_reflTransGen {ι : Type*} {s : ι → Set α}
    (H : ∀ i, IsPreconnected (s i))
    (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) :
    IsPreconnected (⋃ n, s n)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
⊢ ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ univ) i j

Tactic:
simpa [mem_univ] using K i j

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ x ∈ univ, s x)

Tactic:
exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
  simpa [mem_univ] using K i j

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ n, s n)

Tactic:
rw [← biUnion_univ]

Result:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ x ∈ univ, s x)
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem embedding_comp_inv (j : Fin n) : c.embedding (c.index j) (c.invEmbedding j) = j

Proof state:
n : ℕ
c : Composition n
j : Fin n
⊢ (c.embedding (c.index j)) (c.invEmbedding j) = j

Tactic:
rw [Fin.ext_iff]

Result:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j

Proof state:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j

Tactic:
apply add_tsub_cancel_of_le (c.sizeUpTo_index_le j)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.isEmpty = false ↔ ∃ a, m.contains a = true

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.isEmpty = false ↔ ∃ a, m.contains a = true

Tactic:
simp_to_raw using Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem fold_congr {α : Type u} {n m : Nat} (w : n = m)
     (f : (i : Nat) → i < n → α → α) (init : α) :
     fold n f init = fold m (fun i h => f i (by omega)) init

Proof state:
α : Type u
n m : Nat
w : n = m
f : (i : Nat) → i < n → α → α
init : α
⊢ n.fold f init = m.fold (fun i h => f i ⋯) init

Tactic:
subst m

Result:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
init : α
⊢ n.fold f init = n.fold (fun i h => f i ⋯) init

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
init : α
⊢ n.fold f init = n.fold (fun i h => f i ⋯) init

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n m : Nat
w : n = m
f : (i : Nat) → i < n → α → α
init : α
i : Nat
h : i < m
⊢ i < n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_exp_comp_atTop {f : α → ℝ} :
    Tendsto (fun x => exp (f x)) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => rexp (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_def (A : Matrix m n α) :
    ‖A‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ (2 : ℝ)) ^ (1 / 2 : ℝ)

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖(WithLp.equiv 2 (m → WithLp 2 (n → α))).symm fun i => (WithLp.equiv 2 (n → α)).symm fun j => A i j‖₊ =
    (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two,
  WithLp.equiv_symm_pi_apply]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖₊ = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
change ‖(WithLp.equiv 2 _).symm fun i => (WithLp.equiv 2 _).symm fun j => A i j‖₊ = _

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖(WithLp.equiv 2 (m → WithLp 2 (n → α))).symm fun i => (WithLp.equiv 2 (n → α)).symm fun j => A i j‖₊ =
    (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
-- Mathlib/Analysis/Analytic/Composition.lean
theorem mem_compPartialSumTarget_iff {m M N : ℕ} {a : Σ n, Composition n} :
    a ∈ compPartialSumTarget m M N ↔
      m ≤ a.2.length ∧ a.2.length < M ∧ ∀ j : Fin a.2.length, a.2.blocksFun j < N

Proof state:
m M N : ℕ
a : (n : ℕ) × Composition n
⊢ a ∈ compPartialSumTarget m M N ↔ m ≤ a.snd.length ∧ a.snd.length < M ∧ ∀ (j : Fin a.snd.length), a.snd.blocksFun j < N

Tactic:
simp [compPartialSumTarget, compPartialSumTargetSet]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMap_prod_snd {p : TangentBundle (I.prod I') (M × M')} :
    tangentMap (I.prod I') I' Prod.snd p = ⟨p.proj.2, p.2.2⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ tangentMap (I.prod I') I' Prod.snd p = { proj := p.proj.2, snd := p.snd.2 }

Tactic:
simp [tangentMap]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd = p.snd.2

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd = p.snd.2

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma mul_prod_Ioi_eq_prod_Ici (a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Tactic:
rw [Ici_eq_cons_Ioi, prod_cons]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem comap_sup_eq_of_le_range {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
  map_injective_of_ker_le f ((ker_le_comap f H).trans le_sup_left) (ker_le_comap f (H ⊔ K))
    (by
      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)])

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))

Tactic:
rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
  inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coe_mul : ((φ * ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ * ψ :=
  MvPowerSeries.ext fun n => by
    classical
    simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R n) ↑(φ * ψ) = (MvPowerSeries.coeff R n) (↑φ * ↑ψ)

Tactic:
classical
simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R n) ↑(φ * ψ) = (MvPowerSeries.coeff R n) (↑φ * ↑ψ)

Tactic:
simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_erase (h : a ∈ s) : s \ t.erase a = insert a (s \ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ s
⊢ s \ t.erase a = insert a (s \ t)

Tactic:
rw [← sdiff_singleton_eq_erase, sdiff_sdiff_eq_sdiff_union (singleton_subset_iff.2 h), insert_eq,
  union_comm]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, there are open sets `U`,
`V` that separate `t` and `x`. -/
lemma IsCompact.separation_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
    ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Tactic:
simpa [SeparatedNhds] using SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton
  isClosed_singleton <| disjoint_singleton_right.mpr H2

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem _root_.Complex.oangle (w z : ℂ) :
    Complex.orientation.oangle w z = Complex.arg (conj w * z)

Proof state:
w z : ℂ
⊢ Complex.orientation.oangle w z = ↑((starRingEnd ℂ) w * z).arg

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Antivary.sum_smul_lt_sum_smul_comp_perm_iff (hfg : Antivary f g) :
    ∑ i, f i • g i < ∑ i, f i • g (σ i) ↔ ¬Antivary f (g ∘ σ)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f i • g (σ i) ↔ ¬Antivary f (g ∘ ⇑σ)

Tactic:
simp [(hfg.antivaryOn _).sum_smul_lt_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma prob_compl_le_one_sub_of_le_prob {p : ℝ≥0∞} (hμs : p ≤ μ s) (s_mble : MeasurableSet s) :
    μ sᶜ ≤ 1 - p

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst✝ : IsZeroOrProbabilityMeasure 0
hμs : p ≤ 0 s
⊢ 0 sᶜ ≤ 1 - p

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ μ s
s_mble : MeasurableSet s
⊢ μ sᶜ ≤ 1 - p

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst✝ : IsZeroOrProbabilityMeasure 0
hμs : p ≤ 0 s
⊢ 0 sᶜ ≤ 1 - p

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ μ sᶜ ≤ 1 - p

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ μ sᶜ ≤ 1 - p

Tactic:
simpa [prob_compl_eq_one_sub s_mble] using tsub_le_tsub_left hμs 1

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sq : sinh x ^ 2 = cosh x ^ 2 - 1

Proof state:
x : ℝ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)

Proof state:
x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)

Tactic:
simp [sinh_sq]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sigma_zero_apply (n : ℕ) : σ 0 n = #n.divisors

Proof state:
n : ℕ
⊢ (σ 0) n = #n.divisors

Tactic:
simp [sigma_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_cons {r : α → β} : relabel r (c :: f) = (c.relabel r) :: relabel r f

Proof state:
α : Type u_1
β : Type u_2
c : Clause α
f : List (Clause α)
r : α → β
⊢ relabel r (c :: f) = Clause.relabel r c :: relabel r f

Tactic:
simp [relabel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_replicate_iff {l₁ l₂ : List α} {a : α} :
    l₁ ++ l₂ = replicate n a ↔
      l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : List α
a : α
⊢ l₁ ++ l₂ = replicate n a ↔ l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

Tactic:
simp only [eq_replicate_iff, length_append, mem_append, true_and, and_congr_right_iff]

Result:
α : Type u_1
n : Nat
l₁ l₂ : List α
a : α
⊢ l₁.length + l₂.length = n →
    ((∀ (b : α), b ∈ l₁ ∨ b ∈ l₂ → b = a) ↔ (∀ (b : α), b ∈ l₁ → b = a) ∧ ∀ (b : α), b ∈ l₂ → b = a)

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : List α
a : α
⊢ l₁.length + l₂.length = n →
    ((∀ (b : α), b ∈ l₁ ∨ b ∈ l₂ → b = a) ↔ (∀ (b : α), b ∈ l₁ → b = a) ∧ ∀ (b : α), b ∈ l₂ → b = a)

Tactic:
exact fun _ =>
  { mp := fun h => ⟨fun b m => h b (Or.inl m), fun b m => h b (Or.inr m)⟩,
    mpr := fun h b x => Or.casesOn x (fun m => h.left b m) fun m => h.right b m }

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
    (concat x a) &&& (concat y b) = concat (x &&& y) (a && b)

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ x.concat a &&& y.concat b = (x &&& y).concat (a && b)

Tactic:
ext (_ | i) h <;> simp [getLsbD_concat]

Result:
no goals
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem Matrix.lie_transpose (A B : Matrix n n R) : ⁅A, B⁆ᵀ = ⁅Bᵀ, Aᵀ⁆ :=
  show (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ by simp

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A B : Matrix n n R
⊢ (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_sub_left_lt {a b c : Int} (h : a - b < c) : a < b + c

Proof state:
a b c : Int
h : a - b < c
⊢ a < b + c

Tactic:
have h := Int.add_lt_add_right h b

Result:
a b c : Int
h✝ : a - b < c
h : a - b + b < c + b
⊢ a < b + c

Proof state:
a b c : Int
h✝ : a - b < c
h : a - b + b < c + b
⊢ a < b + c

Tactic:
rwa [Int.sub_add_cancel, Int.add_comm] at h

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
lemma integral_indicator₂ (f : α → β → E) (s : Set α) (a : α) :
    ∫ y, s.indicator (f · y) a ∂κ a = s.indicator (fun x ↦ ∫ y, f x y ∂κ x) a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
⊢ ∫ (y : β), s.indicator (fun x => f x y) a ∂κ a = s.indicator (fun x => ∫ (y : β), f x y ∂κ x) a

Tactic:
by_cases ha : a ∈ s <;> simp [ha]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma cauchy_map_iff_tendsto_swapped (𝓕 : Filter ι) (f : ι → G) :
    Cauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Proof state:
ι : Type u_3
G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝓕 : Filter ι
f : ι → G
⊢ Cauchy (map f 𝓕) ↔ 𝓕.NeBot ∧ Tendsto (fun p => f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [cauchy_map_iff, uniformity_eq_comap_nhds_one, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_eraseP_of_neg {l : Array α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
pa : ¬p a = true
⊢ a ∈ l.eraseP p ↔ a ∈ l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : List α
⊢ a ∈ { toList := l }.eraseP p ↔ a ∈ { toList := l }

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : List α
⊢ a ∈ { toList := l }.eraseP p ↔ a ∈ { toList := l }

Tactic:
simpa using List.mem_eraseP_of_neg pa

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem im_star : star a.im = -a.im

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a.im = -a.im

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
  | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true, Nat.succ_ne_zero]
  | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
  | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)

Proof state:
a b : Nat
h : a.succ < b.succ
⊢ b.succ - a.succ ≠ 0

Tactic:
rw [Nat.succ_sub_succ]

Result:
a b : Nat
h : a.succ < b.succ
⊢ b - a ≠ 0

Proof state:
b : Nat
x✝ : 0 < b.succ
⊢ b.succ - 0 ≠ 0

Tactic:
simp only [Nat.sub_zero, ne_eq, not_false_eq_true, Nat.succ_ne_zero]

Result:
no goals

Proof state:
a b : Nat
h : a.succ < b.succ
⊢ b - a ≠ 0

Tactic:
exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_left_comm : Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Tactic:
simp_rw [disjoint_iff_inf_le, inf_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
    (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
a : Option α
b : Option β
⊢ (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y

Tactic:
cases a <;> cases b <;> rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma frontier_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
    frontier (range (𝓡∂ n)) = { y | 0 = y 0 }

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ frontier (range ↑(𝓡∂ n)) = frontier {y | 0 ≤ y 0}

Tactic:
congr!

Result:
case h.e'_3
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y 0}

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ frontier (range ↑(𝓡∂ n)) = {y | 0 = y 0}

Tactic:
calc frontier (range (𝓡∂ n))
  _ = frontier ({ y | 0 ≤ y 0 }) := by
    congr!
    apply range_euclideanHalfSpace
  _ = { y | 0 = y 0 } := frontier_halfSpace 2 _ _

Result:
no goals

Proof state:
case h.e'_3
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y 0}

Tactic:
apply range_euclideanHalfSpace

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem mem_iff (s : Set β) (x : β) : x ∈ l s ↔ ∀ S : α, s ⊆ S → x ∈ S

Proof state:
α : Type u_1
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ l.toFun {x} ≤ l.toFun s ↔ ∀ (S : α), l.toFun s ≤ S → l.toFun {x} ≤ S

Tactic:
exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ x ∈ l.toFun s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S

Tactic:
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]

Result:
α : Type u_1
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ l.toFun {x} ≤ l.toFun s ↔ ∀ (S : α), l.toFun s ≤ S → l.toFun {x} ≤ S
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_ofFn [CommMonoid β] {n : ℕ} (f : Fin n → β) : (List.ofFn f).prod = ∏ i, f i

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin n → β
⊢ (List.ofFn f).prod = ∏ i : Fin n, f i

Tactic:
simp [prod_eq_multiset_prod]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem gen_mem_nhds (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈
    ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ 𝓝 f

Tactic:
rw [UniformOnFun.nhds_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈
    ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_zero_isSolvable : IsSolvable (0 : F[X]).Gal

Proof state:
F : Type u_1
inst✝ : Field F
⊢ IsSolvable (Gal 0)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma indep_iff_forall_subset_not_isCircuit (hI : I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Tactic:
rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem coinduced_nhdsAdjoint (f : α → β) (a : α) (l : Filter α) :
    coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l) :=
  eq_of_forall_ge_iff fun _ ↦ by
    rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]

Proof state:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ coinduced f (nhdsAdjoint a l) ≤ x✝ ↔ nhdsAdjoint (f a) (map f l) ≤ x✝

Tactic:
rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_Ioc_mul_eq_prod_Icc (h : a ≤ b) : (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ioc_eq_prod_Icc h]

Result:
no goals