harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Extension.lean
theorem le_union ⦃σ : Lifts F E K⦄ (hσ : σ ∈ c) : σ ≤ union c hc :=
  have hσ := Set.mem_insert_of_mem ⊥ hσ
  let t (i : ↑(insert ⊥ c)) := i.val.carrier
  ⟨le_iSup t ⟨σ, hσ⟩, fun x ↦ by
    dsimp only [union, AlgHom.comp_apply]
    exact Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)⟩

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
σ : Lifts F E K
hσ✝ : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier
x : ↥σ.carrier
⊢ (union c hc).emb ((inclusion ⋯) x) = σ.emb x

Tactic:
dsimp only [union, AlgHom.comp_apply]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
σ : Lifts F E K
hσ✝ : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier
x : ↥σ.carrier
⊢ (Subalgebra.iSupLift (fun x => (↑x).carrier.toSubalgebra) ⋯ (fun x => (↑x).emb) ⋯ (⨆ x, (↑x).carrier.toSubalgebra) ⋯)
      (↑((⨆ i, (↑i).carrier).equivOfEq (⨆ i, (↑i).carrier.toSubalgebra) ⋯) ((inclusion ⋯) x)) =
    σ.emb x
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive sum_pos]
lemma one_lt_prod (hf : 1 < f) : 1 < ∏ i, f i :=
  Finset.one_lt_prod' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCancelCommMonoid M
f : ι → M
hf : 1 < f
⊢ ∃ i ∈ Finset.univ, 1 < f i

Tactic:
simpa using (Pi.lt_def.1 hf).2

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp) zsmul_singleton]
lemma singleton_zpow (a : α) (n : ℤ) : ({a} : Finset α) ^ n = {a ^ n}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ {a} ^ n = {a ^ n}

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_abs_log_rpow_rpow_nhds_zero {s : ℝ} (r : ℝ) (hs : s < 0) :
    (fun x => |log x| ^ r) =o[𝓝[>] 0] fun x => x ^ s :=
  ((isLittleO_log_rpow_rpow_atTop r (neg_pos.2 hs)).comp_tendsto tendsto_inv_nhdsGT_zero).congr'
    (mem_of_superset (Icc_mem_nhdsGT one_pos) fun x hx => by
      simp [abs_of_nonpos, log_nonpos hx.1 hx.2])
    (eventually_mem_nhdsWithin.mono fun x hx => by
      rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv])

Proof state:
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x => ((fun x => log x ^ r) ∘ fun x => x⁻¹) x = (fun x => |log x| ^ r) x) x}

Tactic:
simp [abs_of_nonpos, log_nonpos hx.1 hx.2]

Result:
no goals

Proof state:
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((fun x => x ^ (-s)) ∘ fun x => x⁻¹) x = (fun x => x ^ s) x

Tactic:
rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]

Result:
no goals
-- Mathlib/Data/Fintype/Inv.lean
theorem invOfMemRange_surjective : Function.Surjective hf.invOfMemRange := fun a =>
  ⟨⟨f a, Set.mem_range_self a⟩, by simp⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ hf.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_polynomial (q : R[X]) (f : R → R) (a : A)
    (hf : ContinuousOn f (q.eval '' (spectrum R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
q : R[X]
f : R → R
a : A
hf : autoParam (ContinuousOn f ((fun a => Polynomial.eval a q) '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (Polynomial.eval x q)) a = cfc f ((aeval a) q)

Tactic:
rw [cfc_comp' .., cfc_polynomial ..]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_biUnion_le_lift {α : Type u} {ι : Type v} (A : ι → Set α) (s : Set ι) :
    lift.{v} #(⋃ x ∈ s, A x) ≤ lift.{u} #s * ⨆ x : s, lift.{v} #(A x.1)

Proof state:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x, A ↑x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
apply mk_iUnion_le_lift

Result:
no goals

Proof state:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x ∈ s, A x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x, A ↑x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_m_density (hκν : fst κ ≤ ν) (a : α) [IsFiniteKernel ν]
    {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ x ∂(ν a),
      Tendsto (fun n ↦ densityProcess κ ν n a x s) atTop (𝓝 (density κ ν a x s))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
inst✝ : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : γ) ∂ν a, Tendsto (fun n => κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))

Tactic:
filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs]
  with t h1 h2 using h2 ▸ h1

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem codisjoint_coe : Codisjoint (s : Set α) t ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : LE α
s t : UpperSet α
⊢ Codisjoint ↑s ↑t ↔ Disjoint s t

Tactic:
simp [disjoint_iff, codisjoint_iff, SetLike.ext'_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) : W'.addXYZ P Q = (P y ^ 2 * Q z) • Q

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addXYZ P Q = (P y ^ 2 * Q z) • Q

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
  addZ_of_Z_eq_zero_left hP hPz, smul_fin3]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
    {fallback : β} : m.contains a = true → get? m a = some (getD m a fallback)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ m.contains a = true → get? m a = some (getD m a fallback)

Tactic:
simp_to_raw using Raw₀.Const.get?_eq_some_getD

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_map_right (f : β → γ) (l₁ : Array α) (l₂ : Array β) :
    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f)

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
l₁ : Array α
l₂ : Array β
⊢ l₁.zip (map f l₂) = map (Prod.map id f) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.getThenInsertIfNew? [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {a : α} {b : β a}
    (h : m.WF) : (m.getThenInsertIfNew? a b).2.WF

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
b : β a
h : m.WF
⊢ (m.getThenInsertIfNew? a b).snd.WF

Tactic:
simpa [Raw.getThenInsertIfNew?, h.size_buckets_pos] using .getThenInsertIfNew?₀ h

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem product_cons : s ×ˢ (b ::ₘ t) = (s.map fun a => (a, b)) + s ×ˢ t

Proof state:
α : Type u_1
β : Type v
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a => (a, b)) s + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.mul' (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
    HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivWithinAt a a' s x
hb : HasFDerivWithinAt b b' s x
⊢ HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x

Tactic:
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
  (a x, b x)).comp_hasFDerivWithinAt x (ha.prod hb)

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_singleton (f : α → β) (a : α) : image f {a} = {f a} :=
  ext fun x => by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : α
x : β
⊢ x ∈ image f {a} ↔ x ∈ {f a}

Tactic:
simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Exponential.lean
theorem Commute.expUnitary {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
    Commute (expUnitary a) (expUnitary b) :=
  calc
    selfAdjoint.expUnitary a * selfAdjoint.expUnitary b =
        selfAdjoint.expUnitary b * selfAdjoint.expUnitary a

Proof state:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a

Tactic:
rw [← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
lemma mul_ite_zero : a * ite P b 0 = ite P (a * b) 0

Proof state:
α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (a * if P then b else 0) = if P then a * b else 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_succ_of_lt (p i : Fin n) (h : i < p) (hi := succ_ne_last_of_lt h) :
    p.predAbove (succ i) = (i.succ).castPred hi

Proof state:
n : ℕ
p i : Fin n
h : i < p
hi : optParam (i.succ ≠ last n) ⋯
⊢ p.predAbove i.succ = i.succ.castPred hi

Tactic:
rw [predAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_mkVector_of_isSome (_ : (f a).isSome) :
   findSome? f (mkVector n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
x✝ : (f a).isSome = true
⊢ findSome? f (mkVector n a) = if n = 0 then none else f a

Tactic:
simp [findSome?_mkVector]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem erase_empty {k : α} {c : Nat} : (empty c : Raw₀ α β).erase k = empty c

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
c : Nat
⊢ (empty c).erase k = empty c

Tactic:
simp [erase, empty]

Result:
no goals
-- Mathlib/Order/Lattice.lean
@[simp] lemma inf_eq_sup : a ⊓ b = a ⊔ b ↔ a = b

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b = a ⊔ b ↔ a = b

Tactic:
rw [← inf_le_sup.ge_iff_eq, sup_le_inf]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem two_mul_sub_one_mem_iff {t : ℝ} : 2 * t - 1 ∈ I ↔ t ∈ Set.Icc (1 / 2 : ℝ) 1

Proof state:
t : ℝ
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1

Tactic:
constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor <;> linarith

Result:
no goals
-- Mathlib/CategoryTheory/DiscreteCategory.lean
theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X

Proof state:
α : Type u₁
X : Discrete α
⊢ { as := X.as } = X

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma lt_smul_iff_one_lt_left [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
    b < a • b ↔ 1 < a := Iff.trans (by rw [one_smul]) (smul_lt_smul_iff_of_pos_right hb)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ b < a • b ↔ 1 • b < a • b

Tactic:
rw [one_smul]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Polynomial.lean
lemma KaehlerDifferential.polynomial_D_apply (P : R[X]) :
    D R R[X] P = derivative P • D R R[X] X

Proof state:
R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (D R R[X]) P = derivative P • (D R R[X]) X

Tactic:
rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modifyHead_succ {l : List α} {f : α → α} {n} :
    (l.modifyHead f)[n + 1]? = l[n + 1]?

Proof state:
α : Type u_1
l : List α
f : α → α
n : Nat
⊢ (modifyHead f l)[n + 1]? = l[n + 1]?

Tactic:
simp [getElem?_modifyHead]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_eq_getValue! [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α}
    (h : containsKey a l = true) : getValue a l h = getValue! a l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
h : containsKey a l = true
⊢ getValue a l h = getValue! a l

Tactic:
rw [getValue!_eq_getValue?, getValue, Option.get_eq_get!]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem update_mem_cylinder (x : ∀ n, E n) (n : ℕ) (y : E n) : update x n y ∈ cylinder x n :=
  mem_cylinder_iff.2 fun i hi => by simp [hi.ne]

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : E n
i : ℕ
hi : i < n
⊢ update x n y i = x i

Tactic:
simp [hi.ne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.get?_val [BEq α] [Hashable α] {m : Raw₀ α (fun _ => β)} {a : α} :
    Raw.Const.get? m.val a = Raw₀.Const.get? m a

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
a : α
⊢ Raw.Const.get? m.val a = Raw₀.Const.get? m a

Tactic:
simp [Raw.Const.get?, m.2]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_mul_of_prime_of_dvd {p n : ℕ} (hp : p.Prime) (h : p ∣ n) :
    (p * n).totient = p * n.totient

Proof state:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n

Tactic:
simpa [(totient_pos.2 hp.pos).ne', mul_comm] using h1

Result:
no goals

Proof state:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ (p * n) = p * φ n

Tactic:
rw [gcd_eq_left h, mul_assoc] at h1

Result:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n

Proof state:
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n

Tactic:
have h1 := totient_gcd_mul_totient_mul p n

Result:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ (p * n) = p * φ n
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.add_self (x : G) : x + x = 0

Proof state:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ x + x = 0

Tactic:
simpa [two_nsmul] using char_nsmul_eq_zero 2 x

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_diff [DecidableEq β] {f : α → β} (finj : Injective f) {l₁ l₂ : List α} :
    map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

Tactic:
simp only [diff_eq_foldl, foldl_map, map_foldl_erase finj]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem encard_isBase_eq (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
    B₁.encard = B₂.encard

Proof state:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
⊢ B₁.encard = B₂.encard

Tactic:
rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
  encard_diff_add_encard_inter]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_of_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] [∀ i, M.HasHomology i]
    [hφ : QuasiIso φ'] [hφφ' : QuasiIso (φ ≫ φ')] :
    QuasiIso φ

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
rw [← quasiIso_iff_comp_right φ φ']

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_nonempty {a b : Ordinal} (h : b ≠ 0) : { o | a < b * succ o }.Nonempty :=
  ⟨a, (succ_le_iff (a := a) (b := b * succ a)).1 <| by
    simpa only [succ_zero, one_mul] using
      mul_le_mul_right' (succ_le_of_lt (Ordinal.pos_iff_ne_zero.2 h)) (succ a)⟩

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ succ a ≤ b * succ a

Tactic:
simpa only [succ_zero, one_mul] using
  mul_le_mul_right' (succ_le_of_lt (Ordinal.pos_iff_ne_zero.2 h)) (succ a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) :
    m.contains a = m.contains b

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a b : α
hab : (a == b) = true
⊢ m.contains a = m.contains b

Tactic:
simp_to_model using List.containsKey_congr hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
    (l.enumFrom n).unzip = (range' n l.length, l)

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (enumFrom n l).unzip = (range' n l.length, l)

Tactic:
simp only [enumFrom_eq_zip_range', unzip_zip, length_range']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) :
  removeNegAssignment (addNegAssignment assignment) = assignment

Proof state:
assignment : Assignment
h : ¬assignment.hasNegAssignment = true
⊢ assignment.addNegAssignment.removeNegAssignment = assignment

Tactic:
cases assignment <;> simp_all [removeNegAssignment, addNegAssignment, hasNegAssignment]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_coe_angle_eq_iff_eq_toReal {z : ℂ} {θ : Real.Angle} :
    (arg z : Real.Angle) = θ ↔ arg z = θ.toReal

Proof state:
z : ℂ
θ : Real.Angle
⊢ ↑z.arg = θ ↔ z.arg = θ.toReal

Tactic:
rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem colon_bot : colon ⊥ N = N.annihilator

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ⊥.colon N = N.annihilator

Tactic:
simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_pair (h : a ≠ b) : (∏ᶠ i ∈ ({a, b} : Set α), f i) = f a * f b

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ {b}.Finite

Tactic:
exacts [h, finite_singleton b]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
rw [finprod_mem_insert, finprod_mem_singleton]

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ {b}.Finite
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem deriv_norm_ne_zero : ‖F.derivative.eval a‖ ≠ 0 := fun h =>
  deriv_sq_norm_ne_zero hnorm (by simp [*, sq])

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
h : ‖Polynomial.eval a (Polynomial.derivative F)‖ = 0
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 = 0

Tactic:
simp [*, sq]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem submodule_map_pow_reverse (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
    (p ^ n).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      p.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) ^ n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n

Tactic:
simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[simp]
lemma cochainsMap_id :
    cochainsMap (MonoidHom.id _) (𝟙 A) = 𝟙 (inhomogeneousCochains A)

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ cochainsMap (MonoidHom.id H) (𝟙 A) = 𝟙 (inhomogeneousCochains A)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whisker_assoc_symm (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    X ◁ f ▷ Z = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ X ◁ f ▷ Z = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma deleteEdges_edgeSet (G G' : SimpleGraph V) : G.deleteEdges G'.edgeSet = G \ G'

Proof state:
case Adj.h.h.a
V : Type u
G G' : SimpleGraph V
x✝¹ x✝ : V
⊢ (G.deleteEdges G'.edgeSet).Adj x✝¹ x✝ ↔ (G \ G').Adj x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G G' : SimpleGraph V
⊢ G.deleteEdges G'.edgeSet = G \ G'

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u
G G' : SimpleGraph V
x✝¹ x✝ : V
⊢ (G.deleteEdges G'.edgeSet).Adj x✝¹ x✝ ↔ (G \ G').Adj x✝¹ x✝
-- Mathlib/Data/Nat/PartENat.lean
theorem find_le (n : ℕ) (h : P n) : find P ≤ n

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P n
⊢ find P ≤ ↑n

Tactic:
rw [le_coe_iff]

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P n
⊢ ∃ (h : (find P).Dom), (find P).get h ≤ n

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P n
⊢ ∃ (h : (find P).Dom), (find P).get h ≤ n

Tactic:
exact ⟨⟨_, h⟩, @Nat.find_min' P _ _ _ h⟩

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

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))

Tactic:
rw [getMsbD, getLsbD]

Result:
no goals