harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem tendsto_card_le_div''_aux {X : Set E} (hX : ∀ ⦃x⦄ ⦃r:ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
    {F : E → ℝ} (hF₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * (F x)) {c : ℝ} (hc : 0 < c) :
    c • {x ∈ X | F x ≤ 1} = {x ∈ X | F x ≤ c ^ card ι}

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ x ∈ c • {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
simp_rw [Set.mem_smul_set_iff_inv_smul_mem₀ hc.ne', Set.mem_setOf_eq, hF₁ _
  (inv_pos_of_pos hc).le, inv_pow, inv_mul_le_iff₀ (pow_pos hc _), mul_one, and_congr_left_iff]

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ F x ≤ c ^ card ι → (c⁻¹ • x ∈ X ↔ x ∈ X)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
⊢ c • {x | x ∈ X ∧ F x ≤ 1} = {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ x ∈ c • {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ F x ≤ c ^ card ι → (c⁻¹ • x ∈ X ↔ x ∈ X)

Tactic:
exact fun _ ↦ ⟨fun h ↦ (smul_inv_smul₀ hc.ne' x) ▸ hX h hc, fun h ↦ hX h (inv_pos_of_pos hc)⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
    B * A⁻¹ = C ↔ B = C * A :=
  ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible],
   fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B C : Matrix n n α
inst✝ : Invertible A
h : B = C * A
⊢ B * A⁻¹ = C

Tactic:
rw [h, mul_inv_cancel_right_of_invertible]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B C : Matrix n n α
inst✝ : Invertible A
h : B * A⁻¹ = C
⊢ B = C * A

Tactic:
rw [← h, inv_mul_cancel_right_of_invertible]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem fromRel_ne : fromRel (fun (_ _ : α) z => z.symm : Symmetric Ne) = {z | ¬IsDiag z}

Proof state:
case h
α : Type u_1
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ z ∈ {z | ¬z.IsDiag}

Tactic:
exact z.ind (by simp)

Result:
no goals

Proof state:
α : Type u_1
z : Sym2 α
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯ ↔ s(x, y) ∈ {z | ¬z.IsDiag}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ fromRel ⋯ = {z | ¬z.IsDiag}

Tactic:
ext z

Result:
case h
α : Type u_1
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ z ∈ {z | ¬z.IsDiag}
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem mem_pregroupoid_of_eqOnSource (PG : Pregroupoid H) {e e' : PartialHomeomorph H H}
    (he' : e ≈ e') (he : PG.property e e.source) : PG.property e' e'.source

Proof state:
H : Type u
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : PartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e) e.source
⊢ PG.property (↑e') e.source

Tactic:
exact PG.congr e.open_source he'.eqOn.symm he

Result:
no goals

Proof state:
H : Type u
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : PartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e) e.source
⊢ PG.property (↑e') e'.source

Tactic:
rw [← he'.1]

Result:
H : Type u
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : PartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e) e.source
⊢ PG.property (↑e') e.source
-- Mathlib/Data/List/Permutation.lean
theorem map_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :
    (permutationsAux2 t ts [] ys id).2.map f = (permutationsAux2 t ts [] ys f).2

Proof state:
case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys ?f').2 = (permutationsAux2 t ts [] ys f).2

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).2 = (permutationsAux2 t ts [] ys f).2

Tactic:
rw [map_permutationsAux2' id, map_id, map_id]

Result:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys ?f').2 = (permutationsAux2 t ts [] ys f).2

case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β

case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = ?f' (map id a)
-- Mathlib/Topology/PartialHomeomorph.lean
theorem map_subtype_source {x : s} (hxe : (x : X) ∈ e.source) :
    e x ∈ (e.subtypeRestr hs).target

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ ↑e.symm ⁻¹' (s.partialHomeomorphSubtypeCoe hs).target

Tactic:
rw [s.partialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s

Tactic:
exact x.prop

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ (e.subtypeRestr hs).target

Tactic:
refine ⟨e.map_source hxe, ?_⟩

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ ↑e.symm ⁻¹' (s.partialHomeomorphSubtypeCoe hs).target
-- Mathlib/Data/List/Sort.lean
theorem sorted_mergeSort' (l : List α) : Sorted r (mergeSort l (r · ·))

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), ((fun x1 x2 => decide (r x1 x2)) a b || (fun x1 x2 => decide (r x1 x2)) b a) = true

Tactic:
simpa using total_of r

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ (fun x1 x2 => decide (r x1 x2)) x✝² x✝¹ = true →
    (fun x1 x2 => decide (r x1 x2)) x✝¹ x✝ = true → (fun x1 x2 => decide (r x1 x2)) x✝² x✝ = true

Tactic:
simpa using trans_of r

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b

Proof state:
a b : Int
⊢ a ∣ -b ↔ a ∣ b

Tactic:
constructor <;> exact fun ⟨k, e⟩ =>
  ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩

Result:
no goals

Proof state:
a b : Int
x✝ : a ∣ b
k : Int
e : b = a * k
⊢ -b = a * -k

Tactic:
simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v}) :
    sInf (range f)ᶜ < lift.{v} (succ #ι).ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
exact card_sInf_range_compl_le_lift f

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < lift.{v, u} (succ #ι).ord

Tactic:
rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_lt_of_mem_ball' (h : b ∈ ball a r) : ‖b‖ < ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans_lt <| add_lt_add_left (by rwa [← dist_eq_norm_div]) _

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ ball a r
⊢ ‖b / a‖ < r

Tactic:
rwa [← dist_eq_norm_div]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_comm (n m : ℕ) : dist n m = dist m n

Proof state:
n m : ℕ
⊢ n.dist m = m.dist n

Tactic:
simp [dist, add_comm]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma F_nat_zero_le {a : ℝ} (ha : 0 ≤ a) {t : ℝ} (ht : 0 < t) :
    ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
rw [← Real.exp_nat_mul, ← Real.exp_add]

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t + ↑n * (-π * t))

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ g_nat 0 a t n = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
simp only [g_nat]

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Proof state:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ g_nat 0 a t = fun i => rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ g_nat 0 a t n = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 0 a t) (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Result:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ g_nat 0 a t = fun i => rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t + ↑n * (-π * t))

Tactic:
ring_nf

Result:
no goals

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 0 ha ht)

Result:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 0 a t) (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_neg (n : ℤ) : W.Ψ (-n) = -W.Ψ n

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.Ψ (-n) = -W.Ψ n

Tactic:
simp only [Ψ, preΨ_neg, C_neg, neg_mul (α := R[X][Y]), even_neg]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_eq_one_iff : sign a = 1 ↔ 0 < a

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = 1
⊢ 0 < a

Tactic:
by_contra hn

Result:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = 1
hn : ¬0 < a
⊢ False

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False

Tactic:
split_ifs at h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
⊢ sign a = 1 ↔ 0 < a

Tactic:
refine ⟨fun h => ?_, fun h => sign_pos h⟩

Result:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = 1
⊢ 0 < a

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = 1
hn : ¬0 < a
⊢ False

Tactic:
rw [sign_apply, if_neg hn] at h

Result:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The two-variable Jacobi theta function is periodic in `z` with period 1. -/
lemma jacobiTheta₂_add_left (z τ : ℂ) : jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Result:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ

Proof state:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
  exp_int_mul_two_pi_mul_I, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem get_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α} {h} :
    l.get a h = getValue a l.toList (contains_eq.symm.trans h)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : AssocList α fun x => β
a : α
h : contains a l = true
⊢ get a l h = getValue a l.toList ⋯

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
h : contains a nil = true
⊢ get a nil h = getValue a nil.toList ⋯

case cons
α : Type u
β : Type v
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, get a tail✝ h = getValue a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ get a (cons key✝ value✝ tail✝) h = getValue a (cons key✝ value✝ tail✝).toList ⋯

Proof state:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
h : contains a nil = true
⊢ get a nil h = getValue a nil.toList ⋯

Tactic:
simp [contains] at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
t : AssocList α fun x => β
ih : ∀ {h : contains a t = true}, get a t h = getValue a t.toList ⋯
h : contains a (cons k v t) = true
⊢ get a (cons k v t) h = getValue a (cons k v t).toList ⋯

Tactic:
simp only [get, toList_cons, List.getValue_cons, ih]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : ∀ {h : contains a tail✝ = true}, get a tail✝ h = getValue a tail✝.toList ⋯
h : contains a (cons key✝ value✝ tail✝) = true
⊢ get a (cons key✝ value✝ tail✝) h = getValue a (cons key✝ value✝ tail✝).toList ⋯

Tactic:
next k v t ih => simp only [get, toList_cons, List.getValue_cons, ih]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem mapRange_neLocus_eq [DecidableEq N] [DecidableEq M] [Zero M] [Zero N] (f g : α →₀ N)
    {F : N → M} (F0 : F 0 = 0) (hF : Function.Injective F) :
    (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a✝ : α
⊢ a✝ ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a✝ ∈ f.neLocus g

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a✝ : α
⊢ a✝ ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a✝ ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus] using hF.ne_iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
    decide (y ∈ a :: l) = (y == a || decide (y ∈ l))

Proof state:
α : Type u_1
a y : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
⊢ decide (y ∈ a :: l) = (y == a || decide (y ∈ l))

Tactic:
cases h : y == a <;> simp_all

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@[simp]
lemma isDynCoverOf_empty {T : X → X} {U : Set (X × X)} {n : ℕ} {s : Set X} :
    IsDynCoverOf T ∅ U n s

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Set X
⊢ IsDynCoverOf T ∅ U n s

Tactic:
simp only [IsDynCoverOf, empty_subset]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem final_of_isTerminal_colimit_comp_yoneda
    (h : IsTerminal (colimit (F ⋙ yoneda))) : Final F

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}

Tactic:
refine Types.isTerminalEquivIsoPUnit _ ?_

Result:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
b : IsTerminal (((evaluation Dᵒᵖ (Type v)).obj (op d)).obj (colimit (F ⋙ yoneda))) :=
  IsTerminal.isTerminalObj ((evaluation Dᵒᵖ (Type v)).obj (op d)) (colimit (F ⋙ yoneda)) h
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))

Tactic:
exact b.ofIso <| preservesColimitIso ((evaluation _ _).obj (Opposite.op d)) (F ⋙ yoneda)

Result:
no goals

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
⊢ F.Final

Tactic:
refine final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)

Result:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))

Tactic:
let b := IsTerminal.isTerminalObj ((evaluation _ _).obj (Opposite.op d)) _ h

Result:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
b : IsTerminal (((evaluation Dᵒᵖ (Type v)).obj (op d)).obj (colimit (F ⋙ yoneda))) :=
  IsTerminal.isTerminalObj ((evaluation Dᵒᵖ (Type v)).obj (op d)) (colimit (F ⋙ yoneda)) h
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))
-- Mathlib/Data/Matroid/Loop.lean
lemma map_loops {f : α → β} {hf : InjOn f M.E} : (M.map f hf).loops = f '' M.loops

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).loops = f '' M.loops

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma le_algebraMap_iff_spectrum_le {r : R} {a : A} (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.819652) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ cfc id a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

Tactic:
exact cfc_le_algebraMap_iff id r a

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.819652) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

Tactic:
nth_rw 1 [← cfc_id R a]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.819652) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ cfc id a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem lintegral_prod_symm [SFinite μ] (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
    ∫⁻ z, f z ∂μ.prod ν = ∫⁻ y, ∫⁻ x, f (x, y) ∂μ ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
exact lintegral_prod _ hf.prod_swap

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
simp_rw [← lintegral_prod_swap f]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem neg_neg {X Y : C} (a : X ⟶ Y) : - -a = a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a - (0 - a) = a

Tactic:
rw [sub_sub_sub, sub_zero, sub_self, sub_zero]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a

Tactic:
conv_lhs =>
  congr; rw [← sub_self a]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a - (0 - a) = a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ - -a = a

Tactic:
rw [neg_def, neg_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_iff_append {a : α} {l : Array α} : a ∈ l ↔ ∃ s t : Array α, l = s.push a ++ t :=
  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩

Proof state:
α : Type u_1
a : α
l : Array α
x✝ : ∃ s t, l = s.push a ++ t
s t : Array α
e : l = s.push a ++ t
⊢ a ∈ s.push a ++ t

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_one : count p 1 = if p 0 then 1 else 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0

Tactic:
simp [count_succ]

Result:
no goals