harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
/-- The operator norm of the second projection `E × F → F` is exactly 1 if `F` is nontrivial. -/
@[simp] lemma norm_snd [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial F]  :
    ‖snd 𝕜 E F‖ = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
⊢ 1 ≤ ‖snd 𝕜 E F‖

Tactic:
have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * (‖0‖ ⊔ ‖f‖)
⊢ 1 ≤ ‖snd 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
⊢ 1 ≤ ‖snd 𝕜 E F‖

Tactic:
let ⟨f, hf⟩ := exists_ne (0 : F)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
⊢ 1 ≤ ‖snd 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * (‖0‖ ⊔ ‖f‖)
⊢ 1 ≤ ‖snd 𝕜 E F‖

Tactic:
rw [norm_zero, max_eq_right (norm_nonneg f)] at this

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * ‖f‖
⊢ 1 ≤ ‖snd 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
⊢ ‖snd 𝕜 E F‖ = 1

Tactic:
refine le_antisymm (norm_snd_le ..) ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
⊢ 1 ≤ ‖snd 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * ‖f‖
⊢ 1 ≤ ‖snd 𝕜 E F‖

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem tsum_star [T2Space α] : star (∑' b, f b) = ∑' b, star (f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
inst✝ : T2Space α
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

Tactic:
by_cases hf : Summable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
inst✝ : T2Space α
hf : Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

case neg
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
inst✝ : T2Space α
hf : ¬Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
inst✝ : T2Space α
hf : ¬Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.ofStar hf),
  star_zero]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
inst✝ : T2Space α
hf : Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

Tactic:
exact hf.hasSum.star.tsum_eq.symm

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_iUnion (s : ι → Set α) (t : α → Set β) :
    ⋂ x ∈ ⋃ i, s i, t x = ⋂ (i) (x ∈ s i), t x

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ ⋂ x ∈ ⋃ i, s i, t x = ⋂ i, ⋂ x ∈ s i, t x

Tactic:
simp [@iInter_comm _ ι]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
    pmap f o h = none ↔ o = none

Proof state:
α : Type u_1
β : Type u_2
o : Option α
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ o → p a
⊢ pmap f o h = none ↔ o = none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_id_comp {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct W X]
    [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] :
    coprod.map (𝟙 W) (f ≫ g) = coprod.map (𝟙 W) f ≫ coprod.map (𝟙 W) g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct W X
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/FiniteDimensional.lean
@[simp]
lemma Real.rank_rat_real : Module.rank ℚ ℝ = continuum

Proof state:
⊢ Module.rank ℚ ℝ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real

Result:
⊢ lift.{0, 0} #ℚ < lift.{0, 0} #ℝ

Proof state:
⊢ lift.{0, 0} #ℚ < lift.{0, 0} #ℝ

Tactic:
simpa [mk_real] using aleph0_lt_continuum

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v)

Proof state:
v i : Nat
⊢ (allOnes v).getLsbD i = decide (i < v)

Tactic:
simp [allOnes]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_le_degree (h : coeff q (natDegree p) ≠ 0) : degree p ≤ degree q

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ ⊥ ≤ q.degree

Tactic:
exact bot_le

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree hp]

Result:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ ↑p.natDegree ≤ q.degree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ p.degree ≤ q.degree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ ↑p.natDegree ≤ q.degree

Tactic:
exact le_degree_of_ne_zero h

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ p.degree ≤ q.degree

Tactic:
rw [hp, degree_zero]

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ ⊥ ≤ q.degree
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_rat_smul [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
    (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module ℚ α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P)
    (hPz : P z = 0) : P y ≠ 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : 0 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
exact hPx <| pow_eq_zero hP.left.symm

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
⊢ P y ≠ 0

Tactic:
intro hPy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : 0 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0

Tactic:
have hPx : P x ≠ 0 := X_ne_zero_of_Z_eq_zero hP hPz

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
⊢ P y ≠ 0
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem injective_tower_top (inj : Injective (algebraMap R A)) : Injective (algebraMap S A)

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
⊢ Injective ⇑(algebraMap S A)

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_

Result:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne : ¬s = 0
⊢ False

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ False

Tactic:
refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)

Result:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ 0 ∣ (algebraMap R A) r

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne : ¬s = 0
⊢ False

Tactic:
have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)

Result:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ False

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
S : Type u_3
A : Type u_4
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ 0 ∣ (algebraMap R A) r

Tactic:
simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_top : (⊤ : L.BoundedFormula α l).Realize v xs ↔ True

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
⊢ ⊤.Realize v xs ↔ True

Tactic:
simp [Top.top]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem finite_toSet (s : Multiset α) : { x | x ∈ s }.Finite

Proof state:
α : Type u
s : Multiset α
⊢ {x | x ∈ s}.Finite

Tactic:
classical simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet

Result:
no goals

Proof state:
α : Type u
s : Multiset α
⊢ {x | x ∈ s}.Finite

Tactic:
simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem supermartingale_of_setIntegral_succ_le [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ}
    (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
    (hf : ∀ i, ∀ s : Set Ω, MeasurableSet[𝒢 i] s → ∫ ω in s, f (i + 1) ω ∂μ ≤ ∫ ω in s, f i ω ∂μ) :
    Supermartingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, (-f) i ω ∂μ ≤ ∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, (-f) i ω ∂μ ≤ ∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ

Tactic:
simpa only [integral_neg, Pi.neg_apply, neg_le_neg_iff]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
⊢ Supermartingale (- -f) 𝒢 μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False

Proof state:
a b : Prop
h : a = False
⊢ (a ∧ b) = False

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_def₂ (x : ℤ[i]) : (x : ℂ) = ⟨x.re, x.im⟩

Proof state:
x : ℤ[i]
⊢ toComplex x = { re := ↑x.re, im := ↑x.im }

Tactic:
apply Complex.ext <;> simp [toComplex_def]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem ImageMap.map_uniq_aux {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g}
    (map : image f.hom ⟶ image g.hom)
    (map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom
⊢ map = map'

Tactic:
apply (cancel_mono (image.ι g.hom)).1 this

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom

Tactic:
rw [map_ι,map_ι']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map = map'

Tactic:
have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι,map_ι']

Result:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom
⊢ map = map'
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_kernel_ι_comp_cokernel_π_zero [S.HasHomology]
    [HasKernel S.g] [HasCokernel S.f] :
    S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S : ShortComplex C
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
this : HasCokernel (kernel.lift S.g S.f ⋯)
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
haveI := HasRightHomology.hasKernel S

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S : ShortComplex C
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
this✝ : HasCokernel (kernel.lift S.g S.f ⋯)
this : HasKernel (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S : ShortComplex C
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
this✝ : HasCokernel (kernel.lift S.g S.f ⋯)
this : HasKernel (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
exact S.exact_iff_i_p_zero (LeftHomologyData.ofHasKernelOfHasCokernel S)
  (RightHomologyData.ofHasCokernelOfHasKernel S)

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S : ShortComplex C
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
haveI := HasLeftHomology.hasCokernel S

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S : ShortComplex C
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
this : HasCokernel (kernel.lift S.g S.f ⋯)
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem ProbabilityMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : Filter ι}
    [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω]
    {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ))
    {F : Set Ω} (F_closed : IsClosed F) :
    (L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F

Proof state:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F

Tactic:
apply FiniteMeasure.limsup_measure_closed_le_of_tendsto
  ((tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds L).mp μs_lim) F_closed

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_pos_iff_nontrivial_of_finite [Finite s] : 0 < s.infsep ↔ s.Nontrivial

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.Nontrivial → 0 < s.einfsep

Tactic:
exact fun _ => einfsep_pos_of_finite

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.infsep ↔ s.Nontrivial

Tactic:
rw [infsep_pos, einfsep_lt_top_iff, and_iff_right_iff_imp]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.Nontrivial → 0 < s.einfsep
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_smul_left (a : ℝ≥0∞) [SFinite μ] [IsSFiniteKernel κ] :
    (a • μ) ⊗ₘ κ = a • (μ ⊗ₘ κ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ (a • μ) ⊗ₘ κ = a • μ ⊗ₘ κ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((a • μ) ⊗ₘ κ) s = (a • μ ⊗ₘ κ) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((a • μ) ⊗ₘ κ) s = (a • μ ⊗ₘ κ) s

Tactic:
simp only [compProd_apply hs, lintegral_smul_measure, smul_apply, smul_eq_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem cancel_left {g : β →ᵈ γ} {f₁ f₂ : α →ᵈ β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => Dilation.ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_zero (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard = 0 ↔ s = ∅

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w)

Proof state:
i w : Nat
⊢ i < w - 1 ↔ i + 1 < w

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
⊢ (intMax w).getLsbD i = decide (i + 1 < w)

Tactic:
rw [← testBit_toNat, toNat_intMax, Nat.testBit_two_pow_sub_one, decide_eq_decide]

Result:
i w : Nat
⊢ i < w - 1 ↔ i + 1 < w
-- Mathlib/Topology/NoetherianSpace.lean
theorem noetherianSpace_set_iff (s : Set α) :
    NoetherianSpace s ↔ ∀ t, t ⊆ s → IsCompact t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t

Tactic:
simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff,
  Subtype.forall_set_subtype]

Result:
no goals