harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/Lemmas.lean
theorem char_ne_zero_of_finite (p : ℕ) [CharP R p] [Finite R] : p ≠ 0

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False

Tactic:
cases nonempty_fintype R

Result:
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False

Tactic:
haveI : CharZero R := charP_to_charZero R

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False

Proof state:
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False

Tactic:
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists'_reverse (l : List α) : sublists' (reverse l) = map reverse (sublists l)

Proof state:
α : Type u
l : List α
⊢ l.reverse.sublists' = map reverse l.sublists

Tactic:
simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem nhdsSet_Ico (h : a < b) : 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem length_takeUntil_le {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.takeUntil u h).length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
have := congr_arg Walk.length (p.take_spec h)

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
rw [length_append] at this

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
exact Nat.le.intro this

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_add_cosh : sinh x + cosh x = exp x

Proof state:
x : ℂ
⊢ sinh x + cosh x = cexp x

Tactic:
rw [add_comm, cosh_add_sinh]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma sup_image₂_left (g : γ → δ) : sup (image₂ f s t) g = sup s fun x ↦ sup t (g <| f x ·)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1)

Tactic:
simp only [image₂, sup_image, sup_product_left]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i => t.sup fun i' => (g ∘ uncurry f) (i, i')) = s.sup fun x => t.sup fun x_1 => g (f x x_1)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i => t.sup fun i' => (g ∘ uncurry f) (i, i')) = s.sup fun x => t.sup fun x_1 => g (f x x_1)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_add_zero_hom_app (a : A) (X : C) :
    (shiftFunctorAdd' C a 0 a (add_zero a)).hom.app X =
    (shiftFunctorZero C A).inv.app (X⟦a⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).hom.app X = (shiftFunctorZero C A).inv.app ((shiftFunctor C a).obj X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_add_zero C a)) X

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Defs.lean
theorem sub_mem_iff_right (hx : x ∈ p) : x - y ∈ p ↔ y ∈ p

Proof state:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n

Proof state:
m n k : Nat
⊢ m.gcd (n + k * m) = m.gcd n

Tactic:
simp [gcd_rec m (n + k * m), gcd_rec m n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      { toList := xs }.zipIdx

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      { toList := xs }.zipIdx

Tactic:
simp [List.findIdx?_eq_findSome?_zipIdx]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_mul_eq_one [MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) :
    f a * f b = 1

Proof state:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f a * f b = 1

Tactic:
rw [← map_mul, h, map_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
lemma mulVec_eigenvectorBasis (j : n) :
    A *ᵥ ⇑(hA.eigenvectorBasis j) = (hA.eigenvalues j) • ⇑(hA.eigenvectorBasis j)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
j : n
⊢ A *ᵥ (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j) =
    hA.eigenvalues j • (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)

Tactic:
simpa only [eigenvectorBasis, OrthonormalBasis.reindex_apply, toEuclideanLin_apply,
  RCLike.real_smul_eq_coe_smul (K := 𝕜)] using
    congr(⇑$((isHermitian_iff_isSymmetric.1 hA).apply_eigenvectorBasis
      finrank_euclideanSpace ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm j)))

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q z = 0) :
    W'.addXYZ P Q = -(Q x * P z) • P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addXYZ P Q = -(Q x * P z) • P

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
  addZ_of_Z_eq_zero_right hQz, smul_fin3]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem mk_toWord : ∀ {x : FreeGroup α}, mk (toWord x) = x

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
exact reduce.self

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {x : FreeGroup α}, mk x.toWord = x

Tactic:
rintro ⟨L⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem lift_aequiv {U : Type*} [CommRing U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f)
    (i : R →+* U) (x hx z) : h'.lift i x hx (h.aequiv h' z) = h.lift i x hx z

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : R[X]
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
U : Type u_2
inst✝ : CommRing U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
⊢ (lift i x h' hx) ((h.aequiv h') z) = (lift i x h hx) z

Tactic:
rw [← h.map_repr z, aequiv_map, lift_map, lift_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_apply_eq_iff_map_symm_apply_eq (e : α ≃ᵐ β) : μ.map e = ν ↔ μ = ν.map e.symm

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
e : α ≃ᵐ β
⊢ map (⇑e) μ = ν ↔ μ = map (⇑e.symm) ν

Tactic:
rw [← (map_measurableEquiv_injective e).eq_iff, map_map_symm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem natCast_inj {m n : ℕ} {R : Type*} [Semiring R] [CharZero R] :
    (↑m : R[X]) = ↑n ↔ m = n

Proof state:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n

Tactic:
apply_fun fun p => p.coeff 0 at h

Result:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Proof state:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

Tactic:
intro h

Result:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n

Proof state:
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
constructor

Result:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Proof state:
case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl

Result:
case mpr
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m

Proof state:
case mpr
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma liftCycles_i {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
    (hk : k ≫ K.d i j = 0) : K.liftCycles k j hj hk ≫ K.iCycles i = k

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ (K.sc i).liftCycles k ⋯ ≫ (K.sc i).iCycles = k

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ K.liftCycles k j hj hk ≫ K.iCycles i = k

Tactic:
dsimp [liftCycles, iCycles]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ (K.sc i).liftCycles k ⋯ ≫ (K.sc i).iCycles = k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_filter_not_isEmpty {L : Array (Array α)} :
    flatten (L.filter fun l => !l.isEmpty) = L.flatten

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (filter (fun l => !l.isEmpty) (List.map List.toArray xss✝).toArray).flatten =
    (List.map List.toArray xss✝).toArray.flatten

Tactic:
simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ (filter (fun l => !l.isEmpty) L).flatten = L.flatten

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (filter (fun l => !l.isEmpty) (List.map List.toArray xss✝).toArray).flatten =
    (List.map List.toArray xss✝).toArray.flatten
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_cons₁_fst (x : α) (xs ys) :
    (suffixLevenshtein C (x :: xs) ys).1 =
      levenshtein C (x :: xs) ys ::
        (suffixLevenshtein C xs ys).1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
ys : List β
⊢ (suffixLevenshtein C (x :: xs) ys).val = levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val

Tactic:
simp [suffixLevenshtein_cons₁]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem count_toList [BEq α] (as : Array α) (a : α) : as.toList.count a = as.count a

Proof state:
α : Type u_1
inst✝ : BEq α
as : Array α
a : α
⊢ List.count a as.toList = count a as

Tactic:
cases as

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ List.count a { toList := toList✝ }.toList = count a { toList := toList✝ }

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ List.count a { toList := toList✝ }.toList = count a { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertManyIfNewUnit_list_singleton {k : α} (h : m.WF) :
    insertManyIfNewUnit m [k] = m.insertIfNew k ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
k : α
h : m.WF
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ [k]).val.val = (Raw₀.insertIfNew ⟨m, ⋯⟩ k ()).val

Tactic:
rw [Raw₀.Const.insertManyIfNewUnit_list_singleton]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
k : α
h : m.WF
⊢ insertManyIfNewUnit m [k] = m.insertIfNew k ()

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
k : α
h : m.WF
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ [k]).val.val = (Raw₀.insertIfNew ⟨m, ⋯⟩ k ()).val
-- Mathlib/Algebra/Group/End.lean
theorem swap_mul_eq_mul_swap (f : Perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
  Equiv.ext fun z => by
    simp only [Perm.mul_apply, swap_apply_def]
    split_ifs <;>
      simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)

Tactic:
split_ifs <;>
  simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (swap x y * f) z = (f * swap (f⁻¹ x) (f⁻¹ y)) z

Tactic:
simp only [Perm.mul_apply, swap_apply_def]

Result:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.ofBijective_coeLinearMap_of_ne (h : IsInternal A)
    {i j : ι} (hij : i ≠ j) (x : A i) :
    (LinearEquiv.ofBijective (coeLinearMap A) h).symm x j = 0

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) j = 0

Tactic:
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_of_ne i j _ hij]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_eq_subtypeClosure (M : Matroid α) (X : Set α) :
    M.closure X = M.subtypeClosure ⟨X ∩ M.E, inter_subset_right⟩

Proof state:
α : Type u_2
M : Matroid α
X : Set α
this :
  ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
⊢ M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

Tactic:
simpa [closure, subtypeClosure, Set.ext_iff]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a

Tactic:
exact fun x ↦ ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩,
  fun ⟨_, h⟩ F hF hXF ↦ h F hF.subset_ground hXF hF⟩

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

Tactic:
suffices ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔
  (x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a) by
  simpa [closure, subtypeClosure, Set.ext_iff]

Result:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
-- Mathlib/Data/Finite/Card.lean
theorem Finite.card_pos_iff [Finite α] : 0 < Nat.card α ↔ Nonempty α

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem Submodule.finrank_le_one_iff_isPrincipal
    (W : Submodule K V) [Module.Free K W] [Module.Finite K W] :
    finrank K W ≤ 1 ↔ W.IsPrincipal

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
W : Submodule K V
inst✝¹ : Free K ↥W
inst✝ : Module.Finite K ↥W
⊢ finrank K ↥W ≤ 1 ↔ W.IsPrincipal

Tactic:
rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_zero_iff_oangle_rev_eq_zero {x y : V} : o.oangle x y = 0 ↔ o.oangle y x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = 0 ↔ o.oangle y x = 0

Tactic:
rw [oangle_rev, neg_eq_zero]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem iSup_div (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) / a = ⨆ i, f i / a

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ i, f i) / a = ⨆ i, f i / a

Tactic:
simp only [div_eq_mul_inv, iSup_mul]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem Q_succ (q : ℕ) : (Q (q + 1) : K[X] ⟶ _) = Q q - P q ≫ Hσ q

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q (q + 1) = Q q - P q ≫ Hσ q

Tactic:
simp only [Q, P_succ, comp_add, comp_id]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q

Tactic:
abel

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem OrderTop.upperBounds_univ [PartialOrder γ] [OrderTop γ] :
    upperBounds (univ : Set γ) = {⊤}

Proof state:
γ : Type v
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}

Tactic:
rw [isGreatest_univ.upperBounds_eq, Ici_top]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsLE {a : H} : Tendsto Inv.inv (𝓝[≤] a) (𝓝[≥] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))

Tactic:
simp [tendsto_principal_principal]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sSup_emptyset [Inhabited s] :
    sSup (∅ : Set s) = default

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
⊢ sSup ∅ = default

Tactic:
simp [sSup]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem zero_testAgainstNN : (0 : FiniteMeasure Ω).testAgainstNN = 0

Proof state:
case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
x✝ : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 x✝ = 0 x✝

Tactic:
simp only [zero_testAgainstNN_apply, Pi.zero_apply]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
⊢ testAgainstNN 0 = 0

Tactic:
funext

Result:
case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
x✝ : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 x✝ = 0 x✝
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem card [NeZero n] : Fintype.card (DihedralGroup n) = 2 * n

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n

Tactic:
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
    (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j]

Proof state:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
j : Nat
v : α
hj : j < a.size
h : i ≠ j
⊢ (a.set i v hi)[j] = a[j]

Tactic:
simp only [set, ← getElem_toList, List.getElem_set_ne h]

Result:
no goals

Proof state:
α : Type ?u.476082
a : Array α
i : Nat
hi : i < a.size
j : Nat
v : α
hj : j < a.size
h : i ≠ j
⊢ j < (a.set i v hi).size

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_eq_finrank_span_cols (A : Matrix m n R) :
    A.rank = finrank R (Submodule.span R (Set.range Aᵀ))

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : Fintype n
inst✝ : CommRing R
A : Matrix m n R
⊢ A.rank = finrank R ↥(Submodule.span R (Set.range Aᵀ))

Tactic:
rw [rank, Matrix.range_mulVecLin]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
@[simp] lemma div_modEq_div (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD (p * c)]

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a b c p : α
hc : c ≠ 0
⊢ a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]

Tactic:
simp [ModEq, ← sub_div, div_eq_iff hc, mul_assoc]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_one : √x = 1 ↔ x = 1 :=
  calc
    √x = 1 ↔ 1 * 1 = x := sqrt_eq_iff_mul_self_eq_of_pos zero_lt_one
    _ ↔ x = 1

Proof state:
x : ℝ
⊢ 1 * 1 = x ↔ x = 1

Tactic:
rw [eq_comm, mul_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem stirlingSeq'_pos (n : ℕ) : 0 < stirlingSeq (n + 1)

Proof state:
n : ℕ
⊢ 0 < ↑(n + 1)! / (√(2 * ↑(n + 1)) * (↑(n + 1) / rexp 1) ^ (n + 1))

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < stirlingSeq (n + 1)

Tactic:
unfold stirlingSeq

Result:
n : ℕ
⊢ 0 < ↑(n + 1)! / (√(2 * ↑(n + 1)) * (↑(n + 1) / rexp 1) ^ (n + 1))
-- Mathlib/Dynamics/BirkhoffSum/Basic.lean
theorem Function.IsFixedPt.birkhoffSum_eq {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M)
    (n : ℕ) : birkhoffSum f g n x = n • g x

Proof state:
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
⊢ birkhoffSum f g n x = n • g x

Tactic:
simp [birkhoffSum, (h.iterate _).eq]

Result:
no goals