harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem leibniz_div (a b : K) : D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ (b * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)

Tactic:
ring_nf

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ b⁻¹ • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)

Tactic:
rw [← inv_mul_mul_self b⁻¹, inv_inv]

Result:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ (b * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)

Tactic:
simp only [div_eq_mul_inv, leibniz, leibniz_inv, inv_pow, neg_smul, smul_neg, smul_smul, add_comm,
  sub_eq_add_neg, smul_add]

Result:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
⊢ b⁻¹ • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pbind_congr {o o' : Option α} (ho : o = o')
    {f : (a : α) → a ∈ o → Option β} {g : (a : α) → a ∈ o' → Option β}
    (hf : ∀ a h, f a (ho ▸ h) = g a h) : o.pbind f = o'.pbind g

Proof state:
α : Type u_1
β : Type u_2
o o' : Option α
ho : o = o'
f : (a : α) → a ∈ o → Option β
g : (a : α) → a ∈ o' → Option β
hf : ∀ (a : α) (h : a ∈ o'), f a ⋯ = g a h
⊢ o.pbind f = o'.pbind g

Tactic:
subst ho

Result:
α : Type u_1
β : Type u_2
o : Option α
f g : (a : α) → a ∈ o → Option β
hf : ∀ (a : α) (h : a ∈ o), f a ⋯ = g a h
⊢ o.pbind f = o.pbind g

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f g : (a : α) → a ∈ o → Option β
hf : ∀ (a : α) (h : a ∈ o), f a ⋯ = g a h
⊢ o.pbind f = o.pbind g

Tactic:
exact (funext fun a => funext fun h => hf a h) ▸ Eq.refl (o.pbind f)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_concat_concat : (l ++ [a, b]).head? = (l ++ [a]).head?

Proof state:
α✝ : Type u_1
l : List α✝
a b : α✝
⊢ (l ++ [a, b]).head? = (l ++ [a]).head?

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_comp [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix v₁ v₃ (f.comp g) =
    LinearMap.toMatrix v₂ v₃ f * LinearMap.toMatrix v₁ v₂ g

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ (toMatrix v₁ v₃) (f ∘ₗ g) = (toMatrix v₂ v₃) f * (toMatrix v₁ v₂) g

Tactic:
simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearEquiv.arrowCongr_comp _ v₂.equivFun,
  LinearMap.toMatrix'_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α] [Inhabited α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k : α}
    (h : containsKey k l = true) :
    getKey! k (insertListIfNewUnit l toInsert) = getKey! k l

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h : containsKey k l = true
⊢ getKey! k (insertListIfNewUnit l toInsert) = getKey! k l

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertListIfNewUnit_of_contains h, getKey!_eq_getKey?]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem coe_equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) :
    ((hST.equiv g).fst : G) = 1 ↔ g ∈ T

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).1 = 1 ↔ g ∈ T

Tactic:
rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Basic.lean
lemma hom_inv_id_apply {X Y : TopCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x

Proof state:
X Y : TopCat
f : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom f.inv) ((ConcreteCategory.hom f.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem adj_iff_exists_edge_coe : G.Adj a b ↔ ∃ e : G.edgeSet, e.val = s(a, b)

Proof state:
V : Type u
G : SimpleGraph V
a b : V
⊢ G.Adj a b ↔ ∃ e, ↑e = s(a, b)

Tactic:
simp only [mem_edgeSet, exists_prop, SetCoe.exists, exists_eq_right, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_extChartAt {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I 𝓘(𝕜, E) x (extChartAt I x) y = y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I 𝓘(𝕜, E) x (↑(extChartAt I x)) y = y

Tactic:
simp_all only [mfld_simps]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_ker (f : G →* G') : f.ker.index = Nat.card f.range

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.ker.index = Nat.card ↥f.range

Tactic:
rw [← MonoidHom.comap_bot, index_comap, relindex_bot_left]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem card_box : #(box n d) = d ^ n

Proof state:
n d : ℕ
⊢ #(box n d) = d ^ n

Tactic:
simp [box]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_congr {s t : Set α} [Fintype s] [Fintype t] (h : s = t) :
    toFinset s = toFinset t

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ s.toFinset = t.toFinset

Tactic:
subst h

Result:
α : Type u_1
s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ s.toFinset = s.toFinset

Proof state:
α : Type u_1
s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ s.toFinset = s.toFinset

Tactic:
congr!

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
lemma isTheta_cpow_exp_re_mul_log (hl : IsExpCmpFilter l) (a : ℂ) :
    (· ^ a) =Θ[l] fun z ↦ Real.exp (re a * Real.log ‖z‖) :=
  calc
    (fun z => z ^ a) =Θ[l] (fun z : ℂ => ‖z‖ ^ re a) :=
      isTheta_cpow_const_rpow fun _ _ => hl.eventually_ne
    _ =ᶠ[l] fun z => Real.exp (re a * Real.log ‖z‖) :=
      (hl.eventually_ne.mono fun z hz => by simp
        [Real.rpow_def_of_pos, norm_pos_iff.mpr hz, mul_comm])

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
a z : ℂ
hz : z ≠ 0
⊢ (fun z => ‖z‖ ^ a.re) z = (fun z => Real.exp (a.re * Real.log ‖z‖)) z

Tactic:
simp
[Real.rpow_def_of_pos, norm_pos_iff.mpr hz, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem srange_eq_map : srange f = (⊤ : NonUnitalSubsemiring R).map f

Proof state:
case h
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x✝ : S
⊢ x✝ ∈ srange f ↔ x✝ ∈ map f ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ srange f = map f ⊤

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x✝ : S
⊢ x✝ ∈ srange f ↔ x✝ ∈ map f ⊤
-- Mathlib/Topology/Inseparable.lean
lemma specializingMap_iff_isClosed_image_closure_singleton (hf : Continuous f) :
    SpecializingMap f ↔ ∀ x, IsClosed (f '' closure {x})

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed (f '' closure {x})

Tactic:
refine ⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
  (fun x ↦ (h x).stableUnderSpecialization)⟩

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
h : SpecializingMap f
x : X
⊢ IsClosed (f '' closure {x})

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
h : SpecializingMap f
x : X
⊢ IsClosed (f '' closure {x})

Tactic:
rw [(specializingMap_iff_closure_singleton hf).mp h x]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
h : SpecializingMap f
x : X
⊢ IsClosed (closure {f x})

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
h : SpecializingMap f
x : X
⊢ IsClosed (closure {f x})

Tactic:
exact isClosed_closure

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_lt_one_iff : b * a⁻¹ < 1 ↔ b < a :=
  _root_.trans mul_inv_lt_iff_lt_mul <| by rw [one_mul]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ b < 1 * a ↔ b < a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_left_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - b < c

Proof state:
a b c : Int
h : a < b + c
⊢ a - b < c

Tactic:
have h := Int.add_lt_add_right h (-b)

Result:
a b c : Int
h✝ : a < b + c
h : a + -b < b + c + -b
⊢ a - b < c

Proof state:
a b c : Int
h✝ : a < b + c
h : a + -b < b + c + -b
⊢ a - b < c

Tactic:
rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version at a point. -/
protected lemma _root_.MDifferentiableAt.mpullback_vectorField
    (hV : MDifferentiableAt I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) (f x₀))
    (hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) :
    MDifferentiableAt I I.tangent
      (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) x₀

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
n : WithTop ℕ∞
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDifferentiableAt I' I'.tangent (fun y => { proj := y, snd := V y }) (f x₀)
hf : ContMDiffAt I I' n f x₀
hf' : (mfderiv I I' f x₀).IsInvertible
hmn : 2 ≤ n
⊢ MDifferentiableAt I I.tangent (fun y => { proj := y, snd := mpullback I I' f V y }) x₀

Tactic:
simpa using MDifferentiableWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) :
    map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂)

Proof state:
α : Type u
β : Type v
f : α → β
l₁ l₂ : List α
⊢ map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)

Tactic:
simp only [reverseAux_eq, map_append, map_reverse]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem zero_or_succ_or_limit (o : Ordinal) : o = 0 ∨ (∃ a, o = succ a) ∨ IsLimit o

Proof state:
o : Ordinal.{u_4}
⊢ o = 0 ∨ (∃ a, o = succ a) ∨ o.IsLimit

Tactic:
simpa [eq_comm] using isMin_or_mem_range_succ_or_isSuccLimit o

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_X_sub_C_pow {x : F} {n : ℕ} :
    ((X - C x) ^ n).natSepDegree = if n = 0 then 0 else 1

Proof state:
F : Type u
inst✝ : Field F
x : F
n : ℕ
⊢ ((X - C x) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X_sub_C]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
protected lemma Nontrivial.erase_nonempty (hs : s.Nontrivial) : (s.erase a).Nonempty :=
  (hs.exists_ne a).imp <| by aesop

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nontrivial
⊢ ∀ (a_1 : α), a_1 ∈ s ∧ a_1 ≠ a → a_1 ∈ s.erase a

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma generateFrom_natGeneratingSequence (α : Type*) [m : MeasurableSpace α]
    [CountablyGenerated α] : generateFrom (range (natGeneratingSequence _)) = m

Proof state:
α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ generateFrom (range (natGeneratingSequence α)) = m

Tactic:
rw [natGeneratingSequence, range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
  generateFrom_countableGeneratingSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < i.castSucc

Proof state:
n : Nat
i : Fin (n + 1)
h : 0 < i
⊢ 0 < i.castSucc

Tactic:
simpa [lt_def] using h

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sdiff_symmDiff_left : a \ a ∆ b = a ⊓ b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ a ∆ b = a ⊓ b

Tactic:
simp [sdiff_symmDiff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_eq_norm_add {v w : E} (h : ⟪v, w⟫ = 0) : ‖w - v‖ = ‖w + v‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫_𝕜 = 0
⊢ ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖

Tactic:
simp only [h, ← @inner_self_eq_norm_mul_norm 𝕜, sub_neg_eq_add, sub_zero, map_sub, zero_re',
  zero_sub, add_zero, map_add, inner_add_right, inner_sub_left, inner_sub_right, inner_re_symm,
  zero_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫_𝕜 = 0
⊢ ‖w - v‖ = ‖w + v‖

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫_𝕜 = 0
⊢ ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem length_toList : length (toList p x) = (cycleOf p x).support.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ (p.toList x).length = (p.cycleOf x).support.card

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_image {γ} {f : β → γ} {g : γ → α} {t : Set β} :
    ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Tactic:
rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem ineqofmemIco' {k : ℕ} (hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊) :
    a ≤ k ∧ k + 1 ≤ b :=
  ineqofmemIco (by rwa [← Finset.coe_Ico])

Proof state:
a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊

Tactic:
rwa [← Finset.coe_Ico]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem card_commutator_closureCommutatorRepresentatives :
    Nat.card (commutator (closureCommutatorRepresentatives G)) = Nat.card (commutator G)

Proof state:
G : Type u
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(map (closureCommutatorRepresentatives G).subtype (_root_.commutator ↥(closureCommutatorRepresentatives G)))

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(_root_.commutator G)

Tactic:
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
  MonoidHom.map_closure, ← commutator_eq_closure]

Result:
G : Type u
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(map (closureCommutatorRepresentatives G).subtype (_root_.commutator ↥(closureCommutatorRepresentatives G)))
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_bot : ⁅I, (⊥ : LieSubmodule R L M)⁆ = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∀ m ∈ ⁅I, ⊥⁆, m = 0

Tactic:
apply lie_le_right

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, ⊥⁆ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∀ m ∈ ⁅I, ⊥⁆, m = 0
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem coeff_pow_nsmul_degree (f : MvPolynomial σ R) (n : ℕ) :
    (f ^ n).coeff (n • m.degree f) = m.leadingCoeff f ^ n

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f

Tactic:
rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]

Result:
no goals

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff ((n + 1) • m.degree f) (f ^ (n + 1)) = m.leadingCoeff f ^ (n + 1)

Tactic:
simp only [add_smul, one_smul, pow_add, pow_one]

Result:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n

Tactic:
induction n with
| zero => simp
| succ n hrec =>
  simp only [add_smul, one_smul, pow_add, pow_one]
  rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]

Result:
no goals

Proof state:
case zero
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (0 • m.degree f) (f ^ 0) = m.leadingCoeff f ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) :
    (a ⊓ ⨆ (i) (j), f i j) = ⨆ (i) (j), a ⊓ f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
f : (i : ι) → κ i → α
a : α
⊢ a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j

Tactic:
simp only [inf_iSup_eq]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Defs.lean
theorem pow_mem_of_mem (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I :=
  Nat.casesOn n (Not.elim (by decide))
    (fun m _hm => (pow_succ a m).symm ▸ I.mul_mem_left (a ^ m) ha) hn

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
ha : a ∈ I
n : ℕ
hn : 0 < n
⊢ ¬0 < Nat.zero

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Equivalence.lean
/-- If `L₁ : C₁ ⥤ D₁` is a localization functor for `W₁ : MorphismProperty C₁`, then if we
transport this functor `L₁` via equivalences `C₁ ≌ C₂` and `D₁ ≌ D₂` to get a functor
`L₂ : C₂ ⥤ D₂`, then `L₂` is also a localization functor for
a suitable `W₂ : MorphismProperty C₂`. -/
lemma of_equivalences (L₁ : C₁ ⥤ D₁) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁]
    (L₂ : C₂ ⥤ D₂) (W₂ : MorphismProperty C₂)
    (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂) [CatCommSq E.functor L₁ L₂ E'.functor]
    (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) :
    L₂.IsLocalization W₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_6, u_1} C₁
inst✝⁴ : Category.{u_8, u_2} C₂
inst✝³ : Category.{u_7, u_4} D₁
inst✝² : Category.{u_9, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
this : (E.functor ⋙ L₂).IsLocalization W₁
⊢ L₂.IsLocalization W₂

Tactic:
exact of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_6, u_1} C₁
inst✝⁴ : Category.{u_8, u_2} C₂
inst✝³ : Category.{u_7, u_4} D₁
inst✝² : Category.{u_9, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
⊢ L₂.IsLocalization W₂

Tactic:
haveI : (E.functor ⋙ L₂).IsLocalization W₁ :=
  of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_6, u_1} C₁
inst✝⁴ : Category.{u_8, u_2} C₂
inst✝³ : Category.{u_7, u_4} D₁
inst✝² : Category.{u_9, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
this : (E.functor ⋙ L₂).IsLocalization W₁
⊢ L₂.IsLocalization W₂
-- Mathlib/Logic/Equiv/Option.lean
theorem option_symm_apply_none_iff : e.symm none = none ↔ e none = none :=
  ⟨fun h => by simpa using (congr_arg e h).symm, fun h => by simpa using (congr_arg e.symm h).symm⟩

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e.symm none = none
⊢ e none = none

Tactic:
simpa using (congr_arg e h).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e none = none
⊢ e.symm none = none

Tactic:
simpa using (congr_arg e.symm h).symm

Result:
no goals
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_right ⦃x y : Tropical R⦄ (h : y ≤ x) : x + y = y :=
  untrop_injective (by simpa using h)

Proof state:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y

Tactic:
simpa using h

Result:
no goals