harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_comp_cast_add {n m : ℕ} {α : Sort*} (f : Fin (n + m) → α) (a : α) :
    (snoc f a : Fin _ → α) ∘ castAdd (m + 1) = f ∘ castAdd m :=
  funext (by unfold comp; exact snoc_cast_add _ _)

Proof state:
n m : ℕ
α : Sort u_2
f : Fin (n + m) → α
a : α
⊢ ∀ (x : Fin n), snoc f a (castAdd (m + 1) x) = f (castAdd m x)

Tactic:
exact snoc_cast_add _ _

Result:
no goals

Proof state:
n m : ℕ
α : Sort u_2
f : Fin (n + m) → α
a : α
⊢ ∀ (x : Fin n), (snoc f a ∘ castAdd (m + 1)) x = (f ∘ castAdd m) x

Tactic:
unfold comp

Result:
n m : ℕ
α : Sort u_2
f : Fin (n + m) → α
a : α
⊢ ∀ (x : Fin n), snoc f a (castAdd (m + 1) x) = f (castAdd m x)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ico' (hb : μ {b} ≠ ∞) :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b

Tactic:
contrapose! hab

Result:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a < b
⊢ a ≤ b

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
by_cases hab : a ≤ b

Result:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [← Ico_union_right hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [Icc_eq_empty hab, Ico_eq_empty]

Result:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a < b
⊢ a ≤ b

Tactic:
exact hab.le

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.ofReal {f : α → ℝ} (hf : Integrable f μ) :
    Integrable (fun x => (f x : 𝕜)) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → ℝ
hf : MemLp f 1 μ
⊢ MemLp (fun x => ↑(f x)) 1 μ

Tactic:
exact hf.ofReal

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x => ↑(f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → ℝ
hf : MemLp f 1 μ
⊢ MemLp (fun x => ↑(f x)) 1 μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
    [a].mapFinIdx f = [f 0 a (by simp)]

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (i : Nat) → α → i < 1 → β
⊢ [a].mapFinIdx f = [f 0 a ⋯]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.30900
β : Type ?u.30905
a : α
f : (i : Nat) → α → i < 1 → β
⊢ 0 < 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem MeasurableEmbedding.aemeasurable_comp_iff {g : β → γ} (hg : MeasurableEmbedding g)
    {μ : Measure α} : AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
⊢ AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable f μ

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ

Tactic:
exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toFinsupp_singleton (a : α) : toFinsupp ({a} : Multiset α) = Finsupp.single a 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toFinsupp {a} = Finsupp.single a 1

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝

Tactic:
rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {s : R}
    (hs : IsSumSq s) : 0 ≤ s

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s : R
hs : IsSumSq s
⊢ 0 ≤ s

Tactic:
induction hs using IsSumSq.rec' with
| zero          => simp
| sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s : R
⊢ 0 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case sq_add
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s x✝ s✝ : R
hx : IsSquare x✝
hs✝ : IsSumSq s✝
h : 0 ≤ s✝
⊢ 0 ≤ x✝ + s✝

Tactic:
exact add_nonneg (IsSquare.nonneg hx) h

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem intCast {f : ArithmeticFunction ℤ} [Ring R] (h : f.IsMultiplicative) :
    IsMultiplicative (f : ArithmeticFunction R) :=
                                 -- Porting note: was `by simp [cop, h]`
  ⟨by simp [h], fun {m n} cop => by simp [h.2 cop]⟩

Proof state:
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ↑f (m * n) = ↑f m * ↑f n

Tactic:
simp [h.2 cop]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_mul : ∀ {p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

Tactic:
apply MvPolynomial.induction_on q

Result:
case h_C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)

case h_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)

case h_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)

Proof state:
case h_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)

Tactic:
simp +contextual [X, eval₂_monomial, eval₂_mul_monomial, ← mul_assoc]

Result:
no goals

Proof state:
case h_C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)

Tactic:
simp [eval₂_C, eval₂_mul_C]

Result:
no goals

Proof state:
case h_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)

Tactic:
simp +contextual [mul_add, eval₂_add]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem dropSlice_eq (xs : List α) (n m : ℕ) : dropSlice n m xs = xs.take n ++ xs.drop (n + m)

Proof state:
case zero
α : Type u
m : ℕ
xs : List α
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs

Tactic:
cases xs <;> simp [dropSlice]

Result:
no goals

Proof state:
case succ
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (n✝ + 1) m xs = take (n✝ + 1) xs ++ drop (n✝ + 1 + m) xs

Tactic:
cases xs <;> simp [dropSlice, *, Nat.succ_add]

Result:
no goals

Proof state:
α : Type u
xs : List α
n m : ℕ
⊢ dropSlice n m xs = take n xs ++ drop (n + m) xs

Tactic:
induction n generalizing xs

Result:
case zero
α : Type u
m : ℕ
xs : List α
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs

case succ
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (n✝ + 1) m xs = take (n✝ + 1) xs ++ drop (n✝ + 1 + m) xs
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_eq_right_iff {p : Prop} [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y

Proof state:
α : Sort u_1
p : Prop
inst✝ : Decidable p
x : p → α
y : α
⊢ (if h : p then x h else y) = y ↔ ∀ (h : p), x h = y

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_of_nonempty_iUnion_eq_univ
    {s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = univ) : Nonempty ι :=
  nonempty_of_nonempty_iUnion (s := s) (by simpa only [h_Union] using univ_nonempty)

Proof state:
α : Type u_1
ι : Sort u_5
s : ι → Set α
inst✝ : Nonempty α
h_Union : ⋃ i, s i = univ
⊢ (⋃ i, s i).Nonempty

Tactic:
simpa only [h_Union] using univ_nonempty

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma vecMul_swap_apply (i j : n) (a : n → R) :
    (a ᵥ* swap R i j) i = a j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ (a ᵥ* swap R i j) i = a j

Tactic:
simp [swap, PEquiv.vecMul_toMatrix_toPEquiv]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_ne_one : a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Proof state:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Result:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Proof state:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_append_of_containsKey_right_eq_false {a : α} {f : Option β → Option β}
    {l l' : List ((_ : α) × β)} (hc : containsKey a l' = false) :
    alterKey a f (l ++ l') = alterKey a f l ++ l'

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hc : containsKey a l' = false
⊢ (match f (getValue? a l) with
    | none => eraseKey a l ++ l'
    | some v => insertEntry a v l ++ l') =
    (match f (getValue? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ++
      l'

Tactic:
split <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hc : containsKey a l' = false
⊢ alterKey a f (l ++ l') = alterKey a f l ++ l'

Tactic:
simp only [alterKey, getValue?_append_of_containsKey_eq_false hc,
  eraseKey_append_of_containsKey_right_eq_false hc, insertEntry_append_of_not_contains_right hc]

Result:
α : Type u
inst✝ : BEq α
β : Type v
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hc : containsKey a l' = false
⊢ (match f (getValue? a l) with
    | none => eraseKey a l ++ l'
    | some v => insertEntry a v l ++ l') =
    (match f (getValue? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ++
      l'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forIn'_mk [Monad m]
    (xs : Array α) (h : xs.size = n) (b : β)
    (f : (a : α) → a ∈ Vector.mk xs h → β → m (ForInStep β)) :
    forIn' (Vector.mk xs h) b f = forIn' xs b (fun a m b => f a (by simpa using m) b) := rfl

Proof state:
m✝ : Type ?u.12349 → Type ?u.12288
α : Type ?u.12293
n : Nat
β : Type ?u.12349
inst✝ : Monad m✝
xs : Array α
h : xs.size = n
b✝ : β
f : (a : α) → a ∈ { toArray := xs, size_toArray := h } → β → m✝ (ForInStep β)
a : α
m : a ∈ xs
b : β
⊢ a ∈ { toArray := xs, size_toArray := h }

Tactic:
simpa using m

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem _root_.NumberField.mixedEmbedding.covolume_idealLattice (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
    ZLattice.covolume (mixedEmbedding.idealLattice K I) =
      (FractionalIdeal.absNorm (I : FractionalIdeal (𝓞 K)⁰ K)) *
        (2 ⁻¹) ^ nrComplexPlaces K * √|discr K|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ ZLattice.covolume (idealLattice K I) volume = ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
  volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
  ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
  ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
  ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), mul_assoc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_rotation_pi_div_two_left (x : V) : ⟪o.rotation (π / 2 : ℝ) x, x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ inner ((o.rotation ↑(π / 2)) x) x = 0

Tactic:
rw [rotation_pi_div_two, inner_rightAngleRotation_self]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps] lemma even_add : Even (m + n) ↔ (Even m ↔ Even n)

Proof state:
m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
simp [even_iff, h₁, h₂, Int.add_emod, one_add_one_eq_two, emod_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_ΨSq_ne_zero [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) :
    (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0

Tactic:
rwa [coeff_ΨSq, pow_ne_zero_iff two_ne_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem one_div_Gamma_eq_self_mul_one_div_Gamma_add_one (s : ℂ) :
    (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Proof state:
s : ℂ
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Tactic:
rcases ne_or_eq s 0 with (h | rfl)

Result:
case inl
s : ℂ
h : s ≠ 0
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

case inr

⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹

Proof state:
case inr

⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹

Tactic:
rw [zero_add, Gamma_zero, inv_zero, zero_mul]

Result:
no goals

Proof state:
case inl
s : ℂ
h : s ≠ 0
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Tactic:
rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry_eq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
    (h : getEntry? a l = some ⟨k, v⟩) {h'} : getEntry a l h' = ⟨k, v⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : getEntry? a l = some ⟨k, v⟩
h' : containsKey a l = true
⊢ getEntry a l h' = ⟨k, v⟩

Tactic:
simp [getEntry, h]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem core_eq (f : α →. β) (s : Set β) : f.core s = f.preimage s ∪ f.Domᶜ

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = f.preimage s ∪ f.Domᶜ

Tactic:
rw [preimage_eq, Set.inter_union_distrib_right, Set.union_comm (Dom f), Set.compl_union_self,
  Set.inter_univ, Set.union_eq_self_of_subset_right (f.compl_dom_subset_core s)]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Ioc : (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem sigma_add :
    ∀ t u : ∀ a, Multiset (σ a), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u => by
    rw [cons_sigma, IH]
    simp [add_comm, add_left_comm, add_assoc]

Proof state:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
simp [add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma fun a => t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
rw [cons_sigma, IH]

Result:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem toNat_add_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) :
    (x + y).toNat = x.toNat + y.toNat

Proof state:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ x.toNat + y.toNat < 2 ^ w

Tactic:
suffices ¬ decide (x.toNat + y.toNat + false.toNat ≥ 2^w) by
  simp only [decide_eq_true_eq] at this
  omega

Result:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ¬decide (x.toNat + y.toNat + false.toNat ≥ 2 ^ w) = true

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
this : ¬decide (x.toNat + y.toNat + false.toNat ≥ 2 ^ w) = true
⊢ x.toNat + y.toNat < 2 ^ w

Tactic:
simp only [decide_eq_true_eq] at this

Result:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
this : ¬x.toNat + y.toNat + false.toNat ≥ 2 ^ w
⊢ x.toNat + y.toNat < 2 ^ w

Proof state:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ¬decide (x.toNat + y.toNat + false.toNat ≥ 2 ^ w) = true

Tactic:
rw [← carry_width]

Result:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ¬carry w x y false = true

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ (x.toNat + y.toNat) % 2 ^ w = x.toNat + y.toNat

Tactic:
apply Nat.mod_eq_of_lt

Result:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ x.toNat + y.toNat < 2 ^ w

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
this : ¬x.toNat + y.toNat + false.toNat ≥ 2 ^ w
⊢ x.toNat + y.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ (x + y).toNat = x.toNat + y.toNat

Tactic:
rw [toNat_add]

Result:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ (x.toNat + y.toNat) % 2 ^ w = x.toNat + y.toNat

Proof state:
case h
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ¬carry w x y false = true

Tactic:
simp [not_eq_true, carry_of_and_eq_zero h]

Result:
no goals