harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem SL2_inv_expl_det (A : SL(2, R)) :
    det ![![A.1 1 1, -A.1 0 1], ![-A.1 1 0, A.1 0 0]] = 1

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1

Tactic:
have := A.2

Result:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
this : (↑A).det = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
this : (↑A).det = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1

Tactic:
rw [Matrix.det_fin_two] at this

Result:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1

Tactic:
convert this

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1

Tactic:
rw [Matrix.det_fin_two, mul_comm]

Result:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 0 -
      ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 0 =
    1

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 0 -
      ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 0 =
    1

Tactic:
simp only [cons_val_zero, cons_val_one, head_cons, mul_neg, neg_mul, neg_neg]

Result:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_append (as : Vector α n) (bs : Vector α m) :
    (as ++ bs).reverse = (bs.reverse ++ as.reverse).cast (by omega)

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
⊢ (as ++ bs).reverse = Vector.cast ⋯ (bs.reverse ++ as.reverse)

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
bs : Vector α m
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ bs).reverse =
    Vector.cast ⋯ (bs.reverse ++ { toArray := as, size_toArray := ⋯ }.reverse)

Proof state:
α : Type ?u.361669
n m : Nat
as : Vector α n
bs : Vector α m
⊢ m + n = n + m

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
m : Nat
bs : Vector α m
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ bs).reverse =
    Vector.cast ⋯ (bs.reverse ++ { toArray := as, size_toArray := ⋯ }.reverse)

Tactic:
rcases bs with ⟨bs, rfl⟩

Result:
case mk.mk
α : Type u_1
as bs : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ { toArray := bs, size_toArray := ⋯ }).reverse =
    Vector.cast ⋯ ({ toArray := bs, size_toArray := ⋯ }.reverse ++ { toArray := as, size_toArray := ⋯ }.reverse)

Proof state:
case mk.mk
α : Type u_1
as bs : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ { toArray := bs, size_toArray := ⋯ }).reverse =
    Vector.cast ⋯ ({ toArray := bs, size_toArray := ⋯ }.reverse ++ { toArray := as, size_toArray := ⋯ }.reverse)

Tactic:
simp [Array.reverse_append]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F K)) :
    @Fintype.card (F⟮α⟯ →ₐ[F] K) (fintypeOfAlgHomAdjoinIntegral F h) = (minpoly F α).natDegree

Proof state:
case h_sep
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (algebraMap F K) (minpoly F α)
⊢ (minpoly F α).Separable

Tactic:
exact h_sep

Result:
no goals

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (algebraMap F K) (minpoly F α)
⊢ Fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree

Tactic:
rw [AlgHom.card_of_powerBasis] <;>
  simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]

Result:
case h_sep
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (algebraMap F K) (minpoly F α)
⊢ (minpoly F α).Separable
-- Mathlib/Data/Finmap.lean
theorem lookup_union_left_of_not_in {a} {s₁ s₂ : Finmap β} (h : a ∉ s₂) :
    lookup a (s₁ ∪ s₂) = lookup a s₁

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
by_cases h' : a ∈ s₁

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
rw [lookup_union_left h']

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem comp {f : β → σ} {g : α → β} (hf : Primrec f) (hg : Primrec g) : Primrec fun a => f (g a) :=
  ((casesOn1 0 (.comp hf (pred.comp hg))).comp (@Primcodable.prim α _)).of_eq fun n => by
    cases @decode α _ n <;> simp [encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n => encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a => f (g a)) (decode n))

Tactic:
cases @decode α _ n <;> simp [encodek]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_eq_zero_iff (n p : ℕ) :
    n.factorization p = 0 ↔ ¬p.Prime ∨ ¬p ∣ n ∨ n = 0

Proof state:
n p : ℕ
⊢ n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
simp_rw [← not_mem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
theorem exterior_eq_exterior_iff_nhdsSet : exterior s = exterior t ↔ 𝓝ˢ s = 𝓝ˢ t

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ exterior s = exterior t ↔ 𝓝ˢ s = 𝓝ˢ t

Tactic:
simp [le_antisymm_iff]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
/-- Compared to `drop_take_append_drop`, the order of summands is swapped. -/
@[simp] lemma drop_take_append_drop' (x : List α) (m n : ℕ) :
    (x.drop m).take n ++ x.drop (n + m) = x.drop m

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

Tactic:
rw [Nat.add_comm, drop_take_append_drop]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_sum (μ : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :
    (sum μ).restrict s = sum fun i => (μ i).restrict s :=
  ext fun t ht => by simp only [sum_apply, restrict_apply, ht, ht.inter hs]

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i => (μ i).restrict s) t

Tactic:
simp only [sum_apply, restrict_apply, ht, ht.inter hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_self {x : BitVec w} : x ^^^ x = 0#w

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ x).getLsbD i = (0#w).getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x ^^^ x = 0#w

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ x).getLsbD i = (0#w).getLsbD i
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_eq_image_lineMap (x y : E) : [x -[𝕜] y] =
    AffineMap.lineMap x y '' Icc (0 : 𝕜) 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ [x-[𝕜]y] = ⇑(AffineMap.lineMap x y) '' Icc 0 1

Tactic:
convert segment_eq_image 𝕜 x y using 2

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem zpow_ne_neg_zpow {a : Solution₁ d} (h : IsFundamental a) {n n' : ℤ} : a ^ n ≠ -a ^ n'

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Tactic:
exact lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
⊢ a ^ n ≠ -a ^ n'

Tactic:
intro hf

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : a ^ n = -a ^ n'
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : 0 < (a ^ n).x
⊢ False

Tactic:
rw [hf, x_neg, lt_neg, neg_zero] at H

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
⊢ False

Tactic:
have H := x_zpow_pos h.x_pos n

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : 0 < (a ^ n).x
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : a ^ n = -a ^ n'
⊢ False

Tactic:
apply_fun Solution₁.x at hf

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
⊢ False
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_prod_id {f : (α × β) → ℝ≥0∞} (hf : Measurable f) (κ : Kernel β α)
    [IsSFiniteKernel κ] (b : β) :
    ∫⁻ p, f p ∂(κ ×ₖ Kernel.id) b = ∫⁻ a, f (a, b) ∂κ b

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst✝ : IsSFiniteKernel κ
b : β
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ Kernel.id) b = ∫⁻ (a : α), f (a, b) ∂κ b

Tactic:
rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n !

Proof state:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ ↑n.succ * Gamma ↑n.succ = ↑(n + 1)!

Tactic:
simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]

Result:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ (↑n + 1) * Gamma (↑n + 1) = (↑n + 1) * ↑n !

Proof state:
n : ℕ
⊢ Gamma (↑n + 1) = ↑n !

Tactic:
induction n with
| zero => simp
| succ n hn =>
  rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]
  simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]
  congr

Result:
no goals

Proof state:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ (↑n + 1) * Gamma (↑n + 1) = (↑n + 1) * ↑n !

Tactic:
congr

Result:
no goals

Proof state:
case zero

⊢ Gamma (↑0 + 1) = ↑0!

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ Gamma (↑(n + 1) + 1) = ↑(n + 1)!

Tactic:
rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]

Result:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ ↑n.succ * Gamma ↑n.succ = ↑(n + 1)!
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma smul_le_iff_le_one_left [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) :
    a • b ≤ b ↔ a ≤ 1 := Iff.trans (by rw [one_smul]) (smul_le_smul_iff_of_pos_right hb)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosMono α β
inst✝ : SMulPosReflectLE α β
hb : 0 < b
⊢ a • b ≤ b ↔ a • b ≤ 1 • b

Tactic:
rw [one_smul]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem finite_const_le_of_tsum_ne_top {ι : Type*} {a : ι → ℝ≥0∞} (tsum_ne_top : ∑' i, a i ≠ ∞)
    {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) : { i : ι | ε ≤ a i }.Finite

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ False

Tactic:
refine tsum_ne_top (top_unique ?_)

Result:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ ⊤ ≤ ∑' (i : ι), a i

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ {i | ε ≤ a i}.Finite

Tactic:
by_contra h

Result:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
⊢ False

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
⊢ False

Tactic:
have := Infinite.to_subtype h

Result:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ False

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ ⊤ ≤ ∑' (i : ι), a i

Tactic:
calc ∞ = ∑' _ : { i | ε ≤ a i }, ε := (tsum_const_eq_top_of_ne_zero ε_ne_zero).symm
_ ≤ ∑' i, a i := tsum_le_tsum_of_inj (↑) Subtype.val_injective (fun _ _ => zero_le _)
  (fun i => i.2) ENNReal.summable ENNReal.summable

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_eq_empty_iff : image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
simp_rw [← not_nonempty_iff_eq_empty, image₂_nonempty_iff, not_and_or]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem _root_.Set.smul_mem_center (r : R) {a : A} (ha : a ∈ Set.center A) :
    r • a ∈ Set.center A where
  comm b

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ r • a * b = b * r • a

Tactic:
rw [mul_smul_comm, smul_mul_assoc, ha.comm]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ b * c * r • a = b * (c * r • a)

Tactic:
rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • a * (b * c) = r • a * b * c

Tactic:
rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ b * r • a * c = b * (r • a * c)

Tactic:
rw [mul_smul_comm, smul_mul_assoc, smul_mul_assoc, mul_smul_comm, ha.mid_assoc]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem order_monomial {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] :
    order (monomial R d a) = if a = 0 then (⊤ : ℕ∞) else ↑(degree d)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ ((monomial R d) a).order = if a = 0 then ⊤ else ↑((weight fun x => 1) d)

Tactic:
exact weightedOrder_monomial _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ ((monomial R d) a).order = if a = 0 then ⊤ else ↑d.degree

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ ((monomial R d) a).order = if a = 0 then ⊤ else ↑((weight fun x => 1) d)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem atEnd : ∀ {s}, Valid s → (s.atEnd ⟨p⟩ ↔ p = utf8ByteSize s.toString)
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.atEnd, h.toString]

Proof state:
p : Nat
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ x✝.atEnd { byteIdx := p } = true ↔ p = x✝.toString.utf8ByteSize

Tactic:
simp [h.atEnd, h.toString]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem isClosed_setOf_continuous [TopologicalSpace α] :
    IsClosed {f : α →ᵤ β | Continuous (toFun f)}

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous (toFun f)}
huf : TendstoUniformly (⇑toFun ∘ id) (toFun f) u
⊢ f ∈ {f | Continuous (toFun f)}

Tactic:
exact huf.continuous (le_principal_iff.mp hu)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous (toFun f)}
huf : u ≤ 𝓝 f
⊢ f ∈ {f | Continuous (toFun f)}

Tactic:
rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous (toFun f)}
huf : TendstoUniformly (⇑toFun ∘ id) (toFun f) u
⊢ f ∈ {f | Continuous (toFun f)}

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
⊢ IsClosed {f | Continuous (toFun f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous (toFun f)}
huf : u ≤ 𝓝 f
⊢ f ∈ {f | Continuous (toFun f)}
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Function.Embedding.toEquivRange_eq_ofInjective :
    f.toEquivRange = Equiv.ofInjective f f.injective

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
⊢ f.toEquivRange = Equiv.ofInjective ⇑f ⋯

Tactic:
ext

Result:
case H.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
x✝ : α
⊢ ↑(f.toEquivRange x✝) = ↑((Equiv.ofInjective ⇑f ⋯) x✝)

Proof state:
case H.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
x✝ : α
⊢ ↑(f.toEquivRange x✝) = ↑((Equiv.ofInjective ⇑f ⋯) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Dense.diff_finite [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s)
    {t : Set X} (ht : t.Finite) : Dense (s \ t)

Proof state:
case h.e'_3.h.e'_4
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ t = ↑ht.toFinset

Tactic:
exact (Finite.coe_toFinset _).symm

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ t)

Tactic:
convert hs.diff_finset ht.toFinset

Result:
case h.e'_3.h.e'_4
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ t = ↑ht.toFinset
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem deriv_inv : deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹

Tactic:
rcases eq_or_ne x 0 with (rfl | hne)

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
⊢ deriv (fun x => x⁻¹) 0 = -(0 ^ 2)⁻¹

case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hne : x ≠ 0
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
⊢ deriv (fun x => x⁻¹) 0 = -(0 ^ 2)⁻¹

Tactic:
simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hne : x ≠ 0
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹

Tactic:
exact (hasDerivAt_inv hne).deriv

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem toReal_neg : ∀ {a : EReal}, toReal (-a) = -toReal a
  | ⊤ => by simp
  | ⊥ => by simp
  | (x : ℝ) => rfl

Proof state:
⊢ (-⊥).toReal = -⊥.toReal

Tactic:
simp

Result:
no goals

Proof state:
⊢ (-⊤).toReal = -⊤.toReal

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
theorem nest_insidePart_add_outsidePart : p.insidePart.nest + p.outsidePart = p

Proof state:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
simp_rw [insidePart, outsidePart, h, dite_false, nest_denest, DyckWord.ext_iff]

Result:
p : DyckWord
h : p ≠ 0
⊢ ↑(p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯) = ↑p

Proof state:
p : DyckWord
h : p ≠ 0
⊢ ↑(p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯) = ↑p

Tactic:
apply take_append_drop

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Functional equation for the odd Hurwitz zeta function (alternative form). -/
lemma completedSinZeta_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s

Tactic:
simp [← completedHurwitzZetaOdd_one_sub]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem absdiscr_prime_pow_succ [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] :
    haveI : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
    NumberField.discr K =
    (-1) ^ ((p : ℕ) ^ k * (p - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
⊢ NumberField.discr K = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
simpa [totient_prime_pow hp.out (succ_pos k)] using absdiscr_prime_pow p (k + 1) K

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- See also `map_yonedaEquiv'` for a more general version. -/
lemma map_yonedaEquiv {X Y : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.val.map g.op (J.yonedaEquiv f) = f.val.app (op Y) g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.val.map g.op (J.yonedaEquiv f) = f.val.app (op Y) g

Tactic:
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Result:
no goals
-- Mathlib/Algebra/Group/Opposite.lean
theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x

Proof state:
α : Type u_1
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
lemma preimage_fst_singleton_eq_range : (Prod.fst ⁻¹' {a} : Set (α × β)) = range (a, ·)

Proof state:
α : Type u_1
β : Type u_2
a : α
⊢ Prod.fst ⁻¹' {a} = range fun x => (a, x)

Tactic:
aesop

Result:
no goals