harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean
lemma one_le_prod {s : List R} (h : ∀ a ∈ s, 1 ≤ a) : 1 ≤ s.prod

Proof state:
case nil
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
h : ∀ (a : R), a ∈ [] → 1 ≤ a
⊢ 1 ≤ [].prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 1 ≤ a) → 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Tactic:
simp only [mem_cons, forall_eq_or_imp] at h

Result:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 1 ≤ a) → 1 ≤ tail.prod
h : 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Proof state:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod

Tactic:
induction s with
| nil => simp
| cons head tail hind =>
  simp only [prod_cons]
  simp only [mem_cons, forall_eq_or_imp] at h
  exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 1 ≤ a) → 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ (head :: tail).prod

Tactic:
simp only [prod_cons]

Result:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 1 ≤ a) → 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 1 ≤ a) → 1 ≤ tail.prod
h : 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Tactic:
exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mod_mul_right_div_self (m n k : Nat) : m % (n * k) / n = m / n % k

Proof state:
case inr.inl
m n : Nat
hn : n > 0
⊢ m % (n * 0) / n = m / n % 0

case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = m / n % k

Tactic:
simp [mod_zero]

Result:
case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = m / n % k

Proof state:
case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = m / n % k

Tactic:
conv => rhs; rw [← mod_add_div m (n * k)]

Result:
case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = (m % (n * k) + n * k * (m / (n * k))) / n % k

Proof state:
case inl
m k : Nat
⊢ m % (0 * k) / 0 = m / 0 % k

case inr
m n k : Nat
hn : n > 0
⊢ m % (n * k) / n = m / n % k

Tactic:
simp [mod_zero]

Result:
case inr
m n k : Nat
hn : n > 0
⊢ m % (n * k) / n = m / n % k

Proof state:
case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = (m % (n * k) + n * k * (m / (n * k))) / n % k

Tactic:
rw [Nat.mul_assoc, add_mul_div_left _ _ hn, add_mul_mod_self_left,
  mod_eq_of_lt (Nat.div_lt_of_lt_mul (mod_lt _ (Nat.mul_pos hn hk)))]

Result:
no goals

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

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hn)

Result:
case inl
m k : Nat
⊢ m % (0 * k) / 0 = m / 0 % k

case inr
m n k : Nat
hn : n > 0
⊢ m % (n * k) / n = m / n % k

Proof state:
case inr
m n k : Nat
hn : n > 0
⊢ m % (n * k) / n = m / n % k

Tactic:
rcases Nat.eq_zero_or_pos k with (rfl | hk)

Result:
case inr.inl
m n : Nat
hn : n > 0
⊢ m % (n * 0) / n = m / n % 0

case inr.inr
m n k : Nat
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = m / n % k
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem curryLeft_same {n : ℕ} (f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') :
    (f.curryLeft m).curryLeft m = 0 :=
  ext fun _ => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one

Proof state:
R' : Type u_10
M'' : Type u_11
N'' : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M''
inst✝² : AddCommMonoid N''
inst✝¹ : Module R' M''
inst✝ : Module R' N''
n : ℕ
f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N''
m : M''
x✝ : Fin n → M''
⊢ Matrix.vecCons m (Matrix.vecCons m x✝) 0 = Matrix.vecCons m (Matrix.vecCons m x✝) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive IsAddUnit.exists_neg]
lemma IsUnit.exists_right_inv (h : IsUnit a) : ∃ b, a * b = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1

Tactic:
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩

Result:
case intro.mk
M : Type u_1
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1

Proof state:
case intro.mk
M : Type u_1
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1

Tactic:
exact ⟨b, hab⟩

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
@[norm_cast move]
lemma piecewise_coe [∀ j, Decidable (j ∈ (s : Set ι))] :
    (s : Set ι).piecewise f g = s.piecewise f g

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : (j : ι) → Decidable (j ∈ ↑s)
⊢ (↑s).piecewise f g = s.piecewise f g

Tactic:
ext

Result:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : (j : ι) → Decidable (j ∈ ↑s)
x✝ : ι
⊢ (↑s).piecewise f g x✝ = s.piecewise f g x✝

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : (j : ι) → Decidable (j ∈ ↑s)
x✝ : ι
⊢ (↑s).piecewise f g x✝ = s.piecewise f g x✝

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.BddAbove.continuous_convolution_left_of_integrable
    [FirstCountableTopology G] [SecondCountableTopologyEither G E]
    (hbf : BddAbove (range fun x => ‖f x‖)) (hf : Continuous f) (hg : Integrable g μ) :
    Continuous (f ⋆[L, μ] g)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedSpace 𝕜 E'
inst✝¹⁰ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : AddCommGroup G
inst✝⁶ : μ.IsAddLeftInvariant
inst✝⁵ : μ.IsNegInvariant
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E
hbf : BddAbove (range fun x => ‖f x‖)
hf : Continuous f
hg : Integrable g μ
⊢ Continuous (f ⋆[L, μ] g)

Tactic:
rw [← convolution_flip]

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedSpace 𝕜 E'
inst✝¹⁰ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : AddCommGroup G
inst✝⁶ : μ.IsAddLeftInvariant
inst✝⁵ : μ.IsNegInvariant
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E
hbf : BddAbove (range fun x => ‖f x‖)
hf : Continuous f
hg : Integrable g μ
⊢ Continuous (g ⋆[L.flip, μ] f)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedSpace 𝕜 E'
inst✝¹⁰ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : AddCommGroup G
inst✝⁶ : μ.IsAddLeftInvariant
inst✝⁵ : μ.IsNegInvariant
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E
hbf : BddAbove (range fun x => ‖f x‖)
hf : Continuous f
hg : Integrable g μ
⊢ Continuous (g ⋆[L.flip, μ] f)

Tactic:
exact hbf.continuous_convolution_right_of_integrable L.flip hg hf

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem mkPiRing_eq_iff {z₁ z₂ : M} :
    ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔
      z₁ = z₂

Proof state:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z₁ z₂ : M
⊢ ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Tactic:
rw [← toMultilinearMap_injective.eq_iff]

Result:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z₁ z₂ : M
⊢ (ContinuousMultilinearMap.mkPiRing R ι z₁).toMultilinearMap =
      (ContinuousMultilinearMap.mkPiRing R ι z₂).toMultilinearMap ↔
    z₁ = z₂

Proof state:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z₁ z₂ : M
⊢ (ContinuousMultilinearMap.mkPiRing R ι z₁).toMultilinearMap =
      (ContinuousMultilinearMap.mkPiRing R ι z₂).toMultilinearMap ↔
    z₁ = z₂

Tactic:
exact MultilinearMap.mkPiRing_eq_iff

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma iInf_toNat : (⨅ i, (f i : ℕ∞)).toNat = ⨅ i, f i

Proof state:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
norm_cast

Result:
no goals

Proof state:
case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℕ
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i
-- Mathlib/Algebra/Lie/Solvable.lean
theorem Surjective.lieAlgebra_isSolvable [hL' : IsSolvable L'] (h : Surjective f) :
    IsSolvable L

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥

Tactic:
simp only [LieIdeal.map_eq_bot_iff, bot_le]

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L' a = ⊥ → derivedSeries R L a = ⊥

Tactic:
intro k hk

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ derivedSeries R L k = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∃ k, derivedSeries R L k = ⊥

Tactic:
apply hL'.imp

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L' a = ⊥ → derivedSeries R L a = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : IsSolvable L'
h : Surjective ⇑f
⊢ IsSolvable L

Tactic:
rw [isSolvable_iff R] at hL' ⊢

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∃ k, derivedSeries R L k = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ derivedSeries R L k = ⊥

Tactic:
rw [← LieIdeal.derivedSeries_map_eq k h, hk]

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
-- Mathlib/Data/ENNReal/Inv.lean
lemma inv_sInf (s : Set ℝ≥0∞) : (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Proof state:
s : Set ℝ≥0∞
⊢ (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Tactic:
simp [sInf_eq_iInf, inv_iInf]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem tendsto_iff_tendstoUniformlyOn {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} :
    Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ F) ((toFun 𝔖) f) p s

Tactic:
simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal, TendstoUniformlyOn,
  Function.comp_apply, mem_setOf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem finIdxOf?_toArray [BEq α] (a : α) (v : Vector α n) :
    v.toArray.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast v.size_toArray.symm)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
v : Vector α n
⊢ v.finIdxOf? a = Option.map (Fin.cast ⋯) (v.finIdxOf? a)

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : Array α
⊢ { toArray := v, size_toArray := ⋯ }.finIdxOf? a =
    Option.map (Fin.cast ⋯) ({ toArray := v, size_toArray := ⋯ }.finIdxOf? a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : Array α
⊢ { toArray := v, size_toArray := ⋯ }.finIdxOf? a =
    Option.map (Fin.cast ⋯) ({ toArray := v, size_toArray := ⋯ }.finIdxOf? a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem tan_add {x y : ℝ}
    (h : ((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) ∨
      (∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y = (2 * l + 1) * π / 2) :
    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Proof state:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ ((∀ (k : ℤ), ↑x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑y = (2 * ↑l + 1) * ↑π / 2

Tactic:
convert h <;> norm_cast

Result:
no goals

Proof state:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div,
  Complex.ofReal_mul, Complex.ofReal_tan] using
  @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_singleton_inter (s : Set α) (x : α) : ({x} ∩ s).encard ≤ 1

Proof state:
α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ 1

Tactic:
rw [← encard_singleton x]

Result:
α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ {x}.encard

Proof state:
α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ {x}.encard

Tactic:
exact encard_le_encard inter_subset_left

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem _root_.Real.toNNReal_prod_of_nonneg (hf : ∀ a, a ∈ s → 0 ≤ f a) :
    Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, Real.toNNReal (f a)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNReal

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNReal

Tactic:
exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_setIfInBounds_self_of_lt (v : Vector α n) (i : Nat) (x : α) (h : i < n) :
    (v.setIfInBounds i x)[i]? = some x

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
h : i < n
⊢ (v.setIfInBounds i x)[i]? = some x

Tactic:
simp [getElem?_setIfInBounds, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem comp_factorThruImage_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage g]
    (h : f ≫ g = 0) : f ≫ factorThruImage g = 0 :=
  zero_of_comp_mono (image.ι g) <| by simp [h]

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : HasImage g
h : f ≫ g = 0
⊢ (f ≫ factorThruImage g) ≫ image.ι g = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem neg_left {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ⟂ᵥ w) : -v ⟂ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ⟂ᵥ w
⊢ -v ⟂ᵥ w

Tactic:
obtain ⟨u, hmu, hu₁, hu₂⟩ := h

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
⊢ -v ⟂ᵥ w

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑(-v) s = 0

Tactic:
rw [neg_apply v s, neg_eq_zero]

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑v s = 0

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑v s = 0

Tactic:
exact hu₁ s hs

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
⊢ -v ⟂ᵥ w

Tactic:
refine ⟨u, hmu, fun s hs => ?_, hu₂⟩

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑(-v) s = 0
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
lemma shiftIso_add_hom_app (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).hom.app X =
      (shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X) ≫
        ((F.shiftIso m a' a'' ha'').hom.app X)⟦n⟧' ≫
        (F.shiftIso n a a' ha').hom.app X

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{?u.4857, u_1} C
inst✝⁶ : Category.{?u.4861, u_2} D
inst✝⁵ : Category.{?u.4865, u_3} E
inst✝⁴ : Category.{?u.4869, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso (m + n) a a'' ⋯).hom.app X =
    (shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X) ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Proof state:
x : ℝ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)

Proof state:
x : ℝ
⊢ ↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)

Tactic:
simp [cos_three_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_lt_top :
    s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ⊤

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
  | [], [] => by simp [isPerm, isEmpty]
  | [], _ :: _ => by simp [isPerm, isEmpty, Perm.nil_eq]
  | a :: l₁, l₂ => by simp [isPerm, isPerm_iff, cons_perm_iff_perm_erase]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ [].isPerm [] = true ↔ [] ~ []

Tactic:
simp [isPerm, isEmpty]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ (a :: l₁).isPerm l₂ = true ↔ a :: l₁ ~ l₂

Tactic:
simp [isPerm, isPerm_iff, cons_perm_iff_perm_erase]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ [].isPerm (head✝ :: tail✝) = true ↔ [] ~ head✝ :: tail✝

Tactic:
simp [isPerm, isEmpty, Perm.nil_eq]

Result:
no goals