harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem even_mul_odd {f : ℕ → M} (he : HasProd (fun k ↦ f (2 * k)) m)
    (ho : HasProd (fun k ↦ f (2 * k + 1)) m') : HasProd f (m * m')

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
this : Injective fun x => 2 * x
ho : HasProd (fun x => f ↑x) m'
⊢ HasProd f (m * m')

Tactic:
refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
this : Injective fun x => 2 * x
ho : HasProd (fun x => f ↑x) m'
⊢ IsCompl (Set.range fun x => 2 * x) (Set.range ((fun x => x + 1) ∘ fun x => 2 * x))

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
ho : HasProd (fun k => f (2 * k + 1)) m'
this : Injective fun x => 2 * x
⊢ HasProd f (m * m')

Tactic:
replace ho := ((add_left_injective 1).comp this).hasProd_range_iff.2 ho

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
this : Injective fun x => 2 * x
ho : HasProd (fun x => f ↑x) m'
⊢ HasProd f (m * m')

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
ho : HasProd (fun k => f (2 * k + 1)) m'
⊢ HasProd f (m * m')

Tactic:
have := mul_right_injective₀ (two_ne_zero' ℕ)

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
ho : HasProd (fun k => f (2 * k + 1)) m'
this : Injective fun x => 2 * x
⊢ HasProd f (m * m')

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k => f (2 * k)) m
this : Injective fun x => 2 * x
ho : HasProd (fun x => f ↑x) m'
⊢ IsCompl (Set.range fun x => 2 * x) (Set.range ((fun x => x + 1) ∘ fun x => 2 * x))

Tactic:
simpa [Function.comp_def] using Nat.isCompl_even_odd

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma snoc_mem_piFinset_snoc {x_last : α (last n)} {x_init : (i : Fin n) → α i.castSucc}
    {s_last : Finset (α (last n))} {s_init : (i : Fin n) → Finset (α i.castSucc)} :
    snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔
      x_last ∈ s_last ∧ x_init ∈ piFinset s_init

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ piFinset s_init

Tactic:
simp_rw [mem_piFinset_iff_last_init, init_snoc, snoc_last]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_neg_set_neg (x : E) : gauge (-s) (-x) = gauge s x

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
⊢ gauge (-s) (-x) = gauge s x

Tactic:
simp_rw [gauge_def', smul_neg, neg_mem_neg]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem integralClosure.isIntegral (x : integralClosure R A) : IsIntegral R x :=
  let ⟨p, hpm, hpx⟩ := x.2
  ⟨p, hpm,
    Subtype.eq <| by
      rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx⟩

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x) p = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0

Tactic:
rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.or_self (b : Bool) : (b || b) = b

Proof state:
b : Bool
⊢ (b || b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_mk_id (f : S.obj Y ⟶ T) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
  homMk'_id _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
⊢ mk (S.map (𝟙 Y) ≫ (mk f).hom) = mk f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Submonoid M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffWithinAt_of_subsingleton [Subsingleton F] : ContDiffWithinAt 𝕜 n f s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n (fun x => 0) s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffWithinAt 𝕜 n (fun x => 0) s x

Tactic:
exact contDiffWithinAt_const

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem ball_sub_ball (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
    ball a ε - ball b δ = ball (a - b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
lemma shiftLeft_lt {x n m : ℕ} (h : x < 2 ^ n) : x <<< m < 2 ^ (n + m)

Proof state:
x n m : ℕ
h : x < 2 ^ n
⊢ x <<< m < 2 ^ (n + m)

Tactic:
simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_flatMap {α β} (f : α → β) (l : Vector α n) :
    map f l = (l.flatMap fun x => #v[f x]).cast (by simp)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f { toArray := l, size_toArray := ⋯ } =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => { toArray := #[f x], size_toArray := ⋯ })

Tactic:
simp [Array.map_eq_flatMap]

Result:
no goals

Proof state:
n : Nat
α : Type ?u.337821
β : Type ?u.337825
f : α → β
l : Vector α n
⊢ n * 1 = n

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α : Type u_1
β : Type u_2
f : α → β
l : Vector α n
⊢ map f l = Vector.cast ⋯ (l.flatMap fun x => { toArray := #[f x], size_toArray := ⋯ })

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f { toArray := l, size_toArray := ⋯ } =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => { toArray := #[f x], size_toArray := ⋯ })
-- Mathlib/Algebra/Star/StarAlgHom.lean
theorem snd_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : (snd R B C).comp (prod f g) = g

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Proof state:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem of_int {z : ℤ} : padicValRat p z = padicValInt p z

Proof state:
p : ℕ
z : ℤ
⊢ padicValRat p ↑z = ↑(padicValInt p z)

Tactic:
simp [padicValRat]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
/-- If `K/F` is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced
  by "generated by images of embeddings". -/
lemma isNormalClosure_iff : IsNormalClosure F K L ↔
    (∀ x : K, (minpoly F x).Splits (algebraMap F L)) ∧ normalClosure F K L = ⊤

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
⊢ IsNormalClosure F K L ↔ (∀ (x : K), Splits (algebraMap F L) (minpoly F x)) ∧ normalClosure F K L = ⊤

Tactic:
refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩ <;>
  simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_nsmul {x : ℝ} {n : ℕ} : ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

Proof state:
x : ℝ
n : ℕ
⊢ ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

Tactic:
simp only [nsmul_eq_mul, ← ofReal_natCast n, ← ofReal_mul n.cast_nonneg]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_fin_three (A : Matrix (Fin 3) (Fin 3) R) :
    det A =
      A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1
      - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0
      + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0

Proof state:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ (-1) ^ 0 * A 0 0 * ((-1) ^ 0 * A 1 1 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 1) +
      ((-1) ^ (0 + 1) * A 0 1 * ((-1) ^ 0 * A 1 0 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 0) +
        (-1) ^ (0 + 1 + 1) * A 0 2 * ((-1) ^ 0 * A 1 0 * A 2 1 + (-1) ^ (0 + 1) * A 1 1 * A 2 0)) =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
ring

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
simp only [det_succ_row_zero, submatrix_apply, Fin.succ_zero_eq_one, submatrix_submatrix,
  det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, Fin.sum_univ_succ,
  Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,
  Fin.succ_succAbove_zero, sum_singleton, Fin.succ_succAbove_one]

Result:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ (-1) ^ 0 * A 0 0 * ((-1) ^ 0 * A 1 1 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 1) +
      ((-1) ^ (0 + 1) * A 0 1 * ((-1) ^ 0 * A 1 0 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 0) +
        (-1) ^ (0 + 1 + 1) * A 0 2 * ((-1) ^ 0 * A 1 0 * A 2 1 + (-1) ^ (0 + 1) * A 1 1 * A 2 0)) =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_sub_right (hf : IntervalIntegrable f volume a b) (c : ℝ) :
    IntervalIntegrable (fun x => f (x - c)) volume (a + c) (b + c)

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (x - c)) volume (a + c) (b + c)

Tactic:
simpa only [sub_neg_eq_add] using IntervalIntegrable.comp_add_right hf (-c)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_zipIdx_map {l : Array α} {f : Nat → α → β} :
    l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
⊢ mapIdx f l =
    map
      (fun x =>
        match x with
        | (a, i) => f i a)
      l.zipIdx

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem other_mem {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other h ∈ z

Proof state:
case h.e'_4
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ z = s(a, Mem.other h)

Tactic:
rw [other_spec h]

Result:
no goals

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
convert mem_mk_right a <| Mem.other h

Result:
case h.e'_4
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ z = s(a, Mem.other h)
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem braiding_hom_snd {X Y : C} : (β_ X Y).hom ≫ snd _ _ = fst _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
⊢ (β_ X Y).hom ≫ snd Y X = fst X Y

Tactic:
simp [braiding_eq_braiding, fst, snd]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem finrank_orthogonal_span_singleton {n : ℕ} [_i : Fact (finrank 𝕜 E = n + 1)] {v : E}
    (hv : v ≠ 0) : finrank 𝕜 (𝕜 ∙ v)ᗮ = n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
⊢ finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n

Tactic:
haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ n

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n

Tactic:
exact Submodule.finrank_add_finrank_orthogonal' <| by
  simp [finrank_span_singleton hv, _i.elim, add_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 ↥(Submodule.span 𝕜 {v}) + n = finrank 𝕜 E

Tactic:
simp [finrank_span_singleton hv, _i.elim, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Count.lean
theorem count_set [BEq α] (a b : α) (l : List α) (i : Nat) (h : i < l.length) :
    (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
i : Nat
h : i < l.length
⊢ count b (l.set i a) = (count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0

Tactic:
simp [count_eq_countP, countP_set, h]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem inter_insert_of_mem (h : a ∈ s) : s ∩ insert a t = insert a (s ∩ t)

Proof state:
α : Type u
s t : Set α
a : α
h : a ∈ s
⊢ s ∩ insert a t = insert a (s ∩ t)

Tactic:
rw [insert_inter_distrib, insert_eq_of_mem h]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sSup_image2 {f : β → γ → α} {s : Set β} {t : Set γ} :
    sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b

Tactic:
rw [← image_prod, sSup_image, biSup_prod]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma id_apply (R : SemiRingCat) (r : R) :
    (𝟙 R : R ⟶ R) r = r

Proof state:
R : SemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma mul_self_sqrt (x : ℝ≥0) : sqrt x * sqrt x = x

Proof state:
x : ℝ≥0
⊢ sqrt x * sqrt x = x

Tactic:
rw [← sq, sq_sqrt]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
theorem toCircle_add (x : AddCircle T) (y : AddCircle T) :
    @toCircle T (x + y) = toCircle x * toCircle y

Proof state:
T : ℝ
x y : AddCircle T
⊢ (x + y).toCircle = x.toCircle * y.toCircle

Tactic:
induction x using QuotientAddGroup.induction_on

Result:
case H
T : ℝ
y : AddCircle T
z✝ : ℝ
⊢ (↑z✝ + y).toCircle = toCircle ↑z✝ * y.toCircle

Proof state:
case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝

Tactic:
simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]

Result:
no goals

Proof state:
case H
T : ℝ
y : AddCircle T
z✝ : ℝ
⊢ (↑z✝ + y).toCircle = toCircle ↑z✝ * y.toCircle

Tactic:
induction y using QuotientAddGroup.induction_on

Result:
case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma reflection_perm_self : P.reflection_perm i (P.reflection_perm i j) = j

Proof state:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root ((P.reflection_perm i) ((P.reflection_perm i) j)) = P.root j

Tactic:
simp only [root_reflection_perm, reflection_same]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflection_perm i) ((P.reflection_perm i) j) = j

Tactic:
apply P.root.injective

Result:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root ((P.reflection_perm i) ((P.reflection_perm i) j)) = P.root j
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_mul_left_eq_self [IsMulLeftInvariant μ] (f : G → E) (g : G) :
    (∫ x, f (g * x) ∂μ) = ∫ x, f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → E
g : G
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding

Result:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
rw [← h_mul.integral_map, map_mul_left_eq_self]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem infinite_iff_infinite_of_encard_eq_encard (h : s.encard = t.encard) :
    s.Infinite ↔ t.Infinite

Proof state:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Infinite ↔ t.Infinite

Tactic:
rw [← encard_eq_top_iff, h, encard_eq_top_iff]

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem isAssociative_left [Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
    Std.Associative ga :=
  ⟨fun x₁ x₂ x₃ ↦ h_inj <| by simp only [h.eq, Std.Associative.assoc (op := gb)]⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))

Tactic:
simp only [h.eq, Std.Associative.assoc (op := gb)]

Result:
no goals
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma ite_pos [LT α] (ha : 0 < a) (hb : 0 < b) : 0 < ite p a b

Proof state:
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_not_self : ∀ (x : Bool), (x || !x) = true

Proof state:
⊢ ∀ (x : Bool), (x || !x) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.symm (h : (fun x => f₁ x - f₂ x) =o[l] g) : (fun x => f₂ x - f₁ x) =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : (fun x => f₁ x - f₂ x) =o[l] g
⊢ (fun x => f₂ x - f₁ x) =o[l] g

Tactic:
simpa only [neg_sub] using h.neg_left

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem geom_lt {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n)
    (h : ∀ k < n, c * u k < u (k + 1)) : c ^ n * u 0 < u n

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

Tactic:
simp

Result:
no goals

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)

Tactic:
simp [_root_.pow_succ', mul_assoc, le_refl]

Result:
no goals

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h

Result:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_zero_one (b : α) : toIcoMod (zero_lt_one' α) 0 b = Int.fract b

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
b : α
⊢ toIcoMod ⋯ 0 b = Int.fract b

Tactic:
simp [toIcoMod_eq_add_fract_mul]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_cons' (s : Finset α) (a : α) (f : α → β)
    (ha : a ∉ s) (comm) :
    noncommProd (cons a s ha) f comm =
      noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr) * f a

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
theorem eq_zero_of_vecMul_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
    (hv : v ᵥ* M = 0) : v = 0 :=
  (nondegenerate_of_det_ne_zero hM).eq_zero_of_ortho fun w => by
    rw [dotProduct_mulVec, hv, zero_dotProduct]

Proof state:
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : v ᵥ* M = 0
w : m → A
⊢ v ⬝ᵥ M *ᵥ w = 0

Tactic:
rw [dotProduct_mulVec, hv, zero_dotProduct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ite_eq_true_else_eq_false {q : Prop} :
    (if b = true then q else b = false) ↔ (b = true → q)

Proof state:
b : Bool
q : Prop
⊢ (if b = true then q else b = false) ↔ b = true → q

Tactic:
cases b <;> simp [not_eq_self]

Result:
no goals