harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Operations.lean
theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} :
    (⨆ i, t i) • N = ⨆ i, t i • N :=
  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (· • s ∈ _)) ht
    (fun i t ht ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
    (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
    (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N

Tactic:
apply zero_mem

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → x • s + y • s ∈ ⨆ i, t✝ i • N

Tactic:
apply add_mem

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ (fun x => x • s ∈ ⨆ i, t✝ i • N) 0

Tactic:
simp_rw [zero_smul]

Result:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ (fun x => x • s ∈ ⨆ i, t✝ i • N) x → (fun x => x • s ∈ ⨆ i, t✝ i • N) y → (fun x => x • s ∈ ⨆ i, t✝ i • N) (x + y)

Tactic:
simp_rw [add_smul]

Result:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → x • s + y • s ∈ ⨆ i, t✝ i • N
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : α → α → Prop)]
    {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁ ≤ l₂

Proof state:
case intro
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ w✝ : List α
⊢ l₁ ≤ l₁ ++ w✝

Tactic:
apply le_append_left

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ l₁ ≤ l₂

Tactic:
rcases h with ⟨_, rfl⟩

Result:
case intro
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ w✝ : List α
⊢ l₁ ≤ l₁ ++ w✝
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem hasFTaylorSeriesUpToOn_pi' {n : WithTop ℕ∞} :
    HasFTaylorSeriesUpToOn n Φ P' s ↔
      ∀ i, HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap
          (P' x m)) s

Proof state:
case h.e'_1.h.e'_11.h.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : WithTop ℕ∞
x✝¹ : E
x✝ : ℕ
⊢ P' x✝¹ x✝ = ContinuousMultilinearMap.pi fun i => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x✝¹ x✝)

Tactic:
ext

Result:
case h.e'_1.h.e'_11.h.h.H.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : WithTop ℕ∞
x✝³ : E
x✝² : ℕ
x✝¹ : Fin x✝² → E
x✝ : ι
⊢ (P' x✝³ x✝²) x✝¹ x✝ =
    (ContinuousMultilinearMap.pi fun i => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x✝³ x✝²)) x✝¹ x✝

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : WithTop ℕ∞
⊢ HasFTaylorSeriesUpToOn n Φ P' s ↔
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s

Tactic:
convert hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)

Result:
case h.e'_1.h.e'_11.h.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : WithTop ℕ∞
x✝¹ : E
x✝ : ℕ
⊢ P' x✝¹ x✝ = ContinuousMultilinearMap.pi fun i => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x✝¹ x✝)

Proof state:
case h.e'_1.h.e'_11.h.h.H.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : WithTop ℕ∞
x✝³ : E
x✝² : ℕ
x✝¹ : Fin x✝² → E
x✝ : ι
⊢ (P' x✝³ x✝²) x✝¹ x✝ =
    (ContinuousMultilinearMap.pi fun i => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x✝³ x✝²)) x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.getRight? = none ↔ x.isLeft = true

Tactic:
cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_def_int (x : 𝓞 (WithVal (v.valuation K))) :
    ‖embedding v x‖ = toNNReal (absNorm_ne_zero v) (v.intValuationDef x)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ ‖(embedding v) ↑x‖ = ↑((toNNReal ⋯) (v.intValuationDef x))

Tactic:
rw [norm_def, adicAbv_def, valuation_eq_intValuationDef]

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem coeffIntegerNormalization_mem_support (p : S[X]) (i : ℕ)
    (h : coeffIntegerNormalization M p i ≠ 0) : i ∈ p.support

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ p.support

Tactic:
contrapose h

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : i ∉ p.support
⊢ ¬coeffIntegerNormalization M p i ≠ 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : i ∉ p.support
⊢ ¬coeffIntegerNormalization M p i ≠ 0

Tactic:
rw [Ne, Classical.not_not, coeffIntegerNormalization, dif_neg h]

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
lemma Ioc_filter_dvd_eq :
    {x ∈ Ioc a b | r ∣ x} =
      (Ioc ⌊a / (r : ℚ)⌋ ⌊b / (r : ℚ)⌋).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩

Proof state:
a b r : ℤ
hr : 0 < r
⊢ filter (fun x => r ∣ x) (Ioc a b) = map { toFun := fun x => x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

Tactic:
ext x

Result:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ filter (fun x => r ∣ x) (Ioc a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

Proof state:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ filter (fun x => r ∣ x) (Ioc a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
  dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Result:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a < x ∧ x ≤ b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a < a_1 * r ∧ a_1 * r ≤ b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x

Proof state:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a < x ∧ x ≤ b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a < a_1 * r ∧ a_1 * r ≤ b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_X : p.comp X = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp X = p

Tactic:
simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a => (monomial e) a) = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a => (monomial e) a) = p

Tactic:
exact sum_monomial_eq _

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_def' (x : WithVal (v.valuation K)) :
    ‖embedding v x‖ = toNNReal (absNorm_ne_zero v) (v.valuation K x)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : WithVal (valuation K v)
⊢ ‖(embedding v) x‖ = ↑((toNNReal ⋯) ((valuation K v) x))

Tactic:
rw [norm_def, adicAbv_def]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegral_add_eq (hf : Periodic f T) (t s : ℝ) :
    ∫ x in t..t + T, f x = ∫ x in s..s + T, f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Tactic:
rcases lt_trichotomy (0 : ℝ) T with (hT | rfl | hT)

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
inst✝ : NormedSpace ℝ E
t s : ℝ
hf : Periodic f 0
⊢ ∫ (x : ℝ) in t..t + 0, f x = ∫ (x : ℝ) in s..s + 0, f x

case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : T < 0
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = ∫ (x : ℝ) in s + T..s, f x

Tactic:
simpa only [← sub_eq_add_neg, add_sub_cancel_right] using
  hf.neg.intervalIntegral_add_eq_of_pos (neg_pos.2 hT) (t + T) (s + T)

Result:
no goals

Proof state:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
inst✝ : NormedSpace ℝ E
t s : ℝ
hf : Periodic f 0
⊢ ∫ (x : ℝ) in t..t + 0, f x = ∫ (x : ℝ) in s..s + 0, f x

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : T < 0
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Tactic:
rw [← neg_inj, ← integral_symm, ← integral_symm]

Result:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = ∫ (x : ℝ) in s + T..s, f x

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Tactic:
exact hf.intervalIntegral_add_eq_of_pos hT t s

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem extraction_forall_of_eventually' {P : ℕ → ℕ → Prop} (h : ∀ n, ∃ N, ∀ k ≥ N, P n k) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
  extraction_forall_of_eventually (by simp [eventually_atTop, h])

Proof state:
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k

Tactic:
simp [eventually_atTop, h]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem isPartitionDisjUnionOfEqDiff (h : π₂.iUnion = ↑I \ π₁.iUnion) :
    IsPartition (π₁.disjUnion π₂ <| h.symm ▸ disjoint_sdiff_self_right) :=
  isPartition_iff_iUnion_eq.2 <| (iUnion_disjUnion _).trans <| by simp [h, π₁.iUnion_subset]

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : π₂.iUnion = ↑I \ π₁.iUnion
⊢ π₁.iUnion ∪ π₂.iUnion = ↑I

Tactic:
simp [h, π₁.iUnion_subset]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_def (D : ℝ) :
    (w D : E → ℝ) = fun x => ((∫ x : E, u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Proof state:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ w D x = ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
⊢ w D = fun x => ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Tactic:
ext1 x

Result:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ w D x = ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.ext {G : Type*} [Group G] {t t' : TopologicalSpace G}
    (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _)
    (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
  TopologicalSpace.ext_nhds fun x ↦ by
    rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]

Proof state:
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ 𝓝 x = 𝓝 x

Tactic:
rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_eq_realSize : ∀ {t : Ordnode α}, Sized t → size t = realSize t
  | nil, _ => rfl
  | node s l x r, ⟨h₁, h₂, h₃⟩ => by
    rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]; rfl

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ (node s l x r).size = (node s l x r).realSize

Tactic:
rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]

Result:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNorm_zero_iff {f : ContinuousMultilinearMap 𝕜 E G} : ‖f‖ = 0 ↔ f = 0

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖f‖ = 0 ↔ f = 0

Tactic:
simp [← (opNorm_nonneg f).le_iff_eq, opNorm_le_iff le_rfl, ContinuousMultilinearMap.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymmPart_indiscrete (n : ℕ) : esymmPart σ R (.indiscrete n) = esymm σ R n

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymmPart σ R (Nat.Partition.indiscrete n) = esymm σ R n

Tactic:
cases n <;> simp [esymmPart]

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
    (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
    (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' where
  mp H := H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
  mpr H :=
    H.symm ▸ by
      apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
      simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m')

Proof state:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'

Tactic:
simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m')

Result:
no goals

Proof state:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit⁻¹ (x • m') = m'

Tactic:
apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective

Result:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'
-- Mathlib/Probability/Martingale/Basic.lean
theorem neg [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) :
    Supermartingale (-f) ℱ μ

Proof state:
case h
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : f i a✝¹ ≤ (μ[f j|↑ℱ i]) a✝¹
⊢ (-μ[f j|↑ℱ i]) a✝¹ ≤ (-f) i a✝¹

Tactic:
simpa

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ -μ[f j|↑ℱ i] ≤ᶠ[ae μ] (-f) i

Tactic:
filter_upwards [hf.2.1 i j hij] with _ _

Result:
case h
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : f i a✝¹ ≤ (μ[f j|↑ℱ i]) a✝¹
⊢ (-μ[f j|↑ℱ i]) a✝¹ ≤ (-f) i a✝¹

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
⊢ Supermartingale (-f) ℱ μ

Tactic:
refine ⟨hf.1.neg, fun i j hij => (condExp_neg ..).le.trans ?_, fun i => (hf.2.2 i).neg⟩

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ -μ[f j|↑ℱ i] ≤ᶠ[ae μ] (-f) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a

Proof state:
case zero
h : 0 ≠ 0
⊢ (pred 0).succ = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
n✝ : Nat
a✝ : n✝ ≠ 0 → n✝.pred.succ = n✝
h : n✝ + 1 ≠ 0
⊢ (n✝ + 1).pred.succ = n✝ + 1

Tactic:
rfl

Result:
no goals

Proof state:
a : Nat
h : a ≠ 0
⊢ a.pred.succ = a

Tactic:
induction a with
| zero => contradiction
| succ => rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_zero (f : Ordinal → Ordinal) : veblenWith f 0 = f

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ veblenWith f 0 = f

Tactic:
rw [veblenWith, if_pos rfl]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem zpow_mod_card (a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ (n % ↑(card G)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
  (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k : α} :
    m.contains k = false → l.contains k = false → getKey? (insertManyIfNewUnit m l).1 k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKey? k = none

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_mul [DecidableEq σ] (φ ψ : MvPolynomial σ R) : (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Tactic:
simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees

Tactic:
exact Multiset.subset_of_le degrees_mul_le

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem coe_rpow_of_ne_zero {x : ℝ≥0} (h : x ≠ 0) (y : ℝ) : (↑(x ^ y) : ℝ≥0∞) = x ^ y

Proof state:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x.rpow y) = if x = 0 ∧ y < 0 then ⊤ else ↑(x.rpow y)

Tactic:
simp [h]

Result:
no goals

Proof state:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
rw [← ENNReal.some_eq_coe]

Result:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x ^ y) = ↑x ^ y