harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Ring/Cast.lean
lemma cast_mono : Monotone (Int.cast : ℤ → R)

Proof state:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
rw [← sub_nonneg] at h

Result:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : 0 ≤ n - m
⊢ ↑m ≤ ↑n

Proof state:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : 0 ≤ n - m
⊢ ↑m ≤ ↑n

Tactic:
lift n - m to ℕ using h with k hk

Result:
case intro
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n

Proof state:
case intro
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k

Tactic:
exact k.cast_nonneg'

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
⊢ Monotone Int.cast

Tactic:
intro m n h

Result:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n

Proof state:
case intro
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n

Tactic:
rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]

Result:
case intro
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_congr {f g : α → Prop} [DecidablePred f] [DecidablePred g]
    (h : ∀ a, f a ↔ g a):
    guard f = guard g

Proof state:
α : Type u_1
f g : α → Prop
inst✝¹ : DecidablePred f
inst✝ : DecidablePred g
h : ∀ (a : α), f a ↔ g a
⊢ guard f = guard g

Tactic:
funext a

Result:
case h
α : Type u_1
f g : α → Prop
inst✝¹ : DecidablePred f
inst✝ : DecidablePred g
h : ∀ (a : α), f a ↔ g a
a : α
⊢ guard f a = guard g a

Proof state:
case h
α : Type u_1
f g : α → Prop
inst✝¹ : DecidablePred f
inst✝ : DecidablePred g
h : ∀ (a : α), f a ↔ g a
a : α
⊢ guard f a = guard g a

Tactic:
simp [guard, h]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_pos (n : ℕ) : 0 < minFac n

Proof state:
n : ℕ
⊢ 0 < n.minFac

Tactic:
by_cases n1 : n = 1

Result:
case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Proof state:
case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
exact (minFac_prime n1).pos

Result:
no goals

Proof state:
case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

Tactic:
simp [n1]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_univ (s s' : Set α) : Set.ite univ s s' = s

Proof state:
α : Type u
s s' : Set α
⊢ univ.ite s s' = s

Tactic:
simp [Set.ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_filterₘ {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
    Perm (toListModel (m.filterₘ f).1.buckets)
      ((toListModel m.1.buckets).filter fun p => f p.1 p.2) :=
  toListModel_updateAllBuckets AssocList.toList_filter (by simp)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
f : (a : α) → β a → Bool
⊢ ∀ {l l' : List ((a : α) × β a)},
    List.filter (fun p => f p.fst p.snd) (l ++ l') ~
      List.filter (fun p => f p.fst p.snd) l ++ List.filter (fun p => f p.fst p.snd) l'

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem mul_rat_iff (hr : r ≠ 0) : LiouvilleWith p (x * r) ↔ LiouvilleWith p x :=
  ⟨fun h => by
    simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel₀ hr, Rat.cast_one, mul_one] using
      h.mul_rat (inv_ne_zero hr),
    fun h => h.mul_rat hr⟩

Proof state:
p x : ℝ
r : ℚ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x

Tactic:
simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel₀ hr, Rat.cast_one, mul_one] using
  h.mul_rat (inv_ne_zero hr)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKey? k' (modifyKey k f l) =
      if k == k' then
        if containsKey k l then some k else none
      else
        getKey? k' l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey? k' (modifyKey k f l) =
    if (k == k') = true then if containsKey k l = true then some k else none else getKey? k' l

Tactic:
simp [modifyKey_eq_alterKey, getKey?_alterKey, containsKey_eq_isSome_getValueCast?, hl]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem IsInitial.principal_add {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) :
    Principal (· + ·) o

Proof state:
case hc
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card

Tactic:
rwa [aleph0_le_card]

Result:
no goals

Proof state:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
rw [← h.ord_card]

Result:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 + x2) o.card.ord

Proof state:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 + x2) o.card.ord

Tactic:
apply principal_add_ord

Result:
case hc
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosedMap_comap_of_isIntegral (hf : f.IsIntegral) :
    IsClosedMap (comap f)

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
⊢ y ∈ ⇑(comap f) '' s

Tactic:
algebraize [f]

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
⊢ y ∈ ⇑(comap f) '' s

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
⊢ StableUnderSpecialization (⇑(comap f) '' s)

Tactic:
rintro _ y e ⟨x, hx, rfl⟩

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
⊢ y ∈ ⇑(comap f) '' s

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
⊢ IsClosedMap ⇑(comap f)

Tactic:
refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
⊢ StableUnderSpecialization (⇑(comap f) '' s)

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
q : Ideal S
hq₁ : q ≥ x.asIdeal
hq₂ : q.IsPrime
hq₃ : Ideal.comap (algebraMap R S) q = y.asIdeal
⊢ y ∈ ⇑(comap f) '' s

Tactic:
refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
  PrimeSpectrum.ext hq₃⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
⊢ y ∈ ⇑(comap f) '' s

Tactic:
obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal
  ((le_iff_specializes _ _).mpr e)

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : (comap f) x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
q : Ideal S
hq₁ : q ≥ x.asIdeal
hq₂ : q.IsPrime
hq₃ : Ideal.comap (algebraMap R S) q = y.asIdeal
⊢ y ∈ ⇑(comap f) '' s
-- Mathlib/Computability/TMToPartrec.lean
theorem trNat_zero : trNat 0 = []

Proof state:
⊢ trNat 0 = []

Tactic:
rw [trNat, Nat.cast_zero]

Result:
⊢ trNum 0 = []

Proof state:
⊢ trNum 0 = []

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousOn_iff'_left [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
simp [ContinuousOn, continuousWithinAt_iff'_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.find?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₂.find? p = none → l₁.find? p = none

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → p x = false) → ∀ (x : α), x ∈ l₁ → p x = false

Tactic:
exact fun w x m => w x (Sublist.mem m h)

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ find? p l₂ = none → find? p l₁ = none

Tactic:
simp only [List.find?_eq_none, Bool.not_eq_true]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → p x = false) → ∀ (x : α), x ∈ l₁ → p x = false
-- Mathlib/Analysis/MellinTransform.lean
theorem MellinConvergent.const_smul {f : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) {𝕜 : Type*}
    [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜) :
    MellinConvergent (fun t => c • f t) s

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hf : MellinConvergent f s
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ MellinConvergent (fun t => c • f t) s

Tactic:
simpa only [MellinConvergent, smul_comm] using hf.smul c

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma homologyι_singleObjOpcyclesSelfIso_inv :
    ((single C c j).obj A).homologyι j ≫ (singleObjOpcyclesSelfIso _ _ _).inv =
      (singleObjHomologySelfIso _ _ _).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).homologyι j ≫ (singleObjOpcyclesSelfIso c j A).inv = (singleObjHomologySelfIso c j A).hom

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
  singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_id]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
/-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
times how many they are. -/
lemma sum_card_le [Fintype α] (h : ∀ a, #{b ∈ B | a ∈ b} ≤ n) : ∑ s ∈ B, #s ≤ Fintype.card α * n :=
  calc
    ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #(filter (fun b => a ∈ b) B) ≤ n
⊢ ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s)

Tactic:
simp_rw [univ_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
    (h : start = l.toArray.size) :
    l.toArray.foldr f init start 0 = l.foldr f init

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
init : β
l : List α
⊢ Array.foldr f init l.toArray = foldr f init l

Tactic:
rw [foldr_toList]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
start : Nat
f : α → β → β
init : β
l : List α
h : start = l.toArray.size
⊢ Array.foldr f init l.toArray start = foldr f init l

Tactic:
subst h

Result:
α : Type u_1
β : Type u_2
f : α → β → β
init : β
l : List α
⊢ Array.foldr f init l.toArray = foldr f init l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_le_of_le_sub_right {a b c : Int} (h : a ≤ c - b) : a + b ≤ c

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

Tactic:
rwa [Int.sub_add_cancel] at h

Result:
no goals

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

Tactic:
have h := Int.add_le_add_right h b

Result:
a b c : Int
h✝ : a ≤ c - b
h : a + b ≤ c - b + b
⊢ a + b ≤ c
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.isCompact_closure_image_of_bounded [ContinuousConstSMul 𝕜₂ M₂]
    [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) {S : Set M₁}
    (hS : Bornology.IsBounded S) : IsCompact (closure <| f '' S) :=
  hf.isCompact_closure_image_of_isVonNBounded <| by rwa [NormedSpace.isVonNBounded_iff]

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : SeminormedAddCommGroup M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : NormedSpace 𝕜₁ M₁
inst✝² : Module 𝕜₂ M₂
inst✝¹ : ContinuousConstSMul 𝕜₂ M₂
inst✝ : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
    (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
n : ℕ
x : α
⊢ (f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x

Tactic:
rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem div_I (z : ℂ) : z / I = -(z * I) :=
  (div_eq_iff_mul_eq I_ne_zero).2 <| by simp [mul_assoc]

Proof state:
z : ℂ
⊢ -(z * I) * I = z

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_append {xs ys : List α} :
    (xs ++ ys).dropWhile p =
      if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys

Proof state:
case cons
α : Type u_1
p : α → Bool
ys : List α
h : α
t : List α
ih : dropWhile p (t ++ ys) = if (dropWhile p t).isEmpty = true then dropWhile p ys else dropWhile p t ++ ys
⊢ (if p h = true then dropWhile p (t ++ ys) else h :: (t ++ ys)) =
    if (if p h = true then dropWhile p t else h :: t).isEmpty = true then dropWhile p ys
    else (if p h = true then dropWhile p t else h :: t) ++ ys

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
ys : List α
h : α
t : List α
ih : dropWhile p (t ++ ys) = if (dropWhile p t).isEmpty = true then dropWhile p ys else dropWhile p t ++ ys
⊢ dropWhile p (h :: t ++ ys) =
    if (dropWhile p (h :: t)).isEmpty = true then dropWhile p ys else dropWhile p (h :: t) ++ ys

Tactic:
simp only [cons_append, dropWhile_cons]

Result:
case cons
α : Type u_1
p : α → Bool
ys : List α
h : α
t : List α
ih : dropWhile p (t ++ ys) = if (dropWhile p t).isEmpty = true then dropWhile p ys else dropWhile p t ++ ys
⊢ (if p h = true then dropWhile p (t ++ ys) else h :: (t ++ ys)) =
    if (if p h = true then dropWhile p t else h :: t).isEmpty = true then dropWhile p ys
    else (if p h = true then dropWhile p t else h :: t) ++ ys

Proof state:
case nil
α : Type u_1
p : α → Bool
ys : List α
⊢ dropWhile p ([] ++ ys) = if (dropWhile p []).isEmpty = true then dropWhile p ys else dropWhile p [] ++ ys

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs ys : List α
⊢ dropWhile p (xs ++ ys) = if (dropWhile p xs).isEmpty = true then dropWhile p ys else dropWhile p xs ++ ys

Tactic:
induction xs with
| nil => simp
| cons h t ih =>
  simp only [cons_append, dropWhile_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma le_iff_eq_or_lt : a ≤ b ↔ a = b ∨ a < b

Proof state:
a b : ℤ
⊢ a ≤ b ↔ a ≤ b ∧ (b ≤ a ∨ ¬b ≤ a)

Tactic:
simp [Decidable.em]

Result:
no goals

Proof state:
a b : ℤ
⊢ a ≤ b ↔ a = b ∨ a < b

Tactic:
rw [Int.le_antisymm_iff, Int.lt_iff_le_not_le, ← and_or_left]

Result:
a b : ℤ
⊢ a ≤ b ↔ a ≤ b ∧ (b ≤ a ∨ ¬b ≤ a)
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_ofReal (r : ℝ) : normSq r = r * r

Proof state:
r : ℝ
⊢ normSq ↑r = r * r

Tactic:
simp [normSq, ofReal]

Result:
no goals
-- Mathlib/Algebra/Exact.lean
lemma Exact.of_ladder_linearEquiv_of_exact
    (h₁₂ : g₁₂ ∘ₗ e₁ = e₂ ∘ₗ f₁₂) (h₂₃ : g₂₃ ∘ₗ e₂ = e₃ ∘ₗ f₂₃)
    (H : Exact f₁₂ f₂₃) : Exact g₁₂ g₂₃

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid N'
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid P'
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
inst✝³ : Module R N
inst✝² : Module R N'
inst✝¹ : Module R P
inst✝ : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃
H : Exact ⇑f₁₂ ⇑f₂₃
⊢ Exact ⇑g₁₂ ⇑g₂₃

Tactic:
rwa [iff_of_ladder_linearEquiv h₁₂ h₂₃]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findRev?_push_of_pos (l : Array α) (h : p a) :
    findRev? p (l.push a) = some a

Proof state:
case mk
α : Type
p : α → Bool
a : α
h : p a = true
toList✝ : List α
⊢ findRev? p ({ toList := toList✝ }.push a) = some a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type
p : α → Bool
a : α
l : Array α
h : p a = true
⊢ findRev? p (l.push a) = some a

Tactic:
cases l

Result:
case mk
α : Type
p : α → Bool
a : α
h : p a = true
toList✝ : List α
⊢ findRev? p ({ toList := toList✝ }.push a) = some a
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem epi_of_cokernel_zero {X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)]
    (w : cokernel.π f = 0) : Epi f :=
  epi_of_cancel_zero f fun g h => by rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0

Tactic:
rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

Result:
no goals
-- Mathlib/RingTheory/Norm/Defs.lean
theorem norm_eq_one_of_not_exists_basis (h : ¬∃ s : Finset S, Nonempty (Basis s R S)) (x : S) :
    norm R x = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
x : S
⊢ (norm R) x = 1

Tactic:
rw [norm_apply, LinearMap.det]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
x : S
⊢ (if H : ∃ s, Nonempty (Basis { x // x ∈ s } R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
x : S
⊢ (if H : ∃ s, Nonempty (Basis { x // x ∈ s } R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1

Tactic:
split_ifs <;> trivial

Result:
no goals
-- Mathlib/FieldTheory/Galois/GaloisClosure.lean
theorem adjoin_map [IsGalois k K] (f : K →ₐ[k] K) (s : Set K) [Finite s] :
    adjoin k (f '' s) = adjoin k s

Proof state:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ adjoin k (⇑f '' s) = adjoin k s

Tactic:
apply val_injective

Result:
case a
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ (adjoin k (⇑f '' s)).toIntermediateField = (adjoin k s).toIntermediateField

Proof state:
case a
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(IntermediateField.adjoin k (⇑f '' s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K

Tactic:
rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]

Result:
no goals

Proof state:
case a
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ (adjoin k (⇑f '' s)).toIntermediateField = (adjoin k s).toIntermediateField

Tactic:
dsimp [adjoin_val]

Result:
case a
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(IntermediateField.adjoin k (⇑f '' s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K
-- Mathlib/RingTheory/Norm/Transitivity.lean
theorem Algebra.norm_norm {A} [Ring A] [Algebra R A] [Algebra S A]
    [IsScalarTower R S A] [Module.Free S A] {a : A} :
    norm R (norm S a) = norm R a

Proof state:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ (norm R) ((norm S) a) = (norm R) a

Tactic:
rw [norm_apply S, norm_apply R a, ← LinearMap.det_restrictScalars]

Result:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)
-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
lemma isClosed_iff_of_isColimit (X : Set c.pt) :
    IsClosed X ↔ ∀ (j : J), IsClosed (c.ι.app j ⁻¹' X)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsClosed X ↔ ∀ (j : J), IsClosed (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff_of_isColimit _ hc,
  Functor.const_obj_obj, Set.preimage_compl]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_toNat (p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod p) = z
  | (n : ℕ), _h => by simp only [Int.cast_natCast, Int.toNat_natCast]
  | Int.negSucc n, h => by simp at h

Proof state:
p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ ↑(Int.negSucc n).toNat = ↑(Int.negSucc n)

Tactic:
simp at h

Result:
no goals

Proof state:
p n : ℕ
_h : 0 ≤ ↑n
⊢ ↑(↑n).toNat = ↑↑n

Tactic:
simp only [Int.cast_natCast, Int.toNat_natCast]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_castSucc_of_le (p i : Fin n) (h : i ≤ p) : p.predAbove (castSucc i) = i

Proof state:
n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), castPred_castSucc]

Result:
no goals