harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup) :
    { a | a ∈ l }.Pairwise r ↔ l.Pairwise r

Proof state:
α : Type u
l : List α
r : α → α → Prop
inst✝ : IsSymm α r
hl : l.Nodup
⊢ {a | a ∈ l}.Pairwise r ↔ Pairwise r l

Tactic:
induction' l with a l ih

Result:
case nil
α : Type u
l : List α
r : α → α → Prop
inst✝ : IsSymm α r
hl : [].Nodup
⊢ {a | a ∈ []}.Pairwise r ↔ Pairwise r []

case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : (a :: l).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Proof state:
case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : (a :: l).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
rw [List.nodup_cons] at hl

Result:
case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : a ∉ l ∧ l.Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Proof state:
case nil
α : Type u
l : List α
r : α → α → Prop
inst✝ : IsSymm α r
hl : [].Nodup
⊢ {a | a ∈ []}.Pairwise r ↔ Pairwise r []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : a ∉ l ∧ l.Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
  imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm

Result:
case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : a ∉ l ∧ l.Nodup
this : ∀ b ∈ l, ¬a = b → r a b ↔ r a b
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Proof state:
case cons
α : Type u
l✝ : List α
r : α → α → Prop
inst✝ : IsSymm α r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : a ∉ l ∧ l.Nodup
this : ∀ b ∈ l, ¬a = b → r a b ↔ r a b
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
simp [Set.setOf_or, Set.pairwise_insert_of_symmetric fun _ _ ↦ symm_of r, ih hl.2, and_comm,
  forall₂_congr this]

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem approximatesLinearOn_empty (f : E → F) (f' : E →L[𝕜] F) (c : ℝ≥0) :
    ApproximatesLinearOn f f' ∅ c

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
c : ℝ≥0
⊢ ApproximatesLinearOn f f' ∅ c

Tactic:
simp [ApproximatesLinearOn]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem trunc_derivative' (f : R⟦X⟧) (n : ℕ) :
    trunc (n-1) (d⁄dX R f) = Polynomial.derivative (trunc n f)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ trunc (n - 1) ((d⁄dX R) f) = Polynomial.derivative (trunc n f)

Tactic:
cases n with
| zero =>
  simp
| succ n =>
  rw [succ_sub_one, trunc_derivative]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ trunc (n + 1 - 1) ((d⁄dX R) f) = Polynomial.derivative (trunc (n + 1) f)

Tactic:
rw [succ_sub_one, trunc_derivative]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ trunc (0 - 1) ((d⁄dX R) f) = Polynomial.derivative (trunc 0 f)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l
  | [], a, h => by contradiction
  | b :: l, a, h => by
    simp? at h says simp only [head?_cons, Option.mem_def, Option.some.injEq] at h
    simp [h]

Proof state:
α : Type u
a : α
h : a ∈ [].head?
⊢ a :: [].tail = []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ a :: (b :: l).tail = b :: l

Tactic:
simp only [head?_cons, Option.mem_def, Option.some.injEq] at h

Result:
α : Type u
b : α
l : List α
a : α
h : b = a
⊢ a :: (b :: l).tail = b :: l

Proof state:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ a :: (b :: l).tail = b :: l

Tactic:
simp? at h says simp only [head?_cons, Option.mem_def, Option.some.injEq] at h

Result:
α : Type u
b : α
l : List α
a : α
h : b = a
⊢ a :: (b :: l).tail = b :: l

Proof state:
α : Type u
b : α
l : List α
a : α
h : b = a
⊢ a :: (b :: l).tail = b :: l

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem slash_one (k : ℤ) (f : ℍ → ℂ) : f ∣[k]1 = f :=
  funext <| by simp [slash, denom]

Proof state:
k : ℤ
f : ℍ → ℂ
⊢ ∀ (x : ℍ), (f ∣[k]1) x = f x

Tactic:
simp [slash, denom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem iff_and_self : (p ↔ q ∧ p) ↔ (p → q)

Proof state:
p q : Prop
⊢ (p ↔ q ∧ p) ↔ p → q

Tactic:
rw [and_comm, iff_self_and]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem neg_limZero {f : CauSeq β abv} (hf : LimZero f) : LimZero (-f)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : f.LimZero
⊢ (-1 * f).LimZero

Tactic:
exact mul_limZero_right _ hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : f.LimZero
⊢ (-f).LimZero

Tactic:
rw [← neg_one_mul f]

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : f.LimZero
⊢ (-1 * f).LimZero
-- Mathlib/Data/Fin/Rev.lean
theorem rev_pred {i : Fin (n + 1)} (h : i ≠ 0) (h' := rev_ne_iff.mpr ((rev_last _).symm ▸ h)) :
    rev (pred i h) = castPred (rev i) h'

Proof state:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : optParam (i.rev ≠ last n) ⋯
⊢ (i.pred h).rev = i.rev.castPred h'

Tactic:
rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem subset_inter {s₁ s₂ u : Finset α} : s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Tactic:
simp +contextual [subset_iff, mem_inter]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_mul_left {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
    normalize (↑a * n) (a * d) (Nat.mul_ne_zero a0 d0) = normalize n d d0

Proof state:
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (↑a * n) (a * d) ⋯ = normalize n d d0

Tactic:
simp [normalize_eq, mk'.injEq, Int.natAbs_mul, Nat.gcd_mul_left,
  Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero a0), Int.ofNat_mul,
  Int.mul_ediv_mul_of_pos _ _ (Int.ofNat_pos.2 <| Nat.pos_of_ne_zero a0)]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_comp : (g.comp f).rTensor M = (g.rTensor M).comp (f.rTensor M)

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
⊢ rTensor M (g ∘ₗ f) = rTensor M g ∘ₗ rTensor M f

Tactic:
ext m n

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : N
n : M
⊢ (((TensorProduct.mk R N M).compr₂ (rTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R N M).compr₂ (rTensor M g ∘ₗ rTensor M f)) m) n

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : N
n : M
⊢ (((TensorProduct.mk R N M).compr₂ (rTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R N M).compr₂ (rTensor M g ∘ₗ rTensor M f)) m) n

Tactic:
simp only [compr₂_apply, mk_apply, comp_apply, rTensor_tmul]

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
@[simp] lemma mkRat_pow (num den : ℕ) (n : ℕ) : mkRat num den ^ n = mkRat (num ^ n) (den ^ n)

Proof state:
num den n : ℕ
⊢ mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)

Tactic:
rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem hσ'_eq_zero {q n m : ℕ} (hnq : n < q) (hnm : c.Rel m n) :
    (hσ' q n m hnm : X _⦋n⦌ ⟶ X _⦋m⦌) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ 0 ≫ eqToHom ⋯ = 0

Tactic:
exact zero_comp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ hσ' q n m hnm = 0

Tactic:
simp only [hσ', hσ]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = 0

Tactic:
split_ifs

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ 0 ≫ eqToHom ⋯ = 0
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_val_map {n : ℕ} (f : Fin n → α) :
    Finset.univ.val.map f = List.ofFn f

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Multiset.map f univ.val = ↑(List.ofFn f)

Tactic:
simp [List.ofFn_eq_map, univ_def]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_closedBall_self : x ∈ closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedBall x ε

Tactic:
rw [mem_closedBall, edist_self]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε

Tactic:
apply zero_le

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem zero_lt_orderTop_of_order {x : HahnSeries Γ R} (hx : 0 < x.order) : 0 < x.orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop

Tactic:
exact (zero_lt_orderTop_iff h).mpr hx

Result:
no goals

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : 0 < x.order
h : x = 0
⊢ 0 < x.orderTop

Tactic:
simp_all only [order_zero, lt_self_iff_false]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : 0 < x.order
⊢ 0 < x.orderTop

Tactic:
by_cases h : x = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : 0 < x.order
h : x = 0
⊢ 0 < x.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_dvd {s : Multiset α} {a : α} : s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and, lcm_dvd_iff])

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α), (s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a) → ((a_1 ::ₘ s).lcm ∣ a ↔ ∀ b ∈ a_1 ::ₘ s, b ∣ a)

Tactic:
simp +contextual [or_imp, forall_and, lcm_dvd_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ b ∈ 0, b ∣ a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

Proof state:
a : Nat
h : a = 0
⊢ 0 ≤ 0

Tactic:
decide

Result:
no goals

Proof state:
a : Nat
h : a = 0
⊢ a ≤ 0

Tactic:
rw [h]

Result:
a : Nat
h : a = 0
⊢ 0 ≤ 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_eq_findSome?_finRange (f : Fin n → Option α) :
    findSome? f = (List.finRange n).findSome? f

Proof state:
case zero
α : Type u_1
f : Fin 0 → Option α
⊢ findSome? f = List.findSome? f (List.finRange 0)

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ findSome? f = List.findSome? f (List.finRange n)

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [findSome?_succ, List.finRange_succ, List.findSome?_cons]
  cases f 0 <;> simp [ih, List.findSome?_map, Function.comp_def]

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → Option α), findSome? f = List.findSome? f (List.finRange n)
f : Fin (n + 1) → Option α
⊢ (f 0 <|> findSome? fun i => f i.succ) =
    match f 0 with
    | some b => some b
    | none => List.findSome? f (List.map succ (List.finRange n))

Tactic:
cases f 0 <;> simp [ih, List.findSome?_map, Function.comp_def]

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → Option α), findSome? f = List.findSome? f (List.finRange n)
f : Fin (n + 1) → Option α
⊢ findSome? f = List.findSome? f (List.finRange (n + 1))

Tactic:
rw [findSome?_succ, List.finRange_succ, List.findSome?_cons]

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → Option α), findSome? f = List.findSome? f (List.finRange n)
f : Fin (n + 1) → Option α
⊢ (f 0 <|> findSome? fun i => f i.succ) =
    match f 0 with
    | some b => some b
    | none => List.findSome? f (List.map succ (List.finRange n))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem erase_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
    m.erase a = Raw₀.erase ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
⊢ m.erase a = (Raw₀.erase ⟨m, ⋯⟩ a).val

Tactic:
simp [Raw.erase, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_bot_order [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
    𝓝 (⊥ : α) = ⨅ (l) (_ : ⊥ < l), 𝓟 (Iio l)

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : OrderTopology α
⊢ 𝓝 ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l)

Tactic:
simp [nhds_eq_order (⊥ : α)]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem modOf_apply_of_not_exists_add (x : k[G]) (g : G) (g' : G)
    (h : ¬∃ d, g' = g + d) : (x %ᵒᶠ g) g' = x g'

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x %ᵒᶠ g) g' = x g'

Tactic:
classical exact Finsupp.filter_apply_pos _ _ h

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x %ᵒᶠ g) g' = x g'

Tactic:
exact Finsupp.filter_apply_pos _ _ h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α}
    (contains : (l.map Sigma.fst).contains k = false)
    {h'} :
    (m.insertMany l).1.get k h' =
    m.get k (contains_of_contains_insertMany_list _ h h' contains)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k : α
contains : (List.map Sigma.fst l).contains k = false
h' : (m.insertMany l).val.contains k = true
⊢ (m.insertMany l).val.get k h' = m.get k ⋯

Tactic:
simp_to_model [insertMany] using List.getValueCast_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1))

Proof state:
case refine_1
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))

Tactic:
simp [fastFibAux]

Result:
no goals

Proof state:
n : ℕ
⊢ n.fastFibAux = (fib n, fib (n + 1))

Tactic:
refine Nat.binaryRec ?_ ?_ n

Result:
case refine_1
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))

case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Proof state:
case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Tactic:
rintro (_|_) n' ih <;>
  simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih,
    congr_arg Prod.snd ih, Prod.mk.inj_iff] <;>
  simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem size_pos {n : ℕ} : 0 < size n ↔ 0 < n

Proof state:
n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < n.size ↔ 0 < n

Tactic:
rw [lt_size]

Result:
n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem algebraMap_eval_S [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((S R n).eval x) = (S R' n).eval (algebraMap R R' x)

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (S R n)) = eval ((algebraMap R R') x) (S R' n)

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_erase_left (a b : α) : (Icc a b).erase a = Ioc a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase a = Ioc a b

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem factorization_one : factorization (1 : α) = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
⊢ factorization 1 = 0

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_polynomial : (W'.baseChange B).toAffine.polynomial =
    (W'.baseChange A).toAffine.polynomial.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toAffine.polynomial = Polynomial.map (mapRingHom ↑f) (baseChange W' A).toAffine.polynomial

Tactic:
rw [← map_polynomial, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
@[simp] lemma toFinset_nsmul (s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset
  | 0, h => by contradiction
  | n + 1, _ => by
    by_cases h : n = 0
    · rw [h, zero_add, one_nsmul]
    · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
h : 0 ≠ 0
⊢ (0 • s).toFinset = s.toFinset

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
by_cases h : n = 0

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
rw [h, zero_add, one_nsmul]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.mul_zero (hs : s.Nonempty) : s * 0 = 0 :=
  s.mul_zero_subset.antisymm <| by simpa [mem_mul] using hs

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
simpa [mem_mul] using hs

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_mod_period_smul (n : ℕ) {m : M} {a : α} :
    m ^ (n % period m a) • a = m ^ n • a

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n % period m a) • a = m ^ n • a

Tactic:
conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
  pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equation_some (X Y : R) : W'.Equation ![X, Y, 1] ↔ W'.toAffine.Equation X Y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
⊢ W'.Equation ![X, Y, 1] ↔ (toAffine W').Equation X Y

Tactic:
simp only [equation_iff, Affine.equation_iff', fin3_def_ext, one_pow, mul_one]

Result:
no goals