harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem toWord_inv (x : FreeGroup α) : x⁻¹.toWord = invRev x.toWord

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

Tactic:
rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.toWord = invRev x.toWord

Tactic:
rcases x with ⟨L⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ (Quot.mk Red.Step L)⁻¹.toWord = invRev (toWord (Quot.mk Red.Step L))
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma f_int_negSucc (k : ℕ) {a : ℝ} (ha : a ≤ 1) (t : ℝ) (n : ℕ) :
    f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Proof state:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ ↑(Int.negSucc n) + a = -(↑n + (1 - a))

Tactic:
push_cast

Result:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ -(↑n + 1) + a = -(↑n + (1 - a))

Proof state:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
have : (Int.negSucc n) + a = -(n + (1 - a)) := by { push_cast; ring }

Result:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Proof state:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]

Result:
no goals

Proof state:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ 0 ≤ ↑n + (1 - a)

Tactic:
linarith

Result:
no goals

Proof state:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ -(↑n + 1) + a = -(↑n + (1 - a))

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (· = ·) = true

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : Array α
⊢ (a.isEqv a fun x1 x2 => decide (x1 = x2)) = true

Tactic:
simp [isEqv, isEqvAux_self]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
    (s₂.map e).affineCombination k p w = s₂.affineCombination k (p ∘ e) (w ∘ e)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ (affineCombination k (map e s₂) p) w = (affineCombination k s₂ (p ∘ ⇑e)) (w ∘ ⇑e)

Tactic:
simp_rw [affineCombination_apply, weightedVSubOfPoint_map]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem completedRiemannZeta₀_one_sub (s : ℂ) :
    completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s

Proof state:
s : ℂ
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s

Tactic:
rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_erase (i : ι) (f : Π₀ i, β i) : (f.erase i).support = f.support.erase i

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
h1 : j = i
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

Tactic:
simp only [h1, mem_support_toFun, erase_apply, ite_true, ne_eq, not_true, not_not,
  Finset.mem_erase, false_and]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase i f).support = f.support.erase i

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

Tactic:
by_cases h1 : j = i

Result:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
h1 : j = i
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

case neg
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
h1 : ¬j = i
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
h1 : ¬j = i
⊢ j ∈ (erase i f).support ↔ j ∈ f.support.erase i

Tactic:
by_cases h2 : f j ≠ 0 <;> simp at h2 <;> simp [h1, h2]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem lift_aleph (o : Ordinal.{u}) : lift.{v} (aleph o) = aleph (Ordinal.lift.{v} o)

Proof state:
o : Ordinal.{u}
⊢ lift.{v, u} (ℵ_ o) = ℵ_ (Ordinal.lift.{v, u} o)

Tactic:
simp [aleph_eq_preAleph]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem IsPeriodicPt.minimalPeriod_le (hn : 0 < n) (hx : IsPeriodicPt f n x) :
    minimalPeriod f x ≤ n

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
classical
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]

Result:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find ⋯ ≤ n

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Radon.lean
/-- Corner case for `helly_theorem'`. -/
private lemma helly_theorem_corner {F : ι → Set E} {s : Finset ι}
    (h_card_small : #s ≤ finrank 𝕜 E + 1)
    (h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
    (⋂ i ∈ s, F i).Nonempty := h_inter s (by simp) h_card_small

Proof state:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
F : ι → Set E
s : Finset ι
h_card_small : #s ≤ finrank 𝕜 E + 1
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
⊢ s ⊆ s

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerLeft_id {η : f ⟶ g}
    {η₁ : f ⟶ 𝟙 a ≫ g} {η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g}
    (e_η₁ : η ≫ (λ_ _).inv = η₁) (e_η₂ : (λ_ _).hom ≫ η₁ = η₂) :
    𝟙 a ◁ η = η₂

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ 𝟙 a ≫ g
η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙 a ◁ η = η₂

Tactic:
simp [e_η₁, e_η₂]

Result:
no goals
-- Mathlib/Data/Bool/AllAny.lean
theorem any_iff_exists_prop : (any l fun a => p a) ↔ ∃ a ∈ l, p a

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.any fun a => decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel (a : α)
    (hf : AEStronglyMeasurable f (κ a)) :
    AEStronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂(Kernel.condKernel κ (a, x)))
      (Kernel.fst κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable f (κ a)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)

Tactic:
rw [← κ.disintegrate κ.condKernel] at hf

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)

Tactic:
exact AEStronglyMeasurable.integral_kernel_compProd hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ ite (0 < y ∧ y ≤ x) ((x - y) % y) x + y * ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 = x

Tactic:
simp [h]

Result:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x

Proof state:
case base
x y : Nat
h : ¬(0 < y ∧ y ≤ x)
⊢ ite (0 < y ∧ y ≤ x) ((x - y) % y) x + y * ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 = x

Tactic:
simp [h]

Result:
no goals

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x

Tactic:
rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]

Result:
no goals

Proof state:
m k : Nat
⊢ m % k + k * (m / k) = m

Tactic:
induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
| base x y h => simp [h]
| ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_integral_le_pos (hf : Integrable f μ) : 0 < μ {x | ∫ a, f a ∂μ ≤ f x}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa only [average_eq_integral] using
  measure_average_le_pos (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
    (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j

Proof state:
n i : Nat
p : Nat → Bool
⊢ find? p (range n) = some i ↔ p i = true ∧ i ∈ range n ∧ ∀ (j : Nat), j < i → (!p j) = true

Tactic:
simp [range_eq_range']

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma exists_of_closure_ssubset (hXY : M.closure X ⊂ M.closure Y) : ∃ e ∈ Y, e ∉ M.closure X

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
⊢ ∃ e ∈ Y, e ∉ M.closure X

Tactic:
by_contra! hcon

Result:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
hcon : ∀ e ∈ Y, e ∈ M.closure X
⊢ False

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
hcon : ∀ e ∈ Y, e ∈ M.closure X
⊢ False

Tactic:
exact hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod_eq_add_emod_right {m n k : Int} (i : Int)
    (H : m % n = k % n) : (m + i) % n = (k + i) % n

Proof state:
m n k i : Int
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n

Tactic:
rw [← emod_add_emod, ← emod_add_emod k, H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_xor_distrib_left  : ∀ (x y z : Bool), (x && (y ^^ z)) = ((x && y) ^^ (x && z))

Proof state:
⊢ ∀ (x y z : Bool), (x && (y ^^ z)) = (x && y ^^ x && z)

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem uniformity_le_symm : 𝓤 α ≤ @Prod.swap α α <$> 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
exact tendsto_swap_uniformity.le_comap

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ Prod.swap <$> 𝓤 α

Tactic:
rw [map_swap_eq_comap_swap]

Result:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive natCast_sub_one_zsmul]
lemma zpow_natCast_sub_one (a : G) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a n 1

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nnnorm_pow_le [NormOneClass α] (a : α) (n : ℕ) : ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n :=
  Nat.recOn n (by simp only [pow_zero, nnnorm_one, le_rfl])
    fun k _hk => nnnorm_pow_le' a k.succ_pos

Proof state:
α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero

Tactic:
simp only [pow_zero, nnnorm_one, le_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem zip_replicate {a : α} {b : β} {m n : Nat} :
    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
m n : Nat
⊢ (take (min (replicate m a).length (replicate n b).length) (replicate m a)).zip
      (take (min (replicate m a).length (replicate n b).length) (replicate n b)) =
    replicate (min m n) (a, b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
m n : Nat
⊢ (replicate m a).zip (replicate n b) = replicate (min m n) (a, b)

Tactic:
rw [zip_eq_zip_take_min]

Result:
α : Type u_1
β : Type u_2
a : α
b : β
m n : Nat
⊢ (take (min (replicate m a).length (replicate n b).length) (replicate m a)).zip
      (take (min (replicate m a).length (replicate n b).length) (replicate n b)) =
    replicate (min m n) (a, b)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a

Tactic:
simp_to_raw using Raw₀.getKey?_insertIfNew

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.getKey? a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a
-- Mathlib/CategoryTheory/NatIso.lean
theorem inv_inv_app {F G : C ⥤ D} (e : F ≅ G) (X : C) : inv (e.inv.app X) = e.hom.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
X : C
⊢ inv (e.inv.app X) = e.hom.app X

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Nat/Choose/Dvd.lean
theorem dvd_choose_add (hp : Prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) :
    p ∣ choose (a + b) a

Proof state:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ (a + b).choose a

Tactic:
have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h

Result:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ (a + b).choose a

Proof state:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a

Tactic:
exact (h₁.resolve_right hbp.not_le).resolve_right hap.not_le

Result:
no goals

Proof state:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ (a + b).choose a

Tactic:
rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul,
  hp.dvd_factorial, hp.dvd_factorial] at h₁

Result:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_abs (x : ℝ) : log⁺ |x| = log⁺ x

Proof state:
x : ℝ
⊢ log⁺ |x| = log⁺ x

Tactic:
simp [posLog]

Result:
no goals
-- Mathlib/Control/Traversable/Equiv.lean
theorem comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : t' α) :
    Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Tactic:
simp [Equiv.map, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem mem_support_iff : n ∈ p.support ↔ p.coeff n ≠ 0

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∈ p.support ↔ p.coeff n ≠ 0

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ n ∈ { toFinsupp := toFinsupp✝ }.support ↔ { toFinsupp := toFinsupp✝ }.coeff n ≠ 0

Proof state:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ n ∈ { toFinsupp := toFinsupp✝ }.support ↔ { toFinsupp := toFinsupp✝ }.coeff n ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Iterate.lean
theorem hIterate_elim {P : Nat → Sort _} (Q : ∀(i : Nat), P i → Prop)
    {n : Nat} (f : ∀(i : Fin n), P i.val → P (i.val+1)) (s : P 0) (init : Q 0 s)
    (step : ∀(k : Fin n) (s : P k.val), Q k.val s → Q (k.val+1) (f k s)) :
    Q n (hIterate P s f)

Proof state:
P : Nat → Sort u_1
Q : (i : Nat) → P i → Prop
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s : P 0
init : Q 0 s
step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)
⊢ Q n (hIterate P s f)

Tactic:
exact hIterateFrom_elim _ _ _ _ init step

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_of_pos (hx : 0 < x) : log x = expOrderIso.symm ⟨x, hx⟩

Proof state:
x : ℝ
hx : 0 < x
⊢ log x = expOrderIso.symm ⟨x, hx⟩

Tactic:
rw [log_of_ne_zero hx.ne']

Result:
x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩

Proof state:
x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩

Tactic:
congr

Result:
case h.e_6.h.e_val
x : ℝ
hx : 0 < x
⊢ |x| = x

Proof state:
case h.e_6.h.e_val
x : ℝ
hx : 0 < x
⊢ |x| = x

Tactic:
exact abs_of_pos hx

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem toNonUnitalSubring_injective :
    Function.Injective (toNonUnitalSubring : NonUnitalSubalgebra R A → NonUnitalSubring A) :=
  fun S T h => ext fun x => by rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Result:
no goals
-- Mathlib/Order/Shrink.lean
@[simp]
lemma equivShrink_symm_top [Top α] : (equivShrink.{u} α).symm ⊤ = ⊤ :=
  (equivShrink.{u} α).injective (by simp)

Proof state:
α : Type v
inst✝¹ : Small.{u, v} α
inst✝ : Top α
⊢ (equivShrink α) ((equivShrink α).symm ⊤) = (equivShrink α) ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
theorem Absorbs.restrict_scalars
    {M N α : Type*} [Monoid N] [SMul M N] [SMul M α] [MulAction N α]
    [IsScalarTower M N α] [Bornology M] [Bornology N] {s t : Set α} (h : Absorbs N s t)
    (hbdd : Tendsto (· • 1 : M → N) (cobounded M) (cobounded N)) :
    Absorbs M s t :=
  (hbdd.eventually h).mono <| fun x hx ↦ by rwa [smul_one_smul N x s] at hx

Proof state:
M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x => x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ (x • 1) • s
⊢ t ⊆ x • s

Tactic:
rwa [smul_one_smul N x s] at hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackP1Iso_hom_snd (i : 𝒰.J) :
    (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd _ _ = pullback.fst _ _ ≫ p2 𝒰 f g

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.map i ≫ f) g = pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_snd]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_iff_sup_eq : IsCoprime I J ↔ I ⊔ J = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I ⊔ J = ⊤

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem natDegree_taylor (p : R[X]) (r : R) : natDegree (taylor r p) = natDegree p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).natDegree = p.natDegree

Tactic:
refine map_natDegree_eq_natDegree _ ?_

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n

Tactic:
intro n c c0

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ ((taylor r) ((monomial n) c)).natDegree = n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ ((taylor r) ((monomial n) c)).natDegree = n

Tactic:
simp [taylor_monomial, natDegree_C_mul_of_mul_ne_zero, natDegree_pow_X_add_C, c0]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.pow_even {χ : MulChar R R'} (hχ : χ.IsQuadratic) {n : ℕ} (hn : Even n) :
    χ ^ n = 1

Proof state:
case intro
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
⊢ χ ^ (2 * n) = 1

Tactic:
rw [pow_mul, hχ.sq_eq_one, one_pow]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even n
⊢ χ ^ n = 1

Tactic:
obtain ⟨n, rfl⟩ := even_iff_two_dvd.mp hn

Result:
case intro
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
⊢ χ ^ (2 * n) = 1