harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Div.lean
theorem not_isField : ¬IsField R[X]

Proof state:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
h : IsField R[X]
this : Field R[X] := h.toField
⊢ False

Tactic:
simpa using congr_arg natDegree (monic_X.eq_one_of_isUnit <| monic_X (R := R).ne_zero.isUnit)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
h : IsField R[X]
⊢ False

Tactic:
letI := h.toField

Result:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
h : IsField R[X]
this : Field R[X] := h.toField
⊢ False

Proof state:
R : Type u
inst✝ : Ring R
⊢ ¬IsField R[X]

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ ¬IsField R[X]

Proof state:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ ¬IsField R[X]

Tactic:
intro h

Result:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
h : IsField R[X]
⊢ False
-- Mathlib/Topology/Order/ScottTopology.lean
lemma isOpen_iff_scottContinuous_mem [Preorder α] {s : Set α} [TopologicalSpace α]
    [IsScott α univ] : IsOpen s ↔ ScottContinuous fun x ↦ x ∈ s

Proof state:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen s ↔ Continuous fun x => x ∈ s

Tactic:
exact isOpen_iff_continuous_mem

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen s ↔ ScottContinuous fun x => x ∈ s

Tactic:
rw [← scottContinuousOn_univ, scottContinuous_iff_continuous (fun _ _ _ ↦ by trivial)]

Result:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen s ↔ Continuous fun x => x ∈ s

Proof state:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x✝² x✝¹ : α
x✝ : x✝² ≤ x✝¹
⊢ {x✝², x✝¹} ∈ univ

Tactic:
trivial

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4

Proof state:
case hneg.hneg.hneg
c : Char
a✝² : ¬c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1
a✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_2
a✝ : ¬c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_3
⊢ 4 ≤ 4

Tactic:
decide

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall_and_right [Nonempty α] (p : α → Prop) (q : Prop) :
    (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q

Proof state:
α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q

Tactic:
rw [forall_and, forall_const]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem fderiv_inner_apply (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : G) :
    fderiv ℝ (fun t => ⟪f t, g t⟫) x y = ⟪f x, fderiv ℝ g x y⟫ + ⟪fderiv ℝ f x y, g x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ((fderivInnerCLM 𝕜 (f x, g x)).comp ((fderiv ℝ f x).prod (fderiv ℝ g x))) y =
    inner (f x) ((fderiv ℝ g x) y) + inner ((fderiv ℝ f x) y) (g x)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ (fderiv ℝ (fun t => inner (f t) (g t)) x) y = inner (f x) ((fderiv ℝ g x) y) + inner ((fderiv ℝ f x) y) (g x)

Tactic:
rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ((fderivInnerCLM 𝕜 (f x, g x)).comp ((fderiv ℝ f x).prod (fderiv ℝ g x))) y =
    inner (f x) ((fderiv ℝ g x) y) + inner ((fderiv ℝ f x) y) (g x)
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem le_valuation_add {x y : ℚ_[p]} (hxy : x + y ≠ 0) :
    min x.valuation y.valuation ≤ (x + y).valuation

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
simpa only [hy, add_zero] using min_le_left _ _

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx,
  norm_eq_zpow_neg_valuation hy, le_max_iff,
  zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
by_cases hx : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
by_cases hy : y = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
simpa only [hx, zero_add] using min_le_right _ _

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := padicNormE.nonarchimedean x y

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_X_pow_mul' (p : R⟦X⟧) (n d : ℕ) :
    coeff R d (X ^ n * p) = ite (n ≤ d) (coeff R (d - n) p) 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff R x.1) (X ^ n) * (coeff R x.2) p = 0

Tactic:
rw [coeff_X_pow, if_neg, zero_mul]

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.1 = n

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R (d - n)) p = (coeff R (d - n + n - n)) p

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R d) (X ^ n * p) = (coeff R (d - n)) p

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R (d - n)) p = (coeff R (d - n + n - n)) p

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.1 = n

Tactic:
have := mem_antidiagonal.mp hx

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
this : x.1 + x.2 = d
⊢ ¬x.1 = n

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
this : x.1 + x.2 = d
⊢ ¬x.1 = n

Tactic:
rw [add_comm] at this

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
this : x.2 + x.1 = d
⊢ ¬x.1 = n

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
this : x.2 + x.1 = d
⊢ ¬x.1 = n

Tactic:
exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff R d) (X ^ n * p) = if n ≤ d then (coeff R (d - n)) p else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R d) (X ^ n * p) = (coeff R (d - n)) p

case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff R d) (X ^ n * p) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff R d) (X ^ n * p) = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff R x.1) (X ^ n) * (coeff R x.2) p = 0
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) : x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

Proof state:
α : Type u
inst✝ : Monoid α
x : α
u₁ u₂ : αˣ
⊢ x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

Tactic:
simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
lemma sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i, f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ sSup (⋃ i, Iic (f i)) = ⨆ i, f i

Tactic:
apply csSup_eq_csSup_of_forall_exists_le

Result:
case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i => f i, x ≤ y

case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i => f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Proof state:
case hs.intro.intro.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
x : α
i : ι
hi : x ∈ (fun i => Iic (f i)) i
⊢ ∃ y ∈ range fun i => f i, x ≤ y

Tactic:
exact ⟨f i, mem_range_self _, hi⟩

Result:
no goals

Proof state:
case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i => f i, x ≤ y

Tactic:
rintro x ⟨-, ⟨i, rfl⟩, hi⟩

Result:
case hs.intro.intro.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
x : α
i : ι
hi : x ∈ (fun i => Iic (f i)) i
⊢ ∃ y ∈ range fun i => f i, x ≤ y

Proof state:
case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i => f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Tactic:
rintro x ⟨i, rfl⟩

Result:
case ht.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
i : ι
⊢ ∃ x ∈ ⋃ i, Iic (f i), (fun i => f i) i ≤ x

Proof state:
case ht.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
i : ι
⊢ ∃ x ∈ ⋃ i, Iic (f i), (fun i => f i) i ≤ x

Tactic:
exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem isPurelyInseparable_adjoin_simple_iff_pow_mem (q : ℕ) [hF : ExpChar F q] {x : E} :
    IsPurelyInseparable F F⟮x⟯ ↔ ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem q]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Centralizer.lean
theorem map_centralizer_le_centralizer_image (s : Set G) (f : G →* G') :
    (Subgroup.centralizer s).map f ≤ Subgroup.centralizer (f '' s)

Proof state:
case intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f h * f g = f g * f h

Tactic:
rw [← map_mul, ← map_mul, hg h hh]

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
⊢ map f (centralizer s) ≤ centralizer (⇑f '' s)

Tactic:
rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩

Result:
case intro.intro.intro.intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f h * f g = f g * f h
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
  ofReal_injective <| by simp [cos_two_mul]

Proof state:
x : ℝ
⊢ ↑(cos (2 * x)) = ↑(2 * cos x ^ 2 - 1)

Tactic:
simp [cos_two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : List α} : lex l₁ l₂ = false ↔ l₂ ≤ l₁

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ ¬Lex (fun x y => x < y) l₁ l₂ ↔ l₂ ≤ l₁

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ l₁

Tactic:
simp only [lex_eq_false_iff_not_lex, decide_eq_true_eq]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ ¬Lex (fun x y => x < y) l₁ l₂ ↔ l₂ ≤ l₁
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    (p.append q).length = p.length + q.length

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).length = nil.length + q.length

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk w✝ w), (p✝.append q).length = p✝.length + q.length
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).length = (cons h✝ p✝).length + q.length

Tactic:
simp [ih, add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).length = p.length + q.length

Tactic:
induction p with
| nil => simp
| cons _ _ ih => simp [ih, add_comm, add_left_comm, add_assoc]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem congr_left {a b c : α} : s(b, a) = s(c, a) ↔ b = c

Proof state:
α : Type u_1
a b c : α
⊢ s(b, a) = s(c, a) ↔ b = c

Tactic:
simp (config := {contextual := true})

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/ModEq.lean
theorem frequently_modEq {n : ℕ} (h : n ≠ 0) (d : ℕ) : ∃ᶠ m in atTop, m ≡ d [MOD n] :=
  ((tendsto_add_atTop_nat d).comp (tendsto_id.nsmul_atTop h.bot_lt)).frequently <|
    Frequently.of_forall fun m => by simp [Nat.modEq_iff_dvd, ← sub_sub]

Proof state:
n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun a => a + d) ∘ fun x => n • id x) m ≡ d [MOD n]

Tactic:
simp [Nat.modEq_iff_dvd, ← sub_sub]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem comp_proof {P Q R : Karoubi C} (g : Hom Q R) (f : Hom P Q) :
    f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q R : Karoubi C
g : Q.Hom R
f : P.Hom Q
⊢ f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p

Tactic:
rw [assoc, comp_p, ← assoc, p_comp]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHomMonomial_single :
    esymmAlgHomMonomial σ (Finsupp.single i k) r = C r * esymm σ R (i + 1) ^ k

Proof state:
σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) r = C r * esymm σ R (↑i + 1) ^ k

Tactic:
rw [esymmAlgHomMonomial, esymmAlgHom_apply, aeval_monomial, algebraMap_eq,
  Finsupp.prod_single_index]

Result:
σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ esymm σ R (↑i + 1) ^ 0 = 1

Proof state:
σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ esymm σ R (↑i + 1) ^ 0 = 1

Tactic:
exact pow_zero _

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem inv_I : (I : K)⁻¹ = -I

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ I⁻¹ = -I

Tactic:
by_cases h : (I : K) = 0

Result:
case pos
K : Type u_1
inst✝ : RCLike K
h : I = 0
⊢ I⁻¹ = -I

case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Proof state:
case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Tactic:
field_simp [I_mul_I_of_nonzero h]

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝ : RCLike K
h : I = 0
⊢ I⁻¹ = -I

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsOpen.frontier_eq (hs : IsOpen s) : frontier s = closure s \ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
hs : IsOpen s
⊢ frontier s = closure s \ s

Tactic:
rw [frontier, hs.interior_eq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_succ {f : Fin (n+1) → Option α} :
    findSome? f = (f 0 <|> findSome? fun i => f i.succ)

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
⊢ foldl n (fun x i => x <|> f i.succ) (f 0) = (f 0 <|> foldl n (fun r i => r <|> f i.succ) none)

Tactic:
cases f 0

Result:
case none
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
⊢ foldl n (fun x i => x <|> f i.succ) none = (none <|> foldl n (fun r i => r <|> f i.succ) none)

case some
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
val✝ : α
⊢ foldl n (fun x i => x <|> f i.succ) (some val✝) = (some val✝ <|> foldl n (fun r i => r <|> f i.succ) none)

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
⊢ findSome? f = (f 0 <|> findSome? fun i => f i.succ)

Tactic:
simp only [findSome?, foldl_succ, Option.none_orElse, Function.comp_apply]

Result:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
⊢ foldl n (fun x i => x <|> f i.succ) (f 0) = (f 0 <|> foldl n (fun r i => r <|> f i.succ) none)

Proof state:
case some
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
val✝ : α
⊢ foldl n (fun x i => x <|> f i.succ) (some val✝) = some val✝

Tactic:
induction n with
| zero => rfl
| succ n ih => rw [foldl_succ, Option.some_orElse, ih (f := fun i => f i.succ)]

Result:
no goals

Proof state:
case some.zero
α : Type u_1
val✝ : α
f : Fin (0 + 1) → Option α
⊢ foldl 0 (fun x i => x <|> f i.succ) (some val✝) = some val✝

Tactic:
rfl

Result:
no goals

Proof state:
case none
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
⊢ foldl n (fun x i => x <|> f i.succ) none = (none <|> foldl n (fun r i => r <|> f i.succ) none)

Tactic:
rw [Option.none_orElse]

Result:
no goals

Proof state:
case some
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
val✝ : α
⊢ foldl n (fun x i => x <|> f i.succ) (some val✝) = (some val✝ <|> foldl n (fun r i => r <|> f i.succ) none)

Tactic:
rw [Option.some_orElse]

Result:
case some
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
val✝ : α
⊢ foldl n (fun x i => x <|> f i.succ) (some val✝) = some val✝

Proof state:
case some.succ
α : Type u_1
val✝ : α
n : Nat
ih : ∀ {f : Fin (n + 1) → Option α}, foldl n (fun x i => x <|> f i.succ) (some val✝) = some val✝
f : Fin (n + 1 + 1) → Option α
⊢ foldl (n + 1) (fun x i => x <|> f i.succ) (some val✝) = some val✝

Tactic:
rw [foldl_succ, Option.some_orElse, ih (f := fun i => f i.succ)]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem mul_star {x y : ℤ} : (⟨x, y⟩ * star ⟨x, y⟩ : ℤ√d) = x * x - d * y * y

Proof state:
d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y

Tactic:
ext <;> simp [sub_eq_add_neg, mul_comm]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem mem_trivChange_source (i j : ι) (p : B × F) :
    p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
erw [mem_prod]

Result:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_even_mul_cos_pow_even (m n : ℕ) :
    (∫ x in a..b, sin x ^ (2 * m) * cos x ^ (2 * n)) =
      ∫ x in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n

Proof state:
a b : ℝ
m n : ℕ
⊢ 2 - 1 = 1

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n) =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n

Tactic:
field_simp [pow_mul, sin_sq, cos_sq, ← sub_sub, (by ring : (2 : ℝ) - 1 = 1)]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem det_matrixToStdBasis :
    (matrixToStdBasis K).det = (2⁻¹ * I) ^ nrComplexPlaces K :=
  calc
  _ = ∏ _k : { w : InfinitePlace K // IsComplex w }, det ((2 : ℂ)⁻¹ • !![1, 1; -I, I])

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ univ
⊢ (2⁻¹ • !![1, 1; -I, I]).det = 2⁻¹ * I

Tactic:
field_simp

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ univ
⊢ (I + I) * 2 = I * (2 * 2)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ univ
⊢ (I + I) * 2 = I * (2 * 2)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k : { w // w.IsComplex }, (2⁻¹ • !![1, 1; -I, I]).det = ∏ _k : { w // w.IsComplex }, 2⁻¹ * I

Tactic:
refine prod_congr (Eq.refl _) (fun _ _ => ?_)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ univ
⊢ (2⁻¹ • !![1, 1; -I, I]).det = 2⁻¹ * I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (matrixToStdBasis K).det = ∏ _k : { w // w.IsComplex }, (2⁻¹ • !![1, 1; -I, I]).det

Tactic:
rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul,
    det_reindex_self, det_blockDiagonal]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k : { w // w.IsComplex }, 2⁻¹ * I = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }

Tactic:
rw [prod_const, Fintype.card]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = (m.getKey? a).isSome

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.contains a = (m.getKey? a).isSome

Tactic:
simp_to_raw using Raw₀.contains_eq_isSome_getKey?

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.integrable_of_lintegral_enorm_bounded' [l.NeBot] [l.IsCountablyGenerated]
    {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → E} (I : ℝ≥0) (hfm : AEStronglyMeasurable f μ)
    (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ‖f x‖ₑ ∂μ ≤ I) : Integrable f μ :=
  hφ.integrable_of_lintegral_enorm_bounded I hfm
    (by simpa only [ENNReal.ofReal_coe_nnreal] using hbounded)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ↑I
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal ↑I

Tactic:
simpa only [ENNReal.ofReal_coe_nnreal] using hbounded

Result:
no goals