harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b = a - a ⊓ b

Tactic:
rcases le_total a b with h | h

Result:
case inl
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - a ⊓ b

case inr
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - a ⊓ b

Proof state:
case inr
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - a ⊓ b

Tactic:
rw [min_eq_right h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - a ⊓ b

Tactic:
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_iff_le_of_ge : IsAtom a ↔ a ≠ ⊥ ∧ ∀ b ≠ ⊥, b ≤ a → a ≤ b :=
  and_congr Iff.rfl <|
    forall_congr' fun b => by
      simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_le]

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b

Tactic:
simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Charpoly/BaseChange.lean
lemma LinearMap.det_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Module.Finite R M]
    {A} [CommRing A] [Algebra R A] (f : M →ₗ[R] M) :
    LinearMap.det (f.baseChange A) = algebraMap R A (LinearMap.det f)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Tactic:
nontriviality A

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
this : Nontrivial R
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Tactic:
rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
this : Nontrivial R
⊢ (-1) ^ Module.finrank A (TensorProduct R A M) * (baseChange A f).charpoly.coeff 0 =
    (algebraMap R A) ((-1) ^ Module.finrank R M * f.charpoly.coeff 0)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
this : Nontrivial R
⊢ (-1) ^ Module.finrank A (TensorProduct R A M) * (baseChange A f).charpoly.coeff 0 =
    (algebraMap R A) ((-1) ^ Module.finrank R M * f.charpoly.coeff 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Tactic:
have := (algebraMap R A).domain_nontrivial

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M →ₗ[R] M
a✝ : Nontrivial A
this : Nontrivial R
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)
-- Mathlib/Order/CompleteLattice.lean
lemma iInf₂_eq_bot (f : ∀ i, κ i → α) : ⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ b > ⊥, ∃ i j, f i j < b

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ b > ⊥, ∃ i j, f i j < b

Tactic:
simp_rw [iInf_psigma', iInf_eq_bot, PSigma.exists]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.HasSum.toNNReal {f : α → ℝ} {y : ℝ} (hf₀ : ∀ n, 0 ≤ f n)
    (hy : HasSum f y) : HasSum (fun x => Real.toNNReal (f x)) y.toNNReal

Proof state:
case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => (f x).toNNReal) (↑y).toNNReal

Tactic:
lift f to α → ℝ≥0 using hf₀

Result:
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => ((fun i => ↑(f i)) x).toNNReal) (↑y).toNNReal

Proof state:
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => ((fun i => ↑(f i)) x).toNNReal) (↑y).toNNReal

Tactic:
simpa [hasSum_coe] using hy

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y
⊢ HasSum (fun x => (f x).toNNReal) y.toNNReal

Tactic:
lift y to ℝ≥0 using hy.nonneg hf₀

Result:
case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => (f x).toNNReal) (↑y).toNNReal
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
theorem homotopyEquiv_hom_ι {X : C} (I J : InjectiveResolution X) :
    I.ι ≫ (homotopyEquiv I J).hom = J.ι

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ I.ι ≫ (I.homotopyEquiv J).hom = J.ι

Tactic:
simp [homotopyEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_take (a : Vector α n) (m : Nat) (hi : i < min n m) :
    (a.take m)[i] = a[i]

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
m : Nat
hi : i < min n m
⊢ (a.take m)[i] = a[i]

Tactic:
cases a

Result:
case mk
α : Type u_1
n i m : Nat
hi : i < min n m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.take m)[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
case mk
α : Type u_1
n i m : Nat
hi : i < min n m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.take m)[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Invariance.lean
theorem bind_add (μ ν : Measure α) (κ : Kernel α β) : (μ + ν).bind κ = μ.bind κ + ν.bind κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
⊢ (μ + ν).bind ⇑κ = μ.bind ⇑κ + ν.bind ⇑κ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
s : Set β
hs : MeasurableSet s
⊢ ((μ + ν).bind ⇑κ) s = (μ.bind ⇑κ + ν.bind ⇑κ) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
s : Set β
hs : MeasurableSet s
⊢ ((μ + ν).bind ⇑κ) s = (μ.bind ⇑κ + ν.bind ⇑κ) s

Tactic:
rw [Measure.bind_apply hs (Kernel.measurable _), lintegral_add_measure, Measure.coe_add,
  Pi.add_apply, Measure.bind_apply hs (Kernel.measurable _),
  Measure.bind_apply hs (Kernel.measurable _)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_iUnion_iff [Countable ι] (s : ι → Set α) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i, s i), p x) ↔ ∀ i, ∀ᵐ x ∂μ.restrict (s i), p x

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

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by
    rw [mul_assoc, ← h, inv_mul_cancel_right]⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
h : g ∈ H.normalizer
n : G
⊢ n * g ∈ H ↔ g * n ∈ H

Tactic:
rw [h, mul_assoc, mul_inv_cancel_right]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
h : ∀ (n : G), n * g ∈ H ↔ g * n ∈ H
n : G
⊢ n ∈ H ↔ g * n * g⁻¹ ∈ H

Tactic:
rw [mul_assoc, ← h, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem IsExtreme.trans (hAB : IsExtreme 𝕜 A B) (hBC : IsExtreme 𝕜 B C) :
    IsExtreme 𝕜 A C

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
⊢ IsExtreme 𝕜 A C

Tactic:
refine ⟨Subset.trans hBC.1 hAB.1, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C ∧ x₂ ∈ C

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C ∧ x₂ ∈ C

Tactic:
obtain ⟨hx₁B, hx₂B⟩ := hAB.2 hx₁A hx₂A (hBC.1 hxC) hx

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ C ∧ x₂ ∈ C

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ C ∧ x₂ ∈ C

Tactic:
exact hBC.2 hx₁B hx₂B hxC hx

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
lemma coe_le_coe {n m : ℕ} : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m

Proof state:
n m : ℕ
⊢ ↑n ≤ ↑m ↔ n ≤ m

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_neg_iff [LinearOrderedRing α] (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Tactic:
rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
  or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
  add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
  and_comm, Decidable.and_or_imp, or_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_eq_zeroLocus_compl (r : R) :
    (basicOpen r : Set (PrimeSpectrum R)) = (zeroLocus {r})ᶜ :=
  Set.ext fun x => by simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
    Set.singleton_subset_iff]

Proof state:
R : Type u
inst✝ : CommSemiring R
r : R
x : PrimeSpectrum R
⊢ x ∈ ↑(basicOpen r) ↔ x ∈ (zeroLocus {r})ᶜ

Tactic:
simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
Set.singleton_subset_iff]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp] lemma eq_ratCast [DivisionRing α] [FunLike F ℚ α] [RingHomClass F ℚ α] (f : F) (q : ℚ) :
    f q = q

Proof state:
F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = ↑q

Tactic:
rw [← map_ratCast f, Rat.cast_id]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} :
    UniformEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, UniformEquicontinuous (uα := u k) F

Proof state:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F

Tactic:
simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]

Result:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformContinuous (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), UniformContinuous (⇑ofFun ∘ swap F)

Proof state:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformContinuous (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), UniformContinuous (⇑ofFun ∘ swap F)

Tactic:
rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem VectorSpace.card_fintype [Fintype K] [Fintype V] : ∃ n : ℕ, card V = card K ^ n

Proof state:
K : Type u_3
V : Type u_4
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n

Tactic:
classical
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩

Result:
no goals

Proof state:
K : Type u_3
V : Type u_4
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n

Tactic:
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem update_inf [∀ i, SemilatticeInf (π i)] (f : ∀ i, π i) (i : ι) (a b : π i) :
    update f i (a ⊓ b) = update f i a ⊓ update f i b :=
  funext fun j => by obtain rfl | hji := eq_or_ne j i <;> simp [update_of_ne, *]

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeInf (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update f i (a ⊓ b) j = (update f i a ⊓ update f i b) j

Tactic:
obtain rfl | hji := eq_or_ne j i <;> simp [update_of_ne, *]

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
lemma predAbove_rev_right (p : Fin n) (i : Fin (n + 1)) :
    p.predAbove i.rev = (p.rev.predAbove i).rev

Proof state:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev

Tactic:
rw [predAbove_rev_left, rev_rev]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithTop.toDual_lt_toDual_iff {x y : WithTop α} :
    WithTop.toDual x < WithTop.toDual y ↔ y < x

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithTop α
⊢ WithTop.toDual x < WithTop.toDual y ↔ y < x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_ne_empty_iff {l : Array α} :
    mapIdx f l ≠ #[] ↔ l ≠ #[]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : Array α
⊢ mapIdx f l ≠ #[] ↔ l ≠ #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem comap_smul (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) (h : a ≠ 0) :
    p.comap (a • f) = p.comap f

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
⊢ comap (a • f) p = comap f p

Tactic:
ext b

Result:
case h
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p

Proof state:
case h
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p

Tactic:
simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem nonempty_iff_eq_singleton_default [Unique α] {s : Finset α} :
    s.Nonempty ↔ s = {default}

Proof state:
α : Type u_1
inst✝ : Unique α
s : Finset α
⊢ s.Nonempty ↔ s = {default}

Tactic:
simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem preimage_empty {f : α → β} : preimage ∅ f (by simp [InjOn]) = ∅ :=
  Finset.coe_injective (by simp)

Proof state:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' ↑∅)

Tactic:
simp [InjOn]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
⊢ ↑(∅.preimage f ⋯) = ↑∅

Tactic:
simp

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
/-- If `μ ≪ ν` and `μ univ = ν univ`, then `toReal` of the Kullback-Leibler divergence is equal to
an integral, without any integrability condition. -/
lemma toReal_klDiv_of_measure_eq (h : μ ≪ ν) (h_eq : μ univ = ν univ) :
    (klDiv μ ν).toReal = ∫ a, llr μ ν a ∂μ

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
simp [toReal_klDiv h h_int, h_eq]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
by_cases h_int : Integrable (llr μ ν) μ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : μ univ = ν univ
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.top_toReal]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_of_multiplicity_odd (m : ℤ) (hm : 0 < m) (p : ℕ) [hp : Fact p.Prime]
    (Hpv : multiplicity (p : ℤ) m % 2 = 1) :
    Irrational (√m) :=
  @irrational_nrt_of_n_not_dvd_multiplicity _ 2 _ (Ne.symm (ne_of_lt hm)) p hp
    (sq_sqrt (Int.cast_nonneg.2 <| le_of_lt hm)) (by rw [Hpv]; exact one_ne_zero)

Proof state:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ multiplicity (↑p) m % 2 ≠ 0

Tactic:
rw [Hpv]

Result:
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ 1 ≠ 0
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_apply_one : Λ 1 = 0

Proof state:
⊢ Λ 1 = 0

Tactic:
simp [vonMangoldt_apply]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem coe_closure_eq (s : Set R) :
    (closure s : Set R) = AddSubmonoid.closure (Subsemigroup.closure s : Set R)

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))

Tactic:
simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid,
  Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0))

Proof state:
w i : Nat
⊢ (1#w).getLsbD i = (decide (0 < w) && decide (i = 0))

Tactic:
simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]

Result:
w i : Nat
⊢ (decide (i < w) && Nat.testBit 1 i) = (decide (0 < w) && decide (i = 0))

Proof state:
w i : Nat
⊢ (decide (i < w) && Nat.testBit 1 i) = (decide (0 < w) && decide (i = 0))

Tactic:
by_cases h : i = 0
  <;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.extendDomain_apply_subtype {b : β'} (h : p b) :
    e.extendDomain f b = f (e (f.symm ⟨b, h⟩))

Proof state:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
b : β'
h : p b
⊢ (e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))

Tactic:
simp [Perm.extendDomain, h]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem IsUnit.isNilpotent_mul_unit_of_commute_iff [MonoidWithZero R] {r u : R}
    (hu : IsUnit u) (h_comm : Commute r u) :
    IsNilpotent (r * u) ↔ IsNilpotent r :=
  exists_congr fun n ↦ by rw [h_comm.mul_pow, (hu.pow n).mul_left_eq_zero]

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
r u : R
hu : IsUnit u
h_comm : Commute r u
n : ℕ
⊢ (r * u) ^ n = 0 ↔ r ^ n = 0

Tactic:
rw [h_comm.mul_pow, (hu.pow n).mul_left_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_toList (o : Option α) :
    o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList

Proof state:
α : Type u_1
o : Option α
⊢ o.toList.attach =
    (Option.map
        (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨a, ⋯⟩)
        o.attach).toList

Tactic:
cases o <;> simp

Result:
no goals

Proof state:
α : Type ?u.8307
o : Option α
x✝ : { x // x ∈ o }
a : α
h : a ∈ o
⊢ a ∈ o.toList

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {p p₁ p₂ : P}
    (h : (∡ p₁ p p₂).sign = 0) : p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π

Tactic:
convert o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a

Proof state:
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
h : 0 < n
⊢ findSome? f (mkArray n a) = f a

Tactic:
simp [findSome?_mkArray, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem div_mul_cancel (a b : G) : a / b * b = a

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a / b * b = a

Tactic:
rw [div_eq_mul_inv, inv_mul_cancel_right a b]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_lt_iff {d} :
    s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
@[parity_simps] lemma even_add_one : Even (n + 1) ↔ ¬Even n

Proof state:
n : ℕ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
simp [even_add]

Result:
no goals