harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) :
    degrees (rename f p) = (degrees p).map f

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ p.support.sup ((fun s => toMultiset s) ∘ Finsupp.mapDomain f) = p.support.sup (Multiset.map f ∘ ⇑toMultiset)

Tactic:
refine Finset.sup_congr rfl fun x _ => ?_

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
x✝ : x ∈ p.support
⊢ ((fun s => toMultiset s) ∘ Finsupp.mapDomain f) x = (Multiset.map f ∘ ⇑toMultiset) x

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ ((rename f) p).degrees = Multiset.map f p.degrees

Tactic:
classical
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
  support_rename_of_injective h, Finset.sup_image]
refine Finset.sup_congr rfl fun x _ => ?_
exact (Finsupp.toMultiset_map _ _).symm

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ ((rename f) p).degrees = Multiset.map f p.degrees

Tactic:
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
  support_rename_of_injective h, Finset.sup_image]

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ p.support.sup ((fun s => toMultiset s) ∘ Finsupp.mapDomain f) = p.support.sup (Multiset.map f ∘ ⇑toMultiset)

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
x✝ : x ∈ p.support
⊢ ((fun s => toMultiset s) ∘ Finsupp.mapDomain f) x = (Multiset.map f ∘ ⇑toMultiset) x

Tactic:
exact (Finsupp.toMultiset_map _ _).symm

Result:
no goals
-- Mathlib/Data/Finset/Update.lean
@[simp]
lemma updateFinset_restrict {s : Finset ι} (x : Π i, π i) :
    updateFinset x s (s.restrict x) = x

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
⊢ updateFinset x s (s.restrict x) = x

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
i : ι
⊢ updateFinset x s (s.restrict x) i = x i

Proof state:
case h
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
i : ι
⊢ updateFinset x s (s.restrict x) i = x i

Tactic:
simp [updateFinset]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.mem_submodule_iff' [Fintype ι] {P : Submodule R M} (b : Basis ι R P) {x : M} :
    x ∈ P ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : M) :=
  b.mem_submodule_iff.trans <|
    Finsupp.equivFunOnFinite.exists_congr_left.trans <|
      exists_congr fun c => by simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
P : Submodule R M
b : Basis ι R ↥P
x : M
c : ι → R
⊢ (x = (equivFunOnFinite.symm c).sum fun i x => x • ↑(b i)) ↔ x = ∑ i : ι, c i • ↑(b i)

Tactic:
simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem range_arcsin : range arcsin = Icc (-(π / 2)) (π / 2)

Proof state:
⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)

Tactic:
simp [Icc]

Result:
no goals

Proof state:
⊢ range arcsin = Icc (-(π / 2)) (π / 2)

Tactic:
rw [arcsin, range_comp Subtype.val]

Result:
⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)
-- Mathlib/Data/Finsupp/Basic.lean
theorem subtypeDomain_eq_zero_iff {f : α →₀ M} (hf : ∀ x ∈ f.support, p x) :
    f.subtypeDomain p = 0 ↔ f = 0 :=
  subtypeDomain_eq_iff (g := 0) hf (by simp)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ x ∈ f.support, p x
⊢ ∀ x ∈ support 0, p x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem tsum_of_norm_bounded {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : HasSum g a)
    (h : ∀ i, ‖f i‖ ≤ g i) : ‖∑' i : ι, f i‖ ≤ a

Proof state:
case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a

Tactic:
rw [tsum_eq_zero_of_not_summable hf, norm_zero]

Result:
case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Proof state:
case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
classical exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

Result:
no goals

Proof state:
case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖∑' (i : ι), f i‖ ≤ a

Tactic:
by_cases hf : Summable f

Result:
case pos
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a

case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a

Proof state:
case pos
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a

Tactic:
exact hf.hasSum.norm_le_of_bounded hg h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_smul (r : α) (A : Matrix n n α) :
    adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate

Tactic:
rw [adjugate, adjugate, transpose_smul, cramer_smul]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (of fun i => (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • of fun i => Aᵀ.cramer (Pi.single i 1)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (of fun i => (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • of fun i => Aᵀ.cramer (Pi.single i 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_intCast_le (n : ℤ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natDegree ≤ Zero.zero

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_sum_mul_antidiagonal_of_summable_mul
    (h : Summable fun x : A × A ↦ f x.1 * g x.2) :
    Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]

Result:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun x => ∑' (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f x.1 * g x.2
⊢ Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h

Result:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Proof state:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun x => ∑' (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
exact h.sigma' fun n ↦ (hasSum_fintype _).summable

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
lemma prod_norm_eq_add_idemFst [Fact (1 ≤ p)] (hp : 0 < p.toReal) (x : WithLp p (α × β)) :
    ‖x‖ = (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ ‖x‖ = (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rw [WithLp.prod_norm_eq_add hp, ← WithLp.norm_equiv_symm_fst p α β x.1,
  ← WithLp.norm_equiv_symm_snd p α β x.2]

Result:
α : Type u_2
β : Type u_3
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ (‖(WithLp.equiv p (α × β)).symm (x.1, 0)‖ ^ p.toReal + ‖(WithLp.equiv p (α × β)).symm (0, x.2)‖ ^ p.toReal) ^
      (1 / p.toReal) =
    (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ (‖(WithLp.equiv p (α × β)).symm (x.1, 0)‖ ^ p.toReal + ‖(WithLp.equiv p (α × β)).symm (0, x.2)‖ ^ p.toReal) ^
      (1 / p.toReal) =
    (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem left_eq_mul₀ (ha : a ≠ 0) : a = a * b ↔ b = 1

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
ha : a ≠ 0
⊢ a = a * b ↔ b = 1

Tactic:
rw [eq_comm, mul_eq_left₀ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ #[s + n]

Proof state:
s n : Nat
⊢ range' s (n + 1) = range' s n ++ #[s + n]

Tactic:
simp [range'_concat]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_four : tan (π / 4) = 1

Proof state:
⊢ √2 / 2 / (√2 / 2) = 1

Tactic:
have h : √2 / 2 > 0 := by positivity

Result:
h : √2 / 2 > 0
⊢ √2 / 2 / (√2 / 2) = 1

Proof state:
⊢ tan (π / 4) = 1

Tactic:
rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]

Result:
⊢ √2 / 2 / (√2 / 2) = 1

Proof state:
⊢ √2 / 2 > 0

Tactic:
positivity

Result:
no goals

Proof state:
h : √2 / 2 > 0
⊢ √2 / 2 / (√2 / 2) = 1

Tactic:
exact div_self (ne_of_gt h)

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformly_iff_tendsto {F : ι → α → β} {f : α → β} {p : Filter ι} :
    TendstoUniformly F f p ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)

Tactic:
simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem coeff_zero_prod : (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Tactic:
simpa using coeff_zero_multiset_prod (s.1.map f)

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.neg [AddGroup α] (h : Periodic f c) : Periodic f (-c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)

Tactic:
simpa only [sub_eq_add_neg, Periodic] using h.sub_eq

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem isUnit_det_zpow_iff {A : M} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0

Proof state:
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit (A ^ (-↑z - 1)).det ↔ IsUnit A.det ∨ -↑z - 1 = 0

Tactic:
rw [← neg_add', ← Int.ofNat_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
  isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]

Result:
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Proof state:
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Tactic:
simp

Result:
no goals

Proof state:
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit (A ^ (↑z + 1)).det ↔ IsUnit A.det ∨ ↑z + 1 = 0

Tactic:
rw [← Int.ofNat_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
  Int.ofNat_inj]

Result:
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Proof state:
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0

Tactic:
simp

Result:
no goals

Proof state:
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (A ^ 0).det ↔ IsUnit A.det ∨ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℤ
⊢ IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0

Tactic:
induction z with
| hz => simp
| hp z =>
  rw [← Int.ofNat_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
    Int.ofNat_inj]
  simp
| hn z =>
  rw [← neg_add', ← Int.ofNat_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
    isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
  simp

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
private lemma I_zero : I 0 θ * θ = 2 * sin θ

Proof state:
θ : ℝ
⊢ I 0 θ * θ = 2 * sin θ

Tactic:
rw [mul_comm, I]

Result:
θ : ℝ
⊢ θ * ∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ 0 * cos (x * θ) = 2 * sin θ

Proof state:
θ : ℝ
⊢ θ * ∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ 0 * cos (x * θ) = 2 * sin θ

Tactic:
simp [mul_integral_comp_mul_right, two_mul]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem esymm_mul_psum_to_weight [DecidableEq σ] (k : ℕ) :
    ∑ a ∈ antidiagonal k with a.fst < k, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd =
      ∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k),
      MvPolynomial.NewtonIdentities.weight σ R k t

Tactic:
rw [← sum_congr rfl (fun a ha ↦ esymm_mul_psum_summand_to_weight σ R k a (mem_filter.mp ha).left),
  sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum σ R k]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α} :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.contains k = (l.map Prod.fst).contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
⊢ (insertMany empty l).val.contains k = (List.map Prod.fst l).contains k

Tactic:
simp [contains_insertMany_list _ Raw.WF.empty₀]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
    i < (extract.loop as size start bs).size

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
⊢ i < (extract.loop as size start bs).size

Tactic:
rw [size_extract_loop]

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
⊢ i < bs.size + min size (as.size - start)

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
⊢ i < bs.size + min size (as.size - start)

Tactic:
apply Nat.lt_of_lt_of_le hlt

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
⊢ bs.size ≤ bs.size + min size (as.size - start)

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hlt : i < bs.size
⊢ bs.size ≤ bs.size + min size (as.size - start)

Tactic:
exact Nat.le_add_right ..

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBound_comm (a b : α) {i j : Nat} (v : Vector α n) (h : i ≠ j) :
    (v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a

Proof state:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
v : Array α
⊢ (v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a

Tactic:
rw [Array.setIfInBounds_comm _ _ _ h]

Result:
no goals

Proof state:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i a).setIfInBounds j b =
    ({ toArray := v, size_toArray := ⋯ }.setIfInBounds j b).setIfInBounds i a

Tactic:
simp only [setIfInBounds_mk, mk.injEq]

Result:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
v : Array α
⊢ (v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a

Proof state:
α : Type u_1
n : Nat
a b : α
i j : Nat
v : Vector α n
h : i ≠ j
⊢ (v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i a).setIfInBounds j b =
    ({ toArray := v, size_toArray := ⋯ }.setIfInBounds j b).setIfInBounds i a
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ * n‼
  | 0 => rfl
  | k + 1 => by
    rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]

Proof state:
k : ℕ
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼

Tactic:
rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
  mul_assoc]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem Bool.sup_eq_bor : (· ⊔ ·) = or

Proof state:
⊢ (fun x1 x2 => x1 ⊔ x2) = or

Tactic:
dsimp

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Colimits.lean
theorem Quot.desc_colimitCocone [DecidableEq J] (F : J ⥤ AddCommGrp.{w}) [Small.{w} (Quot F)] :
    Quot.desc F (colimitCocone F) = (Shrink.addEquiv (α := Quot F)).symm.toAddMonoidHom

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (desc F (colimitCocone F)) ((ι F j) x) = Shrink.addEquiv.symm.toAddMonoidHom ((ι F j) x)

Tactic:
simp only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe]

Result:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (desc F (colimitCocone F)) ((ι F j) x) = Shrink.addEquiv.symm ((ι F j) x)

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (desc F (colimitCocone F)) ((ι F j) x) = Shrink.addEquiv.symm ((ι F j) x)

Tactic:
erw [Quot.ι_desc]

Result:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j)) x = Shrink.addEquiv.symm ((ι F j) x)

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j)) x = Shrink.addEquiv.symm ((ι F j) x)

Tactic:
simp

Result:
no goals

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
⊢ desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Result:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrp
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (desc F (colimitCocone F)) ((ι F j) x) = Shrink.addEquiv.symm.toAddMonoidHom ((ι F j) x)
-- Mathlib/Analysis/Normed/Ring/Ultra.lean
lemma nnnorm_natCast_le_one (n : ℕ) :
    ‖(n : R)‖₊ ≤ 1

Proof state:
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
n : ℕ
⊢ ‖↑n‖₊ ≤ 1

Tactic:
induction n with
| zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
| succ n hn => simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
  nnnorm_add_one_le_max_nnnorm_one (n : R)

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
n : ℕ
hn : ‖↑n‖₊ ≤ 1
⊢ ‖↑(n + 1)‖₊ ≤ 1

Tactic:
simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
nnnorm_add_one_le_max_nnnorm_one (n : R)

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
⊢ ‖↑0‖₊ ≤ 1

Tactic:
simp only [Nat.cast_zero, nnnorm_zero, zero_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
    xs.isEmpty = false ↔ ∃ x, x ∈ xs

Proof state:
α : Type u_1
xs : Array α
⊢ xs.isEmpty = false ↔ ∃ x, x ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.isEmpty = false ↔ ∃ x, x ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.isEmpty = false ↔ ∃ x, x ∈ { toList := toList✝ }

Tactic:
simpa using List.isEmpty_eq_false_iff_exists_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insert_self [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] {b : β a} :
    (m.insert a b).get! a = b

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
b : β a
⊢ (m.insert a b).get! a = b

Tactic:
simp_to_model [insert] using List.getValueCast!_insertEntry_self

Result:
no goals