harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) :
    foldr.loop (n+1) f (i+1) h x =
      f 0 (foldr.loop n (fun j => f j.succ) i (Nat.le_of_succ_le_succ h) x)

Proof state:
case zero
n : Nat
α : Sort u_1
f : Fin (n + 1) → α → α
x : α
h : 0 + 1 ≤ n + 1
⊢ foldr.loop (n + 1) f (0 + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) 0 ⋯ x)

Tactic:
simp [foldr_loop_succ, foldr_loop_zero]

Result:
no goals

Proof state:
case succ
n : Nat
α : Sort u_1
f : Fin (n + 1) → α → α
i : Nat
ih : ∀ (x : α) (h : i + 1 ≤ n + 1), foldr.loop (n + 1) f (i + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) i ⋯ x)
x : α
h : i + 1 + 1 ≤ n + 1
⊢ foldr.loop (n + 1) f (i + 1 + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) (i + 1) ⋯ x)

Tactic:
rw [foldr_loop_succ, ih]

Result:
case succ
n : Nat
α : Sort u_1
f : Fin (n + 1) → α → α
i : Nat
ih : ∀ (x : α) (h : i + 1 ≤ n + 1), foldr.loop (n + 1) f (i + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) i ⋯ x)
x : α
h : i + 1 + 1 ≤ n + 1
⊢ f 0 (foldr.loop n (fun j => f j.succ) i ⋯ (f ⟨i + 1, h⟩ x)) = f 0 (foldr.loop n (fun j => f j.succ) (i + 1) ⋯ x)

Proof state:
n : Nat
α : Sort u_1
i : Nat
f : Fin (n + 1) → α → α
x : α
h : i + 1 ≤ n + 1
⊢ foldr.loop (n + 1) f (i + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) i ⋯ x)

Tactic:
induction i generalizing x with
| zero => simp [foldr_loop_succ, foldr_loop_zero]
| succ i ih => rw [foldr_loop_succ, ih]; rfl

Result:
no goals

Proof state:
case succ
n : Nat
α : Sort u_1
f : Fin (n + 1) → α → α
i : Nat
ih : ∀ (x : α) (h : i + 1 ≤ n + 1), foldr.loop (n + 1) f (i + 1) h x = f 0 (foldr.loop n (fun j => f j.succ) i ⋯ x)
x : α
h : i + 1 + 1 ≤ n + 1
⊢ f 0 (foldr.loop n (fun j => f j.succ) i ⋯ (f ⟨i + 1, h⟩ x)) = f 0 (foldr.loop n (fun j => f j.succ) (i + 1) ⋯ x)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem boole_getElem_le_count (a : α) (l : Array α) (i : Nat) (h : i < l.size) :
    (if l[i] == a then 1 else 0) ≤ l.count a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
i : Nat
h : i < l.size
⊢ (if (l[i] == a) = true then 1 else 0) ≤ count a l

Tactic:
rw [count_eq_countP]

Result:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
i : Nat
h : i < l.size
⊢ (if (l[i] == a) = true then 1 else 0) ≤ countP (fun x => x == a) l
-- Mathlib/Analysis/Normed/Group/Int.lean
theorem norm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Proof state:
α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Tactic:
rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa using norm_pow_le_mul_norm

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem morphismRestrict_ι {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (f ∣_ U) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ∣_ U ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
delta morphismRestrict

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem minCardFinsetOfMemConvexHull_card_le_card {t : Finset E} (ht₁ : ↑t ⊆ s)
    (ht₂ : x ∈ convexHull 𝕜 (t : Set E)) : #(minCardFinsetOfMemConvexHull hx) ≤ #t :=
  Function.argminOn_le _ _ (by exact ⟨ht₁, ht₂⟩)

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : x ∈ (convexHull 𝕜) ↑t
⊢ t ∈ {t | ↑t ⊆ s ∧ x ∈ (convexHull 𝕜) ↑t}

Tactic:
exact ⟨ht₁, ht₂⟩

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem im_ofReal_mul (r : ℝ) (z : K) : im (↑r * z) = r * im z

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (↑r * z) = r * im z

Tactic:
simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem edgeFinset_replaceVertex_of_adj (ha : G.Adj s t) : (G.replaceVertex s t).edgeFinset =
    (G.edgeFinset \ G.incidenceFinset t ∪ (G.neighborFinset s).image (s(·, t))) \ {s(t, t)}

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset =
    (G.edgeFinset \ G.incidenceFinset t ∪ image (fun x => s(x, t)) (G.neighborFinset s)) \ {s(t, t)}

Tactic:
simp only [incidenceFinset, neighborFinset, ← Set.toFinset_diff, ← Set.toFinset_image,
  ← Set.toFinset_union, ← Set.toFinset_singleton]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset =
    ((G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}).toFinset

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset =
    ((G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}).toFinset

Tactic:
exact Set.toFinset_congr (G.edgeSet_replaceVertex_of_adj ha)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
    gcd (m / k) (n / k) = gcd m n / k :=
  match eq_zero_or_pos k with
  | .inl H0 => by simp [H0]
  | .inr H3 => by
    apply Nat.eq_of_mul_eq_mul_right H3
    rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
        Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]

Proof state:
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ (m / k).gcd (n / k) * k = m.gcd n / k * k

Tactic:
rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
    Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]

Result:
no goals

Proof state:
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ (m / k).gcd (n / k) = m.gcd n / k

Tactic:
apply Nat.eq_of_mul_eq_mul_right H3

Result:
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ (m / k).gcd (n / k) * k = m.gcd n / k * k

Proof state:
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H0 : k = 0
⊢ (m / k).gcd (n / k) = m.gcd n / k

Tactic:
simp [H0]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma rankPos_iff_exists_isCocircuit : M.RankPos ↔ ∃ K, M.IsCocircuit K

Proof state:
α : Type u_1
M : Matroid α
⊢ M.RankPos ↔ ∃ K, M.IsCocircuit K

Tactic:
rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem inter_singleton_eq_empty : s ∩ {a} = ∅ ↔ a ∉ s

Proof state:
α : Type u
s : Set α
a : α
⊢ s ∩ {a} = ∅ ↔ a ∉ s

Tactic:
rw [inter_comm, singleton_inter_eq_empty]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem HasSum.mul_right (a₂) (hf : HasSum f a₁) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
hf : HasSum f a₁
⊢ HasSum (fun i => f i * a₂) (a₁ * a₂)

Tactic:
simpa only using hf.map (AddMonoidHom.mulRight a₂) (continuous_id.mul continuous_const)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_mul_self_left (a b : E) : dist (a * b) b = ‖a‖

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist (a * b) b = ‖a‖

Tactic:
rw [dist_comm, dist_mul_self_right]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem pullbackAssoc_hom_fst [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) =
    pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂

Tactic:
rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_const_smul_le : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ :=
  eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
    (Eventually.of_forall fun _ => by simp [nnnorm_smul_le])

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
simp [nnnorm_smul_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_le_iff_le_exp (hx : 0 < x) : log x ≤ y ↔ x ≤ exp y

Proof state:
x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ rexp y

Tactic:
rw [← exp_le_exp, exp_log hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `F` is a binary operation on `ℕ → ℂ` with the property that the `LSeries` of `F f g`
converges whenever the `LSeries` of `f` and `g` do, then the abscissa of absolute convergence
of `F f g` is at most the maximum of the abscissa of absolute convergence of `f`
and that of `g`. -/
lemma LSeries.abscissaOfAbsConv_binop_le {F : (ℕ → ℂ) → (ℕ → ℂ) → (ℕ → ℂ)}
    (hF : ∀ {f g s}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s)
    (f g : ℕ → ℂ) :
    abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Proof state:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (F f g) ≤ abscissaOfAbsConv f ⊔ abscissaOfAbsConv g

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦  hF ?_ ?_

Result:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : abscissaOfAbsConv f ⊔ abscissaOfAbsConv g < ↑x
⊢ LSeriesSummable f ↑x

case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : abscissaOfAbsConv f ⊔ abscissaOfAbsConv g < ↑x
⊢ LSeriesSummable g ↑x

Proof state:
case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : abscissaOfAbsConv f ⊔ abscissaOfAbsConv g < ↑x
⊢ LSeriesSummable g ↑x

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
  (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx

Result:
no goals

Proof state:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : abscissaOfAbsConv f ⊔ abscissaOfAbsConv g < ↑x
⊢ LSeriesSummable f ↑x

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
  (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Action/Prod.lean
theorem smul_zero_mk {α : Type*} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) :
    a • ((0 : α), c) = (0, a • c)

Proof state:
M : Type u_1
β : Type u_4
inst✝³ : SMul M β
α : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)

Tactic:
rw [Prod.smul_mk, smul_zero]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem swap : Nat.Primrec (unpaired (swap Nat.pair)) :=
  (pair right left).of_eq fun n => by simp

Proof state:
n : ℕ
⊢ Nat.pair (unpair n).2 (unpair n).1 = unpaired (swap Nat.pair) n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_map_equiv [Fintype β] (e : α ≃ β) : (s.map e.toEmbedding).dens = s.dens

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
e : α ≃ β
⊢ (map e.toEmbedding s).dens = s.dens

Tactic:
simp [dens, Fintype.card_congr e]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem OrderIso.map_iSup [CompleteLattice β] (f : α ≃o β) (x : ι → α) :
    f (⨆ i, x i) = ⨆ i, f (x i) :=
  eq_of_forall_ge_iff <| f.surjective.forall.2
  fun x => by simp only [f.le_iff_le, iSup_le_iff]

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : ι → α
x : α
⊢ f (⨆ i, x✝ i) ≤ f x ↔ ⨆ i, f (x✝ i) ≤ f x

Tactic:
simp only [f.le_iff_le, iSup_le_iff]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem cg_iff : CG L M ↔ ∃ S : Set M, S.Countable ∧ closure L S = (⊤ : L.Substructure M)

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ CG L M ↔ ∃ S, S.Countable ∧ (closure L).toFun S = ⊤

Tactic:
rw [cg_def, Substructure.cg_def]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem le_mul_of_le_one_right [ExistsAddOfLE α] [PosMulMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
ha : a ≤ 0
h : b ≤ 1
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive] lemma mul [Semigroup α] {a b : α} (ha : MulLECancellable a)
    (hb : MulLECancellable b) : MulLECancellable (a * b) :=
  fun c d hcd ↦ hb <| ha <| by rwa [← mul_assoc, ← mul_assoc]

Proof state:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
rwa [← mul_assoc, ← mul_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_iInf_ne_zero {ι : Type*} [Finite ι] {f : ι → Subgroup G}
    (hf : ∀ i, (f i).index ≠ 0) : (⨅ i, f i).index ≠ 0

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
⊢ (⨅ i, f i).index ≠ 0

Tactic:
simp_rw [← relindex_top_right] at hf ⊢

Result:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relindex ⊤ ≠ 0
⊢ (⨅ i, f i).relindex ⊤ ≠ 0

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relindex ⊤ ≠ 0
⊢ (⨅ i, f i).relindex ⊤ ≠ 0

Tactic:
exact relindex_iInf_ne_zero hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α}
    {v : β k} : getKeyD k (insertEntry k v l) fallback = k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k fallback : α
v : β k
⊢ getKeyD k (insertEntry k v l) fallback = k

Tactic:
rw [getKeyD_insertEntry, if_pos BEq.refl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_ne_zero_iff {x y : ℂ} :
    x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0

Proof state:
x y : ℂ
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0

Tactic:
rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_subtype_eq_of_mulSupport_subset {f : β → α} {s : Set β} (hs : mulSupport f ⊆ s) :
    ∏' x : s, f x = ∏' x, f x :=
  Subtype.val_injective.tprod_eq <| by simpa

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s : Set β
hs : mulSupport f ⊆ s
⊢ mulSupport f ⊆ Set.range Subtype.val

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n

Proof state:
n m : Nat
⊢ n * (m - 1) = n * m - n

Tactic:
rw [Nat.mul_comm, Nat.sub_one_mul , Nat.mul_comm]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem inv_im (z : K) : im z⁻¹ = -im z / normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z⁻¹ = -im z / normSq z

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSomeRev?_push_of_isNone (l : Array α) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isNone = true
toList✝ : List α
⊢ findSomeRev? f ({ toList := toList✝ }.push a) = findSomeRev? f { toList := toList✝ }

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
l : Array α
h : (f a).isNone = true
⊢ findSomeRev? f (l.push a) = findSomeRev? f l

Tactic:
cases l

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isNone = true
toList✝ : List α
⊢ findSomeRev? f ({ toList := toList✝ }.push a) = findSomeRev? f { toList := toList✝ }
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem aleph_one_le_continuum : ℵ₁ ≤ 𝔠

Proof state:
⊢ ℵ_ 1 ≤ 𝔠

Tactic:
rw [← succ_aleph0]

Result:
⊢ Order.succ ℵ₀ ≤ 𝔠

Proof state:
⊢ Order.succ ℵ₀ ≤ 𝔠

Tactic:
exact Order.succ_le_of_lt aleph0_lt_continuum

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem incl_range : K.incl.range = K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.incl.range.toSubmodule = K.toSubmodule

Tactic:
exact (K : Submodule R L).range_subtype

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.incl.range = K

Tactic:
rw [← toSubmodule_inj]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.incl.range.toSubmodule = K.toSubmodule
-- Mathlib/Logic/Encodable/Basic.lean
theorem encode_injective [Encodable α] : Function.Injective (@encode α _)
  | x, y, e => Option.some.inj <| by rw [← encodek, e, encodek]

Proof state:
α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y

Tactic:
rw [← encodek, e, encodek]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem cast_eq_iff_heq {α β} (h : α = β) {a : α} {b : β} : Equiv.cast h a = b ↔ HEq a b

Proof state:
α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ HEq a b

Tactic:
simp [coe_refl]

Result:
no goals

Proof state:
α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h) a = b ↔ HEq a b

Tactic:
subst h

Result:
α : Sort u_1
a b : α
⊢ (Equiv.cast ⋯) a = b ↔ HEq a b
-- Mathlib/CategoryTheory/GradedObject.lean
theorem comapEq_trans {β γ : Type w} {f g h : β → γ} (k : f = g) (l : g = h) :
    comapEq C (k.trans l) = comapEq C k ≪≫ comapEq C l

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g h : β → γ
k : f = g
l : g = h
⊢ comapEq C ⋯ = comapEq C k ≪≫ comapEq C l

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma odd_mul : Odd (m * n) ↔ Odd m ∧ Odd n

Proof state:
m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
simp [← not_even_iff_odd, not_or, parity_simps]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subtype_eq_prod_filter (f : α → β) {p : α → Prop} [DecidablePred p] :
    ∏ x ∈ s.subtype p, f x = ∏ x ∈ s with p x, f x

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
this : ∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x = ∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p) x)
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ filter (fun x => p x) s, f x

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ filter (fun x => p x) s, f x

Tactic:
have := prod_map (s.subtype p) (Function.Embedding.subtype _) f

Result:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
this : ∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x = ∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p) x)
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ filter (fun x => p x) s, f x
-- Mathlib/Data/List/Rotate.lean
theorem singleton_eq_rotate_iff {l : List α} {n : ℕ} {x : α} : [x] = l.rotate n ↔ [x] = l

Proof state:
α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = l.rotate n ↔ [x] = l

Tactic:
rw [eq_comm, rotate_eq_singleton_iff, eq_comm]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma natDegree_minpolyDiv_lt [Nontrivial S] :
    natDegree (minpolyDiv R x) < natDegree (minpoly R x)

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree < (minpoly R x).natDegree

Tactic:
rw [← natDegree_minpolyDiv_succ hx]

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree < (minpolyDiv R x).natDegree + 1

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree < (minpolyDiv R x).natDegree + 1

Tactic:
exact Nat.lt_succ_self _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.keys.isEmpty = m.isEmpty

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.keys.isEmpty = m.isEmpty

Tactic:
simp_to_raw using Raw₀.isEmpty_keys ⟨m, h.size_buckets_pos⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_some (x : Option α) : x.bind some = x

Proof state:
α : Type u_1
x : Option α
⊢ x.bind some = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_eq_card_pow_dvd (n : ℕ) {p : ℕ} (pp : p.Prime) :
    n.factorization p = #{i ∈ Ico 1 n | p ^ i ∣ n}

Proof state:
n p : ℕ
pp : Prime p
⊢ n.factorization p = #(Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n))

Tactic:
simp [← Icc_factorization_eq_pow_dvd n pp]

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem num_mul_den_eq_num_mul_den_iff_eq {x y : K} :
    num A y * den A x = num A x * den A y ↔ x = y :=
  ⟨fun h ↦ by simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h, fun h ↦ by rw [h]⟩

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : num A y * ↑(den A x) = num A x * ↑(den A y)
⊢ x = y

Tactic:
simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ num A y * ↑(den A x) = num A x * ↑(den A y)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem not_isMax_zero [Zero α] [One α] [ZeroLEOneClass α] [NeZero (1 : α)] : ¬ IsMax (0 : α)

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ¬IsMax 0

Tactic:
rw [not_isMax_iff]

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ∃ b, 0 < b

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ∃ b, 0 < b

Tactic:
exact ⟨1, one_pos⟩

Result:
no goals