harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_gaussian_complex {b : ℂ} (hb : 0 < re b) :
    ∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ)

Proof state:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (fun {b} => ∫ (x : ℝ), cexp (-b * ↑x ^ 2)) {c | 0 < c.re}

Tactic:
exact continuousOn_of_forall_continuousAt continuousAt_gaussian_integral

Result:
no goals

Proof state:
b✝ : ℂ
hb✝ : 0 < b✝.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : b ∈ {c | 0 < c.re}
⊢ 0 < π * b.re / normSq b

Tactic:
exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))

Result:
no goals

Proof state:
b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : b = 0
⊢ re 0 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler (w z : ℂ) : Complex.orientation.kahler w z = conj w * z

Proof state:
w z : ℂ
⊢ (Complex.orientation.kahler w) z = (starRingEnd ℂ) w * z

Tactic:
rw [Orientation.kahler_apply_apply]

Result:
w z : ℂ
⊢ ↑(inner w z) + (Complex.orientation.areaForm w) z • I = (starRingEnd ℂ) w * z

Proof state:
w z : ℂ
⊢ ↑(inner w z) + (Complex.orientation.areaForm w) z • I = (starRingEnd ℂ) w * z

Tactic:
apply Complex.ext <;> simp

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

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

Tactic:
rw [insert_inter_distrib, insert_eq_of_mem h]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_eq_mk'_iff (m₁ m₂ : M) (s₁ s₂ : S) :
    mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ s : S, s • s₁ • m₂ = s • s₂ • m₁

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) = (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) ↔
    ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (∃ u, u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Tactic:
simp_rw [eq_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) = (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) ↔
    ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Tactic:
rw [(fromLocalizedModule.inj S f).eq_iff, LocalizedModule.mk_eq]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (∃ u, u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' height plus coheight.
-/
lemma krullDim_eq_iSup_height_add_coheight_of_nonempty [Nonempty α] :
    krullDim α = ↑(⨆ (a : α), height a + coheight a)

Proof state:
case h.coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh

Result:
case h.coe.coe.intro.intro
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)

Tactic:
rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe]

Result:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ a, height a ≤ ⨆ a, height a + coheight a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, height a + coheight a)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_of_xn_modEq_lem1 {i n} : ∀ {j}, i < j → j < n → xn a1 i % xn a1 n < xn a1 j % xn a1 n
  | 0, ij, _ => absurd ij (Nat.not_lt_zero _)
  | j + 1, ij, jn => by
    suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
      (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
        (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
        rw [h]; exact this
    rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
        Nat.mod_eq_of_lt (strictMono_x _ jn)]
    exact strictMono_x _ (Nat.lt_succ_self _)

Proof state:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
exact this

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
    Nat.mod_eq_of_lt (strictMono_x _ jn)]

Result:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)

Proof state:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
rw [h]

Result:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
  (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
    (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
    rw [h]; exact this

Result:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)

Tactic:
exact strictMono_x _ (Nat.lt_succ_self _)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
theorem FiniteField.isSquare_two_iff :
    IsSquare (2 : F) ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF,
  χ₈_nat_eq_if_mod_eight]

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
omega

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
omega

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
have h := FiniteField.even_card_of_char_two hF

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
have h := FiniteField.odd_card_of_char_ne_two hF

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
by_cases hF : ringChar F = 2

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
lemma derivWithin_const_mul_field (u : 𝕜') :
    derivWithin (fun y => u * v y) s x = u * derivWithin v s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun y => u * v y) s x = u * derivWithin v s x

Tactic:
simp_rw [mul_comm u]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun y => v y * u) s x = derivWithin v s x * u

Tactic:
exact derivWithin_mul_const_field u

Result:
no goals
-- Mathlib/Data/Finset/CastCard.lean
theorem cast_card_erase_of_mem {R} [AddGroupWithOne R] {s : Finset α} (hs : a ∈ s) :
    (#(s.erase a) : R) = #s - 1

Proof state:
α : Type u_1
a : α
inst✝¹ : DecidableEq α
R : Type u_4
inst✝ : AddGroupWithOne R
s : Finset α
hs : a ∈ s
⊢ 1 ≤ #s

Tactic:
rw [Nat.add_one_le_iff, Finset.card_pos]

Result:
α : Type u_1
a : α
inst✝¹ : DecidableEq α
R : Type u_4
inst✝ : AddGroupWithOne R
s : Finset α
hs : a ∈ s
⊢ s.Nonempty

Proof state:
α : Type u_1
a : α
inst✝¹ : DecidableEq α
R : Type u_4
inst✝ : AddGroupWithOne R
s : Finset α
hs : a ∈ s
⊢ ↑(#(s.erase a)) = ↑(#s) - 1

Tactic:
rw [card_erase_of_mem hs, Nat.cast_sub, Nat.cast_one]

Result:
α : Type u_1
a : α
inst✝¹ : DecidableEq α
R : Type u_4
inst✝ : AddGroupWithOne R
s : Finset α
hs : a ∈ s
⊢ 1 ≤ #s

Proof state:
α : Type u_1
a : α
inst✝¹ : DecidableEq α
R : Type u_4
inst✝ : AddGroupWithOne R
s : Finset α
hs : a ∈ s
⊢ s.Nonempty

Tactic:
exact ⟨a, hs⟩

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_prime_pow (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
    orderOf x = p ^ (n + 1)

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)

Tactic:
apply minimalPeriod_eq_prime_pow <;> rwa [isPeriodicPt_mul_iff_pow_eq_one]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Braiding.lean
lemma braiding_naturality_left [HasTensor Y Z] [HasTensor Z Y] [HasTensor X Z] [HasTensor Z X]
    (f : X ⟶ Y) :
    whiskerRight f Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ whiskerLeft Z f

Proof state:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ whiskerRight f Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ whiskerLeft Z f

Tactic:
dsimp [braiding]

Result:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ (whiskerRight f Z ≫ fun k => tensorObjDesc fun i j hij => (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) =
    (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) ≫ whiskerLeft Z f

Proof state:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ (whiskerRight f Z ≫ fun k => tensorObjDesc fun i j hij => (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) =
    (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) ≫ whiskerLeft Z f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocSemiring_injective :
    Function.Injective (@toNonUnitalNonAssocSemiring R)

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegral_add_zsmul_eq (hf : Periodic f T) (n : ℤ) (t : ℝ)
    (h_int : ∀ t₁ t₂, IntervalIntegrable f MeasureSpace.volume t₁ t₂) :
    ∫ x in t..t + n • T, f x = n • ∫ x in t..t + T, f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∫ (x : ℝ) in 0 ..n • T, f x = n • ∫ (x : ℝ) in 0 ..T, f x
⊢ ∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x

Tactic:
simp only [hf.intervalIntegral_add_eq t 0, (hf.zsmul n).intervalIntegral_add_eq t 0, zero_add,
  this]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
lemma listTake_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
    List.take k (alternatingWord i j (2 * p)) =
    if Even k then alternatingWord i j k else alternatingWord j i k

Proof state:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord j i (k + 1)

Tactic:
rw [← List.take_concat_get _ _ (by simp [h]; omega), alternatingWord_succ, ← hk]

Result:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i

Proof state:
case succ
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
have hk : k < 2 * p := by omega

Result:
case succ
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : k < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem mem_grothendieckTopology :
    Sieve.generate (presieveOfCovering U) ∈ Opens.grothendieckTopology X (iSup U)

Proof state:
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx

Result:
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Proof state:
X : TopCat
ι : Type v
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCovering U) ∈ (Opens.grothendieckTopology ↑X) (iSup U)

Tactic:
intro x hx

Result:
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Proof state:
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_mul (f g : R[X]) :
    hasseDeriv k (f * g) = ∑ ij ∈ antidiagonal k, hasseDeriv ij.1 f * hasseDeriv ij.2 g

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
rw [mem_antidiagonal] at hx

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.1 + x.2 = k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkAtomCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.atom var) = none) :
    (aig.mkAtomCached var).aig.decls = aig.decls.push (.atom var)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.get? (Decl.atom var) = none
⊢ (match aig.cache.get? (Decl.atom var) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                invariant := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.atom var)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.get? (Decl.atom var) = none
⊢ (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)

Tactic:
simp only [mkAtomCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hcache : aig.cache.get? (Decl.atom var) = none
⊢ (match aig.cache.get? (Decl.atom var) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
                invariant := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.atom var)
-- Mathlib/FieldTheory/IsSepClosed.lean
theorem IsSepClosed.splits_codomain [IsSepClosed K] {f : k →+* K}
    (p : k[X]) (h : p.Separable) : p.Splits f

Proof state:
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : p.Separable
⊢ Splits f p

Tactic:
convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h)

Result:
case a
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : p.Separable
⊢ Splits f p ↔ Splits (RingHom.id K) (map f p)

Proof state:
case a
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : p.Separable
⊢ Splits f p ↔ Splits (RingHom.id K) (map f p)

Tactic:
simp [splits_map_iff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_monomial (f : σ → τ) (d : σ →₀ ℕ) (r : R) :
    rename f (monomial d r) = monomial (d.mapDomain f) r

Proof state:
case h_zero
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), X b ^ 0 = 1

Tactic:
exact fun n => pow_zero _

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ (rename f) ((monomial d) r) = (monomial (Finsupp.mapDomain f d)) r

Tactic:
rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
  Finsupp.prod_mapDomain_index]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ((algebraMap R (MvPolynomial τ R)) r * d.prod fun i k => (X ∘ f) i ^ k) = C r * d.prod fun a m => X (f a) ^ m

case h_zero
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), X b ^ 0 = 1

case h_add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ), X b ^ (m₁ + m₂) = X b ^ m₁ * X b ^ m₂

Proof state:
case h_add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ), X b ^ (m₁ + m₂) = X b ^ m₁ * X b ^ m₂

Tactic:
exact fun n i₁ i₂ => pow_add _ _ _

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ((algebraMap R (MvPolynomial τ R)) r * d.prod fun i k => (X ∘ f) i ^ k) = C r * d.prod fun a m => X (f a) ^ m

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
l : List β₁
init : α
⊢ foldrM g init (map f l) = foldrM (fun x y => g (f x) y) init l

Tactic:
induction l generalizing g init <;> simp [*]

Result:
no goals