harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_mem_iff {f : 𝕜 → F} {t : Set 𝕜} {s : Set F} {x : 𝕜} :
    derivWithin f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨
        ¬DifferentiableWithinAt 𝕜 f t x ∧ (0 : F) ∈ s

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableWithinAt 𝕜 f t x <;>
  simp [derivWithin_zero_of_not_differentiableWithinAt, *]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma inv_natCast_cpow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
    0 < ((n : ℂ) ^ (x : ℂ))⁻¹

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < (↑n ^ ↑x)⁻¹

Tactic:
refine RCLike.inv_pos_of_pos ?_

Result:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑n ^ ↑x

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑(↑n ^ x)

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑n ^ ↑x

Tactic:
rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']

Result:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑(↑n ^ x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x)

Proof state:
case h
β : Type u_1
α : Type u_2
x : β
l : Array α
⊢ map (Function.const α x) l = mkArray l.size x

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
x : β
⊢ map (Function.const α x) = fun x_1 => mkArray x_1.size x

Tactic:
funext l

Result:
case h
β : Type u_1
α : Type u_2
x : β
l : Array α
⊢ map (Function.const α x) l = mkArray l.size x
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_of_inv_mul_eq (h : b⁻¹ * a = c) : a = b * c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : b⁻¹ * a = c
⊢ a = b * c

Tactic:
simp [h.symm, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem isoSheafify_inv {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) :
    (J.isoSheafify hP).inv = J.sheafifyLift (𝟙 _) hP

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (J.isoSheafify hP).inv = J.sheafifyLift (𝟙 P) hP

Tactic:
apply J.sheafifyLift_unique

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ J.toSheafify P ≫ (J.isoSheafify hP).inv = 𝟙 P

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ J.toSheafify P ≫ (J.isoSheafify hP).inv = 𝟙 P

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem nat_iff {f : ℕ →. ℕ} : Partrec f ↔ Nat.Partrec f

Proof state:
f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f

Tactic:
simp [Partrec, map_id']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_ciSup (c : Cardinal.{v}) : c * (⨆ i, f i) = ⨆ i, c * f i

Proof state:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ c * ⨆ i, f i = ⨆ i, c * f i

Tactic:
rw [mul_comm, Cardinal.ciSup_mul f]

Result:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i

Proof state:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i

Tactic:
simp_rw [mul_comm]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
@[simp]
lemma factorizationLCMLeft_zero_left : factorizationLCMLeft 0 b = 1

Proof state:
b : ℕ
⊢ factorizationLCMLeft 0 b = 1

Tactic:
simp [factorizationLCMLeft]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factors'_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :
    Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ a_1, ∃ (h : a_1 ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk a_1, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Tactic:
use q

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ (h : q ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a

Tactic:
apply Multiset.mem_pmap.mpr

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ a_1, ∃ (h : a_1 ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk a_1, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ (h : q ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Tactic:
use hq

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Tactic:
exact Subtype.eq (Eq.symm (mk_eq_mk_iff_associated.mpr hpq))

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a

Tactic:
obtain ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd ha0 hp hd

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a
-- Mathlib/Order/Chain.lean
theorem Monotone.isChain_range [LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    IsChain (· ≤ ·) (range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 => x1 ≤ x2) (f '' univ)

Tactic:
exact hf.isChain_image (isChain_of_trichotomous _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 => x1 ≤ x2) (range f)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 => x1 ≤ x2) (f '' univ)
-- Mathlib/Data/Rat/Defs.lean
theorem mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : d ≠ 0 :=
  fun this => hq <| by simpa [this] using hqnd

Proof state:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0

Tactic:
simpa [this] using hqnd

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff_singleton_lt_of_mem {a : α} (h : a ∈ s) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ (s \ {a}).ncard < s.ncard

Tactic:
rw [← ncard_diff_singleton_add_one h hs]

Result:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1

Tactic:
apply lt_add_one

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem dyadicMap_apply (m : ℤ) (p : Submonoid.powers (2 : ℤ)) :
    dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) =
      m * powHalf (Submonoid.log p)

Proof state:
m : ℤ
p : ↥(Submonoid.powers 2)
⊢ dyadicMap (Localization.mk m p) = ↑m * powHalf (Submonoid.log p)

Tactic:
rfl

Result:
no goals

Proof state:
m : ℤ
p : ↥(Submonoid.powers 2)
⊢ dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = ↑m * powHalf (Submonoid.log p)

Tactic:
rw [← Localization.mk_eq_mk']

Result:
m : ℤ
p : ↥(Submonoid.powers 2)
⊢ dyadicMap (Localization.mk m p) = ↑m * powHalf (Submonoid.log p)
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_min' (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : exponent G ≤ n

Proof state:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n

Tactic:
rw [exponent, dif_pos]

Result:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n

case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Proof state:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n

Tactic:
apply Nat.find_min'

Result:
case h
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1

Proof state:
case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Tactic:
exact ⟨n, hpos, hG⟩

Result:
no goals

Proof state:
case h
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
exact ⟨hpos, hG⟩

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
@[to_additive (attr := simp)]
lemma map_mk (f : M →* N) (val inv : M) (val_inv inv_val) :
    map f (mk val inv val_inv inv_val) = mk (f val) (f inv)
      (by rw [← f.map_mul, val_inv, f.map_one]) (by rw [← f.map_mul, inv_val, f.map_one]) := rfl

Proof state:
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f inv * f val = 1

Tactic:
rw [← f.map_mul, inv_val, f.map_one]

Result:
no goals

Proof state:
α : Type u_1
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f val * f inv = 1

Tactic:
rw [← f.map_mul, val_inv, f.map_one]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
lemma fac_aux₁ {n : ℕ}
    (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (i : ℕ) (hi : i < n) :
    X.map (mkOfSucc ⟨i, hi⟩).op (lift s x) =
      s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩)) x

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ X.map (mkOfSucc ⟨i, hi⟩).op (lift s x) = s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) ⋯) x

Tactic:
dsimp [lift]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ X.map (mkOfSucc ⟨i, hi⟩).op
      (spineToSimplex
        {
          vertex := fun i =>
            s.π.app
              (StructuredArrow.mk
                (((Truncated.inclusion 2).obj { obj := ⦋0⦌, property := lift.proof_1 }).const ⦋n⦌ i).op)
              x,
          arrow := fun i => s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op) x, arrow_src := ⋯,
          arrow_tgt := ⋯ }) =
    s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) ⋯) x

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ X.map (mkOfSucc ⟨i, hi⟩).op
      (spineToSimplex
        {
          vertex := fun i =>
            s.π.app
              (StructuredArrow.mk
                (((Truncated.inclusion 2).obj { obj := ⦋0⦌, property := lift.proof_1 }).const ⦋n⦌ i).op)
              x,
          arrow := fun i => s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op) x, arrow_src := ⋯,
          arrow_tgt := ⋯ }) =
    s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) ⋯) x

Tactic:
rw [spineToSimplex_arrow]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ {
          vertex := fun i =>
            s.π.app
              (StructuredArrow.mk
                (((Truncated.inclusion 2).obj { obj := ⦋0⦌, property := lift.proof_1 }).const ⦋n⦌ i).op)
              x,
          arrow := fun i => s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op) x, arrow_src := ⋯,
          arrow_tgt := ⋯ }.arrow
      ⟨i, hi⟩ =
    s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) ⋯) x

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ {
          vertex := fun i =>
            s.π.app
              (StructuredArrow.mk
                (((Truncated.inclusion 2).obj { obj := ⦋0⦌, property := lift.proof_1 }).const ⦋n⦌ i).op)
              x,
          arrow := fun i => s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op) x, arrow_src := ⋯,
          arrow_tgt := ⋯ }.arrow
      ⟨i, hi⟩ =
    s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) ⋯) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_sub' (h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n)

Proof state:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
rw [even_sub h, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem Option.traverse_eq_map_id {α β} (f : α → β) (x : Option α) :
    Option.traverse ((pure : _ → Id _) ∘ f) x = (pure : _ → Id _) (f <$> x)

Proof state:
α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b

Proof state:
a b : Int
H : a ∣ b
⊢ a * (b / a) = b

Tactic:
rw [Int.mul_comm, Int.ediv_mul_cancel H]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem moment_zero (hp : p ≠ 0) : moment 0 p μ = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
hp : p ≠ 0
⊢ moment 0 p μ = 0

Tactic:
simp only [moment, hp, zero_pow, Ne, not_false_iff, Pi.zero_apply, integral_const,
  smul_eq_mul, mul_zero, integral_zero]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem isRadical_iff_span_singleton [CommSemiring R] :
    IsRadical y ↔ (Ideal.span ({y} : Set R)).IsRadical

Proof state:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ (Ideal.span {y}).IsRadical

Tactic:
simp_rw [IsRadical, ← Ideal.mem_span_singleton]

Result:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical

Proof state:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical

Tactic:
exact forall_swap.trans (forall_congr' fun r => exists_imp.symm)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_piecewise [DecidableEq α] (s t : Finset α) (f g : α → β) :
    (∏ x ∈ s, (t.piecewise f g) x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f g : α → β
⊢ ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Tactic:
simp only [piecewise]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f g : α → β
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f g : α → β
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Tactic:
rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_toOuterMeasure (hf : AEMeasurable f μ) :
    (μ.map f).toOuterMeasure = (OuterMeasure.map f μ.toOuterMeasure).trim

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ).toOuterMeasure = ((OuterMeasure.map f) μ.toOuterMeasure).trim

Tactic:
rw [← trimmed, OuterMeasure.trim_eq_trim_iff]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ ∀ (s : Set β), MeasurableSet s → (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s

Tactic:
simp [hf, hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ ∀ (s : Set β), MeasurableSet s → (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s

Tactic:
intro s hs

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
    (empty c : Raw α β).get! a = default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
c : Nat
⊢ (empty c).get! a = default

Tactic:
simp_to_raw using Raw₀.get!_empty

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem mem_eraseLast_of_ne_of_mem {s : CompositionSeries X} {x : X}
    (hx : x ≠ s.last) (hxs : x ∈ s) : x ∈ s.eraseLast

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i < (s.length - 1).succ

Tactic:
conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
  Nat.add_one_sub_one]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i < s.length

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i ≠ s.length

Tactic:
simpa [last, s.inj, Fin.ext_iff] using hx

Result:
no goals

Proof state:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ s.toFun i ∈ eraseLast s

Tactic:
refine ⟨Fin.castSucc (n := s.length + 1) i, ?_⟩

Result:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ (eraseLast s).toFun ↑↑i.castSucc = s.toFun i

Proof state:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ s.toFun i ∈ eraseLast s

Tactic:
have hi : (i : ℕ) < (s.length - 1).succ := by
  conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
    Nat.add_one_sub_one]
  exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)

Result:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ s.toFun i ∈ eraseLast s

Proof state:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ (eraseLast s).toFun ↑↑i.castSucc = s.toFun i

Tactic:
simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ ↑i < s.length

Tactic:
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ≠ last s
hxs : x ∈ s
⊢ x ∈ eraseLast s

Tactic:
rcases hxs with ⟨i, rfl⟩

Result:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
⊢ s.toFun i ∈ eraseLast s
-- Mathlib/Algebra/Module/SpanRank.lean
lemma FG.generators_ncard {p : Submodule R M} (h : p.FG) :
    (generators p).ncard = spanFinrank p

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ p.generators.ncard = p.spanFinrank

Tactic:
rw [← Nat.cast_inj (R := Cardinal), ← fg_iff_spanRank_eq_spanFinrank.mpr h, Set.ncard, Set.encard,
   ENat.card, generators_card, toNat_toENat, ← spanFinrank]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ↑p.spanFinrank = p.spanRank

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ↑p.spanFinrank = p.spanRank

Tactic:
exact (fg_iff_spanRank_eq_spanFinrank.mpr h).symm

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ f ≫ ⋯.lift = 𝟙 P ∧ ⋯.lift ≫ f = 𝟙 Q

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q

Tactic:
simp

Result:
no goals