harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/Basic.lean
theorem IndepFun.cgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ)
    (h_int_X : Integrable (fun ω => exp (t * X ω)) μ)
    (h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) :
    cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
simp [hμ]

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)

Tactic:
exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne'

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
by_cases hμ : μ = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem Ideal.finite_factors {I : Ideal R} (hI : I ≠ 0) :
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}.Finite

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Finite { x // x.asIdeal ∣ I }

Tactic:
refine
  Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Injective fun v => ⟨(↑v).asIdeal, ⋯⟩

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Injective fun v => ⟨(↑v).asIdeal, ⋯⟩

Tactic:
intro v w hvw

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v => ⟨(↑v).asIdeal, ⋯⟩) v = (fun v => ⟨(↑v).asIdeal, ⋯⟩) w
⊢ v = w

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.asIdeal ∣ I}.Finite

Tactic:
rw [← Set.finite_coe_iff, Set.coe_setOf]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Finite { x // x.asIdeal ∣ I }

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v => ⟨(↑v).asIdeal, ⋯⟩) v = (fun v => ⟨(↑v).asIdeal, ⋯⟩) w
⊢ v = w

Tactic:
simp? at hvw says simp only [Subtype.mk.injEq] at hvw

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (↑v).asIdeal = (↑w).asIdeal
⊢ v = w

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (↑v).asIdeal = (↑w).asIdeal
⊢ v = w

Tactic:
exact Subtype.coe_injective (HeightOneSpectrum.ext hvw)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v => ⟨(↑v).asIdeal, ⋯⟩) v = (fun v => ⟨(↑v).asIdeal, ⋯⟩) w
⊢ v = w

Tactic:
simp only [Subtype.mk.injEq] at hvw

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (↑v).asIdeal = (↑w).asIdeal
⊢ v = w

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Finite { x // x.asIdeal ∣ I }

Tactic:
haveI h_fin := fintypeSubtypeDvd I hI

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Finite { x // x.asIdeal ∣ I }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem Perm.trans {l₁ l₂ l₃ : Array α} (h₁ : l₁ ~ l₂) (h₂ : l₂ ~ l₃) : l₁ ~ l₃

Proof state:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ toList✝ : List α
h₁ : toList✝² ~ toList✝¹
h₂ : toList✝¹ ~ toList✝
⊢ { toList := toList✝² } ~ { toList := toList✝ }

Tactic:
simpa using h₁.trans h₂

Result:
no goals

Proof state:
case mk
α : Type u_1
l₂ l₃ : Array α
h₂ : l₂ ~ l₃
toList✝ : List α
h₁ : { toList := toList✝ } ~ l₂
⊢ { toList := toList✝ } ~ l₃

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
l₃ : Array α
toList✝¹ toList✝ : List α
h₂ : { toList := toList✝ } ~ l₃
h₁ : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝¹ } ~ l₃

Proof state:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ : List α
h₁ : { toList := toList✝² } ~ { toList := toList✝¹ }
toList✝ : List α
h₂ : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝² } ~ { toList := toList✝ }

Tactic:
simp only [perm_toArray] at h₁ h₂

Result:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ toList✝ : List α
h₁ : toList✝² ~ toList✝¹
h₂ : toList✝¹ ~ toList✝
⊢ { toList := toList✝² } ~ { toList := toList✝ }

Proof state:
α : Type u_1
l₁ l₂ l₃ : Array α
h₁ : l₁ ~ l₂
h₂ : l₂ ~ l₃
⊢ l₁ ~ l₃

Tactic:
cases l₁

Result:
case mk
α : Type u_1
l₂ l₃ : Array α
h₂ : l₂ ~ l₃
toList✝ : List α
h₁ : { toList := toList✝ } ~ l₂
⊢ { toList := toList✝ } ~ l₃

Proof state:
case mk.mk
α : Type u_1
l₃ : Array α
toList✝¹ toList✝ : List α
h₂ : { toList := toList✝ } ~ l₃
h₁ : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝¹ } ~ l₃

Tactic:
cases l₃

Result:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ : List α
h₁ : { toList := toList✝² } ~ { toList := toList✝¹ }
toList✝ : List α
h₂ : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝² } ~ { toList := toList✝ }
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y * y :=
  ⟨fun h => by rw [← h, mul_self_sqrt hx], fun h => by rw [h, sqrt_mul_self hy]⟩

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
⊢ x = y * y

Tactic:
rw [← h, mul_self_sqrt hx]

Result:
no goals

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ √x = y

Tactic:
rw [h, sqrt_mul_self hy]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem neg [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) :
    Submartingale (-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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : (μ[f j|↑ℱ i]) a✝¹ ≤ f i a✝¹
⊢ (-f) i a✝¹ ≤ (-μ[f j|↑ℱ 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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] μ[(-f) j|↑ℱ i]

Tactic:
refine EventuallyLE.trans ?_ (condExp_neg ..).symm.le

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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] -μ[f j|↑ℱ i]

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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] -μ[f j|↑ℱ 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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : (μ[f j|↑ℱ i]) a✝¹ ≤ f i a✝¹
⊢ (-f) i a✝¹ ≤ (-μ[f j|↑ℱ 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 : Supermartingale f ℱ μ
⊢ Submartingale (-f) ℱ μ

Tactic:
refine ⟨hf.1.neg, fun i j hij => ?_, 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 : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ (-f) i ≤ᶠ[ae μ] μ[(-f) j|↑ℱ i]
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_cofinite_iff (h : ∀ x, g'' x = 0 → f'' x = 0) :
    f'' =O[cofinite] g'' ↔ ∃ C, ∀ x, ‖f'' x‖ ≤ C * ‖g'' x‖

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
h' : f'' =O[cofinite] g''
C : ℝ
_C₀ : C > 0
hC : ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f'' x‖ ≤ C * ‖g'' x‖
x : α
hx : g'' x = 0
⊢ ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
simp [h _ hx, hx]

Result:
no goals

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
classical
exact ⟨fun h' =>
  let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
  ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
  fun h => (isBigO_top.2 h).mono le_top⟩

Result:
no goals

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
exact ⟨fun h' =>
  let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
  ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
  fun h => (isBigO_top.2 h).mono le_top⟩

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_le_pred_iff {a b : Fin (n + 1)} (ha : a ≠ last n) (hb : b ≠ 0) :
    castPred a ha ≤ pred b hb ↔ a < b

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a.castPred ha ≤ b.pred hb ↔ a < b

Tactic:
rw [le_pred_iff, succ_castPred_le_iff]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem cast_zero : IsNat (a : R) (nat_lit 0) → a = 0
  | ⟨e⟩ => by simp [e]

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
e : a = ↑0
⊢ a = 0

Tactic:
simp [e]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem degree_gcd_le_left {p : R[X]} (hp : p ≠ 0) (q) : (gcd p q).degree ≤ p.degree

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
this : (gcd p q).degree ≤ ↑p.natDegree
⊢ (gcd p q).degree ≤ p.degree

Tactic:
rwa [degree_eq_natDegree hp]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
⊢ (gcd p q).degree ≤ p.degree

Tactic:
have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
this : (gcd p q).degree ≤ ↑p.natDegree
⊢ (gcd p q).degree ≤ p.degree
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_one : p.comp 1 = C (p.eval 1)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp 1 = C (eval 1 p)

Tactic:
rw [← C_1, comp_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
    forM r f = forM (List.range' r.start r.size r.step) f

Proof state:
m : Type u_1 → Type u_2
inst✝ : Monad m
r : Range
f : Nat → m PUnit
⊢ forM r f = forM (List.range' r.start r.size r.step) f

Tactic:
simp only [forM, Range.forM, forM_loop_eq_forM_range', size]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma div_helper (b : G₀) (h : a ≠ 0) : 1 / (a * b) * a = 1 / b

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ 1 / (a * b) * a = 1 / b

Tactic:
rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem aux : ((g x * f x ^ (g x - 1)) • (1 : ℂ →L[ℂ] ℂ).smulRight f' +
    (f x ^ g x * log (f x)) • (1 : ℂ →L[ℂ] ℂ).smulRight g') 1 =
      g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'

Proof state:
f g : ℂ → ℂ
f' g' x : ℂ
⊢ ((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
        (f x ^ g x * log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1 =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'

Tactic:
simp only [Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.one_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.add_apply, Pi.smul_apply,
  ContinuousLinearMap.coe_smul']

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (interior (⇑φ ⁻¹' s)).Nonempty

Tactic:
rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_eq_sup'_normAtPlace (x : mixedSpace K) :
    ‖x‖ = univ.sup' univ_nonempty fun w ↦ normAtPlace w x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖ = univ.sup' ⋯ fun w => (normAtPlace w) x

Tactic:
rw [← coe_nnnorm, nnnorm_eq_sup_normAtPlace, ← sup'_eq_sup univ_nonempty, ← NNReal.val_eq_coe,
  ← OrderHom.Subtype.val_coe, map_finset_sup', OrderHom.Subtype.val_coe]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ univ.sup' ⋯ (Subtype.val ∘ fun w => ⟨(normAtPlace w) x, ⋯⟩) = univ.sup' ⋯ fun w => (normAtPlace w) x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ univ.sup' ⋯ (Subtype.val ∘ fun w => ⟨(normAtPlace w) x, ⋯⟩) = univ.sup' ⋯ fun w => (normAtPlace w) x

Tactic:
simp only [Function.comp_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem pairwise_disjoint :
    Pairwise fun C D : G.ComponentCompl K => Disjoint (C : Set V) (D : Set V)

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ Disjoint ↑C ↑D

Tactic:
rw [Set.disjoint_iff]

Result:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
⊢ Pairwise fun C D => Disjoint ↑C ↑D

Tactic:
rintro C D ne

Result:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ Disjoint ↑C ↑D

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅

Tactic:
exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
@[reassoc (attr := simp)]
lemma germToPullbackStalk_stalkPullbackHom
    (f : X ⟶ Y) (F : Y.Presheaf C) (U : Opens X) (x : X) (hx : x ∈ U) :
    germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x =
      ((pullback C f).obj F).germ _ x hx

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑Y
hV : unop (op U) ≤ (Opens.map f).obj V
⊢ ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x =
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ ((pullback C f).obj F).germ U x hx

Tactic:
simp only [pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc,
  germ_stalkPullbackHom, germ_res]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x = ((pullback C f).obj F).germ U x hx

Tactic:
ext V hV

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑Y
hV : unop (op U) ≤ (Opens.map f).obj V
⊢ ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x =
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ ((pullback C f).obj F).germ U x hx
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_add_int (a : α) (m : ℤ) : fract (a + m) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ fract (a + ↑m) = fract a

Tactic:
rw [fract]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_himp_self_left (a b : α) : a ⊔ b ⇨ a = b ⇨ a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a = b ⇨ a

Tactic:
rw [sup_himp_distrib, himp_self, top_inf_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma lintegral_eapprox_le_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) (n : ℕ) :
    (eapprox f n).lintegral μ ≤ ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (eapprox f n).lintegral μ ≤ ⨆ n, (eapprox f n).lintegral μ

Tactic:
exact le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (eapprox f n).lintegral μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (eapprox f n).lintegral μ ≤ ⨆ n, (eapprox f n).lintegral μ
-- Mathlib/Data/Finset/Image.lean
theorem filter_image {p : β → Prop} [DecidablePred p] :
    (s.image f).filter p = (s.filter fun a ↦ p (f a)).image f :=
  ext fun b => by
    simp only [mem_filter, mem_image, exists_prop]
    exact
      ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
       by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ (∃ a ∈ s, f a = f x) ∧ p (f x)

Tactic:
exact ⟨⟨x, h1, rfl⟩, h2⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = f x

Tactic:
exact ⟨x, ⟨h1, h2⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = b

Tactic:
exact
  ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
   by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (image f s) ↔ b ∈ image f (filter (fun a => p (f a)) s)

Tactic:
simp only [mem_filter, mem_image, exists_prop]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, (a ∈ s ∧ p (f a)) ∧ f a = b) → (∃ a ∈ s, f a = b) ∧ p b

Tactic:
rintro ⟨x, ⟨h1, h2⟩, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ (∃ a ∈ s, f a = f x) ∧ p (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, f a = b) ∧ p b → ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = b

Tactic:
rintro ⟨⟨x, h1, rfl⟩, h2⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ ∃ a, (a ∈ s ∧ p (f a)) ∧ f a = f x
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_eq_zero {a b : Ordinal} : a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Proof state:
case inl
b : Ordinal.{u_1}
⊢ 0 ^ b = 0 ↔ 0 = 0 ∧ b ≠ 0

Tactic:
obtain rfl | hb := eq_or_ne b 0

Result:
case inl.inl

⊢ 0 ^ 0 = 0 ↔ 0 = 0 ∧ 0 ≠ 0

case inl.inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ 0 ^ b = 0 ↔ 0 = 0 ∧ b ≠ 0

Proof state:
case inl.inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ 0 ^ b = 0 ↔ 0 = 0 ∧ b ≠ 0

Tactic:
simp [hb]

Result:
no goals

Proof state:
case inr
a b : Ordinal.{u_1}
ha : a ≠ 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp [opow_ne_zero b ha, ha]

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
b : Ordinal.{u_1}
⊢ 0 ^ b = 0 ↔ 0 = 0 ∧ b ≠ 0

case inr
a b : Ordinal.{u_1}
ha : a ≠ 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Proof state:
case inl.inl

⊢ 0 ^ 0 = 0 ↔ 0 = 0 ∧ 0 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem some_eq_map_iff {f : α → β} {y : β} {v : WithBot α} :
    .some y = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = y

Proof state:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ ↑y = map f v ↔ ∃ x, v = ↑x ∧ f x = y

Tactic:
cases v <;> simp [eq_comm]

Result:
no goals