harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.iUnion {ι : Type*} (f : ι → Set α) [Finite ι]
    [hf : ∀ i, NoetherianSpace (f i)] : NoetherianSpace (⋃ i, f i)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
⊢ ∀ t ⊆ ⋃ i, f i, IsCompact t

Tactic:
intro t ht

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact t

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact (⋃ i, t ∩ f i)

Tactic:
exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact t

Tactic:
rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact (⋃ i, t ∩ f i)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ i, f i)

Tactic:
simp_rw [noetherianSpace_set_iff] at hf ⊢

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
⊢ ∀ t ⊆ ⋃ i, f i, IsCompact t
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_sSup_of_directed {s : Set (Submodule R M)} {z} (hs : s.Nonempty)
    (hdir : DirectedOn (· ≤ ·) s) : z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
have : Nonempty s := hs.to_subtype

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
this : Nonempty ↑s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
this : Nonempty ↑s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem toRelIsoLT_ofRelIsoLT {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : toRelIsoLT (ofRelIsoLT e) = e

Proof state:
case h
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2
x✝ : α
⊢ (ofRelIsoLT e).toRelIsoLT x✝ = e x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2
⊢ (ofRelIsoLT e).toRelIsoLT = e

Tactic:
ext

Result:
case h
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2
x✝ : α
⊢ (ofRelIsoLT e).toRelIsoLT x✝ = e x✝
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_insert (x y : ZFSet) : (insert x y).toSet = insert x y.toSet

Proof state:
x y : ZFSet.{u_1}
⊢ (insert x y).toSet = insert x y.toSet

Tactic:
ext

Result:
case h
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (insert x y).toSet ↔ x✝ ∈ insert x y.toSet

Proof state:
case h
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (insert x y).toSet ↔ x✝ ∈ insert x y.toSet

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.map_ofComp_surjective :
    Function.Surjective (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Surjective
    ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))

Tactic:
exact (Prod.fst_surjective).comp (compEquiv Q P).surjective

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Surjective ⇑(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Tactic:
rw [← fst_compEquiv]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Surjective
    ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}
    (h : m.WF) {hc : k ∈ Const.modify m k f} : (Const.modify m k f).getKey k hc = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ (modify m k f).contains k = true → (modify m k f).getKey k hc = k

Tactic:
simp_to_raw using Raw₀.Const.getKey_modify_self

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
hc✝ : k ∈ modify m k f
hc : (modify m k f).contains k = true
⊢ (modify m k f).getKey k hc✝ = k

Tactic:
revert hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ (modify m k f).contains k = true → (modify m k f).getKey k hc = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ (modify m k f).getKey k hc = k

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : β → β
h : m.WF
hc✝ : k ∈ modify m k f
hc : (modify m k f).contains k = true
⊢ (modify m k f).getKey k hc✝ = k
-- Mathlib/Data/ENNReal/Order.lean
theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : StrictMono (a * ·)

Proof state:
case intro
a : ℝ≥0
h0 : ↑a ≠ 0
⊢ StrictMono fun x => ↑a * x

Tactic:
rw [coe_ne_zero] at h0

Result:
case intro
a : ℝ≥0
h0 : a ≠ 0
⊢ StrictMono fun x => ↑a * x

Proof state:
a : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ⊤
⊢ StrictMono fun x => a * x

Tactic:
lift a to ℝ≥0 using hinf

Result:
case intro
a : ℝ≥0
h0 : ↑a ≠ 0
⊢ StrictMono fun x => ↑a * x

Proof state:
case intro
a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : ↑a * y ≤ ↑a * x
⊢ y ≤ x

Tactic:
simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel₀ h0, coe_one, one_mul]
  using mul_le_mul_left' h (↑a⁻¹)

Result:
no goals

Proof state:
case intro
a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : x < y
⊢ (fun x => ↑a * x) x < (fun x => ↑a * x) y

Tactic:
contrapose! h

Result:
case intro
a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : ↑a * y ≤ ↑a * x
⊢ y ≤ x

Proof state:
case intro
a : ℝ≥0
h0 : a ≠ 0
⊢ StrictMono fun x => ↑a * x

Tactic:
intro x y h

Result:
case intro
a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : x < y
⊢ (fun x => ↑a * x) x < (fun x => ↑a * x) y
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_isRelPrime_iff {a b : M} :
    IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Tactic:
simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasDerivAt_ofReal_cpow_const {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ 0) :
    HasDerivAt (fun y : ℝ => (y : ℂ) ^ r) (r * x ^ (r - 1)) x

Proof state:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ?m.182529 ≠ -1

Tactic:
rwa [ne_eq, sub_eq_neg_self]

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ HasDerivAt (fun y => ↑y ^ r) (r * ↑x ^ (r - 1)) x

Tactic:
have := HasDerivAt.const_mul r <| hasDerivAt_ofReal_cpow_const' hx
  (by rwa [ne_eq, sub_eq_neg_self])

Result:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
this : HasDerivAt (fun y => r * (↑y ^ (r - 1 + 1) / (r - 1 + 1))) (r * ↑x ^ (r - 1)) x
⊢ HasDerivAt (fun y => ↑y ^ r) (r * ↑x ^ (r - 1)) x

Proof state:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
this : HasDerivAt (fun y => r * (↑y ^ (r - 1 + 1) / (r - 1 + 1))) (r * ↑x ^ (r - 1)) x
⊢ HasDerivAt (fun y => ↑y ^ r) (r * ↑x ^ (r - 1)) x

Tactic:
simpa [sub_add_cancel, mul_div_cancel₀ _ hr] using this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
⊢ m ∣ n

Tactic:
have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h

Result:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ n

Proof state:
m n : Nat
⊢ ↑m ∣ ↑n ↔ m ∣ n

Tactic:
refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩

Result:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
⊢ m ∣ n

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ n

Tactic:
rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]

Result:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ 0

Proof state:
m n : Nat
x✝ : m ∣ n
k : Nat
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
rw [e, Int.ofNat_mul]

Result:
no goals

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
⊢ m ∣ n

Tactic:
match Int.le_total a 0 with
| .inl h =>
  have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
  rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
  apply Nat.dvd_zero
| .inr h => match a, eq_ofNat_of_zero_le h with
  | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩

Result:
no goals

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : 0 ≤ a
⊢ m ∣ n

Tactic:
match a, eq_ofNat_of_zero_le h with
| _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩

Result:
no goals

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
ae : ↑n = ↑m * a
h : a ≤ 0
this : ↑n ≤ 0
⊢ m ∣ 0

Tactic:
apply Nat.dvd_zero

Result:
no goals

Proof state:
m n : Nat
x✝ : ↑m ∣ ↑n
a : Int
k : Nat
ae : ↑n = ↑m * ↑k
h : 0 ≤ ↑k
⊢ m ∣ n

Tactic:
exact ⟨k, Int.ofNat.inj ae⟩

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
theorem range_smul_pow_stabilizes (r : R) :
    ∃ n : ℕ, ∀ m, n ≤ m →
      LinearMap.range (r ^ n • LinearMap.id : M →ₗ[R] M) =
      LinearMap.range (r ^ m • LinearMap.id : M →ₗ[R] M) :=
  monotone_stabilizes
    ⟨fun n => LinearMap.range (r ^ n • LinearMap.id : M →ₗ[R] M), fun n m h x ⟨y, hy⟩ =>
      ⟨r ^ (m - n) • y, by
        dsimp at hy ⊢
        rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]⟩⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x

Tactic:
rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : (r ^ m • LinearMap.id) y = x
⊢ (r ^ n • LinearMap.id) (r ^ (m - n) • y) = x

Tactic:
dsimp at hy ⊢

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem _root_.Continuous.inner_ {f g : ℝ → E} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => inner_ 𝕜 (f x) (g x)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous fun x =>
    4⁻¹ *
      (𝓚 ‖f x + g x‖ * 𝓚 ‖f x + g x‖ - 𝓚 ‖f x - g x‖ * 𝓚 ‖f x - g x‖ + I * 𝓚 ‖I • f x + g x‖ * 𝓚 ‖I • f x + g x‖ -
        I * 𝓚 ‖I • f x - g x‖ * 𝓚 ‖I • f x - g x‖)

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous fun x => _root_.inner_ 𝕜 (f x) (g x)

Tactic:
unfold _root_.inner_

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous fun x =>
    4⁻¹ *
      (𝓚 ‖f x + g x‖ * 𝓚 ‖f x + g x‖ - 𝓚 ‖f x - g x‖ * 𝓚 ‖f x - g x‖ + I * 𝓚 ‖I • f x + g x‖ * 𝓚 ‖I • f x + g x‖ -
        I * 𝓚 ‖I • f x - g x‖ * 𝓚 ‖I • f x - g x‖)
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem inter_insert_of_mem {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₁) :
    s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
rw [inter_comm, insert_inter_of_mem h, inter_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_const (c : ε) (hq_pos : 0 < q) :
    eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Proof state:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
suffices hq_cancel : q * (1 / q) = 1 by rw [hq_cancel, ENNReal.rpow_one]

Result:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1

Proof state:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ

Tactic:
rw [← ENNReal.rpow_mul]

Result:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ 0 ≤ 1 / q

Tactic:
simp [hq_pos.le]

Result:
no goals

Proof state:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1

Tactic:
rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ eLpNorm' (fun x => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, lintegral_const,
  ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
rw [hq_cancel, ENNReal.rpow_one]

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
congr

Result:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem isIntegral_algEquiv {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B]
    (f : A ≃ₐ[R] B) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x :=
  ⟨fun h ↦ by simpa using h.map f.symm, IsIntegral.map f⟩

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A ≃ₐ[R] B
x : A
h : IsIntegral R (f x)
⊢ IsIntegral R x

Tactic:
simpa using h.map f.symm

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem toNFA_evalFrom_match (M : DFA α σ) (start : σ) (s : List α) :
    M.toNFA.evalFrom {start} s = {M.evalFrom start s}

Proof state:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
⊢ M.toNFA.evalFrom {start} s = {M.evalFrom start s}

Tactic:
change List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}

Result:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}

Proof state:
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ M.toNFA.stepSet {start} a = {M.step start a}

Tactic:
simp [NFA.stepSet]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}

Tactic:
induction' s with a s ih generalizing start

Result:
case nil
α : Type u
σ : Type v
M : DFA α σ
start : σ
⊢ List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}

case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {start} (a :: s) = {List.foldl M.step start (a :: s)}

Proof state:
case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {start} (a :: s) = {List.foldl M.step start (a :: s)}

Tactic:
rw [List.foldl, List.foldl,
  show M.toNFA.stepSet {start} a = {M.step start a} by simp [NFA.stepSet] ]

Result:
case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (M.step start a) s}

Proof state:
case cons
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (M.step start a) s}

Tactic:
tauto

Result:
no goals

Proof state:
case nil
α : Type u
σ : Type v
M : DFA α σ
start : σ
⊢ List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.conePointUniqueUpToIso_inv (f : J → C) [HasBiproduct f] {b : Bicone f}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).inv = biproduct.desc b.ι

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = desc b.ι

Tactic:
refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_

Result:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ (ι f j ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv) ≫ b.toCone.π.app j' =
    (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = desc b.ι

Tactic:
classical
refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
  biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ (ι f j ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv) ≫ b.toCone.π.app j' =
    (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'

Tactic:
rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
  biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma one_sub_sq_div_two_le_cos : 1 - x ^ 2 / 2 ≤ cos x

Proof state:
case inl

⊢ 1 - 0 ^ 2 / 2 ≤ cos 0

case inr
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
case inl => simp

Result:
case inr
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
exact (one_sub_sq_div_two_lt_cos hx).le

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
case inr => exact (one_sub_sq_div_two_lt_cos hx).le

Result:
no goals

Proof state:
⊢ 1 - 0 ^ 2 / 2 ≤ cos 0

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl

⊢ 1 - 0 ^ 2 / 2 ≤ cos 0

case inr
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 ≤ cos x
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.factor_eq_gcd_right_right {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m)
    (bn : b ∣ n) : a = m.gcd (b * a)

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (b * a)

Tactic:
rw [gcd_comm]

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
apply Coprime.factor_eq_gcd_right cop am bn

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem uncurry_ihom_map (g : Y ⟶ Y') :
    uncurry ((ihom A).map g) = (ihom.ev A).app Y ≫ g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ uncurry ((ihom A).map g) = (ihom.ev A).app Y ≫ g

Tactic:
apply curry_injective

Result:
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ curry (uncurry ((ihom A).map g)) = curry ((ihom.ev A).app Y ≫ g)

Proof state:
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ curry (uncurry ((ihom A).map g)) = curry ((ihom.ev A).app Y ≫ g)

Tactic:
rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_injective : Injective (coeff : R[X] → ℕ → R)

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
p q : R[ℕ]
⊢ { toFinsupp := p }.coeff = { toFinsupp := q }.coeff → { toFinsupp := p } = { toFinsupp := q }

Tactic:
simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ Injective coeff

Tactic:
rintro ⟨p⟩ ⟨q⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
p q : R[ℕ]
⊢ { toFinsupp := p }.coeff = { toFinsupp := q }.coeff → { toFinsupp := p } = { toFinsupp := q }